Theorem addcmpblnq 5024

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 4992	. . . . . . . 8 |- (((A .N G) e. N. /\ (B .N F) e. N.) -> ((A .N G) +N (B .N F)) e. N.)
2		mulclpi 4993	. . . . . . . 8 |- ((A e. N. /\ G e. N.) -> (A .N G) e. N.)
3		mulclpi 4993	. . . . . . . 8 |- ((B e. N. /\ F e. N.) -> (B .N F) e. N.)
4	1, 2, 3	syl2an 454	. . . . . . 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 508	. . . . . 6 |- (((A e. N. /\ B e. N.) /\ (F e. N. /\ G e. N.)) -> ((A .N G) +N (B .N F)) e. N.)
6		mulclpi 4993	. . . . . . 7 |- ((B e. N. /\ G e. N.) -> (B .N G) e. N.)
7	6	ad2ant2l 408	. . . . . 6 |- (((A e. N. /\ B e. N.) /\ (F e. N. /\ G e. N.)) -> (B .N G) e. N.)
8	5, 7	jca 288	. . . . 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.))
9		addclpi 4992	. . . . . . . 8 |- (((C .N S) e. N. /\ (D .N R) e. N.) -> ((C .N S) +N (D .N R)) e. N.)
10		mulclpi 4993	. . . . . . . 8 |- ((C e. N. /\ S e. N.) -> (C .N S) e. N.)
11		mulclpi 4993	. . . . . . . 8 |- ((D e. N. /\ R e. N.) -> (D .N R) e. N.)
12	9, 10, 11	syl2an 454	. . . . . . 7 |- (((C e. N. /\ S e. N.) /\ (D e. N. /\ R e. N.)) -> ((C .N S) +N (D .N R)) e. N.)
13	12	an42s 508	. . . . . 6 |- (((C e. N. /\ D e. N.) /\ (R e. N. /\ S e. N.)) -> ((C .N S) +N (D .N R)) e. N.)
14		mulclpi 4993	. . . . . . 7 |- ((D e. N. /\ S e. N.) -> (D .N S) e. N.)
15	14	ad2ant2l 408	. . . . . 6 |- (((C e. N. /\ D e. N.) /\ (R e. N. /\ S e. N.)) -> (D .N S) e. N.)
16	13, 15	jca 288	. . . . 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.))
17	8, 16	anim12i 333	. . . 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.)))
18	17	an4s 507	. . 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.)))
19		enqbreq 5016	. . 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)))))
20	18, 19	syl 10	. 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)))))
21		opreq1 3953	. . . 4 |- ((A .N D) = (B .N C) -> ((A .N D) .N (G .N S)) = ((B .N C) .N (G .N S)))
22		opreq2 3954	. . . 4 |- ((F .N S) = (G .N R) -> ((B .N D) .N (F .N S)) = ((B .N D) .N (G .N R)))
23	21, 22	opreqan12d 3964	. . 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))))
24		oprex 3968	. . . . 5 |- (A .N G) e. V
25		oprex 3968	. . . . 5 |- (B .N F) e. V
26		oprex 3968	. . . . 5 |- (D .N S) e. V
27		visset 1804	. . . . . 6 |- x e. V
28		visset 1804	. . . . . 6 |- y e. V
29	27, 28	mulcompi 4996	. . . . 5 |- (x .N y) = (y .N x)
30		visset 1804	. . . . . 6 |- z e. V
31	28, 30	distrpi 4998	. . . . 5 |- (x .N (y +N z)) = ((x .N y) +N (x .N z))
32	24, 25, 26, 29, 31	caoprdistrr 4053	. . . 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)))
33		cmpblnq.1	. . . . . 6 |- A e. V
34		cmpblnq.6	. . . . . 6 |- G e. V
35		cmpblnq.4	. . . . . 6 |- D e. V
36	28, 30	mulasspi 4997	. . . . . 6 |- ((x .N y) .N z) = (x .N (y .N z))
37		cmpblnq.8	. . . . . 6 |- S e. V
38	33, 34, 35, 29, 36, 37	caopr4 4050	. . . . 5 |- ((A .N G) .N (D .N S)) = ((A .N D) .N (G .N S))
39		cmpblnq.2	. . . . . 6 |- B e. V
40		cmpblnq.5	. . . . . 6 |- F e. V
41	39, 40, 35, 29, 36, 37	caopr4 4050	. . . . 5 |- ((B .N F) .N (D .N S)) = ((B .N D) .N (F .N S))
42	38, 41	opreq12i 3958	. . . 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)))
43	32, 42	eqtr 1487	. . 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)))
44		oprex 3968	. . . . 5 |- (C .N S) e. V
45		oprex 3968	. . . . 5 |- (D .N R) e. V
46	44, 45	distrpi 4998	. . . 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)))
47		cmpblnq.3	. . . . . 6 |- C e. V
48	39, 34, 47, 29, 36, 37	caopr4 4050	. . . . 5 |- ((B .N G) .N (C .N S)) = ((B .N C) .N (G .N S))
49		cmpblnq.7	. . . . . 6 |- R e. V
50	39, 34, 35, 29, 36, 49	caopr4 4050	. . . . 5 |- ((B .N G) .N (D .N R)) = ((B .N D) .N (G .N R))
51	48, 50	opreq12i 3958	. . . 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)))
52	46, 51	eqtr 1487	. . 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)))
53	23, 43, 52	3eqtr4g 1523	. 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))))
54	20, 53	syl5bir 210	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 .N D) = (B .N C) /\ (F .N S) = (G .N R)) ->