Theorem mulcmpblnr 5155

Description: Lemma showing compatibility of multiplication.

Hypotheses

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

Assertion

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

Proof of Theorem mulcmpblnr

Step	Hyp	Ref	Expression
1		mulclpr 5094	. . . . 5 |- ((D e. P. /\ F e. P.) -> (D .P. F) e. P.)
2		pm3.27 323	. . . . 5 |- ((C e. P. /\ D e. P.) -> D e. P.)
3		pm3.26 319	. . . . 5 |- ((F e. P. /\ G e. P.) -> F e. P.)
4	1, 2, 3	syl2an 454	. . . 4 |- (((C e. P. /\ D e. P.) /\ (F e. P. /\ G e. P.)) -> (D .P. F) e. P.)
5		addclpr 5092	. . . . . . . . . . 11 |- ((((A .P. F) +P. (B .P. G)) e. P. /\ ((C .P. S) +P. (D .P. R)) e. P.) -> (((A .P. F) +P. (B .P. G)) +P. ((C .P. S) +P. (D .P. R))) e. P.)
6		oprex 3968	. . . . . . . . . . . . . . 15 |- (((A .P. F) +P. (B .P. G)) +P. ((C .P. S) +P. (D .P. R))) e. V
7		oprex 3968	. . . . . . . . . . . . . . 15 |- (((A .P. G) +P. (B .P. F)) +P. ((C .P. R) +P. (D .P. S))) e. V
8	6, 7	addcanpr 5124	. . . . . . . . . . . . . 14 |- (((D .P. F) e. P. /\ (((A .P. F) +P. (B .P. G)) +P. ((C .P. S) +P. (D .P. R))) e. P.) -> (((D .P. F) +P. (((A .P. F) +P. (B .P. G)) +P. ((C .P. S) +P. (D .P. R)))) = ((D .P. F) +P. (((A .P. G) +P. (B .P. F)) +P. ((C .P. R) +P. (D .P. S)))) -> (((A .P. F) +P. (B .P. G)) +P. ((C .P. S) +P. (D .P. R))) = (((A .P. G) +P. (B .P. F)) +P. ((C .P. R) +P. (D .P. S)))))
9		cmpblnr.1	. . . . . . . . . . . . . . 15 |- A e. V
10		cmpblnr.2	. . . . . . . . . . . . . . 15 |- B e. V
11		cmpblnr.3	. . . . . . . . . . . . . . 15 |- C e. V
12		cmpblnr.4	. . . . . . . . . . . . . . 15 |- D e. V
13		cmpblnr.5	. . . . . . . . . . . . . . 15 |- F e. V
14		cmpblnr.6	. . . . . . . . . . . . . . 15 |- G e. V
15		cmpblnr.7	. . . . . . . . . . . . . . 15 |- R e. V
16		cmpblnr.8	. . . . . . . . . . . . . . 15 |- S e. V
17	9, 10, 11, 12, 13, 14, 15, 16	mulcmpblnrlem 5154	. . . . . . . . . . . . . 14 |- (((A +P. D) = (B +P. C) /\ (F +P. S) = (G +P. R)) -> ((D .P. F) +P. (((A .P. F) +P. (B .P. G)) +P. ((C .P. S) +P. (D .P. R)))) = ((D .P. F) +P. (((A .P. G) +P. (B .P. F)) +P. ((C .P. R) +P. (D .P. S)))))
18	8, 17	syl5 21	. . . . . . . . . . . . 13 |- (((D .P. F) e. P. /\ (((A .P. F) +P. (B .P. G)) +P. ((C .P. S) +P. (D .P. R))) e. P.) -> (((A +P. D) = (B +P. C) /\ (F +P. S) = (G +P. R)) -> (((A .P. F) +P. (B .P. G)) +P. ((C .P. S) +P. (D .P. R))) = (((A .P. G) +P. (B .P. F)) +P. ((C .P. R) +P. (D .P. S)))))
19	18	expcom 374	. . . . . . . . . . . 12 |- ((((A .P. F) +P. (B .P. G)) +P. ((C .P. S) +P. (D .P. R))) e. P. -> ((D .P. F) e. P. -> (((A +P. D) = (B +P. C) /\ (F +P. S) = (G +P. R)) -> (((A .P. F) +P. (B .P. G)) +P. ((C .P. S) +P. (D .P. R))) = (((A .P. G) +P. (B .P. F)) +P. ((C .P. R) +P. (D .P. S))))))
20	19	imp3a 361	. . . . . . . . . . 11 |- ((((A .P. F) +P. (B .P. G)) +P. ((C .P. S) +P. (D .P. R))) e. P. -> (((D .P. F) e. P. /\ ((A +P. D) = (B +P. C) /\ (F +P. S) = (G +P. R))) -> (((A .P. F) +P. (B .P. G)) +P. ((C .P. S) +P. (D .P. R))) = (((A .P. G) +P. (B .P. F)) +P. ((C .P. R) +P. (D .P. S)))))
21	5, 20	syl 10	. . . . . . . . . 10 |- ((((A .P. F) +P. (B .P. G)) e. P. /\ ((C .P. S) +P. (D .P. R)) e. P.) -> (((D .P. F) e. P. /\ ((A +P. D) = (B +P. C) /\ (F +P. S) = (G +P. R))) -> (((A .P. F) +P. (B .P. G)) +P. ((C .P. S) +P. (D .P. R))) = (((A .P. G) +P. (B .P. F)) +P. ((C .P. R) +P. (D .P. S)))))
22	21	ad2ant2rl 411	. . . . . . . . 9 |- (((((A .P. F) +P. (B .P. G)) e. P. /\ ((A .P. G) +P. (B .P. F)) e. P.) /\ (((C .P. R) +P. (D .P. S)) e. P. /\ ((C .P. S) +P. (D .P. R)) e. P.)) -> (((D .P. F) e. P. /\ ((A +P. D) = (B +P. C) /\ (F +P. S) = (G +P. R))) -> (((A .P. F) +P. (B .P. G)) +P. ((C .P. S) +P. (D .P. R))) = (((A .P. G) +P. (B .P. F)) +P. ((C .P. R) +P. (D .P. S)))))
23		enrbreq 5146	. . . . . . . . 9 |- (((((A .P. F) +P. (B .P. G)) e. P. /\ ((A .P. G) +P. (B .P. F)) e. P.) /\ (((C .P. R) +P. (D .P. S)) e. P. /\ ((C .P. S) +P. (D .P. R)) e. P.)) -> (<.((A .P. F) +P. (B .P. G)), ((A .P. G) +P. (B .P. F))>. ~R <.((C .P. R) +P. (D .P. S)), ((C .P. S) +P. (D .P. R))>. <-> (((A .P. F) +P. (B .P. G)) +P. ((C .P. S) +P. (D .P. R))) = (((A .P. G) +P. (B .P. F)) +P. ((C .P. R) +P. (D .P. S)))))
24	22, 23	sylibrd 204	. . . . . . . 8 |- (((((A .P. F) +P. (B .P. G)) e. P. /\ ((A .P. G) +P. (B .P. F)) e. P.) /\ (((C .P. R) +P. (D .P. S)) e. P. /\ ((C .P. S) +P. (D .P. R)) e. P.)) -> (((D .P. F) e. P. /\ ((A +P. D) = (B +P. C) /\ (F +P. S) = (G +P. R))) -> <.((A .P. F) +P. (B .P. G)), ((A .P. G) +P. (B .P. F))>. ~R <.((C .P. R) +P. (D .P. S)), ((C .P. S) +P. (D .P. R))>.))
25		rnlem 771	. . . . . . . . 9 |- (((A e. P. /\ B e. P.) /\ (F e. P. /\ G e. P.)) <-> (((A e. P. /\ F e. P.) /\ (B e. P. /\ G e. P.)) /\ ((A e. P. /\ G e. P.) /\ (B e. P. /\ F e. P.))))
26		addclpr 5092	. . . . . . . . . . 11 |- (((A .P. F) e. P. /\ (B .P. G) e. P.) -> ((A .P. F) +P. (B .P. G)) e. P.)
27		mulclpr 5094	. . . . . . . . . . 11 |- ((A e. P. /\ F e. P.) -> (A .P. F) e. P.)
28		mulclpr 5094	. . . . . . . . . . 11 |- ((B e. P. /\ G e. P.) -> (B .P. G) e. P.)
29	26, 27, 28	syl2an 454	. . . . . . . . . 10 |- (((A e. P. /\ F e. P.) /\ (B e. P. /\ G e. P.)) -> ((A .P. F) +P. (B .P. G)) e. P.)
30		addclpr 5092	. . . . . . . . . . 11 |- (((A .P. G) e. P. /\ (B .P. F) e. P.) -> ((A .P. G) +P. (B .P. F)) e. P.)
31		mulclpr 5094	. . . . . . . . . . 11 |- ((A e. P. /\ G e. P.) -> (A .P. G) e. P.)
32		mulclpr 5094	. . . . . . . . . . 11 |- ((B e. P. /\ F e. P.) -> (B .P. F) e. P.)
33	30, 31, 32	syl2an 454	. . . . . . . . . 10 |- (((A e. P. /\ G e. P.) /\ (B e. P. /\ F e. P.)) -> ((A .P. G) +P. (B .P. F)) e. P.)
34	29, 33	anim12i 333	. . . . . . . . 9 |- ((((A e. P. /\ F e. P.) /\ (B e. P. /\ G e. P.)) /\ ((A e. P. /\ G e. P.) /\ (B e. P. /\ F e. P.))) -> (((A .P. F) +P. (B