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 ( ( 𝐴 ·R 𝐵 ) ·R 𝐶 ) = ( 𝐴 ·R ( 𝐵 ·R 𝐶 ) )

Proof

Step Hyp Ref Expression
1 df-nr ⊢ R = ( ( P × P ) / ~R )
2 mulsrpr ⊢ ( ( ( 𝑥 ∈ P ∧ 𝑦 ∈ P ) ∧ ( 𝑧 ∈ P ∧ 𝑤 ∈ P ) ) → ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ~R ·R [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R ) = [ ⟨ ( ( 𝑥 ·P 𝑧 ) +P ( 𝑦 ·P 𝑤 ) ) , ( ( 𝑥 ·P 𝑤 ) +P ( 𝑦 ·P 𝑧 ) ) ⟩ ] ~R )
3 mulsrpr ⊢ ( ( ( 𝑧 ∈ P ∧ 𝑤 ∈ P ) ∧ ( 𝑣 ∈ P ∧ 𝑢 ∈ P ) ) → ( [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R ·R [ ⟨ 𝑣 , 𝑢 ⟩ ] ~R ) = [ ⟨ ( ( 𝑧 ·P 𝑣 ) +P ( 𝑤 ·P 𝑢 ) ) , ( ( 𝑧 ·P 𝑢 ) +P ( 𝑤 ·P 𝑣 ) ) ⟩ ] ~R )
4 mulsrpr ⊢ ( ( ( ( ( 𝑥 ·P 𝑧 ) +P ( 𝑦 ·P 𝑤 ) ) ∈ P ∧ ( ( 𝑥 ·P 𝑤 ) +P ( 𝑦 ·P 𝑧 ) ) ∈ P ) ∧ ( 𝑣 ∈ P ∧ 𝑢 ∈ P ) ) → ( [ ⟨ ( ( 𝑥 ·P 𝑧 ) +P ( 𝑦 ·P 𝑤 ) ) , ( ( 𝑥 ·P 𝑤 ) +P ( 𝑦 ·P 𝑧 ) ) ⟩ ] ~R ·R [ ⟨ 𝑣 , 𝑢 ⟩ ] ~R ) = [ ⟨ ( ( ( ( 𝑥 ·P 𝑧 ) +P ( 𝑦 ·P 𝑤 ) ) ·P 𝑣 ) +P ( ( ( 𝑥 ·P 𝑤 ) +P ( 𝑦 ·P 𝑧 ) ) ·P 𝑢 ) ) , ( ( ( ( 𝑥 ·P 𝑧 ) +P ( 𝑦 ·P 𝑤 ) ) ·P 𝑢 ) +P ( ( ( 𝑥 ·P 𝑤 ) +P ( 𝑦 ·P 𝑧 ) ) ·P 𝑣 ) ) ⟩ ] ~R )
5 mulsrpr ⊢ ( ( ( 𝑥 ∈ P ∧ 𝑦 ∈ P ) ∧ ( ( ( 𝑧 ·P 𝑣 ) +P ( 𝑤 ·P 𝑢 ) ) ∈ P ∧ ( ( 𝑧 ·P 𝑢 ) +P ( 𝑤 ·P 𝑣 ) ) ∈ P ) ) → ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ~R ·R [ ⟨ ( ( 𝑧 ·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 𝑢 ) ) ) ) ⟩ ] ~R )
6 mulclpr ⊢ ( ( 𝑥 ∈ P ∧ 𝑧 ∈ P ) → ( 𝑥 ·P 𝑧 ) ∈ P )
7 mulclpr ⊢ ( ( 𝑦 ∈ P ∧ 𝑤 ∈ P ) → ( 𝑦 ·P 𝑤 ) ∈ P )
8 addclpr ⊢ ( ( ( 𝑥 ·P 𝑧 ) ∈ P ∧ ( 𝑦 ·P 𝑤 ) ∈ P ) → ( ( 𝑥 ·P 𝑧 ) +P ( 𝑦 ·P 𝑤 ) ) ∈ P )
9 6 7 8 syl2an ⊢ ( ( ( 𝑥 ∈ P ∧ 𝑧 ∈ P ) ∧ ( 𝑦 ∈ P ∧ 𝑤 ∈ P ) ) → ( ( 𝑥 ·P 𝑧 ) +P ( 𝑦 ·P 𝑤 ) ) ∈ P )
10 9 an4s ⊢ ( ( ( 𝑥 ∈ P ∧ 𝑦 ∈ P ) ∧ ( 𝑧 ∈ P ∧ 𝑤 ∈ P ) ) → ( ( 𝑥 ·P 𝑧 ) +P ( 𝑦 ·P 𝑤 ) ) ∈ P )
11 mulclpr ⊢ ( ( 𝑥 ∈ P ∧ 𝑤 ∈ P ) → ( 𝑥 ·P 𝑤 ) ∈ P )
12 mulclpr ⊢ ( ( 𝑦 ∈ P ∧ 𝑧 ∈ P ) → ( 𝑦 ·P 𝑧 ) ∈ P )
13 addclpr ⊢ ( ( ( 𝑥 ·P 𝑤 ) ∈ P ∧ ( 𝑦 ·P 𝑧 ) ∈ P ) → ( ( 𝑥 ·P 𝑤 ) +P ( 𝑦 ·P 𝑧 ) ) ∈ P )
14 11 12 13 syl2an ⊢ ( ( ( 𝑥 ∈ P ∧ 𝑤 ∈ P ) ∧ ( 𝑦 ∈ P ∧ 𝑧 ∈ P ) ) → ( ( 𝑥 ·P 𝑤 ) +P ( 𝑦 ·P 𝑧 ) ) ∈ P )
15 14 an42s ⊢ ( ( ( 𝑥 ∈ P ∧ 𝑦 ∈ P ) ∧ ( 𝑧 ∈ P ∧ 𝑤 ∈ P ) ) → ( ( 𝑥 ·P 𝑤 ) +P ( 𝑦 ·P 𝑧 ) ) ∈ P )
16 10 15 jca ⊢ ( ( ( 𝑥 ∈ P ∧ 𝑦 ∈ P ) ∧ ( 𝑧 ∈ P ∧ 𝑤 ∈ P ) ) → ( ( ( 𝑥 ·P 𝑧 ) +P ( 𝑦 ·P 𝑤 ) ) ∈ P ∧ ( ( 𝑥 ·P 𝑤 ) +P ( 𝑦 ·P 𝑧 ) ) ∈ P ) )
17 mulclpr ⊢ ( ( 𝑧 ∈ P ∧ 𝑣 ∈ P ) → ( 𝑧 ·P 𝑣 ) ∈ P )
18 mulclpr ⊢ ( ( 𝑤 ∈ P ∧ 𝑢 ∈ P ) → ( 𝑤 ·P 𝑢 ) ∈ P )
19 addclpr ⊢ ( ( ( 𝑧 ·P 𝑣 ) ∈ P ∧ ( 𝑤 ·P 𝑢 ) ∈ P ) → ( ( 𝑧 ·P 𝑣 ) +P ( 𝑤 ·P 𝑢 ) ) ∈ P )
20 17 18 19 syl2an ⊢ ( ( ( 𝑧 ∈ P ∧ 𝑣 ∈ P ) ∧ ( 𝑤 ∈ P ∧ 𝑢 ∈ P ) ) → ( ( 𝑧 ·P 𝑣 ) +P ( 𝑤 ·P 𝑢 ) ) ∈ P )
21 20 an4s ⊢ ( ( ( 𝑧 ∈ P ∧ 𝑤 ∈ P ) ∧ ( 𝑣 ∈ P ∧ 𝑢 ∈ P ) ) → ( ( 𝑧 ·P 𝑣 ) +P ( 𝑤 ·P 𝑢 ) ) ∈ P )
22 mulclpr ⊢ ( ( 𝑧 ∈ P ∧ 𝑢 ∈ P ) → ( 𝑧 ·P 𝑢 ) ∈ P )
23 mulclpr ⊢ ( ( 𝑤 ∈ P ∧ 𝑣 ∈ P ) → ( 𝑤 ·P 𝑣 ) ∈ P )
24 addclpr ⊢ ( ( ( 𝑧 ·P 𝑢 ) ∈ P ∧ ( 𝑤 ·P 𝑣 ) ∈ P ) → ( ( 𝑧 ·P 𝑢 ) +P ( 𝑤 ·P 𝑣 ) ) ∈ P )
25 22 23 24 syl2an ⊢ ( ( ( 𝑧 ∈ P ∧ 𝑢 ∈ P ) ∧ ( 𝑤 ∈ P ∧ 𝑣 ∈ P ) ) → ( ( 𝑧 ·P 𝑢 ) +P ( 𝑤 ·P 𝑣 ) ) ∈ P )
26 25 an42s ⊢ ( ( ( 𝑧 ∈ P ∧ 𝑤 ∈ P ) ∧ ( 𝑣 ∈ P ∧ 𝑢 ∈ P ) ) → ( ( 𝑧 ·P 𝑢 ) +P ( 𝑤 ·P 𝑣 ) ) ∈ P )
27 21 26 jca ⊢ ( ( ( 𝑧 ∈ P ∧ 𝑤 ∈ P ) ∧ ( 𝑣 ∈ P ∧ 𝑢 ∈ P ) ) → ( ( ( 𝑧 ·P 𝑣 ) +P ( 𝑤 ·P 𝑢 ) ) ∈ P ∧ ( ( 𝑧 ·P 𝑢 ) +P ( 𝑤 ·P 𝑣 ) ) ∈ P ) )
28 vex ⊢ 𝑥 ∈ V
29 vex ⊢ 𝑦 ∈ V
30 vex ⊢ 𝑧 ∈ V
31 mulcompr ⊢ ( 𝑓 ·P 𝑔 ) = ( 𝑔 ·P 𝑓 )
32 distrpr ⊢ ( 𝑓 ·P ( 𝑔 +P ℎ ) ) = ( ( 𝑓 ·P 𝑔 ) +P ( 𝑓 ·P ℎ ) )
33 vex ⊢ 𝑤 ∈ V
34 vex ⊢ 𝑣 ∈ V
35 mulasspr ⊢ ( ( 𝑓 ·P 𝑔 ) ·P ℎ ) = ( 𝑓 ·P ( 𝑔 ·P ℎ ) )
36 vex ⊢ 𝑢 ∈ V
37 addcompr ⊢ ( 𝑓 +P 𝑔 ) = ( 𝑔 +P 𝑓 )
38 addasspr ⊢ ( ( 𝑓 +P 𝑔 ) +P ℎ ) = ( 𝑓 +P ( 𝑔 +P ℎ ) )
39 28 29 30 31 32 33 34 35 36 37 38 caovlem2 ⊢ ( ( ( ( 𝑥 ·P 𝑧 ) +P ( 𝑦 ·P 𝑤 ) ) ·P 𝑣 ) +P ( ( ( 𝑥 ·P 𝑤 ) +P ( 𝑦 ·P 𝑧 ) ) ·P 𝑢 ) ) = ( ( 𝑥 ·P ( ( 𝑧 ·P 𝑣 ) +P ( 𝑤 ·P 𝑢 ) ) ) +P ( 𝑦 ·P ( ( 𝑧 ·P 𝑢 ) +P ( 𝑤 ·P 𝑣 ) ) ) )
40 28 29 30 31 32 33 36 35 34 37 38 caovlem2 ⊢ ( ( ( ( 𝑥 ·P 𝑧 ) +P ( 𝑦 ·P 𝑤 ) ) ·P 𝑢 ) +P ( ( ( 𝑥 ·P 𝑤 ) +P ( 𝑦 ·P 𝑧 ) ) ·P 𝑣 ) ) = ( ( 𝑥 ·P ( ( 𝑧 ·P 𝑢 ) +P ( 𝑤 ·P 𝑣 ) ) ) +P ( 𝑦 ·P ( ( 𝑧 ·P 𝑣 ) +P ( 𝑤 ·P 𝑢 ) ) ) )
41 1 2 3 4 5 16 27 39 40 ecovass ⊢ ( ( 𝐴 ∈ R ∧ 𝐵 ∈ R ∧ 𝐶 ∈ R ) → ( ( 𝐴 ·R 𝐵 ) ·R 𝐶 ) = ( 𝐴 ·R ( 𝐵 ·R 𝐶 ) ) )
42 dmmulsr ⊢ dom ·R = ( R × R )
43 0nsr ⊢ ¬ ∅ ∈ R
44 42 43 ndmovass ⊢ ( ¬ ( 𝐴 ∈ R ∧ 𝐵 ∈ R ∧ 𝐶 ∈ R ) → ( ( 𝐴 ·R 𝐵 ) ·R 𝐶 ) = ( 𝐴 ·R ( 𝐵 ·R 𝐶 ) ) )
45 41 44 pm2.61i ⊢ ( ( 𝐴 ·R 𝐵 ) ·R 𝐶 ) = ( 𝐴 ·R ( 𝐵 ·R 𝐶 ) )