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	⊢ 𝐺 = ( 1st ‘ 𝑊 )
	vciOLD.2	⊢ 𝑆 = ( 2nd ‘ 𝑊 )
	vciOLD.3	⊢ 𝑋 = ran 𝐺
Assertion	vcidOLD	⊢ ( ( 𝑊 ∈ CVecOLD ∧ 𝐴 ∈ 𝑋 ) → ( 1 𝑆 𝐴 ) = 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		vciOLD.1	⊢ 𝐺 = ( 1st ‘ 𝑊 )
2		vciOLD.2	⊢ 𝑆 = ( 2nd ‘ 𝑊 )
3		vciOLD.3	⊢ 𝑋 = ran 𝐺
4	1 2 3	vciOLD	⊢ ( 𝑊 ∈ CVecOLD → ( 𝐺 ∈ AbelOp ∧ 𝑆 : ( ℂ × 𝑋 ) ⟶ 𝑋 ∧ ∀ 𝑥 ∈ 𝑋 ( ( 1 𝑆 𝑥 ) = 𝑥 ∧ ∀ 𝑦 ∈ ℂ ( ∀ 𝑧 ∈ 𝑋 ( 𝑦 𝑆 ( 𝑥 𝐺 𝑧 ) ) = ( ( 𝑦 𝑆 𝑥 ) 𝐺 ( 𝑦 𝑆 𝑧 ) ) ∧ ∀ 𝑧 ∈ ℂ ( ( ( 𝑦 + 𝑧 ) 𝑆 𝑥 ) = ( ( 𝑦 𝑆 𝑥 ) 𝐺 ( 𝑧 𝑆 𝑥 ) ) ∧ ( ( 𝑦 · 𝑧 ) 𝑆 𝑥 ) = ( 𝑦 𝑆 ( 𝑧 𝑆 𝑥 ) ) ) ) ) ) )
5		simpl	⊢ ( ( ( 1 𝑆 𝑥 ) = 𝑥 ∧ ∀ 𝑦 ∈ ℂ ( ∀ 𝑧 ∈ 𝑋 ( 𝑦 𝑆 ( 𝑥 𝐺 𝑧 ) ) = ( ( 𝑦 𝑆 𝑥 ) 𝐺 ( 𝑦 𝑆 𝑧 ) ) ∧ ∀ 𝑧 ∈ ℂ ( ( ( 𝑦 + 𝑧 ) 𝑆 𝑥 ) = ( ( 𝑦 𝑆 𝑥 ) 𝐺 ( 𝑧 𝑆 𝑥 ) ) ∧ ( ( 𝑦 · 𝑧 ) 𝑆 𝑥 ) = ( 𝑦 𝑆 ( 𝑧 𝑆 𝑥 ) ) ) ) ) → ( 1 𝑆 𝑥 ) = 𝑥 )
6	5	ralimi	⊢ ( ∀ 𝑥 ∈ 𝑋 ( ( 1 𝑆 𝑥 ) = 𝑥 ∧ ∀ 𝑦 ∈ ℂ ( ∀ 𝑧 ∈ 𝑋 ( 𝑦 𝑆 ( 𝑥 𝐺 𝑧 ) ) = ( ( 𝑦 𝑆 𝑥 ) 𝐺 ( 𝑦 𝑆 𝑧 ) ) ∧ ∀ 𝑧 ∈ ℂ ( ( ( 𝑦 + 𝑧 ) 𝑆 𝑥 ) = ( ( 𝑦 𝑆 𝑥 ) 𝐺 ( 𝑧 𝑆 𝑥 ) ) ∧ ( ( 𝑦 · 𝑧 ) 𝑆 𝑥 ) = ( 𝑦 𝑆 ( 𝑧 𝑆 𝑥 ) ) ) ) ) → ∀ 𝑥 ∈ 𝑋 ( 1 𝑆 𝑥 ) = 𝑥 )
7	6	3ad2ant3	⊢ ( ( 𝐺 ∈ AbelOp ∧ 𝑆 : ( ℂ × 𝑋 ) ⟶ 𝑋 ∧ ∀ 𝑥 ∈ 𝑋 ( ( 1 𝑆 𝑥 ) = 𝑥 ∧ ∀ 𝑦 ∈ ℂ ( ∀ 𝑧 ∈ 𝑋 ( 𝑦 𝑆 ( 𝑥 𝐺 𝑧 ) ) = ( ( 𝑦 𝑆 𝑥 ) 𝐺 ( 𝑦 𝑆 𝑧 ) ) ∧ ∀ 𝑧 ∈ ℂ ( ( ( 𝑦 + 𝑧 ) 𝑆 𝑥 ) = ( ( 𝑦 𝑆 𝑥 ) 𝐺 ( 𝑧 𝑆 𝑥 ) ) ∧ ( ( 𝑦 · 𝑧 ) 𝑆 𝑥 ) = ( 𝑦 𝑆 ( 𝑧 𝑆 𝑥 ) ) ) ) ) ) → ∀ 𝑥 ∈ 𝑋 ( 1 𝑆 𝑥 ) = 𝑥 )
8	4 7	syl	⊢ ( 𝑊 ∈ CVecOLD → ∀ 𝑥 ∈ 𝑋 ( 1 𝑆 𝑥 ) = 𝑥 )
9		oveq2	⊢ ( 𝑥 = 𝐴 → ( 1 𝑆 𝑥 ) = ( 1 𝑆 𝐴 ) )
10		id	⊢ ( 𝑥 = 𝐴 → 𝑥 = 𝐴 )
11	9 10	eqeq12d	⊢ ( 𝑥 = 𝐴 → ( ( 1 𝑆 𝑥 ) = 𝑥 ↔ ( 1 𝑆 𝐴 ) = 𝐴 ) )
12	11	rspccva	⊢ ( ( ∀ 𝑥 ∈ 𝑋 ( 1 𝑆 𝑥 ) = 𝑥 ∧ 𝐴 ∈ 𝑋 ) → ( 1 𝑆 𝐴 ) = 𝐴 )
13	8 12	sylan	⊢ ( ( 𝑊 ∈ CVecOLD ∧ 𝐴 ∈ 𝑋 ) → ( 1 𝑆 𝐴 ) = 𝐴 )