Theorem mulcmpblnr

Description: Lemma showing compatibility of multiplication. (Contributed by NM, 5-Sep-1995) (New usage is discouraged.)

	Ref	Expression
Assertion	mulcmpblnr	⊢ ( ( ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) ∧ ( 𝐶 ∈ P ∧ 𝐷 ∈ P ) ) ∧ ( ( 𝐹 ∈ P ∧ 𝐺 ∈ P ) ∧ ( 𝑅 ∈ P ∧ 𝑆 ∈ P ) ) ) → ( ( ( 𝐴 +P 𝐷 ) = ( 𝐵 +P 𝐶 ) ∧ ( 𝐹 +P 𝑆 ) = ( 𝐺 +P 𝑅 ) ) → ⟨ ( ( 𝐴 ·P 𝐹 ) +P ( 𝐵 ·P 𝐺 ) ) , ( ( 𝐴 ·P 𝐺 ) +P ( 𝐵 ·P 𝐹 ) ) ⟩ ~R ⟨ ( ( 𝐶 ·P 𝑅 ) +P ( 𝐷 ·P 𝑆 ) ) , ( ( 𝐶 ·P 𝑆 ) +P ( 𝐷 ·P 𝑅 ) ) ⟩ ) )

Proof

Step	Hyp	Ref	Expression
1		mulcmpblnrlem	⊢ ( ( ( 𝐴 +P 𝐷 ) = ( 𝐵 +P 𝐶 ) ∧ ( 𝐹 +P 𝑆 ) = ( 𝐺 +P 𝑅 ) ) → ( ( 𝐷 ·P 𝐹 ) +P ( ( ( 𝐴 ·P 𝐹 ) +P ( 𝐵 ·P 𝐺 ) ) +P ( ( 𝐶 ·P 𝑆 ) +P ( 𝐷 ·P 𝑅 ) ) ) ) = ( ( 𝐷 ·P 𝐹 ) +P ( ( ( 𝐴 ·P 𝐺 ) +P ( 𝐵 ·P 𝐹 ) ) +P ( ( 𝐶 ·P 𝑅 ) +P ( 𝐷 ·P 𝑆 ) ) ) ) )
2		mulclpr	⊢ ( ( 𝐷 ∈ P ∧ 𝐹 ∈ P ) → ( 𝐷 ·P 𝐹 ) ∈ P )
3	2	ad2ant2lr	⊢ ( ( ( 𝐶 ∈ P ∧ 𝐷 ∈ P ) ∧ ( 𝐹 ∈ P ∧ 𝐺 ∈ P ) ) → ( 𝐷 ·P 𝐹 ) ∈ P )
4	3	ad2ant2lr	⊢ ( ( ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) ∧ ( 𝐶 ∈ P ∧ 𝐷 ∈ P ) ) ∧ ( ( 𝐹 ∈ P ∧ 𝐺 ∈ P ) ∧ ( 𝑅 ∈ P ∧ 𝑆 ∈ P ) ) ) → ( 𝐷 ·P 𝐹 ) ∈ P )
5		simplll	⊢ ( ( ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) ∧ ( 𝐶 ∈ P ∧ 𝐷 ∈ P ) ) ∧ ( ( 𝐹 ∈ P ∧ 𝐺 ∈ P ) ∧ ( 𝑅 ∈ P ∧ 𝑆 ∈ P ) ) ) → 𝐴 ∈ P )
6		simprll	⊢ ( ( ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) ∧ ( 𝐶 ∈ P ∧ 𝐷 ∈ P ) ) ∧ ( ( 𝐹 ∈ P ∧ 𝐺 ∈ P ) ∧ ( 𝑅 ∈ P ∧ 𝑆 ∈ P ) ) ) → 𝐹 ∈ P )
7		mulclpr	⊢ ( ( 𝐴 ∈ P ∧ 𝐹 ∈ P ) → ( 𝐴 ·P 𝐹 ) ∈ P )
8	5 6 7	syl2anc	⊢ ( ( ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) ∧ ( 𝐶 ∈ P ∧ 𝐷 ∈ P ) ) ∧ ( ( 𝐹 ∈ P ∧ 𝐺 ∈ P ) ∧ ( 𝑅 ∈ P ∧ 𝑆 ∈ P ) ) ) → ( 𝐴 ·P 𝐹 ) ∈ P )
9		simpllr	⊢ ( ( ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) ∧ ( 𝐶 ∈ P ∧ 𝐷 ∈ P ) ) ∧ ( ( 𝐹 ∈ P ∧ 𝐺 ∈ P ) ∧ ( 𝑅 ∈ P ∧ 𝑆 ∈ P ) ) ) → 𝐵 ∈ P )
10		simprlr	⊢ ( ( ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) ∧ ( 𝐶 ∈ P ∧ 𝐷 ∈ P ) ) ∧ ( ( 𝐹 ∈ P ∧ 𝐺 ∈ P ) ∧ ( 𝑅 ∈ P ∧ 𝑆 ∈ P ) ) ) → 𝐺 ∈ P )
11		mulclpr	⊢ ( ( 𝐵 ∈ P ∧ 𝐺 ∈ P ) → ( 𝐵 ·P 𝐺 ) ∈ P )
12	9 10 11	syl2anc	⊢ ( ( ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) ∧ ( 𝐶 ∈ P ∧ 𝐷 ∈ P ) ) ∧ ( ( 𝐹 ∈ P ∧ 𝐺 ∈ P ) ∧ ( 𝑅 ∈ P ∧ 𝑆 ∈ P ) ) ) → ( 𝐵 ·P 𝐺 ) ∈ P )
13		addclpr	⊢ ( ( ( 𝐴 ·P 𝐹 ) ∈ P ∧ ( 𝐵 ·P 𝐺 ) ∈ P ) → ( ( 𝐴 ·P 𝐹 ) +P ( 𝐵 ·P 𝐺 ) ) ∈ P )
14	8 12 13	syl2anc	⊢ ( ( ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) ∧ ( 𝐶 ∈ P ∧ 𝐷 ∈ P ) ) ∧ ( ( 𝐹 ∈ P ∧ 𝐺 ∈ P ) ∧ ( 𝑅 ∈ P ∧ 𝑆 ∈ P ) ) ) → ( ( 𝐴 ·P 𝐹 ) +P ( 𝐵 ·P 𝐺 ) ) ∈ P )
15		simplrl	⊢ ( ( ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) ∧ ( 𝐶 ∈ P ∧ 𝐷 ∈ P ) ) ∧ ( ( 𝐹 ∈ P ∧ 𝐺 ∈ P ) ∧ ( 𝑅 ∈ P ∧ 𝑆 ∈ P ) ) ) → 𝐶 ∈ P )
16		simprrr	⊢ ( ( ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) ∧ ( 𝐶 ∈ P ∧ 𝐷 ∈ P ) ) ∧ ( ( 𝐹 ∈ P ∧ 𝐺 ∈ P ) ∧ ( 𝑅 ∈ P ∧ 𝑆 ∈ P ) ) ) → 𝑆 ∈ P )
17		mulclpr	⊢ ( ( 𝐶 ∈ P ∧ 𝑆 ∈ P ) → ( 𝐶 ·P 𝑆 ) ∈ P )
18	15 16 17	syl2anc	⊢ ( ( ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) ∧ ( 𝐶 ∈ P ∧ 𝐷 ∈ P ) ) ∧ ( ( 𝐹 ∈ P ∧ 𝐺 ∈ P ) ∧ ( 𝑅 ∈ P ∧ 𝑆 ∈ P ) ) ) → ( 𝐶 ·P 𝑆 ) ∈ P )
19		simplrr	⊢ ( ( ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) ∧ ( 𝐶 ∈ P ∧ 𝐷 ∈ P ) ) ∧ ( ( 𝐹 ∈ P ∧ 𝐺 ∈ P ) ∧ ( 𝑅 ∈ P ∧ 𝑆 ∈ P ) ) ) → 𝐷 ∈ P )
20		simprrl	⊢ ( ( ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) ∧ ( 𝐶 ∈ P ∧ 𝐷 ∈ P ) ) ∧ ( ( 𝐹 ∈ P ∧ 𝐺 ∈ P ) ∧ ( 𝑅 ∈ P ∧ 𝑆 ∈ P ) ) ) → 𝑅 ∈ P )
21		mulclpr	⊢ ( ( 𝐷 ∈ P ∧ 𝑅 ∈ P ) → ( 𝐷 ·P 𝑅 ) ∈ P )
22	19 20 21	syl2anc	⊢ ( ( ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) ∧ ( 𝐶 ∈ P ∧ 𝐷 ∈ P ) ) ∧ ( ( 𝐹 ∈ P ∧ 𝐺 ∈ P ) ∧ ( 𝑅 ∈ P ∧ 𝑆 ∈ P ) ) ) → ( 𝐷 ·P 𝑅 ) ∈ P )
23		addclpr	⊢ ( ( ( 𝐶 ·P 𝑆 ) ∈ P ∧ ( 𝐷 ·P 𝑅 ) ∈ P ) → ( ( 𝐶 ·P 𝑆 ) +P ( 𝐷 ·P 𝑅 ) ) ∈ P )
24	18 22 23	syl2anc	⊢ ( ( ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) ∧ ( 𝐶 ∈ P ∧ 𝐷 ∈ P ) ) ∧ ( ( 𝐹 ∈ P ∧ 𝐺 ∈ P ) ∧ ( 𝑅 ∈ P ∧ 𝑆 ∈ P ) ) ) → ( ( 𝐶 ·P 𝑆 ) +P ( 𝐷 ·P 𝑅 ) ) ∈ P )
25		addclpr	⊢ ( ( ( ( 𝐴 ·P 𝐹 ) +P ( 𝐵 ·P 𝐺 ) ) ∈ P ∧ ( ( 𝐶 ·P 𝑆 ) +P ( 𝐷 ·P 𝑅 ) ) ∈ P ) → ( ( ( 𝐴 ·P 𝐹 ) +P ( 𝐵 ·P 𝐺 ) ) +P ( ( 𝐶 ·P 𝑆 ) +P ( 𝐷 ·P 𝑅 ) ) ) ∈ P )
26	14 24 25	syl2anc	⊢ ( ( ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) ∧ ( 𝐶 ∈ P ∧ 𝐷 ∈ P ) ) ∧ ( ( 𝐹 ∈ P ∧ 𝐺 ∈ P ) ∧ ( 𝑅 ∈ P ∧ 𝑆 ∈ P ) ) ) → ( ( ( 𝐴 ·P 𝐹 ) +P ( 𝐵 ·P 𝐺 ) ) +P ( ( 𝐶 ·P 𝑆 ) +P ( 𝐷 ·P 𝑅 ) ) ) ∈ P )
27		addcanpr	⊢ ( ( ( 𝐷 ·P 𝐹 ) ∈ P ∧ ( ( ( 𝐴 ·P 𝐹 ) +P ( 𝐵 ·P 𝐺 ) ) +P ( ( 𝐶 ·P 𝑆 ) +P ( 𝐷 ·P 𝑅 ) ) ) ∈ P ) → ( ( ( 𝐷 ·P 𝐹 ) +P ( ( ( 𝐴 ·P 𝐹 ) +P ( 𝐵 ·P 𝐺 ) ) +P ( ( 𝐶 ·P 𝑆 ) +P ( 𝐷 ·P 𝑅 ) ) ) ) = ( ( 𝐷 ·P 𝐹 ) +P ( ( ( 𝐴 ·P 𝐺 ) +P ( 𝐵 ·P 𝐹 ) ) +P ( ( 𝐶 ·P 𝑅 ) +P ( 𝐷 ·P 𝑆 ) ) ) ) → ( ( ( 𝐴 ·P 𝐹 ) +P ( 𝐵 ·P 𝐺 ) ) +P ( ( 𝐶 ·P 𝑆 ) +P ( 𝐷 ·P 𝑅 ) ) ) = ( ( ( 𝐴 ·P 𝐺 ) +P ( 𝐵 ·P 𝐹 ) ) +P ( ( 𝐶 ·P 𝑅 ) +P ( 𝐷 ·P 𝑆 ) ) ) ) )
28	4 26 27	syl2anc	⊢ ( ( ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) ∧ ( 𝐶 ∈ P ∧ 𝐷 ∈ P ) ) ∧ ( ( 𝐹 ∈ P ∧ 𝐺 ∈ P ) ∧ ( 𝑅 ∈ P ∧ 𝑆 ∈ P ) ) ) → ( ( ( 𝐷 ·P 𝐹 ) +P ( ( ( 𝐴 ·P 𝐹 ) +P ( 𝐵 ·P 𝐺 ) ) +P ( ( 𝐶 ·P 𝑆 ) +P ( 𝐷 ·P 𝑅 ) ) ) ) = ( ( 𝐷 ·P 𝐹 ) +P ( ( ( 𝐴 ·P 𝐺 ) +P ( 𝐵 ·P 𝐹 ) ) +P ( ( 𝐶 ·P 𝑅 ) +P ( 𝐷 ·P 𝑆 ) ) ) ) → ( ( ( 𝐴 ·P 𝐹 ) +P ( 𝐵 ·P 𝐺 ) ) +P ( ( 𝐶 ·P 𝑆 ) +P ( 𝐷 ·P 𝑅 ) ) ) = ( ( ( 𝐴 ·P 𝐺 ) +P ( 𝐵 ·P 𝐹 ) ) +P ( ( 𝐶 ·P 𝑅 ) +P ( 𝐷 ·P 𝑆 ) ) ) ) )
29	1 28	syl5	⊢ ( ( ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) ∧ ( 𝐶 ∈ P ∧ 𝐷 ∈ P ) ) ∧ ( ( 𝐹 ∈ P ∧ 𝐺 ∈ P ) ∧ ( 𝑅 ∈ P ∧ 𝑆 ∈ P ) ) ) → ( ( ( 𝐴 +P 𝐷 ) = ( 𝐵 +P 𝐶 ) ∧ ( 𝐹 +P 𝑆 ) = ( 𝐺 +P 𝑅 ) ) → ( ( ( 𝐴 ·P 𝐹 ) +P ( 𝐵 ·P 𝐺 ) ) +P ( ( 𝐶 ·P 𝑆 ) +P ( 𝐷 ·P 𝑅 ) ) ) = ( ( ( 𝐴 ·P 𝐺 ) +P ( 𝐵 ·P 𝐹 ) ) +P ( ( 𝐶 ·P 𝑅 ) +P ( 𝐷 ·P 𝑆 ) ) ) ) )
30		mulclpr	⊢ ( ( 𝐴 ∈ P ∧ 𝐺 ∈ P ) → ( 𝐴 ·P 𝐺 ) ∈ P )
31		mulclpr	⊢ ( ( 𝐵 ∈ P ∧ 𝐹 ∈ P ) → ( 𝐵 ·P 𝐹 ) ∈ P )
32		addclpr	⊢ ( ( ( 𝐴 ·P 𝐺 ) ∈ P ∧ ( 𝐵 ·P 𝐹 ) ∈ P ) → ( ( 𝐴 ·P 𝐺 ) +P ( 𝐵 ·P 𝐹 ) ) ∈ P )
33	30 31 32	syl2an	⊢ ( ( ( 𝐴 ∈ P ∧ 𝐺 ∈ P ) ∧ ( 𝐵 ∈ P ∧ 𝐹 ∈ P ) ) → ( ( 𝐴 ·P 𝐺 ) +P ( 𝐵 ·P 𝐹 ) ) ∈ P )
34	5 10 9 6 33	syl22anc	⊢ ( ( ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) ∧ ( 𝐶 ∈ P ∧ 𝐷 ∈ P ) ) ∧ ( ( 𝐹 ∈ P ∧ 𝐺 ∈ P ) ∧ ( 𝑅 ∈ P ∧ 𝑆 ∈ P ) ) ) → ( ( 𝐴 ·P 𝐺 ) +P ( 𝐵 ·P 𝐹 ) ) ∈ P )
35		mulclpr	⊢ ( ( 𝐶 ∈ P ∧ 𝑅 ∈ P ) → ( 𝐶 ·P 𝑅 ) ∈ P )
36		mulclpr	⊢ ( ( 𝐷 ∈ P ∧ 𝑆 ∈ P ) → ( 𝐷 ·P 𝑆 ) ∈ P )
37		addclpr	⊢ ( ( ( 𝐶 ·P 𝑅 ) ∈ P ∧ ( 𝐷 ·P 𝑆 ) ∈ P ) → ( ( 𝐶 ·P 𝑅 ) +P ( 𝐷 ·P 𝑆 ) ) ∈ P )
38	35 36 37	syl2an	⊢ ( ( ( 𝐶 ∈ P ∧ 𝑅 ∈ P ) ∧ ( 𝐷 ∈ P ∧ 𝑆 ∈ P ) ) → ( ( 𝐶 ·P 𝑅 ) +P ( 𝐷 ·P 𝑆 ) ) ∈ P )
39	15 20 19 16 38	syl22anc	⊢ ( ( ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) ∧ ( 𝐶 ∈ P ∧ 𝐷 ∈ P ) ) ∧ ( ( 𝐹 ∈ P ∧ 𝐺 ∈ P ) ∧ ( 𝑅 ∈ P ∧ 𝑆 ∈ P ) ) ) → ( ( 𝐶 ·P 𝑅 ) +P ( 𝐷 ·P 𝑆 ) ) ∈ P )
40		enrbreq	⊢ ( ( ( ( ( 𝐴 ·P 𝐹 ) +P ( 𝐵 ·P 𝐺 ) ) ∈ P ∧ ( ( 𝐴 ·P 𝐺 ) +P ( 𝐵 ·P 𝐹 ) ) ∈ P ) ∧ ( ( ( 𝐶 ·P 𝑅 ) +P ( 𝐷 ·P 𝑆 ) ) ∈ P ∧ ( ( 𝐶 ·P 𝑆 ) +P ( 𝐷 ·P 𝑅 ) ) ∈ P ) ) → ( ⟨ ( ( 𝐴 ·P 𝐹 ) +P ( 𝐵 ·P 𝐺 ) ) , ( ( 𝐴 ·P 𝐺 ) +P ( 𝐵 ·P 𝐹 ) ) ⟩ ~R ⟨ ( ( 𝐶 ·P 𝑅 ) +P ( 𝐷 ·P 𝑆 ) ) , ( ( 𝐶 ·P 𝑆 ) +P ( 𝐷 ·P 𝑅 ) ) ⟩ ↔ ( ( ( 𝐴 ·P 𝐹 ) +P ( 𝐵 ·P 𝐺 ) ) +P ( ( 𝐶 ·P 𝑆 ) +P ( 𝐷 ·P 𝑅 ) ) ) = ( ( ( 𝐴 ·P 𝐺 ) +P ( 𝐵 ·P 𝐹 ) ) +P ( ( 𝐶 ·P 𝑅 ) +P ( 𝐷 ·P 𝑆 ) ) ) ) )
41	14 34 39 24 40	syl22anc	⊢ ( ( ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) ∧ ( 𝐶 ∈ P ∧ 𝐷 ∈ P ) ) ∧ ( ( 𝐹 ∈ P ∧ 𝐺 ∈ P ) ∧ ( 𝑅 ∈ P ∧ 𝑆 ∈ P ) ) ) → ( ⟨ ( ( 𝐴 ·P 𝐹 ) +P ( 𝐵 ·P 𝐺 ) ) , ( ( 𝐴 ·P 𝐺 ) +P ( 𝐵 ·P 𝐹 ) ) ⟩ ~R ⟨ ( ( 𝐶 ·P 𝑅 ) +P ( 𝐷 ·P 𝑆 ) ) , ( ( 𝐶 ·P 𝑆 ) +P ( 𝐷 ·P 𝑅 ) ) ⟩ ↔ ( ( ( 𝐴 ·P 𝐹 ) +P ( 𝐵 ·P 𝐺 ) ) +P ( ( 𝐶 ·P 𝑆 ) +P ( 𝐷 ·P 𝑅 ) ) ) = ( ( ( 𝐴 ·P 𝐺 ) +P ( 𝐵 ·P 𝐹 ) ) +P ( ( 𝐶 ·P 𝑅 ) +P ( 𝐷 ·P 𝑆 ) ) ) ) )
42	29 41	sylibrd	⊢ ( ( ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) ∧ ( 𝐶 ∈ P ∧ 𝐷 ∈ P ) ) ∧ ( ( 𝐹 ∈ P ∧ 𝐺 ∈ P ) ∧ ( 𝑅 ∈ P ∧ 𝑆 ∈ P ) ) ) → ( ( ( 𝐴 +P 𝐷 ) = ( 𝐵 +P 𝐶 ) ∧ ( 𝐹 +P 𝑆 ) = ( 𝐺 +P 𝑅 ) ) → ⟨ ( ( 𝐴 ·P 𝐹 ) +P ( 𝐵 ·P 𝐺 ) ) , ( ( 𝐴 ·P 𝐺 ) +P ( 𝐵 ·P 𝐹 ) ) ⟩ ~R ⟨ ( ( 𝐶 ·P 𝑅 ) +P ( 𝐷 ·P 𝑆 ) ) , ( ( 𝐶 ·P 𝑆 ) +P ( 𝐷 ·P 𝑅 ) ) ⟩ ) )