Theorem mulcmpblnr 3977

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		addclpr 3914	. . . . . . . . . . . . 13 |- ((((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.)
2		oprex 3018	. . . . . . . . . . . . . . . . . 18 |- (((A .P F) +P. (B .P G)) +P. ((C .P S) +P. (D .P R))) e. V
3		oprex 3018	. . . . . . . . . . . . . . . . . 18 |- (((A .P G) +P. (B .P F)) +P. ((C .P R) +P. (D .P S))) e. V
4	2, 3	addcanpr 3946	. . . . . . . . . . . . . . . . 17 |- (((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)))))
5		cmpblnr.1	. . . . . . . . . . . . . . . . . 18 |- A e. V
6		cmpblnr.2	. . . . . . . . . . . . . . . . . 18 |- B e. V
7		cmpblnr.3	. . . . . . . . . . . . . . . . . 18 |- C e. V
8		cmpblnr.4	. . . . . . . . . . . . . . . . . 18 |- D e. V
9		cmpblnr.5	. . . . . . . . . . . . . . . . . 18 |- F e. V
10		cmpblnr.6	. . . . . . . . . . . . . . . . . 18 |- G e. V
11		cmpblnr.7	. . . . . . . . . . . . . . . . . 18 |- R e. V
12		cmpblnr.8	. . . . . . . . . . . . . . . . . 18 |- S e. V
13	5, 6, 7, 8, 9, 10, 11, 12	mulcmpblnrlem 3976	. . . . . . . . . . . . . . . . 17 |- (((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)))))
14	4, 13	syl5 22	. . . . . . . . . . . . . . . 16 |- (((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)))))
15	14	exp 291	. . . . . . . . . . . . . . 15 |- ((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))))))
16	15	com12 13	. . . . . . . . . . . . . 14 |- ((((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))))))
17	16	imp3a 279	. . . . . . . . . . . . 13 |- ((((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)))))
18	1, 17	syl 12	. . . . . . . . . . . 12 |- ((((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)))))
19	18	adantrl 311	. . . . . . . . . . 11 |- ((((A .P F) +P. (B .P G)) 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)))))
20	19	adantlr 310	. . . . . . . . . 10 |- (((((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)))))
21		enrbreq 3968	. . . . . . . . . 10 |- (((((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)))))
22	20, 21	sylibrd 179	. . . . . . . . 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)), ((A .P G) +P. (B .P F))>. ~R <.((C .P R) +P. (D .P S)), ((C .P S) +P. (D .P R))>.))
23		rnlem 579	. . . . . . . . . 10 |- (((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.))))
24		addclpr 3914	. . . . . . . . . . . 12 |- (((A .P F) e. P. /\ (B .P G) e. P.) -> ((A .P F) +P. (B .P G)) e. P.)
25		mulclpr 3916	. . . . . . . . . . . 12 |- ((A e. P. /\ F e. P.) -> (A .P F) e. P.)
26		mulclpr 3916	. . . . . . . . . . . 12 |- ((B e. P. /\ G e. P.) -> (B .P G) e. P.)
27	24, 25, 26	syl2an 349	. . . . . . . . . . 11 |- (((A e. P. /\ F e. P.) /\ (B e. P. /\ G e. P.)) -> ((A .P F) +P. (B .P G)) e. P.)
28		addclpr 3914	. . . . . . . . . . . 12 |- (((A .P G) e. P. /\ (B .P F) e. P.) -> ((A .P G) +P. (B .P