Metamath Proof Explorer

Theorem isvcOLD

Description: The predicate "is a complex vector space." (Contributed by NM, 31-May-2008) Obsolete version of iscvsp . (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Hypothesis isvcOLD.1 ⊢ 𝑋 = ran 𝐺
Assertion isvcOLD ( ⟨ 𝐺 , 𝑆 ⟩ ∈ CVecOLD ↔ ( 𝐺 ∈ AbelOp ∧ 𝑆 : ( ℂ × 𝑋 ) ⟶ 𝑋 ∧ ∀ 𝑥 ∈ 𝑋 ( ( 1 𝑆 𝑥 ) = 𝑥 ∧ ∀ 𝑦 ∈ ℂ ( ∀ 𝑧 ∈ 𝑋 ( 𝑦 𝑆 ( 𝑥 𝐺 𝑧 ) ) = ( ( 𝑦 𝑆 𝑥 ) 𝐺 ( 𝑦 𝑆 𝑧 ) ) ∧ ∀ 𝑧 ∈ ℂ ( ( ( 𝑦 + 𝑧 ) 𝑆 𝑥 ) = ( ( 𝑦 𝑆 𝑥 ) 𝐺 ( 𝑧 𝑆 𝑥 ) ) ∧ ( ( 𝑦 · 𝑧 ) 𝑆 𝑥 ) = ( 𝑦 𝑆 ( 𝑧 𝑆 𝑥 ) ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 isvcOLD.1 ⊢ 𝑋 = ran 𝐺
2 vcex ⊢ ( ⟨ 𝐺 , 𝑆 ⟩ ∈ CVecOLD → ( 𝐺 ∈ V ∧ 𝑆 ∈ V ) )
3 elex ⊢ ( 𝐺 ∈ AbelOp → 𝐺 ∈ V )
4 3 adantr ⊢ ( ( 𝐺 ∈ AbelOp ∧ 𝑆 : ( ℂ × 𝑋 ) ⟶ 𝑋 ) → 𝐺 ∈ V )
5 cnex ⊢ ℂ ∈ V
6 ablogrpo ⊢ ( 𝐺 ∈ AbelOp → 𝐺 ∈ GrpOp )
7 rnexg ⊢ ( 𝐺 ∈ GrpOp → ran 𝐺 ∈ V )
8 1 7 eqeltrid ⊢ ( 𝐺 ∈ GrpOp → 𝑋 ∈ V )
9 6 8 syl ⊢ ( 𝐺 ∈ AbelOp → 𝑋 ∈ V )
10 xpexg ⊢ ( ( ℂ ∈ V ∧ 𝑋 ∈ V ) → ( ℂ × 𝑋 ) ∈ V )
11 5 9 10 sylancr ⊢ ( 𝐺 ∈ AbelOp → ( ℂ × 𝑋 ) ∈ V )
12 fex ⊢ ( ( 𝑆 : ( ℂ × 𝑋 ) ⟶ 𝑋 ∧ ( ℂ × 𝑋 ) ∈ V ) → 𝑆 ∈ V )
13 11 12 sylan2 ⊢ ( ( 𝑆 : ( ℂ × 𝑋 ) ⟶ 𝑋 ∧ 𝐺 ∈ AbelOp ) → 𝑆 ∈ V )
14 13 ancoms ⊢ ( ( 𝐺 ∈ AbelOp ∧ 𝑆 : ( ℂ × 𝑋 ) ⟶ 𝑋 ) → 𝑆 ∈ V )
15 4 14 jca ⊢ ( ( 𝐺 ∈ AbelOp ∧ 𝑆 : ( ℂ × 𝑋 ) ⟶ 𝑋 ) → ( 𝐺 ∈ V ∧ 𝑆 ∈ V ) )
16 15 3adant3 ⊢ ( ( 𝐺 ∈ AbelOp ∧ 𝑆 : ( ℂ × 𝑋 ) ⟶ 𝑋 ∧ ∀ 𝑥 ∈ 𝑋 ( ( 1 𝑆 𝑥 ) = 𝑥 ∧ ∀ 𝑦 ∈ ℂ ( ∀ 𝑧 ∈ 𝑋 ( 𝑦 𝑆 ( 𝑥 𝐺 𝑧 ) ) = ( ( 𝑦 𝑆 𝑥 ) 𝐺 ( 𝑦 𝑆 𝑧 ) ) ∧ ∀ 𝑧 ∈ ℂ ( ( ( 𝑦 + 𝑧 ) 𝑆 𝑥 ) = ( ( 𝑦 𝑆 𝑥 ) 𝐺 ( 𝑧 𝑆 𝑥 ) ) ∧ ( ( 𝑦 · 𝑧 ) 𝑆 𝑥 ) = ( 𝑦 𝑆 ( 𝑧 𝑆 𝑥 ) ) ) ) ) ) → ( 𝐺 ∈ V ∧ 𝑆 ∈ V ) )
17 1 isvclem ⊢ ( ( 𝐺 ∈ V ∧ 𝑆 ∈ V ) → ( ⟨ 𝐺 , 𝑆 ⟩ ∈ CVecOLD ↔ ( 𝐺 ∈ AbelOp ∧ 𝑆 : ( ℂ × 𝑋 ) ⟶ 𝑋 ∧ ∀ 𝑥 ∈ 𝑋 ( ( 1 𝑆 𝑥 ) = 𝑥 ∧ ∀ 𝑦 ∈ ℂ ( ∀ 𝑧 ∈ 𝑋 ( 𝑦 𝑆 ( 𝑥 𝐺 𝑧 ) ) = ( ( 𝑦 𝑆 𝑥 ) 𝐺 ( 𝑦 𝑆 𝑧 ) ) ∧ ∀ 𝑧 ∈ ℂ ( ( ( 𝑦 + 𝑧 ) 𝑆 𝑥 ) = ( ( 𝑦 𝑆 𝑥 ) 𝐺 ( 𝑧 𝑆 𝑥 ) ) ∧ ( ( 𝑦 · 𝑧 ) 𝑆 𝑥 ) = ( 𝑦 𝑆 ( 𝑧 𝑆 𝑥 ) ) ) ) ) ) ) )
18 2 16 17 pm5.21nii ⊢ ( ⟨ 𝐺 , 𝑆 ⟩ ∈ CVecOLD ↔ ( 𝐺 ∈ AbelOp ∧ 𝑆 : ( ℂ × 𝑋 ) ⟶ 𝑋 ∧ ∀ 𝑥 ∈ 𝑋 ( ( 1 𝑆 𝑥 ) = 𝑥 ∧ ∀ 𝑦 ∈ ℂ ( ∀ 𝑧 ∈ 𝑋 ( 𝑦 𝑆 ( 𝑥 𝐺 𝑧 ) ) = ( ( 𝑦 𝑆 𝑥 ) 𝐺 ( 𝑦 𝑆 𝑧 ) ) ∧ ∀ 𝑧 ∈ ℂ ( ( ( 𝑦 + 𝑧 ) 𝑆 𝑥 ) = ( ( 𝑦 𝑆 𝑥 ) 𝐺 ( 𝑧 𝑆 𝑥 ) ) ∧ ( ( 𝑦 · 𝑧 ) 𝑆 𝑥 ) = ( 𝑦 𝑆 ( 𝑧 𝑆 𝑥 ) ) ) ) ) ) )