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