Metamath Proof Explorer

Theorem vcidOLD

Description: Identity element for the scalar product of a complex vector space. (Contributed by NM, 3-Nov-2006) Obsolete theorem, use clmvs1 together with cvsclm instead. (New usage is discouraged.) (Proof modification is discouraged.)

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

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	$⊢ (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 1 S x = x$
6	5	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 1 S x = x$
7	6	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 1 S x = x$
8	4 7	syl	$⊢ W \in {CVec}_{OLD} \to \forall x \in X 1 S x = x$
9		oveq2	$⊢ x = A \to 1 S x = 1 S A$
10		id	$⊢ x = A \to x = A$
11	9 10	eqeq12d	$⊢ x = A \to (1 S x = x \leftrightarrow 1 S A = A)$
12	11	rspccva	$⊢ (\forall x \in X 1 S x = x \land A \in X) \to 1 S A = A$
13	8 12	sylan	$⊢ (W \in {CVec}_{OLD} \land A \in X) \to 1 S A = A$