vcdi

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	vcdi	$⊢ (W \in {CVec}_{OLD} \land (A \in ℂ \land B \in X \land C \in X)) \to A S (B G C) = (A S B) G (A 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	$⊢ (\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 X y S (x G z) = (y S x) G (y S z)$
6	5	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 X y S (x G z) = (y S x) G (y S z)$
7	6	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 X y S (x G z) = (y S x) G (y S z)$
8	7	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 X y S (x G z) = (y S x) G (y S z)$
9	8	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 X y S (x G z) = (y S x) G (y S z)$
10	4 9	syl	$⊢ W \in {CVec}_{OLD} \to \forall x \in X \forall y \in ℂ \forall z \in X y S (x G z) = (y S x) G (y S z)$
11		oveq1	$⊢ x = B \to x G z = B G z$
12	11	oveq2d	$⊢ x = B \to y S (x G z) = y S (B G z)$
13		oveq2	$⊢ x = B \to y S x = y S B$
14	13	oveq1d	$⊢ x = B \to (y S x) G (y S z) = (y S B) G (y S z)$
15	12 14	eqeq12d	$⊢ x = B \to (y S (x G z) = (y S x) G (y S z) \leftrightarrow y S (B G z) = (y S B) G (y S z))$
16		oveq1	$⊢ y = A \to y S (B G z) = A S (B G z)$
17		oveq1	$⊢ y = A \to y S B = A S B$
18		oveq1	$⊢ y = A \to y S z = A S z$
19	17 18	oveq12d	$⊢ y = A \to (y S B) G (y S z) = (A S B) G (A S z)$
20	16 19	eqeq12d	$⊢ y = A \to (y S (B G z) = (y S B) G (y S z) \leftrightarrow A S (B G z) = (A S B) G (A S z))$
21		oveq2	$⊢ z = C \to B G z = B G C$
22	21	oveq2d	$⊢ z = C \to A S (B G z) = A S (B G C)$
23		oveq2	$⊢ z = C \to A S z = A S C$
24	23	oveq2d	$⊢ z = C \to (A S B) G (A S z) = (A S B) G (A S C)$
25	22 24	eqeq12d	$⊢ z = C \to (A S (B G z) = (A S B) G (A S z) \leftrightarrow A S (B G C) = (A S B) G (A S C))$
26	15 20 25	rspc3v	$⊢ (B \in X \land A \in ℂ \land C \in X) \to (\forall x \in X \forall y \in ℂ \forall z \in X y S (x G z) = (y S x) G (y S z) \to A S (B G C) = (A S B) G (A S C))$
27	10 26	syl5	$⊢ (B \in X \land A \in ℂ \land C \in X) \to (W \in {CVec}_{OLD} \to A S (B G C) = (A S B) G (A S C))$
28	27	3com12	$⊢ (A \in ℂ \land B \in X \land C \in X) \to (W \in {CVec}_{OLD} \to A S (B G C) = (A S B) G (A S C))$
29	28	impcom	$⊢ (W \in {CVec}_{OLD} \land (A \in ℂ \land B \in X \land C \in X)) \to A S (B G C) = (A S B) G (A S C)$

Metamath Proof Explorer

Theorem vcdi

Proof