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 𝐶 ) )