Metamath Proof Explorer

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 𝑅 ) ) ⟩ ) )