axdistr

Description: Distributive law for complex numbers (left-distributivity). Axiom 11 of 22 for real and complex numbers, derived from ZF set theory. This construction-dependent theorem should not be referenced directly, nor should the proven axiom ax-distr be used later. Instead, use adddi . (Contributed by NM, 2-Sep-1995) (New usage is discouraged.)

		Ref	Expression
	Assertion	axdistr	$⊢ (A \in ℂ \land B \in ℂ \land C \in ℂ) \to A (B + C) = A B + A C$

Proof

Step	Hyp	Ref	Expression
1		dfcnqs	$⊢ ℂ = (𝑹 \times 𝑹) / E^{-1}$
2		addcnsrec	$⊢ ((z \in 𝑹 \land w \in 𝑹) \land (v \in 𝑹 \land u \in 𝑹)) \to [⟨z, w⟩] E^{-1} + [⟨v, u⟩] E^{-1} = [⟨z +_{𝑹} v, w +_{𝑹} u⟩] E^{-1}$
3		mulcnsrec	$⊢ ((x \in 𝑹 \land y \in 𝑹) \land (z +_{𝑹} v \in 𝑹 \land w +_{𝑹} u \in 𝑹)) \to [⟨x, y⟩] E^{-1} [⟨z +_{𝑹} v, w +_{𝑹} u⟩] E^{-1} = [⟨(x \cdot_{𝑹} (z +_{𝑹} v)) +_{𝑹} ({-1}_{𝑹} \cdot_{𝑹} (y \cdot_{𝑹} (w +_{𝑹} u))), (y \cdot_{𝑹} (z +_{𝑹} v)) +_{𝑹} (x \cdot_{𝑹} (w +_{𝑹} u))⟩] E^{-1}$
4		mulcnsrec	$⊢ ((x \in 𝑹 \land y \in 𝑹) \land (z \in 𝑹 \land w \in 𝑹)) \to [⟨x, y⟩] E^{-1} [⟨z, w⟩] E^{-1} = [⟨(x \cdot_{𝑹} z) +_{𝑹} ({-1}_{𝑹} \cdot_{𝑹} (y \cdot_{𝑹} w)), (y \cdot_{𝑹} z) +_{𝑹} (x \cdot_{𝑹} w)⟩] E^{-1}$
5		mulcnsrec	$⊢ ((x \in 𝑹 \land y \in 𝑹) \land (v \in 𝑹 \land u \in 𝑹)) \to [⟨x, y⟩] E^{-1} [⟨v, u⟩] E^{-1} = [⟨(x \cdot_{𝑹} v) +_{𝑹} ({-1}_{𝑹} \cdot_{𝑹} (y \cdot_{𝑹} u)), (y \cdot_{𝑹} v) +_{𝑹} (x \cdot_{𝑹} u)⟩] E^{-1}$
6		addcnsrec	$⊢ (((x \cdot_{𝑹} z) +_{𝑹} ({-1}_{𝑹} \cdot_{𝑹} (y \cdot_{𝑹} w)) \in 𝑹 \land (y \cdot_{𝑹} z) +_{𝑹} (x \cdot_{𝑹} w) \in 𝑹) \land ((x \cdot_{𝑹} v) +_{𝑹} ({-1}_{𝑹} \cdot_{𝑹} (y \cdot_{𝑹} u)) \in 𝑹 \land (y \cdot_{𝑹} v) +_{𝑹} (x \cdot_{𝑹} u) \in 𝑹)) \to [⟨(x \cdot_{𝑹} z) +_{𝑹} ({-1}_{𝑹} \cdot_{𝑹} (y \cdot_{𝑹} w)), (y \cdot_{𝑹} z) +_{𝑹} (x \cdot_{𝑹} w)⟩] E^{-1} + [⟨(x \cdot_{𝑹} v) +_{𝑹} ({-1}_{𝑹} \cdot_{𝑹} (y \cdot_{𝑹} u)), (y \cdot_{𝑹} v) +_{𝑹} (x \cdot_{𝑹} u)⟩] E^{-1} = [⟨((x \cdot_{𝑹} z) +_{𝑹} ({-1}_{𝑹} \cdot_{𝑹} (y \cdot_{𝑹} w))) +_{𝑹} ((x \cdot_{𝑹} v) +_{𝑹} ({-1}_{𝑹} \cdot_{𝑹} (y \cdot_{𝑹} u))), ((y \cdot_{𝑹} z) +_{𝑹} (x \cdot_{𝑹} w)) +_{𝑹} ((y \cdot_{𝑹} v) +_{𝑹} (x \cdot_{𝑹} u))⟩] E^{-1}$
7		addclsr	$⊢ (z \in 𝑹 \land v \in 𝑹) \to z +_{𝑹} v \in 𝑹$
8		addclsr	$⊢ (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		mulclsr	$⊢ (x \in 𝑹 \land z \in 𝑹) \to x \cdot_{𝑹} z \in 𝑹$
12		m1r	$⊢ {-1}_{𝑹} \in 𝑹$
13		mulclsr	$⊢ (y \in 𝑹 \land w \in 𝑹) \to y \cdot_{𝑹} w \in 𝑹$
14		mulclsr	$⊢ ({-1}_{𝑹} \in 𝑹 \land y \cdot_{𝑹} w \in 𝑹) \to {-1}_{𝑹} \cdot_{𝑹} (y \cdot_{𝑹} w) \in 𝑹$
15	12 13 14	sylancr	$⊢ (y \in 𝑹 \land w \in 𝑹) \to {-1}_{𝑹} \cdot_{𝑹} (y \cdot_{𝑹} w) \in 𝑹$
16		addclsr	$⊢ (x \cdot_{𝑹} z \in 𝑹 \land {-1}_{𝑹} \cdot_{𝑹} (y \cdot_{𝑹} w) \in 𝑹) \to (x \cdot_{𝑹} z) +_{𝑹} ({-1}_{𝑹} \cdot_{𝑹} (y \cdot_{𝑹} w)) \in 𝑹$
17	11 15 16	syl2an	$⊢ ((x \in 𝑹 \land z \in 𝑹) \land (y \in 𝑹 \land w \in 𝑹)) \to (x \cdot_{𝑹} z) +_{𝑹} ({-1}_{𝑹} \cdot_{𝑹} (y \cdot_{𝑹} w)) \in 𝑹$
18	17	an4s	$⊢ ((x \in 𝑹 \land y \in 𝑹) \land (z \in 𝑹 \land w \in 𝑹)) \to (x \cdot_{𝑹} z) +_{𝑹} ({-1}_{𝑹} \cdot_{𝑹} (y \cdot_{𝑹} w)) \in 𝑹$
19		mulclsr	$⊢ (y \in 𝑹 \land z \in 𝑹) \to y \cdot_{𝑹} z \in 𝑹$
20		mulclsr	$⊢ (x \in 𝑹 \land w \in 𝑹) \to x \cdot_{𝑹} w \in 𝑹$
21		addclsr	$⊢ (y \cdot_{𝑹} z \in 𝑹 \land x \cdot_{𝑹} w \in 𝑹) \to (y \cdot_{𝑹} z) +_{𝑹} (x \cdot_{𝑹} w) \in 𝑹$
22	19 20 21	syl2anr	$⊢ ((x \in 𝑹 \land w \in 𝑹) \land (y \in 𝑹 \land z \in 𝑹)) \to (y \cdot_{𝑹} z) +_{𝑹} (x \cdot_{𝑹} w) \in 𝑹$
23	22	an42s	$⊢ ((x \in 𝑹 \land y \in 𝑹) \land (z \in 𝑹 \land w \in 𝑹)) \to (y \cdot_{𝑹} z) +_{𝑹} (x \cdot_{𝑹} w) \in 𝑹$
24	18 23	jca	$⊢ ((x \in 𝑹 \land y \in 𝑹) \land (z \in 𝑹 \land w \in 𝑹)) \to ((x \cdot_{𝑹} z) +_{𝑹} ({-1}_{𝑹} \cdot_{𝑹} (y \cdot_{𝑹} w)) \in 𝑹 \land (y \cdot_{𝑹} z) +_{𝑹} (x \cdot_{𝑹} w) \in 𝑹)$
25		mulclsr	$⊢ (x \in 𝑹 \land v \in 𝑹) \to x \cdot_{𝑹} v \in 𝑹$
26		mulclsr	$⊢ (y \in 𝑹 \land u \in 𝑹) \to y \cdot_{𝑹} u \in 𝑹$
27		mulclsr	$⊢ ({-1}_{𝑹} \in 𝑹 \land y \cdot_{𝑹} u \in 𝑹) \to {-1}_{𝑹} \cdot_{𝑹} (y \cdot_{𝑹} u) \in 𝑹$
28	12 26 27	sylancr	$⊢ (y \in 𝑹 \land u \in 𝑹) \to {-1}_{𝑹} \cdot_{𝑹} (y \cdot_{𝑹} u) \in 𝑹$
29		addclsr	$⊢ (x \cdot_{𝑹} v \in 𝑹 \land {-1}_{𝑹} \cdot_{𝑹} (y \cdot_{𝑹} u) \in 𝑹) \to (x \cdot_{𝑹} v) +_{𝑹} ({-1}_{𝑹} \cdot_{𝑹} (y \cdot_{𝑹} u)) \in 𝑹$
30	25 28 29	syl2an	$⊢ ((x \in 𝑹 \land v \in 𝑹) \land (y \in 𝑹 \land u \in 𝑹)) \to (x \cdot_{𝑹} v) +_{𝑹} ({-1}_{𝑹} \cdot_{𝑹} (y \cdot_{𝑹} u)) \in 𝑹$
31	30	an4s	$⊢ ((x \in 𝑹 \land y \in 𝑹) \land (v \in 𝑹 \land u \in 𝑹)) \to (x \cdot_{𝑹} v) +_{𝑹} ({-1}_{𝑹} \cdot_{𝑹} (y \cdot_{𝑹} u)) \in 𝑹$
32		mulclsr	$⊢ (y \in 𝑹 \land v \in 𝑹) \to y \cdot_{𝑹} v \in 𝑹$
33		mulclsr	$⊢ (x \in 𝑹 \land u \in 𝑹) \to x \cdot_{𝑹} u \in 𝑹$
34		addclsr	$⊢ (y \cdot_{𝑹} v \in 𝑹 \land x \cdot_{𝑹} u \in 𝑹) \to (y \cdot_{𝑹} v) +_{𝑹} (x \cdot_{𝑹} u) \in 𝑹$
35	32 33 34	syl2anr	$⊢ ((x \in 𝑹 \land u \in 𝑹) \land (y \in 𝑹 \land v \in 𝑹)) \to (y \cdot_{𝑹} v) +_{𝑹} (x \cdot_{𝑹} u) \in 𝑹$
36	35	an42s	$⊢ ((x \in 𝑹 \land y \in 𝑹) \land (v \in 𝑹 \land u \in 𝑹)) \to (y \cdot_{𝑹} v) +_{𝑹} (x \cdot_{𝑹} u) \in 𝑹$
37	31 36	jca	$⊢ ((x \in 𝑹 \land y \in 𝑹) \land (v \in 𝑹 \land u \in 𝑹)) \to ((x \cdot_{𝑹} v) +_{𝑹} ({-1}_{𝑹} \cdot_{𝑹} (y \cdot_{𝑹} u)) \in 𝑹 \land (y \cdot_{𝑹} v) +_{𝑹} (x \cdot_{𝑹} u) \in 𝑹)$
38		distrsr	$⊢ x \cdot_{𝑹} (z +_{𝑹} v) = (x \cdot_{𝑹} z) +_{𝑹} (x \cdot_{𝑹} v)$
39		distrsr	$⊢ y \cdot_{𝑹} (w +_{𝑹} u) = (y \cdot_{𝑹} w) +_{𝑹} (y \cdot_{𝑹} u)$
40	39	oveq2i	$⊢ {-1}_{𝑹} \cdot_{𝑹} (y \cdot_{𝑹} (w +_{𝑹} u)) = {-1}_{𝑹} \cdot_{𝑹} ((y \cdot_{𝑹} w) +_{𝑹} (y \cdot_{𝑹} u))$
41		distrsr	$⊢ {-1}_{𝑹} \cdot_{𝑹} ((y \cdot_{𝑹} w) +_{𝑹} (y \cdot_{𝑹} u)) = ({-1}_{𝑹} \cdot_{𝑹} (y \cdot_{𝑹} w)) +_{𝑹} ({-1}_{𝑹} \cdot_{𝑹} (y \cdot_{𝑹} u))$
42	40 41	eqtri	$⊢ {-1}_{𝑹} \cdot_{𝑹} (y \cdot_{𝑹} (w +_{𝑹} u)) = ({-1}_{𝑹} \cdot_{𝑹} (y \cdot_{𝑹} w)) +_{𝑹} ({-1}_{𝑹} \cdot_{𝑹} (y \cdot_{𝑹} u))$
43	38 42	oveq12i	$⊢ (x \cdot_{𝑹} (z +_{𝑹} v)) +_{𝑹} ({-1}_{𝑹} \cdot_{𝑹} (y \cdot_{𝑹} (w +_{𝑹} u))) = ((x \cdot_{𝑹} z) +_{𝑹} (x \cdot_{𝑹} v)) +_{𝑹} (({-1}_{𝑹} \cdot_{𝑹} (y \cdot_{𝑹} w)) +_{𝑹} ({-1}_{𝑹} \cdot_{𝑹} (y \cdot_{𝑹} u)))$
44		ovex	$⊢ x \cdot_{𝑹} z \in V$
45		ovex	$⊢ x \cdot_{𝑹} v \in V$
46		ovex	$⊢ {-1}_{𝑹} \cdot_{𝑹} (y \cdot_{𝑹} w) \in V$
47		addcomsr	$⊢ f +_{𝑹} g = g +_{𝑹} f$
48		addasssr	$⊢ (f +_{𝑹} g) +_{𝑹} h = f +_{𝑹} (g +_{𝑹} h)$
49		ovex	$⊢ {-1}_{𝑹} \cdot_{𝑹} (y \cdot_{𝑹} u) \in V$
50	44 45 46 47 48 49	caov4	$⊢ ((x \cdot_{𝑹} z) +_{𝑹} (x \cdot_{𝑹} v)) +_{𝑹} (({-1}_{𝑹} \cdot_{𝑹} (y \cdot_{𝑹} w)) +_{𝑹} ({-1}_{𝑹} \cdot_{𝑹} (y \cdot_{𝑹} u))) = ((x \cdot_{𝑹} z) +_{𝑹} ({-1}_{𝑹} \cdot_{𝑹} (y \cdot_{𝑹} w))) +_{𝑹} ((x \cdot_{𝑹} v) +_{𝑹} ({-1}_{𝑹} \cdot_{𝑹} (y \cdot_{𝑹} u)))$
51	43 50	eqtri	$⊢ (x \cdot_{𝑹} (z +_{𝑹} v)) +_{𝑹} ({-1}_{𝑹} \cdot_{𝑹} (y \cdot_{𝑹} (w +_{𝑹} u))) = ((x \cdot_{𝑹} z) +_{𝑹} ({-1}_{𝑹} \cdot_{𝑹} (y \cdot_{𝑹} w))) +_{𝑹} ((x \cdot_{𝑹} v) +_{𝑹} ({-1}_{𝑹} \cdot_{𝑹} (y \cdot_{𝑹} u)))$
52		distrsr	$⊢ y \cdot_{𝑹} (z +_{𝑹} v) = (y \cdot_{𝑹} z) +_{𝑹} (y \cdot_{𝑹} v)$
53		distrsr	$⊢ x \cdot_{𝑹} (w +_{𝑹} u) = (x \cdot_{𝑹} w) +_{𝑹} (x \cdot_{𝑹} u)$
54	52 53	oveq12i	$⊢ (y \cdot_{𝑹} (z +_{𝑹} v)) +_{𝑹} (x \cdot_{𝑹} (w +_{𝑹} u)) = ((y \cdot_{𝑹} z) +_{𝑹} (y \cdot_{𝑹} v)) +_{𝑹} ((x \cdot_{𝑹} w) +_{𝑹} (x \cdot_{𝑹} u))$
55		ovex	$⊢ y \cdot_{𝑹} z \in V$
56		ovex	$⊢ y \cdot_{𝑹} v \in V$
57		ovex	$⊢ x \cdot_{𝑹} w \in V$
58		ovex	$⊢ x \cdot_{𝑹} u \in V$
59	55 56 57 47 48 58	caov4	$⊢ ((y \cdot_{𝑹} z) +_{𝑹} (y \cdot_{𝑹} v)) +_{𝑹} ((x \cdot_{𝑹} w) +_{𝑹} (x \cdot_{𝑹} u)) = ((y \cdot_{𝑹} z) +_{𝑹} (x \cdot_{𝑹} w)) +_{𝑹} ((y \cdot_{𝑹} v) +_{𝑹} (x \cdot_{𝑹} u))$
60	54 59	eqtri	$⊢ (y \cdot_{𝑹} (z +_{𝑹} v)) +_{𝑹} (x \cdot_{𝑹} (w +_{𝑹} u)) = ((y \cdot_{𝑹} z) +_{𝑹} (x \cdot_{𝑹} w)) +_{𝑹} ((y \cdot_{𝑹} v) +_{𝑹} (x \cdot_{𝑹} u))$
61	1 2 3 4 5 6 10 24 37 51 60	ecovdi	$⊢ (A \in ℂ \land B \in ℂ \land C \in ℂ) \to A (B + C) = A B + A C$

Metamath Proof Explorer

Theorem axdistr

Proof