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 \cdot_{𝑹} B) \cdot_{𝑹} C = A \cdot_{𝑹} (B \cdot_{𝑹} C)$

Proof

Step	Hyp	Ref	Expression
1		df-nr	$⊢ 𝑹 = (𝑷 \times 𝑷) / ~_{𝑹}$
2		mulsrpr	$⊢ ((x \in 𝑷 \land y \in 𝑷) \land (z \in 𝑷 \land w \in 𝑷)) \to [⟨x, y⟩] ~_{𝑹} \cdot_{𝑹} [⟨z, w⟩] ~_{𝑹} = [⟨(x \cdot_{𝑷} z) +_{𝑷} (y \cdot_{𝑷} w), (x \cdot_{𝑷} w) +_{𝑷} (y \cdot_{𝑷} z)⟩] ~_{𝑹}$
3		mulsrpr	$⊢ ((z \in 𝑷 \land w \in 𝑷) \land (v \in 𝑷 \land u \in 𝑷)) \to [⟨z, w⟩] ~_{𝑹} \cdot_{𝑹} [⟨v, u⟩] ~_{𝑹} = [⟨(z \cdot_{𝑷} v) +_{𝑷} (w \cdot_{𝑷} u), (z \cdot_{𝑷} u) +_{𝑷} (w \cdot_{𝑷} v)⟩] ~_{𝑹}$
4		mulsrpr	$⊢ (((x \cdot_{𝑷} z) +_{𝑷} (y \cdot_{𝑷} w) \in 𝑷 \land (x \cdot_{𝑷} w) +_{𝑷} (y \cdot_{𝑷} z) \in 𝑷) \land (v \in 𝑷 \land u \in 𝑷)) \to [⟨(x \cdot_{𝑷} z) +_{𝑷} (y \cdot_{𝑷} w), (x \cdot_{𝑷} w) +_{𝑷} (y \cdot_{𝑷} z)⟩] ~_{𝑹} \cdot_{𝑹} [⟨v, u⟩] ~_{𝑹} = [⟨(((x \cdot_{𝑷} z) +_{𝑷} (y \cdot_{𝑷} w)) \cdot_{𝑷} v) +_{𝑷} (((x \cdot_{𝑷} w) +_{𝑷} (y \cdot_{𝑷} z)) \cdot_{𝑷} u), (((x \cdot_{𝑷} z) +_{𝑷} (y \cdot_{𝑷} w)) \cdot_{𝑷} u) +_{𝑷} (((x \cdot_{𝑷} w) +_{𝑷} (y \cdot_{𝑷} z)) \cdot_{𝑷} v)⟩] ~_{𝑹}$
5		mulsrpr	$⊢ ((x \in 𝑷 \land y \in 𝑷) \land ((z \cdot_{𝑷} v) +_{𝑷} (w \cdot_{𝑷} u) \in 𝑷 \land (z \cdot_{𝑷} u) +_{𝑷} (w \cdot_{𝑷} v) \in 𝑷)) \to [⟨x, y⟩] ~_{𝑹} \cdot_{𝑹} [⟨(z \cdot_{𝑷} v) +_{𝑷} (w \cdot_{𝑷} u), (z \cdot_{𝑷} u) +_{𝑷} (w \cdot_{𝑷} v)⟩] ~_{𝑹} = [⟨(x \cdot_{𝑷} ((z \cdot_{𝑷} v) +_{𝑷} (w \cdot_{𝑷} u))) +_{𝑷} (y \cdot_{𝑷} ((z \cdot_{𝑷} u) +_{𝑷} (w \cdot_{𝑷} v))), (x \cdot_{𝑷} ((z \cdot_{𝑷} u) +_{𝑷} (w \cdot_{𝑷} v))) +_{𝑷} (y \cdot_{𝑷} ((z \cdot_{𝑷} v) +_{𝑷} (w \cdot_{𝑷} u)))⟩] ~_{𝑹}$
6		mulclpr	$⊢ (x \in 𝑷 \land z \in 𝑷) \to x \cdot_{𝑷} z \in 𝑷$
7		mulclpr	$⊢ (y \in 𝑷 \land w \in 𝑷) \to y \cdot_{𝑷} w \in 𝑷$
8		addclpr	$⊢ (x \cdot_{𝑷} z \in 𝑷 \land y \cdot_{𝑷} w \in 𝑷) \to (x \cdot_{𝑷} z) +_{𝑷} (y \cdot_{𝑷} w) \in 𝑷$
9	6 7 8	syl2an	$⊢ ((x \in 𝑷 \land z \in 𝑷) \land (y \in 𝑷 \land w \in 𝑷)) \to (x \cdot_{𝑷} z) +_{𝑷} (y \cdot_{𝑷} w) \in 𝑷$
10	9	an4s	$⊢ ((x \in 𝑷 \land y \in 𝑷) \land (z \in 𝑷 \land w \in 𝑷)) \to (x \cdot_{𝑷} z) +_{𝑷} (y \cdot_{𝑷} w) \in 𝑷$
11		mulclpr	$⊢ (x \in 𝑷 \land w \in 𝑷) \to x \cdot_{𝑷} w \in 𝑷$
12		mulclpr	$⊢ (y \in 𝑷 \land z \in 𝑷) \to y \cdot_{𝑷} z \in 𝑷$
13		addclpr	$⊢ (x \cdot_{𝑷} w \in 𝑷 \land y \cdot_{𝑷} z \in 𝑷) \to (x \cdot_{𝑷} w) +_{𝑷} (y \cdot_{𝑷} z) \in 𝑷$
14	11 12 13	syl2an	$⊢ ((x \in 𝑷 \land w \in 𝑷) \land (y \in 𝑷 \land z \in 𝑷)) \to (x \cdot_{𝑷} w) +_{𝑷} (y \cdot_{𝑷} z) \in 𝑷$
15	14	an42s	$⊢ ((x \in 𝑷 \land y \in 𝑷) \land (z \in 𝑷 \land w \in 𝑷)) \to (x \cdot_{𝑷} w) +_{𝑷} (y \cdot_{𝑷} z) \in 𝑷$
16	10 15	jca	$⊢ ((x \in 𝑷 \land y \in 𝑷) \land (z \in 𝑷 \land w \in 𝑷)) \to ((x \cdot_{𝑷} z) +_{𝑷} (y \cdot_{𝑷} w) \in 𝑷 \land (x \cdot_{𝑷} w) +_{𝑷} (y \cdot_{𝑷} z) \in 𝑷)$
17		mulclpr	$⊢ (z \in 𝑷 \land v \in 𝑷) \to z \cdot_{𝑷} v \in 𝑷$
18		mulclpr	$⊢ (w \in 𝑷 \land u \in 𝑷) \to w \cdot_{𝑷} u \in 𝑷$
19		addclpr	$⊢ (z \cdot_{𝑷} v \in 𝑷 \land w \cdot_{𝑷} u \in 𝑷) \to (z \cdot_{𝑷} v) +_{𝑷} (w \cdot_{𝑷} u) \in 𝑷$
20	17 18 19	syl2an	$⊢ ((z \in 𝑷 \land v \in 𝑷) \land (w \in 𝑷 \land u \in 𝑷)) \to (z \cdot_{𝑷} v) +_{𝑷} (w \cdot_{𝑷} u) \in 𝑷$
21	20	an4s	$⊢ ((z \in 𝑷 \land w \in 𝑷) \land (v \in 𝑷 \land u \in 𝑷)) \to (z \cdot_{𝑷} v) +_{𝑷} (w \cdot_{𝑷} u) \in 𝑷$
22		mulclpr	$⊢ (z \in 𝑷 \land u \in 𝑷) \to z \cdot_{𝑷} u \in 𝑷$
23		mulclpr	$⊢ (w \in 𝑷 \land v \in 𝑷) \to w \cdot_{𝑷} v \in 𝑷$
24		addclpr	$⊢ (z \cdot_{𝑷} u \in 𝑷 \land w \cdot_{𝑷} v \in 𝑷) \to (z \cdot_{𝑷} u) +_{𝑷} (w \cdot_{𝑷} v) \in 𝑷$
25	22 23 24	syl2an	$⊢ ((z \in 𝑷 \land u \in 𝑷) \land (w \in 𝑷 \land v \in 𝑷)) \to (z \cdot_{𝑷} u) +_{𝑷} (w \cdot_{𝑷} v) \in 𝑷$
26	25	an42s	$⊢ ((z \in 𝑷 \land w \in 𝑷) \land (v \in 𝑷 \land u \in 𝑷)) \to (z \cdot_{𝑷} u) +_{𝑷} (w \cdot_{𝑷} v) \in 𝑷$
27	21 26	jca	$⊢ ((z \in 𝑷 \land w \in 𝑷) \land (v \in 𝑷 \land u \in 𝑷)) \to ((z \cdot_{𝑷} v) +_{𝑷} (w \cdot_{𝑷} u) \in 𝑷 \land (z \cdot_{𝑷} u) +_{𝑷} (w \cdot_{𝑷} v) \in 𝑷)$
28		vex	$⊢ x \in V$
29		vex	$⊢ y \in V$
30		vex	$⊢ z \in V$
31		mulcompr	$⊢ f \cdot_{𝑷} g = g \cdot_{𝑷} f$
32		distrpr	$⊢ f \cdot_{𝑷} (g +_{𝑷} h) = (f \cdot_{𝑷} g) +_{𝑷} (f \cdot_{𝑷} h)$
33		vex	$⊢ w \in V$
34		vex	$⊢ v \in V$
35		mulasspr	$⊢ (f \cdot_{𝑷} g) \cdot_{𝑷} h = f \cdot_{𝑷} (g \cdot_{𝑷} h)$
36		vex	$⊢ u \in 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 \cdot_{𝑷} z) +_{𝑷} (y \cdot_{𝑷} w)) \cdot_{𝑷} v) +_{𝑷} (((x \cdot_{𝑷} w) +_{𝑷} (y \cdot_{𝑷} z)) \cdot_{𝑷} u) = (x \cdot_{𝑷} ((z \cdot_{𝑷} v) +_{𝑷} (w \cdot_{𝑷} u))) +_{𝑷} (y \cdot_{𝑷} ((z \cdot_{𝑷} u) +_{𝑷} (w \cdot_{𝑷} v)))$
40	28 29 30 31 32 33 36 35 34 37 38	caovlem2	$⊢ (((x \cdot_{𝑷} z) +_{𝑷} (y \cdot_{𝑷} w)) \cdot_{𝑷} u) +_{𝑷} (((x \cdot_{𝑷} w) +_{𝑷} (y \cdot_{𝑷} z)) \cdot_{𝑷} v) = (x \cdot_{𝑷} ((z \cdot_{𝑷} u) +_{𝑷} (w \cdot_{𝑷} v))) +_{𝑷} (y \cdot_{𝑷} ((z \cdot_{𝑷} v) +_{𝑷} (w \cdot_{𝑷} u)))$
41	1 2 3 4 5 16 27 39 40	ecovass	$⊢ (A \in 𝑹 \land B \in 𝑹 \land C \in 𝑹) \to (A \cdot_{𝑹} B) \cdot_{𝑹} C = A \cdot_{𝑹} (B \cdot_{𝑹} C)$
42		dmmulsr	$⊢ dom \cdot_{𝑹} = 𝑹 \times 𝑹$
43		0nsr	$⊢ \neg \emptyset \in 𝑹$
44	42 43	ndmovass	$⊢ \neg (A \in 𝑹 \land B \in 𝑹 \land C \in 𝑹) \to (A \cdot_{𝑹} B) \cdot_{𝑹} C = A \cdot_{𝑹} (B \cdot_{𝑹} C)$
45	41 44	pm2.61i	$⊢ (A \cdot_{𝑹} B) \cdot_{𝑹} C = A \cdot_{𝑹} (B \cdot_{𝑹} C)$

Metamath Proof Explorer

Theorem mulasssr

Proof