This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem omopthlem2

Description: Lemma for omopthi . (Contributed by Scott Fenton, 16-Apr-2012) (Revised by Mario Carneiro, 17-Nov-2014)

Ref Expression
Hypotheses omopthlem2.1 
|- A e. _om
omopthlem2.2 
|- B e. _om
omopthlem2.3 
|- C e. _om
omopthlem2.4 
|- D e. _om
Assertion omopthlem2 
|- ( ( A +o B ) e. C -> -. ( ( C .o C ) +o D ) = ( ( ( A +o B ) .o ( A +o B ) ) +o B ) )

Proof

Step Hyp Ref Expression
1 omopthlem2.1 
 |-  A e. _om
2 omopthlem2.2 
 |-  B e. _om
3 omopthlem2.3 
 |-  C e. _om
4 omopthlem2.4 
 |-  D e. _om
5 3 3 nnmcli 
 |-  ( C .o C ) e. _om
6 5 4 nnacli 
 |-  ( ( C .o C ) +o D ) e. _om
7 6 nnoni 
 |-  ( ( C .o C ) +o D ) e. On
8 7 onirri 
 |-  -. ( ( C .o C ) +o D ) e. ( ( C .o C ) +o D )
9 eleq1 
 |-  ( ( ( C .o C ) +o D ) = ( ( ( A +o B ) .o ( A +o B ) ) +o B ) -> ( ( ( C .o C ) +o D ) e. ( ( C .o C ) +o D ) <-> ( ( ( A +o B ) .o ( A +o B ) ) +o B ) e. ( ( C .o C ) +o D ) ) )
10 8 9 mtbii 
 |-  ( ( ( C .o C ) +o D ) = ( ( ( A +o B ) .o ( A +o B ) ) +o B ) -> -. ( ( ( A +o B ) .o ( A +o B ) ) +o B ) e. ( ( C .o C ) +o D ) )
11 nnaword1 
 |-  ( ( ( C .o C ) e. _om /\ D e. _om ) -> ( C .o C ) C_ ( ( C .o C ) +o D ) )
12 5 4 11 mp2an 
 |-  ( C .o C ) C_ ( ( C .o C ) +o D )
13 1 2 nnacli 
 |-  ( A +o B ) e. _om
14 13 1 nnacli 
 |-  ( ( A +o B ) +o A ) e. _om
15 nnaword1 
 |-  ( ( B e. _om /\ ( ( A +o B ) +o A ) e. _om ) -> B C_ ( B +o ( ( A +o B ) +o A ) ) )
16 2 14 15 mp2an 
 |-  B C_ ( B +o ( ( A +o B ) +o A ) )
17 nnacom 
 |-  ( ( B e. _om /\ ( ( A +o B ) +o A ) e. _om ) -> ( B +o ( ( A +o B ) +o A ) ) = ( ( ( A +o B ) +o A ) +o B ) )
18 2 14 17 mp2an 
 |-  ( B +o ( ( A +o B ) +o A ) ) = ( ( ( A +o B ) +o A ) +o B )
19 16 18 sseqtri 
 |-  B C_ ( ( ( A +o B ) +o A ) +o B )
20 nnaass 
 |-  ( ( ( A +o B ) e. _om /\ A e. _om /\ B e. _om ) -> ( ( ( A +o B ) +o A ) +o B ) = ( ( A +o B ) +o ( A +o B ) ) )
21 13 1 2 20 mp3an 
 |-  ( ( ( A +o B ) +o A ) +o B ) = ( ( A +o B ) +o ( A +o B ) )
22 nnm2 
 |-  ( ( A +o B ) e. _om -> ( ( A +o B ) .o 2o ) = ( ( A +o B ) +o ( A +o B ) ) )
23 13 22 ax-mp 
 |-  ( ( A +o B ) .o 2o ) = ( ( A +o B ) +o ( A +o B ) )
24 21 23 eqtr4i 
 |-  ( ( ( A +o B ) +o A ) +o B ) = ( ( A +o B ) .o 2o )
25 19 24 sseqtri 
 |-  B C_ ( ( A +o B ) .o 2o )
26 2onn 
 |-  2o e. _om
27 13 26 nnmcli 
 |-  ( ( A +o B ) .o 2o ) e. _om
28 13 13 nnmcli 
 |-  ( ( A +o B ) .o ( A +o B ) ) e. _om
29 nnawordi 
 |-  ( ( B e. _om /\ ( ( A +o B ) .o 2o ) e. _om /\ ( ( A +o B ) .o ( A +o B ) ) e. _om ) -> ( B C_ ( ( A +o B ) .o 2o ) -> ( B +o ( ( A +o B ) .o ( A +o B ) ) ) C_ ( ( ( A +o B ) .o 2o ) +o ( ( A +o B ) .o ( A +o B ) ) ) ) )
30 2 27 28 29 mp3an 
 |-  ( B C_ ( ( A +o B ) .o 2o ) -> ( B +o ( ( A +o B ) .o ( A +o B ) ) ) C_ ( ( ( A +o B ) .o 2o ) +o ( ( A +o B ) .o ( A +o B ) ) ) )
31 25 30 ax-mp 
 |-  ( B +o ( ( A +o B ) .o ( A +o B ) ) ) C_ ( ( ( A +o B ) .o 2o ) +o ( ( A +o B ) .o ( A +o B ) ) )
32 nnacom 
 |-  ( ( ( ( A +o B ) .o ( A +o B ) ) e. _om /\ B e. _om ) -> ( ( ( A +o B ) .o ( A +o B ) ) +o B ) = ( B +o ( ( A +o B ) .o ( A +o B ) ) ) )
33 28 2 32 mp2an 
 |-  ( ( ( A +o B ) .o ( A +o B ) ) +o B ) = ( B +o ( ( A +o B ) .o ( A +o B ) ) )
34 nnacom 
 |-  ( ( ( ( A +o B ) .o ( A +o B ) ) e. _om /\ ( ( A +o B ) .o 2o ) e. _om ) -> ( ( ( A +o B ) .o ( A +o B ) ) +o ( ( A +o B ) .o 2o ) ) = ( ( ( A +o B ) .o 2o ) +o ( ( A +o B ) .o ( A +o B ) ) ) )
35 28 27 34 mp2an 
 |-  ( ( ( A +o B ) .o ( A +o B ) ) +o ( ( A +o B ) .o 2o ) ) = ( ( ( A +o B ) .o 2o ) +o ( ( A +o B ) .o ( A +o B ) ) )
36 31 33 35 3sstr4i 
 |-  ( ( ( A +o B ) .o ( A +o B ) ) +o B ) C_ ( ( ( A +o B ) .o ( A +o B ) ) +o ( ( A +o B ) .o 2o ) )
37 13 3 omopthlem1 
 |-  ( ( A +o B ) e. C -> ( ( ( A +o B ) .o ( A +o B ) ) +o ( ( A +o B ) .o 2o ) ) e. ( C .o C ) )
38 28 2 nnacli 
 |-  ( ( ( A +o B ) .o ( A +o B ) ) +o B ) e. _om
39 38 nnoni 
 |-  ( ( ( A +o B ) .o ( A +o B ) ) +o B ) e. On
40 5 nnoni 
 |-  ( C .o C ) e. On
41 ontr2 
 |-  ( ( ( ( ( A +o B ) .o ( A +o B ) ) +o B ) e. On /\ ( C .o C ) e. On ) -> ( ( ( ( ( A +o B ) .o ( A +o B ) ) +o B ) C_ ( ( ( A +o B ) .o ( A +o B ) ) +o ( ( A +o B ) .o 2o ) ) /\ ( ( ( A +o B ) .o ( A +o B ) ) +o ( ( A +o B ) .o 2o ) ) e. ( C .o C ) ) -> ( ( ( A +o B ) .o ( A +o B ) ) +o B ) e. ( C .o C ) ) )
42 39 40 41 mp2an 
 |-  ( ( ( ( ( A +o B ) .o ( A +o B ) ) +o B ) C_ ( ( ( A +o B ) .o ( A +o B ) ) +o ( ( A +o B ) .o 2o ) ) /\ ( ( ( A +o B ) .o ( A +o B ) ) +o ( ( A +o B ) .o 2o ) ) e. ( C .o C ) ) -> ( ( ( A +o B ) .o ( A +o B ) ) +o B ) e. ( C .o C ) )
43 36 37 42 sylancr 
 |-  ( ( A +o B ) e. C -> ( ( ( A +o B ) .o ( A +o B ) ) +o B ) e. ( C .o C ) )
44 12 43 sselid 
 |-  ( ( A +o B ) e. C -> ( ( ( A +o B ) .o ( A +o B ) ) +o B ) e. ( ( C .o C ) +o D ) )
45 10 44 nsyl3 
 |-  ( ( A +o B ) e. C -> -. ( ( C .o C ) +o D ) = ( ( ( A +o B ) .o ( A +o B ) ) +o B ) )