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 ) )