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 ∈ CVec OLD ∧ A ∈ X → 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 ∈ CVec OLD → G ∈ AbelOp ∧ S : ℂ × X ⟶ X ∧ ∀ x ∈ X 1 S x = x ∧ ∀ y ∈ ℂ ∀ z ∈ X y S x G z = y S x G y S z ∧ ∀ z ∈ ℂ y + z S x = y S x G z S x ∧ y ⁢ z S x = y S z S x
5 simpl ⊢ 1 S x = x ∧ ∀ y ∈ ℂ ∀ z ∈ X y S x G z = y S x G y S z ∧ ∀ z ∈ ℂ y + z S x = y S x G z S x ∧ y ⁢ z S x = y S z S x → 1 S x = x
6 5 ralimi ⊢ ∀ x ∈ X 1 S x = x ∧ ∀ y ∈ ℂ ∀ z ∈ X y S x G z = y S x G y S z ∧ ∀ z ∈ ℂ y + z S x = y S x G z S x ∧ y ⁢ z S x = y S z S x → ∀ x ∈ X 1 S x = x
7 6 3ad2ant3 ⊢ G ∈ AbelOp ∧ S : ℂ × X ⟶ X ∧ ∀ x ∈ X 1 S x = x ∧ ∀ y ∈ ℂ ∀ z ∈ X y S x G z = y S x G y S z ∧ ∀ z ∈ ℂ y + z S x = y S x G z S x ∧ y ⁢ z S x = y S z S x → ∀ x ∈ X 1 S x = x
8 4 7 syl ⊢ W ∈ CVec OLD → ∀ x ∈ X 1 S x = x
9 oveq2 ⊢ x = A → 1 S x = 1 S A
10 id ⊢ x = A → x = A
11 9 10 eqeq12d ⊢ x = A → 1 S x = x ↔ 1 S A = A
12 11 rspccva ⊢ ∀ x ∈ X 1 S x = x ∧ A ∈ X → 1 S A = A
13 8 12 sylan ⊢ W ∈ CVec OLD ∧ A ∈ X → 1 S A = A