vcdir

Description: Distributive law for the scalar product of a complex vector space. (Contributed by NM, 3-Nov-2006) (New usage is discouraged.)

	Ref	Expression
Hypotheses	vciOLD.1	$⊢ G = 1^{st} (W)$
	vciOLD.2	$⊢ S = 2^{nd} (W)$
	vciOLD.3	$⊢ X = ran G$
Assertion	vcdir	$⊢ (W \in {CVec}_{OLD} \land (A \in ℂ \land B \in ℂ \land C \in X)) \to (A + B) S C = (A S C) G (B S C)$

Proof

Step	Hyp	Ref	Expression
1		vciOLD.1	$⊢ G = 1^{st} (W)$
2		vciOLD.2	$⊢ S = 2^{nd} (W)$
3		vciOLD.3	$⊢ X = ran G$
4	1 2 3	vciOLD	$⊢ W \in {CVec}_{OLD} \to (G \in AbelOp \land S : ℂ \times X ⟶ X \land \forall x \in X (1 S x = x \land \forall y \in ℂ (\forall z \in X y S (x G z) = (y S x) G (y S z) \land \forall z \in ℂ ((y + z) S x = (y S x) G (z S x) \land y z S x = y S (z S x)))))$
5		simpl	$⊢ ((y + z) S x = (y S x) G (z S x) \land y z S x = y S (z S x)) \to (y + z) S x = (y S x) G (z S x)$
6	5	ralimi	$⊢ \forall z \in ℂ ((y + z) S x = (y S x) G (z S x) \land y z S x = y S (z S x)) \to \forall z \in ℂ (y + z) S x = (y S x) G (z S x)$
7	6	adantl	$⊢ (\forall z \in X y S (x G z) = (y S x) G (y S z) \land \forall z \in ℂ ((y + z) S x = (y S x) G (z S x) \land y z S x = y S (z S x))) \to \forall z \in ℂ (y + z) S x = (y S x) G (z S x)$
8	7	ralimi	$⊢ \forall y \in ℂ (\forall z \in X y S (x G z) = (y S x) G (y S z) \land \forall z \in ℂ ((y + z) S x = (y S x) G (z S x) \land y z S x = y S (z S x))) \to \forall y \in ℂ \forall z \in ℂ (y + z) S x = (y S x) G (z S x)$
9	8	adantl	$⊢ (1 S x = x \land \forall y \in ℂ (\forall z \in X y S (x G z) = (y S x) G (y S z) \land \forall z \in ℂ ((y + z) S x = (y S x) G (z S x) \land y z S x = y S (z S x)))) \to \forall y \in ℂ \forall z \in ℂ (y + z) S x = (y S x) G (z S x)$
10	9	ralimi	$⊢ \forall x \in X (1 S x = x \land \forall y \in ℂ (\forall z \in X y S (x G z) = (y S x) G (y S z) \land \forall z \in ℂ ((y + z) S x = (y S x) G (z S x) \land y z S x = y S (z S x)))) \to \forall x \in X \forall y \in ℂ \forall z \in ℂ (y + z) S x = (y S x) G (z S x)$
11	10	3ad2ant3	$⊢ (G \in AbelOp \land S : ℂ \times X ⟶ X \land \forall x \in X (1 S x = x \land \forall y \in ℂ (\forall z \in X y S (x G z) = (y S x) G (y S z) \land \forall z \in ℂ ((y + z) S x = (y S x) G (z S x) \land y z S x = y S (z S x))))) \to \forall x \in X \forall y \in ℂ \forall z \in ℂ (y + z) S x = (y S x) G (z S x)$
12	4 11	syl	$⊢ W \in {CVec}_{OLD} \to \forall x \in X \forall y \in ℂ \forall z \in ℂ (y + z) S x = (y S x) G (z S x)$
13		oveq2	$⊢ x = C \to (y + z) S x = (y + z) S C$
14		oveq2	$⊢ x = C \to y S x = y S C$
15		oveq2	$⊢ x = C \to z S x = z S C$
16	14 15	oveq12d	$⊢ x = C \to (y S x) G (z S x) = (y S C) G (z S C)$
17	13 16	eqeq12d	$⊢ x = C \to ((y + z) S x = (y S x) G (z S x) \leftrightarrow (y + z) S C = (y S C) G (z S C))$
18		oveq1	$⊢ y = A \to y + z = A + z$
19	18	oveq1d	$⊢ y = A \to (y + z) S C = (A + z) S C$
20		oveq1	$⊢ y = A \to y S C = A S C$
21	20	oveq1d	$⊢ y = A \to (y S C) G (z S C) = (A S C) G (z S C)$
22	19 21	eqeq12d	$⊢ y = A \to ((y + z) S C = (y S C) G (z S C) \leftrightarrow (A + z) S C = (A S C) G (z S C))$
23		oveq2	$⊢ z = B \to A + z = A + B$
24	23	oveq1d	$⊢ z = B \to (A + z) S C = (A + B) S C$
25		oveq1	$⊢ z = B \to z S C = B S C$
26	25	oveq2d	$⊢ z = B \to (A S C) G (z S C) = (A S C) G (B S C)$
27	24 26	eqeq12d	$⊢ z = B \to ((A + z) S C = (A S C) G (z S C) \leftrightarrow (A + B) S C = (A S C) G (B S C))$
28	17 22 27	rspc3v	$⊢ (C \in X \land A \in ℂ \land B \in ℂ) \to (\forall x \in X \forall y \in ℂ \forall z \in ℂ (y + z) S x = (y S x) G (z S x) \to (A + B) S C = (A S C) G (B S C))$
29	12 28	syl5	$⊢ (C \in X \land A \in ℂ \land B \in ℂ) \to (W \in {CVec}_{OLD} \to (A + B) S C = (A S C) G (B S C))$
30	29	3coml	$⊢ (A \in ℂ \land B \in ℂ \land C \in X) \to (W \in {CVec}_{OLD} \to (A + B) S C = (A S C) G (B S C))$
31	30	impcom	$⊢ (W \in {CVec}_{OLD} \land (A \in ℂ \land B \in ℂ \land C \in X)) \to (A + B) S C = (A S C) G (B S C)$

Metamath Proof Explorer

Theorem vcdir

Proof