Metamath Proof Explorer

Theorem mulasssr

Description: Multiplication of signed reals is associative. (Contributed by NM, 2-Sep-1995) (Revised by Mario Carneiro, 28-Apr-2015) (New usage is discouraged.)

Ref Expression
Assertion mulasssr ⊢ A ⋅ 𝑹 B ⋅ 𝑹 C = A ⋅ 𝑹 B ⋅ 𝑹 C

Proof

Step Hyp Ref Expression
1 df-nr ⊢ 𝑹 = 𝑷 × 𝑷 / ~ 𝑹
2 mulsrpr ⊢ x ∈ 𝑷 ∧ y ∈ 𝑷 ∧ z ∈ 𝑷 ∧ w ∈ 𝑷 → x y ~ 𝑹 ⋅ 𝑹 z w ~ 𝑹 = x ⋅ 𝑷 z + 𝑷 y ⋅ 𝑷 w x ⋅ 𝑷 w + 𝑷 y ⋅ 𝑷 z ~ 𝑹
3 mulsrpr ⊢ z ∈ 𝑷 ∧ w ∈ 𝑷 ∧ v ∈ 𝑷 ∧ u ∈ 𝑷 → z w ~ 𝑹 ⋅ 𝑹 v u ~ 𝑹 = z ⋅ 𝑷 v + 𝑷 w ⋅ 𝑷 u z ⋅ 𝑷 u + 𝑷 w ⋅ 𝑷 v ~ 𝑹
4 mulsrpr ⊢ x ⋅ 𝑷 z + 𝑷 y ⋅ 𝑷 w ∈ 𝑷 ∧ x ⋅ 𝑷 w + 𝑷 y ⋅ 𝑷 z ∈ 𝑷 ∧ v ∈ 𝑷 ∧ u ∈ 𝑷 → x ⋅ 𝑷 z + 𝑷 y ⋅ 𝑷 w x ⋅ 𝑷 w + 𝑷 y ⋅ 𝑷 z ~ 𝑹 ⋅ 𝑹 v u ~ 𝑹 = x ⋅ 𝑷 z + 𝑷 y ⋅ 𝑷 w ⋅ 𝑷 v + 𝑷 x ⋅ 𝑷 w + 𝑷 y ⋅ 𝑷 z ⋅ 𝑷 u x ⋅ 𝑷 z + 𝑷 y ⋅ 𝑷 w ⋅ 𝑷 u + 𝑷 x ⋅ 𝑷 w + 𝑷 y ⋅ 𝑷 z ⋅ 𝑷 v ~ 𝑹
5 mulsrpr ⊢ x ∈ 𝑷 ∧ y ∈ 𝑷 ∧ z ⋅ 𝑷 v + 𝑷 w ⋅ 𝑷 u ∈ 𝑷 ∧ z ⋅ 𝑷 u + 𝑷 w ⋅ 𝑷 v ∈ 𝑷 → x y ~ 𝑹 ⋅ 𝑹 z ⋅ 𝑷 v + 𝑷 w ⋅ 𝑷 u z ⋅ 𝑷 u + 𝑷 w ⋅ 𝑷 v ~ 𝑹 = x ⋅ 𝑷 z ⋅ 𝑷 v + 𝑷 w ⋅ 𝑷 u + 𝑷 y ⋅ 𝑷 z ⋅ 𝑷 u + 𝑷 w ⋅ 𝑷 v x ⋅ 𝑷 z ⋅ 𝑷 u + 𝑷 w ⋅ 𝑷 v + 𝑷 y ⋅ 𝑷 z ⋅ 𝑷 v + 𝑷 w ⋅ 𝑷 u ~ 𝑹
6 mulclpr ⊢ x ∈ 𝑷 ∧ z ∈ 𝑷 → x ⋅ 𝑷 z ∈ 𝑷
7 mulclpr ⊢ y ∈ 𝑷 ∧ w ∈ 𝑷 → y ⋅ 𝑷 w ∈ 𝑷
8 addclpr ⊢ x ⋅ 𝑷 z ∈ 𝑷 ∧ y ⋅ 𝑷 w ∈ 𝑷 → x ⋅ 𝑷 z + 𝑷 y ⋅ 𝑷 w ∈ 𝑷
9 6 7 8 syl2an ⊢ x ∈ 𝑷 ∧ z ∈ 𝑷 ∧ y ∈ 𝑷 ∧ w ∈ 𝑷 → x ⋅ 𝑷 z + 𝑷 y ⋅ 𝑷 w ∈ 𝑷
10 9 an4s ⊢ x ∈ 𝑷 ∧ y ∈ 𝑷 ∧ z ∈ 𝑷 ∧ w ∈ 𝑷 → x ⋅ 𝑷 z + 𝑷 y ⋅ 𝑷 w ∈ 𝑷
11 mulclpr ⊢ x ∈ 𝑷 ∧ w ∈ 𝑷 → x ⋅ 𝑷 w ∈ 𝑷
12 mulclpr ⊢ y ∈ 𝑷 ∧ z ∈ 𝑷 → y ⋅ 𝑷 z ∈ 𝑷
13 addclpr ⊢ x ⋅ 𝑷 w ∈ 𝑷 ∧ y ⋅ 𝑷 z ∈ 𝑷 → x ⋅ 𝑷 w + 𝑷 y ⋅ 𝑷 z ∈ 𝑷
14 11 12 13 syl2an ⊢ x ∈ 𝑷 ∧ w ∈ 𝑷 ∧ y ∈ 𝑷 ∧ z ∈ 𝑷 → x ⋅ 𝑷 w + 𝑷 y ⋅ 𝑷 z ∈ 𝑷
15 14 an42s ⊢ x ∈ 𝑷 ∧ y ∈ 𝑷 ∧ z ∈ 𝑷 ∧ w ∈ 𝑷 → x ⋅ 𝑷 w + 𝑷 y ⋅ 𝑷 z ∈ 𝑷
16 10 15 jca ⊢ x ∈ 𝑷 ∧ y ∈ 𝑷 ∧ z ∈ 𝑷 ∧ w ∈ 𝑷 → x ⋅ 𝑷 z + 𝑷 y ⋅ 𝑷 w ∈ 𝑷 ∧ x ⋅ 𝑷 w + 𝑷 y ⋅ 𝑷 z ∈ 𝑷
17 mulclpr ⊢ z ∈ 𝑷 ∧ v ∈ 𝑷 → z ⋅ 𝑷 v ∈ 𝑷
18 mulclpr ⊢ w ∈ 𝑷 ∧ u ∈ 𝑷 → w ⋅ 𝑷 u ∈ 𝑷
19 addclpr ⊢ z ⋅ 𝑷 v ∈ 𝑷 ∧ w ⋅ 𝑷 u ∈ 𝑷 → z ⋅ 𝑷 v + 𝑷 w ⋅ 𝑷 u ∈ 𝑷
20 17 18 19 syl2an ⊢ z ∈ 𝑷 ∧ v ∈ 𝑷 ∧ w ∈ 𝑷 ∧ u ∈ 𝑷 → z ⋅ 𝑷 v + 𝑷 w ⋅ 𝑷 u ∈ 𝑷
21 20 an4s ⊢ z ∈ 𝑷 ∧ w ∈ 𝑷 ∧ v ∈ 𝑷 ∧ u ∈ 𝑷 → z ⋅ 𝑷 v + 𝑷 w ⋅ 𝑷 u ∈ 𝑷
22 mulclpr ⊢ z ∈ 𝑷 ∧ u ∈ 𝑷 → z ⋅ 𝑷 u ∈ 𝑷
23 mulclpr ⊢ w ∈ 𝑷 ∧ v ∈ 𝑷 → w ⋅ 𝑷 v ∈ 𝑷
24 addclpr ⊢ z ⋅ 𝑷 u ∈ 𝑷 ∧ w ⋅ 𝑷 v ∈ 𝑷 → z ⋅ 𝑷 u + 𝑷 w ⋅ 𝑷 v ∈ 𝑷
25 22 23 24 syl2an ⊢ z ∈ 𝑷 ∧ u ∈ 𝑷 ∧ w ∈ 𝑷 ∧ v ∈ 𝑷 → z ⋅ 𝑷 u + 𝑷 w ⋅ 𝑷 v ∈ 𝑷
26 25 an42s ⊢ z ∈ 𝑷 ∧ w ∈ 𝑷 ∧ v ∈ 𝑷 ∧ u ∈ 𝑷 → z ⋅ 𝑷 u + 𝑷 w ⋅ 𝑷 v ∈ 𝑷
27 21 26 jca ⊢ z ∈ 𝑷 ∧ w ∈ 𝑷 ∧ v ∈ 𝑷 ∧ u ∈ 𝑷 → z ⋅ 𝑷 v + 𝑷 w ⋅ 𝑷 u ∈ 𝑷 ∧ z ⋅ 𝑷 u + 𝑷 w ⋅ 𝑷 v ∈ 𝑷
28 vex ⊢ x ∈ V
29 vex ⊢ y ∈ V
30 vex ⊢ z ∈ V
31 mulcompr ⊢ f ⋅ 𝑷 g = g ⋅ 𝑷 f
32 distrpr ⊢ f ⋅ 𝑷 g + 𝑷 h = f ⋅ 𝑷 g + 𝑷 f ⋅ 𝑷 h
33 vex ⊢ w ∈ V
34 vex ⊢ v ∈ V
35 mulasspr ⊢ f ⋅ 𝑷 g ⋅ 𝑷 h = f ⋅ 𝑷 g ⋅ 𝑷 h
36 vex ⊢ u ∈ V
37 addcompr ⊢ f + 𝑷 g = g + 𝑷 f
38 addasspr ⊢ f + 𝑷 g + 𝑷 h = f + 𝑷 g + 𝑷 h
39 28 29 30 31 32 33 34 35 36 37 38 caovlem2 ⊢ x ⋅ 𝑷 z + 𝑷 y ⋅ 𝑷 w ⋅ 𝑷 v + 𝑷 x ⋅ 𝑷 w + 𝑷 y ⋅ 𝑷 z ⋅ 𝑷 u = x ⋅ 𝑷 z ⋅ 𝑷 v + 𝑷 w ⋅ 𝑷 u + 𝑷 y ⋅ 𝑷 z ⋅ 𝑷 u + 𝑷 w ⋅ 𝑷 v
40 28 29 30 31 32 33 36 35 34 37 38 caovlem2 ⊢ x ⋅ 𝑷 z + 𝑷 y ⋅ 𝑷 w ⋅ 𝑷 u + 𝑷 x ⋅ 𝑷 w + 𝑷 y ⋅ 𝑷 z ⋅ 𝑷 v = x ⋅ 𝑷 z ⋅ 𝑷 u + 𝑷 w ⋅ 𝑷 v + 𝑷 y ⋅ 𝑷 z ⋅ 𝑷 v + 𝑷 w ⋅ 𝑷 u
41 1 2 3 4 5 16 27 39 40 ecovass ⊢ A ∈ 𝑹 ∧ B ∈ 𝑹 ∧ C ∈ 𝑹 → A ⋅ 𝑹 B ⋅ 𝑹 C = A ⋅ 𝑹 B ⋅ 𝑹 C
42 dmmulsr ⊢ dom ⁡ ⋅ 𝑹 = 𝑹 × 𝑹
43 0nsr ⊢ ¬ ∅ ∈ 𝑹
44 42 43 ndmovass ⊢ ¬ A ∈ 𝑹 ∧ B ∈ 𝑹 ∧ C ∈ 𝑹 → A ⋅ 𝑹 B ⋅ 𝑹 C = A ⋅ 𝑹 B ⋅ 𝑹 C
45 41 44 pm2.61i ⊢ A ⋅ 𝑹 B ⋅ 𝑹 C = A ⋅ 𝑹 B ⋅ 𝑹 C