distrsr

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

		Ref	Expression
	Assertion	distrsr	$⊢ A \cdot_{𝑹} (B +_{𝑹} C) = (A \cdot_{𝑹} B) +_{𝑹} (A \cdot_{𝑹} C)$

Proof

Step	Hyp	Ref	Expression
1		df-nr	$⊢ 𝑹 = (𝑷 \times 𝑷) / ~_{𝑹}$
2		addsrpr	$⊢ ((z \in 𝑷 \land w \in 𝑷) \land (v \in 𝑷 \land u \in 𝑷)) \to [⟨z, w⟩] ~_{𝑹} +_{𝑹} [⟨v, u⟩] ~_{𝑹} = [⟨z +_{𝑷} v, w +_{𝑷} u⟩] ~_{𝑹}$
3		mulsrpr	$⊢ ((x \in 𝑷 \land y \in 𝑷) \land (z +_{𝑷} v \in 𝑷 \land w +_{𝑷} u \in 𝑷)) \to [⟨x, y⟩] ~_{𝑹} \cdot_{𝑹} [⟨z +_{𝑷} v, w +_{𝑷} u⟩] ~_{𝑹} = [⟨(x \cdot_{𝑷} (z +_{𝑷} v)) +_{𝑷} (y \cdot_{𝑷} (w +_{𝑷} u)), (x \cdot_{𝑷} (w +_{𝑷} u)) +_{𝑷} (y \cdot_{𝑷} (z +_{𝑷} v))⟩] ~_{𝑹}$
4		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)⟩] ~_{𝑹}$
5		mulsrpr	$⊢ ((x \in 𝑷 \land y \in 𝑷) \land (v \in 𝑷 \land u \in 𝑷)) \to [⟨x, y⟩] ~_{𝑹} \cdot_{𝑹} [⟨v, u⟩] ~_{𝑹} = [⟨(x \cdot_{𝑷} v) +_{𝑷} (y \cdot_{𝑷} u), (x \cdot_{𝑷} u) +_{𝑷} (y \cdot_{𝑷} v)⟩] ~_{𝑹}$
6		addsrpr	$⊢ (((x \cdot_{𝑷} z) +_{𝑷} (y \cdot_{𝑷} w) \in 𝑷 \land (x \cdot_{𝑷} w) +_{𝑷} (y \cdot_{𝑷} z) \in 𝑷) \land ((x \cdot_{𝑷} v) +_{𝑷} (y \cdot_{𝑷} u) \in 𝑷 \land (x \cdot_{𝑷} u) +_{𝑷} (y \cdot_{𝑷} v) \in 𝑷)) \to [⟨(x \cdot_{𝑷} z) +_{𝑷} (y \cdot_{𝑷} w), (x \cdot_{𝑷} w) +_{𝑷} (y \cdot_{𝑷} z)⟩] ~_{𝑹} +_{𝑹} [⟨(x \cdot_{𝑷} v) +_{𝑷} (y \cdot_{𝑷} u), (x \cdot_{𝑷} u) +_{𝑷} (y \cdot_{𝑷} v)⟩] ~_{𝑹} = [⟨((x \cdot_{𝑷} z) +_{𝑷} (y \cdot_{𝑷} w)) +_{𝑷} ((x \cdot_{𝑷} v) +_{𝑷} (y \cdot_{𝑷} u)), ((x \cdot_{𝑷} w) +_{𝑷} (y \cdot_{𝑷} z)) +_{𝑷} ((x \cdot_{𝑷} u) +_{𝑷} (y \cdot_{𝑷} v))⟩] ~_{𝑹}$
7		addclpr	$⊢ (z \in 𝑷 \land v \in 𝑷) \to z +_{𝑷} v \in 𝑷$
8		addclpr	$⊢ (w \in 𝑷 \land u \in 𝑷) \to w +_{𝑷} u \in 𝑷$
9	7 8	anim12i	$⊢ ((z \in 𝑷 \land v \in 𝑷) \land (w \in 𝑷 \land u \in 𝑷)) \to (z +_{𝑷} v \in 𝑷 \land w +_{𝑷} u \in 𝑷)$
10	9	an4s	$⊢ ((z \in 𝑷 \land w \in 𝑷) \land (v \in 𝑷 \land u \in 𝑷)) \to (z +_{𝑷} v \in 𝑷 \land w +_{𝑷} u \in 𝑷)$
11		mulclpr	$⊢ (x \in 𝑷 \land z \in 𝑷) \to x \cdot_{𝑷} z \in 𝑷$
12		mulclpr	$⊢ (y \in 𝑷 \land w \in 𝑷) \to y \cdot_{𝑷} w \in 𝑷$
13		addclpr	$⊢ (x \cdot_{𝑷} z \in 𝑷 \land y \cdot_{𝑷} w \in 𝑷) \to (x \cdot_{𝑷} z) +_{𝑷} (y \cdot_{𝑷} w) \in 𝑷$
14	11 12 13	syl2an	$⊢ ((x \in 𝑷 \land z \in 𝑷) \land (y \in 𝑷 \land w \in 𝑷)) \to (x \cdot_{𝑷} z) +_{𝑷} (y \cdot_{𝑷} w) \in 𝑷$
15	14	an4s	$⊢ ((x \in 𝑷 \land y \in 𝑷) \land (z \in 𝑷 \land w \in 𝑷)) \to (x \cdot_{𝑷} z) +_{𝑷} (y \cdot_{𝑷} w) \in 𝑷$
16		mulclpr	$⊢ (x \in 𝑷 \land w \in 𝑷) \to x \cdot_{𝑷} w \in 𝑷$
17		mulclpr	$⊢ (y \in 𝑷 \land z \in 𝑷) \to y \cdot_{𝑷} z \in 𝑷$
18		addclpr	$⊢ (x \cdot_{𝑷} w \in 𝑷 \land y \cdot_{𝑷} z \in 𝑷) \to (x \cdot_{𝑷} w) +_{𝑷} (y \cdot_{𝑷} z) \in 𝑷$
19	16 17 18	syl2an	$⊢ ((x \in 𝑷 \land w \in 𝑷) \land (y \in 𝑷 \land z \in 𝑷)) \to (x \cdot_{𝑷} w) +_{𝑷} (y \cdot_{𝑷} z) \in 𝑷$
20	19	an42s	$⊢ ((x \in 𝑷 \land y \in 𝑷) \land (z \in 𝑷 \land w \in 𝑷)) \to (x \cdot_{𝑷} w) +_{𝑷} (y \cdot_{𝑷} z) \in 𝑷$
21	15 20	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 𝑷)$
22		mulclpr	$⊢ (x \in 𝑷 \land v \in 𝑷) \to x \cdot_{𝑷} v \in 𝑷$
23		mulclpr	$⊢ (y \in 𝑷 \land u \in 𝑷) \to y \cdot_{𝑷} u \in 𝑷$
24		addclpr	$⊢ (x \cdot_{𝑷} v \in 𝑷 \land y \cdot_{𝑷} u \in 𝑷) \to (x \cdot_{𝑷} v) +_{𝑷} (y \cdot_{𝑷} u) \in 𝑷$
25	22 23 24	syl2an	$⊢ ((x \in 𝑷 \land v \in 𝑷) \land (y \in 𝑷 \land u \in 𝑷)) \to (x \cdot_{𝑷} v) +_{𝑷} (y \cdot_{𝑷} u) \in 𝑷$
26	25	an4s	$⊢ ((x \in 𝑷 \land y \in 𝑷) \land (v \in 𝑷 \land u \in 𝑷)) \to (x \cdot_{𝑷} v) +_{𝑷} (y \cdot_{𝑷} u) \in 𝑷$
27		mulclpr	$⊢ (x \in 𝑷 \land u \in 𝑷) \to x \cdot_{𝑷} u \in 𝑷$
28		mulclpr	$⊢ (y \in 𝑷 \land v \in 𝑷) \to y \cdot_{𝑷} v \in 𝑷$
29		addclpr	$⊢ (x \cdot_{𝑷} u \in 𝑷 \land y \cdot_{𝑷} v \in 𝑷) \to (x \cdot_{𝑷} u) +_{𝑷} (y \cdot_{𝑷} v) \in 𝑷$
30	27 28 29	syl2an	$⊢ ((x \in 𝑷 \land u \in 𝑷) \land (y \in 𝑷 \land v \in 𝑷)) \to (x \cdot_{𝑷} u) +_{𝑷} (y \cdot_{𝑷} v) \in 𝑷$
31	30	an42s	$⊢ ((x \in 𝑷 \land y \in 𝑷) \land (v \in 𝑷 \land u \in 𝑷)) \to (x \cdot_{𝑷} u) +_{𝑷} (y \cdot_{𝑷} v) \in 𝑷$
32	26 31	jca	$⊢ ((x \in 𝑷 \land y \in 𝑷) \land (v \in 𝑷 \land u \in 𝑷)) \to ((x \cdot_{𝑷} v) +_{𝑷} (y \cdot_{𝑷} u) \in 𝑷 \land (x \cdot_{𝑷} u) +_{𝑷} (y \cdot_{𝑷} v) \in 𝑷)$
33		distrpr	$⊢ x \cdot_{𝑷} (z +_{𝑷} v) = (x \cdot_{𝑷} z) +_{𝑷} (x \cdot_{𝑷} v)$
34		distrpr	$⊢ y \cdot_{𝑷} (w +_{𝑷} u) = (y \cdot_{𝑷} w) +_{𝑷} (y \cdot_{𝑷} u)$
35	33 34	oveq12i	$⊢ (x \cdot_{𝑷} (z +_{𝑷} v)) +_{𝑷} (y \cdot_{𝑷} (w +_{𝑷} u)) = ((x \cdot_{𝑷} z) +_{𝑷} (x \cdot_{𝑷} v)) +_{𝑷} ((y \cdot_{𝑷} w) +_{𝑷} (y \cdot_{𝑷} u))$
36		ovex	$⊢ x \cdot_{𝑷} z \in V$
37		ovex	$⊢ x \cdot_{𝑷} v \in V$
38		ovex	$⊢ y \cdot_{𝑷} w \in V$
39		addcompr	$⊢ f +_{𝑷} g = g +_{𝑷} f$
40		addasspr	$⊢ (f +_{𝑷} g) +_{𝑷} h = f +_{𝑷} (g +_{𝑷} h)$
41		ovex	$⊢ y \cdot_{𝑷} u \in V$
42	36 37 38 39 40 41	caov4	$⊢ ((x \cdot_{𝑷} z) +_{𝑷} (x \cdot_{𝑷} v)) +_{𝑷} ((y \cdot_{𝑷} w) +_{𝑷} (y \cdot_{𝑷} u)) = ((x \cdot_{𝑷} z) +_{𝑷} (y \cdot_{𝑷} w)) +_{𝑷} ((x \cdot_{𝑷} v) +_{𝑷} (y \cdot_{𝑷} u))$
43	35 42	eqtri	$⊢ (x \cdot_{𝑷} (z +_{𝑷} v)) +_{𝑷} (y \cdot_{𝑷} (w +_{𝑷} u)) = ((x \cdot_{𝑷} z) +_{𝑷} (y \cdot_{𝑷} w)) +_{𝑷} ((x \cdot_{𝑷} v) +_{𝑷} (y \cdot_{𝑷} u))$
44		distrpr	$⊢ x \cdot_{𝑷} (w +_{𝑷} u) = (x \cdot_{𝑷} w) +_{𝑷} (x \cdot_{𝑷} u)$
45		distrpr	$⊢ y \cdot_{𝑷} (z +_{𝑷} v) = (y \cdot_{𝑷} z) +_{𝑷} (y \cdot_{𝑷} v)$
46	44 45	oveq12i	$⊢ (x \cdot_{𝑷} (w +_{𝑷} u)) +_{𝑷} (y \cdot_{𝑷} (z +_{𝑷} v)) = ((x \cdot_{𝑷} w) +_{𝑷} (x \cdot_{𝑷} u)) +_{𝑷} ((y \cdot_{𝑷} z) +_{𝑷} (y \cdot_{𝑷} v))$
47		ovex	$⊢ x \cdot_{𝑷} w \in V$
48		ovex	$⊢ x \cdot_{𝑷} u \in V$
49		ovex	$⊢ y \cdot_{𝑷} z \in V$
50		ovex	$⊢ y \cdot_{𝑷} v \in V$
51	47 48 49 39 40 50	caov4	$⊢ ((x \cdot_{𝑷} w) +_{𝑷} (x \cdot_{𝑷} u)) +_{𝑷} ((y \cdot_{𝑷} z) +_{𝑷} (y \cdot_{𝑷} v)) = ((x \cdot_{𝑷} w) +_{𝑷} (y \cdot_{𝑷} z)) +_{𝑷} ((x \cdot_{𝑷} u) +_{𝑷} (y \cdot_{𝑷} v))$
52	46 51	eqtri	$⊢ (x \cdot_{𝑷} (w +_{𝑷} u)) +_{𝑷} (y \cdot_{𝑷} (z +_{𝑷} v)) = ((x \cdot_{𝑷} w) +_{𝑷} (y \cdot_{𝑷} z)) +_{𝑷} ((x \cdot_{𝑷} u) +_{𝑷} (y \cdot_{𝑷} v))$
53	1 2 3 4 5 6 10 21 32 43 52	ecovdi	$⊢ (A \in 𝑹 \land B \in 𝑹 \land C \in 𝑹) \to A \cdot_{𝑹} (B +_{𝑹} C) = (A \cdot_{𝑹} B) +_{𝑹} (A \cdot_{𝑹} C)$
54		dmaddsr	$⊢ dom +_{𝑹} = 𝑹 \times 𝑹$
55		0nsr	$⊢ \neg \emptyset \in 𝑹$
56		dmmulsr	$⊢ dom \cdot_{𝑹} = 𝑹 \times 𝑹$
57	54 55 56	ndmovdistr	$⊢ \neg (A \in 𝑹 \land B \in 𝑹 \land C \in 𝑹) \to A \cdot_{𝑹} (B +_{𝑹} C) = (A \cdot_{𝑹} B) +_{𝑹} (A \cdot_{𝑹} C)$
58	53 57	pm2.61i	$⊢ A \cdot_{𝑹} (B +_{𝑹} C) = (A \cdot_{𝑹} B) +_{𝑹} (A \cdot_{𝑹} C)$

Metamath Proof Explorer

Theorem distrsr

Proof