Theorem addcmpblnq 3846

Description: Lemma showing compatibility of addition.

Hypotheses

Ref	Expression
cmpblnq.1	|- A e. V
cmpblnq.2	|- B e. V
cmpblnq.3	|- C e. V
cmpblnq.4	|- D e. V
cmpblnq.5	|- F e. V
cmpblnq.6	|- G e. V
cmpblnq.7	|- R e. V
cmpblnq.8	|- S e. V

Assertion

Ref	Expression
addcmpblnq	|- ((((A e. N. /\ B e. N.) /\ (C e. N. /\ D e. N.)) /\ ((F e. N. /\ G e. N.) /\ (R e. N. /\ S e. N.))) -> (((A .N D) = (B .N C) /\ (F .N S) = (G .N R)) -> <.((A .N G) +N (B .N F)), (B .N G)>. ~Q <.((C .N S) +N (D .N R)), (D .N S)>.))

Proof of Theorem addcmpblnq

Step	Hyp	Ref	Expression
1		addclpi 3814	. . . . . . . 8 |- (((A .N G) e. N. /\ (B .N F) e. N.) -> ((A .N G) +N (B .N F)) e. N.)
2		mulclpi 3815	. . . . . . . 8 |- ((A e. N. /\ G e. N.) -> (A .N G) e. N.)
3		mulclpi 3815	. . . . . . . 8 |- ((B e. N. /\ F e. N.) -> (B .N F) e. N.)
4	1, 2, 3	syl2an 349	. . . . . . 7 |- (((A e. N. /\ G e. N.) /\ (B e. N. /\ F e. N.)) -> ((A .N G) +N (B .N F)) e. N.)
5	4	an42s 391	. . . . . 6 |- (((A e. N. /\ B e. N.) /\ (F e. N. /\ G e. N.)) -> ((A .N G) +N (B .N F)) e. N.)
6		mulclpi 3815	. . . . . . . 8 |- ((B e. N. /\ G e. N.) -> (B .N G) e. N.)
7	6	adantl 305	. . . . . . 7 |- (((A e. N. /\ F e. N.) /\ (B e. N. /\ G e. N.)) -> (B .N G) e. N.)
8	7	an4s 390	. . . . . 6 |- (((A e. N. /\ B e. N.) /\ (F e. N. /\ G e. N.)) -> (B .N G) e. N.)
9	5, 8	jca 236	. . . . 5 |- (((A e. N. /\ B e. N.) /\ (F e. N. /\ G e. N.)) -> (((A .N G) +N (B .N F)) e. N. /\ (B .N G) e. N.))
10		addclpi 3814	. . . . . . . 8 |- (((C .N S) e. N. /\ (D .N R) e. N.) -> ((C .N S) +N (D .N R)) e. N.)
11		mulclpi 3815	. . . . . . . 8 |- ((C e. N. /\ S e. N.) -> (C .N S) e. N.)
12		mulclpi 3815	. . . . . . . 8 |- ((D e. N. /\ R e. N.) -> (D .N R) e. N.)
13	10, 11, 12	syl2an 349	. . . . . . 7 |- (((C e. N. /\ S e. N.) /\ (D e. N. /\ R e. N.)) -> ((C .N S) +N (D .N R)) e. N.)
14	13	an42s 391	. . . . . 6 |- (((C e. N. /\ D e. N.) /\ (R e. N. /\ S e. N.)) -> ((C .N S) +N (D .N R)) e. N.)
15		mulclpi 3815	. . . . . . . 8 |- ((D e. N. /\ S e. N.) -> (D .N S) e. N.)
16	15	adantl 305	. . . . . . 7 |- (((C e. N. /\ R e. N.) /\ (D e. N. /\ S e. N.)) -> (D .N S) e. N.)
17	16	an4s 390	. . . . . 6 |- (((C e. N. /\ D e. N.) /\ (R e. N. /\ S e. N.)) -> (D .N S) e. N.)
18	14, 17	jca 236	. . . . 5 |- (((C e. N. /\ D e. N.) /\ (R e. N. /\ S e. N.)) -> (((C .N S) +N (D .N R)) e. N. /\ (D .N S) e. N.))
19	9, 18	anim12i 268	. . . 4 |- ((((A e. N. /\ B e. N.) /\ (F e. N. /\ G e. N.)) /\ ((C e. N. /\ D e. N.) /\ (R e. N. /\ S e. N.))) -> ((((A .N G) +N (B .N F)) e. N. /\ (B .N G) e. N.) /\ (((C .N S) +N (D .N R)) e. N. /\ (D .N S) e. N.)))
20	19	an4s 390	. . 3 |- ((((A e. N. /\ B e. N.) /\ (C e. N. /\ D e. N.)) /\ ((F e. N. /\ G e. N.) /\ (R e. N. /\ S e. N.))) -> ((((A .N G) +N (B .N F)) e. N. /\ (B .N G) e. N.) /\ (((C .N S) +N (D .N R)) e. N. /\ (D .N S) e. N.)))
21		enqbreq 3838	. . 3 |- (((((A .N G) +N (B .N F)) e. N. /\ (B .N G) e. N.) /\ (((C .N S) +N (D .N R)) e. N. /\ (D .N S) e. N.)) -> (<.((A .N G) +N (B .N F)), (B .N G)>. ~Q <.((C .N S) +N (D .N R)), (D .N S)>. <-> (((A .N G) +N (B .N F)) .N (D .N S)) = ((B .N G) .N ((C .N S) +N (D .N R)))))
22	20, 21	syl 12	. 2 |- ((((A e. N. /\ B e. N.) /\ (C e. N. /\ D e. N.)) /\ ((F e. N. /\ G e. N.) /\ (R e. N. /\ S e. N.))) -> (<.((A .N G) +N (B .N F)), (B .N G)>. ~Q <.((C .N S) +N (D .N R)), (D .N S)>. <-> (((A .N G) +N (B .N F)) .N (D .N S)) = ((B .N G) .N ((C .N S) +N (D .N R)))))
23		opreq1 3006	. . . 4 |- ((A .N D) = (B .N C) -> ((A .N D) .N (G .N S)) = ((B .N C) .N (G .N S)))
24		opreq2 3007	. . . 4 |- ((F .N S) = (G .N R) -> ((B .N D) .N (F .N S)) = ((B .N D) .N (G .N R)))
25	23, 24	opreqan12d 3015	. . 3 |- (((A .N D) = (B .N C) /\ (F .N S) = (G .N R)) -> (((A .N D) .N (G .N S)) +N ((B .N D) .N (F .N S))) = (((B .N C) .N (G .N S)) +N ((B .N D) .N (G .N R))))
26		oprex 3018	. . . . 5 |- (A .N G) e. V
27		oprex 3018	. . . . 5 |- (B .N F) e. V
28		oprex 3018	. . . . 5 |- (D .N S) e. V
29		visset 1350	. . . . . 6 |- x e. V
30		visset 1350	. . . . . 6 |- y e. V
31	29, 30	mulcompi 3818	. . . . 5 |- (x .N y) = (y .N x)
32		visset 1350	. . . . . 6 |- z e. V
33	30, 32	distrpi 3820	. . . . 5 |- (x .N (y +N z)) = ((x .N y) +N (x .N z))
34	26, 27, 28, 31, 33	caoprdistrr 3081	. . . 4 |- (((A .N G) +N (B .N F)) .N (D .N S)) = (((A .N G) .N (D .N S)) +N ((B .N F) .N (D .N S)))
35		cmpblnq.1	. . . . . 6 |- A e. V
36		cmpblnq.6	. . . . . 6 |- G e. V
37		cmpblnq.4	. . . . . 6 |- D e. V
38	30, 32	mulasspi 3819	. . . . . 6 |- ((x .N y) .N z) = (x .N (y .N z))
39		cmpblnq.8	. . . . . 6 |- S e. V
40	35, 36, 37, 31, 38, 39	caopr4 3078	. . . . 5 |- ((A .N G) .N (D .N S)) = ((A .N D) .N (G .N S))
41		cmpblnq.2	. . . . . 6 |- B e. V
42		cmpblnq.5	. . . . . 6 |- F e. V
43	41, 42, 37, 31, 38, 39	caopr4 3078	. . . . 5 |- ((B .N F) .N (D .N S)) = ((B .N D) .N (F .N S))
44	40, 43	opreq12i 3011	. . . 4 |- (((A .N G) .N (D .N S)) +N ((B .N F) .N (D .N S))) = (((A .N D) .N (G .N S)) +N ((B .N D) .N (F .N S)))
45	34, 44	eqtr 1119	. . 3 |- (((A .N G) +N (B .N F)) .N (D .N S)) = (((A .N D) .N (G .N S)) +N ((B .N D) .N (F .N S)))
46		oprex 3018	. . . . 5 |- (C .N S) e. V
47		oprex 3018	. . . . 5 |- (D .N R) e. V
48	46, 47	distrpi 3820	. . . 4 |- ((B .N G) .N ((C .N S) +N (D .N R))) = (((B .N G) .N (C .N S)) +N ((B .N G) .N (D .N R)))
49		cmpblnq.3	. . . . . 6 |- C e. V
50	41, 36, 49, 31, 38, 39	caopr4 3078	. . . . 5 |- ((B .N G) .N (C .N S)) = ((B .N C) .N (G .N S))
51		cmpblnq.7	. . . . . 6 |- R e. V
52	41, 36, 37, 31, 38, 51	caopr4 3078	. . . . 5 |- ((B .N G) .N (D .N R)) = ((B .N D) .N (G .N R))
53	50, 52	opreq12i 3011	. . . 4 |- (((B .N G) .N (C .N S)) +N ((B .N G) .N (D .N R))) = (((B .N C) .N (G .N S)) +N ((B .N D) .N (G .N R)))
54	48, 53	eqtr 1119	. . 3 |- ((B .N G) .N ((C .N S) +N (D .N R))) = (((B .N C) .N (G .N S)) +N ((B .N D) .N (G .N R)))
55	25, 45, 54	3eqtr4g 1147	. 2 |- (((A .N D) = (B .N C) /\ (F .N S) = (G .N R)) -> (((A .N G) +N (B .N F)) .N (D .N S)) = ((B .N G) .N ((C .N S) +N (D .N R))))
56	22, 55	syl5bir 184	1 |- ((((A e. N. /\ B e. N.) /\ (C e. N. /\ D e. N.)) /\ ((F e. N. /\ G e. N.) /\ (R e. N. /\ S e. N.))) -> (((A