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 ⊢ A ∈ 𝑷 ∧ B ∈ 𝑷 ∧ C ∈ 𝑷 ∧ D ∈ 𝑷 ∧ F ∈ 𝑷 ∧ G ∈ 𝑷 ∧ R ∈ 𝑷 ∧ S ∈ 𝑷 → A + 𝑷 D = B + 𝑷 C ∧ F + 𝑷 S = G + 𝑷 R → A ⋅ 𝑷 F + 𝑷 B ⋅ 𝑷 G A ⋅ 𝑷 G + 𝑷 B ⋅ 𝑷 F ~ 𝑹 C ⋅ 𝑷 R + 𝑷 D ⋅ 𝑷 S C ⋅ 𝑷 S + 𝑷 D ⋅ 𝑷 R

Proof

Step Hyp Ref Expression
1 mulcmpblnrlem ⊢ A + 𝑷 D = B + 𝑷 C ∧ F + 𝑷 S = G + 𝑷 R → D ⋅ 𝑷 F + 𝑷 A ⋅ 𝑷 F + 𝑷 B ⋅ 𝑷 G + 𝑷 C ⋅ 𝑷 S + 𝑷 D ⋅ 𝑷 R = D ⋅ 𝑷 F + 𝑷 A ⋅ 𝑷 G + 𝑷 B ⋅ 𝑷 F + 𝑷 C ⋅ 𝑷 R + 𝑷 D ⋅ 𝑷 S
2 mulclpr ⊢ D ∈ 𝑷 ∧ F ∈ 𝑷 → D ⋅ 𝑷 F ∈ 𝑷
3 2 ad2ant2lr ⊢ C ∈ 𝑷 ∧ D ∈ 𝑷 ∧ F ∈ 𝑷 ∧ G ∈ 𝑷 → D ⋅ 𝑷 F ∈ 𝑷
4 3 ad2ant2lr ⊢ A ∈ 𝑷 ∧ B ∈ 𝑷 ∧ C ∈ 𝑷 ∧ D ∈ 𝑷 ∧ F ∈ 𝑷 ∧ G ∈ 𝑷 ∧ R ∈ 𝑷 ∧ S ∈ 𝑷 → D ⋅ 𝑷 F ∈ 𝑷
5 simplll ⊢ A ∈ 𝑷 ∧ B ∈ 𝑷 ∧ C ∈ 𝑷 ∧ D ∈ 𝑷 ∧ F ∈ 𝑷 ∧ G ∈ 𝑷 ∧ R ∈ 𝑷 ∧ S ∈ 𝑷 → A ∈ 𝑷
6 simprll ⊢ A ∈ 𝑷 ∧ B ∈ 𝑷 ∧ C ∈ 𝑷 ∧ D ∈ 𝑷 ∧ F ∈ 𝑷 ∧ G ∈ 𝑷 ∧ R ∈ 𝑷 ∧ S ∈ 𝑷 → F ∈ 𝑷
7 mulclpr ⊢ A ∈ 𝑷 ∧ F ∈ 𝑷 → A ⋅ 𝑷 F ∈ 𝑷
8 5 6 7 syl2anc ⊢ A ∈ 𝑷 ∧ B ∈ 𝑷 ∧ C ∈ 𝑷 ∧ D ∈ 𝑷 ∧ F ∈ 𝑷 ∧ G ∈ 𝑷 ∧ R ∈ 𝑷 ∧ S ∈ 𝑷 → A ⋅ 𝑷 F ∈ 𝑷
9 simpllr ⊢ A ∈ 𝑷 ∧ B ∈ 𝑷 ∧ C ∈ 𝑷 ∧ D ∈ 𝑷 ∧ F ∈ 𝑷 ∧ G ∈ 𝑷 ∧ R ∈ 𝑷 ∧ S ∈ 𝑷 → B ∈ 𝑷
10 simprlr ⊢ A ∈ 𝑷 ∧ B ∈ 𝑷 ∧ C ∈ 𝑷 ∧ D ∈ 𝑷 ∧ F ∈ 𝑷 ∧ G ∈ 𝑷 ∧ R ∈ 𝑷 ∧ S ∈ 𝑷 → G ∈ 𝑷
11 mulclpr ⊢ B ∈ 𝑷 ∧ G ∈ 𝑷 → B ⋅ 𝑷 G ∈ 𝑷
12 9 10 11 syl2anc ⊢ A ∈ 𝑷 ∧ B ∈ 𝑷 ∧ C ∈ 𝑷 ∧ D ∈ 𝑷 ∧ F ∈ 𝑷 ∧ G ∈ 𝑷 ∧ R ∈ 𝑷 ∧ S ∈ 𝑷 → B ⋅ 𝑷 G ∈ 𝑷
13 addclpr ⊢ A ⋅ 𝑷 F ∈ 𝑷 ∧ B ⋅ 𝑷 G ∈ 𝑷 → A ⋅ 𝑷 F + 𝑷 B ⋅ 𝑷 G ∈ 𝑷
14 8 12 13 syl2anc ⊢ A ∈ 𝑷 ∧ B ∈ 𝑷 ∧ C ∈ 𝑷 ∧ D ∈ 𝑷 ∧ F ∈ 𝑷 ∧ G ∈ 𝑷 ∧ R ∈ 𝑷 ∧ S ∈ 𝑷 → A ⋅ 𝑷 F + 𝑷 B ⋅ 𝑷 G ∈ 𝑷
15 simplrl ⊢ A ∈ 𝑷 ∧ B ∈ 𝑷 ∧ C ∈ 𝑷 ∧ D ∈ 𝑷 ∧ F ∈ 𝑷 ∧ G ∈ 𝑷 ∧ R ∈ 𝑷 ∧ S ∈ 𝑷 → C ∈ 𝑷
16 simprrr ⊢ A ∈ 𝑷 ∧ B ∈ 𝑷 ∧ C ∈ 𝑷 ∧ D ∈ 𝑷 ∧ F ∈ 𝑷 ∧ G ∈ 𝑷 ∧ R ∈ 𝑷 ∧ S ∈ 𝑷 → S ∈ 𝑷
17 mulclpr ⊢ C ∈ 𝑷 ∧ S ∈ 𝑷 → C ⋅ 𝑷 S ∈ 𝑷
18 15 16 17 syl2anc ⊢ A ∈ 𝑷 ∧ B ∈ 𝑷 ∧ C ∈ 𝑷 ∧ D ∈ 𝑷 ∧ F ∈ 𝑷 ∧ G ∈ 𝑷 ∧ R ∈ 𝑷 ∧ S ∈ 𝑷 → C ⋅ 𝑷 S ∈ 𝑷
19 simplrr ⊢ A ∈ 𝑷 ∧ B ∈ 𝑷 ∧ C ∈ 𝑷 ∧ D ∈ 𝑷 ∧ F ∈ 𝑷 ∧ G ∈ 𝑷 ∧ R ∈ 𝑷 ∧ S ∈ 𝑷 → D ∈ 𝑷
20 simprrl ⊢ A ∈ 𝑷 ∧ B ∈ 𝑷 ∧ C ∈ 𝑷 ∧ D ∈ 𝑷 ∧ F ∈ 𝑷 ∧ G ∈ 𝑷 ∧ R ∈ 𝑷 ∧ S ∈ 𝑷 → R ∈ 𝑷
21 mulclpr ⊢ D ∈ 𝑷 ∧ R ∈ 𝑷 → D ⋅ 𝑷 R ∈ 𝑷
22 19 20 21 syl2anc ⊢ A ∈ 𝑷 ∧ B ∈ 𝑷 ∧ C ∈ 𝑷 ∧ D ∈ 𝑷 ∧ F ∈ 𝑷 ∧ G ∈ 𝑷 ∧ R ∈ 𝑷 ∧ S ∈ 𝑷 → D ⋅ 𝑷 R ∈ 𝑷
23 addclpr ⊢ C ⋅ 𝑷 S ∈ 𝑷 ∧ D ⋅ 𝑷 R ∈ 𝑷 → C ⋅ 𝑷 S + 𝑷 D ⋅ 𝑷 R ∈ 𝑷
24 18 22 23 syl2anc ⊢ A ∈ 𝑷 ∧ B ∈ 𝑷 ∧ C ∈ 𝑷 ∧ D ∈ 𝑷 ∧ F ∈ 𝑷 ∧ G ∈ 𝑷 ∧ R ∈ 𝑷 ∧ S ∈ 𝑷 → C ⋅ 𝑷 S + 𝑷 D ⋅ 𝑷 R ∈ 𝑷
25 addclpr ⊢ A ⋅ 𝑷 F + 𝑷 B ⋅ 𝑷 G ∈ 𝑷 ∧ C ⋅ 𝑷 S + 𝑷 D ⋅ 𝑷 R ∈ 𝑷 → A ⋅ 𝑷 F + 𝑷 B ⋅ 𝑷 G + 𝑷 C ⋅ 𝑷 S + 𝑷 D ⋅ 𝑷 R ∈ 𝑷
26 14 24 25 syl2anc ⊢ A ∈ 𝑷 ∧ B ∈ 𝑷 ∧ C ∈ 𝑷 ∧ D ∈ 𝑷 ∧ F ∈ 𝑷 ∧ G ∈ 𝑷 ∧ R ∈ 𝑷 ∧ S ∈ 𝑷 → A ⋅ 𝑷 F + 𝑷 B ⋅ 𝑷 G + 𝑷 C ⋅ 𝑷 S + 𝑷 D ⋅ 𝑷 R ∈ 𝑷
27 addcanpr ⊢ D ⋅ 𝑷 F ∈ 𝑷 ∧ A ⋅ 𝑷 F + 𝑷 B ⋅ 𝑷 G + 𝑷 C ⋅ 𝑷 S + 𝑷 D ⋅ 𝑷 R ∈ 𝑷 → D ⋅ 𝑷 F + 𝑷 A ⋅ 𝑷 F + 𝑷 B ⋅ 𝑷 G + 𝑷 C ⋅ 𝑷 S + 𝑷 D ⋅ 𝑷 R = D ⋅ 𝑷 F + 𝑷 A ⋅ 𝑷 G + 𝑷 B ⋅ 𝑷 F + 𝑷 C ⋅ 𝑷 R + 𝑷 D ⋅ 𝑷 S → A ⋅ 𝑷 F + 𝑷 B ⋅ 𝑷 G + 𝑷 C ⋅ 𝑷 S + 𝑷 D ⋅ 𝑷 R = A ⋅ 𝑷 G + 𝑷 B ⋅ 𝑷 F + 𝑷 C ⋅ 𝑷 R + 𝑷 D ⋅ 𝑷 S
28 4 26 27 syl2anc ⊢ A ∈ 𝑷 ∧ B ∈ 𝑷 ∧ C ∈ 𝑷 ∧ D ∈ 𝑷 ∧ F ∈ 𝑷 ∧ G ∈ 𝑷 ∧ R ∈ 𝑷 ∧ S ∈ 𝑷 → D ⋅ 𝑷 F + 𝑷 A ⋅ 𝑷 F + 𝑷 B ⋅ 𝑷 G + 𝑷 C ⋅ 𝑷 S + 𝑷 D ⋅ 𝑷 R = D ⋅ 𝑷 F + 𝑷 A ⋅ 𝑷 G + 𝑷 B ⋅ 𝑷 F + 𝑷 C ⋅ 𝑷 R + 𝑷 D ⋅ 𝑷 S → A ⋅ 𝑷 F + 𝑷 B ⋅ 𝑷 G + 𝑷 C ⋅ 𝑷 S + 𝑷 D ⋅ 𝑷 R = A ⋅ 𝑷 G + 𝑷 B ⋅ 𝑷 F + 𝑷 C ⋅ 𝑷 R + 𝑷 D ⋅ 𝑷 S
29 1 28 syl5 ⊢ A ∈ 𝑷 ∧ B ∈ 𝑷 ∧ C ∈ 𝑷 ∧ D ∈ 𝑷 ∧ F ∈ 𝑷 ∧ G ∈ 𝑷 ∧ R ∈ 𝑷 ∧ S ∈ 𝑷 → A + 𝑷 D = B + 𝑷 C ∧ F + 𝑷 S = G + 𝑷 R → A ⋅ 𝑷 F + 𝑷 B ⋅ 𝑷 G + 𝑷 C ⋅ 𝑷 S + 𝑷 D ⋅ 𝑷 R = A ⋅ 𝑷 G + 𝑷 B ⋅ 𝑷 F + 𝑷 C ⋅ 𝑷 R + 𝑷 D ⋅ 𝑷 S
30 mulclpr ⊢ A ∈ 𝑷 ∧ G ∈ 𝑷 → A ⋅ 𝑷 G ∈ 𝑷
31 mulclpr ⊢ B ∈ 𝑷 ∧ F ∈ 𝑷 → B ⋅ 𝑷 F ∈ 𝑷
32 addclpr ⊢ A ⋅ 𝑷 G ∈ 𝑷 ∧ B ⋅ 𝑷 F ∈ 𝑷 → A ⋅ 𝑷 G + 𝑷 B ⋅ 𝑷 F ∈ 𝑷
33 30 31 32 syl2an ⊢ A ∈ 𝑷 ∧ G ∈ 𝑷 ∧ B ∈ 𝑷 ∧ F ∈ 𝑷 → A ⋅ 𝑷 G + 𝑷 B ⋅ 𝑷 F ∈ 𝑷
34 5 10 9 6 33 syl22anc ⊢ A ∈ 𝑷 ∧ B ∈ 𝑷 ∧ C ∈ 𝑷 ∧ D ∈ 𝑷 ∧ F ∈ 𝑷 ∧ G ∈ 𝑷 ∧ R ∈ 𝑷 ∧ S ∈ 𝑷 → A ⋅ 𝑷 G + 𝑷 B ⋅ 𝑷 F ∈ 𝑷
35 mulclpr ⊢ C ∈ 𝑷 ∧ R ∈ 𝑷 → C ⋅ 𝑷 R ∈ 𝑷
36 mulclpr ⊢ D ∈ 𝑷 ∧ S ∈ 𝑷 → D ⋅ 𝑷 S ∈ 𝑷
37 addclpr ⊢ C ⋅ 𝑷 R ∈ 𝑷 ∧ D ⋅ 𝑷 S ∈ 𝑷 → C ⋅ 𝑷 R + 𝑷 D ⋅ 𝑷 S ∈ 𝑷
38 35 36 37 syl2an ⊢ C ∈ 𝑷 ∧ R ∈ 𝑷 ∧ D ∈ 𝑷 ∧ S ∈ 𝑷 → C ⋅ 𝑷 R + 𝑷 D ⋅ 𝑷 S ∈ 𝑷
39 15 20 19 16 38 syl22anc ⊢ A ∈ 𝑷 ∧ B ∈ 𝑷 ∧ C ∈ 𝑷 ∧ D ∈ 𝑷 ∧ F ∈ 𝑷 ∧ G ∈ 𝑷 ∧ R ∈ 𝑷 ∧ S ∈ 𝑷 → C ⋅ 𝑷 R + 𝑷 D ⋅ 𝑷 S ∈ 𝑷
40 enrbreq ⊢ A ⋅ 𝑷 F + 𝑷 B ⋅ 𝑷 G ∈ 𝑷 ∧ A ⋅ 𝑷 G + 𝑷 B ⋅ 𝑷 F ∈ 𝑷 ∧ C ⋅ 𝑷 R + 𝑷 D ⋅ 𝑷 S ∈ 𝑷 ∧ C ⋅ 𝑷 S + 𝑷 D ⋅ 𝑷 R ∈ 𝑷 → A ⋅ 𝑷 F + 𝑷 B ⋅ 𝑷 G A ⋅ 𝑷 G + 𝑷 B ⋅ 𝑷 F ~ 𝑹 C ⋅ 𝑷 R + 𝑷 D ⋅ 𝑷 S C ⋅ 𝑷 S + 𝑷 D ⋅ 𝑷 R ↔ A ⋅ 𝑷 F + 𝑷 B ⋅ 𝑷 G + 𝑷 C ⋅ 𝑷 S + 𝑷 D ⋅ 𝑷 R = A ⋅ 𝑷 G + 𝑷 B ⋅ 𝑷 F + 𝑷 C ⋅ 𝑷 R + 𝑷 D ⋅ 𝑷 S
41 14 34 39 24 40 syl22anc ⊢ A ∈ 𝑷 ∧ B ∈ 𝑷 ∧ C ∈ 𝑷 ∧ D ∈ 𝑷 ∧ F ∈ 𝑷 ∧ G ∈ 𝑷 ∧ R ∈ 𝑷 ∧ S ∈ 𝑷 → A ⋅ 𝑷 F + 𝑷 B ⋅ 𝑷 G A ⋅ 𝑷 G + 𝑷 B ⋅ 𝑷 F ~ 𝑹 C ⋅ 𝑷 R + 𝑷 D ⋅ 𝑷 S C ⋅ 𝑷 S + 𝑷 D ⋅ 𝑷 R ↔ A ⋅ 𝑷 F + 𝑷 B ⋅ 𝑷 G + 𝑷 C ⋅ 𝑷 S + 𝑷 D ⋅ 𝑷 R = A ⋅ 𝑷 G + 𝑷 B ⋅ 𝑷 F + 𝑷 C ⋅ 𝑷 R + 𝑷 D ⋅ 𝑷 S
42 29 41 sylibrd ⊢ A ∈ 𝑷 ∧ B ∈ 𝑷 ∧ C ∈ 𝑷 ∧ D ∈ 𝑷 ∧ F ∈ 𝑷 ∧ G ∈ 𝑷 ∧ R ∈ 𝑷 ∧ S ∈ 𝑷 → A + 𝑷 D = B + 𝑷 C ∧ F + 𝑷 S = G + 𝑷 R → A ⋅ 𝑷 F + 𝑷 B ⋅ 𝑷 G A ⋅ 𝑷 G + 𝑷 B ⋅ 𝑷 F ~ 𝑹 C ⋅ 𝑷 R + 𝑷 D ⋅ 𝑷 S C ⋅ 𝑷 S + 𝑷 D ⋅ 𝑷 R