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 ⊢X=ran⁡G
Assertion isvcOLD ⊢GS∈CVecOLD↔G∈AbelOp∧S:ℂ×X⟶X∧∀x∈X1Sx=x∧∀y∈ℂ∀z∈XySxGz=ySxGySz∧∀z∈ℂy+zSx=ySxGzSx∧y⁢zSx=ySzSx

Proof

Step Hyp Ref Expression
1 isvcOLD.1 ⊢X=ran⁡G
2 vcex ⊢GS∈CVecOLD→G∈V∧S∈V
3 elex ⊢G∈AbelOp→G∈V
4 3 adantr ⊢G∈AbelOp∧S:ℂ×X⟶X→G∈V
5 cnex ⊢ℂ∈V
6 ablogrpo ⊢G∈AbelOp→G∈GrpOp
7 rnexg ⊢G∈GrpOp→ran⁡G∈V
8 1 7 eqeltrid ⊢G∈GrpOp→X∈V
9 6 8 syl ⊢G∈AbelOp→X∈V
10 xpexg ⊢ℂ∈V∧X∈V→ℂ×X∈V
11 5 9 10 sylancr ⊢G∈AbelOp→ℂ×X∈V
12 fex ⊢S:ℂ×X⟶X∧ℂ×X∈V→S∈V
13 11 12 sylan2 ⊢S:ℂ×X⟶X∧G∈AbelOp→S∈V
14 13 ancoms ⊢G∈AbelOp∧S:ℂ×X⟶X→S∈V
15 4 14 jca ⊢G∈AbelOp∧S:ℂ×X⟶X→G∈V∧S∈V
16 15 3adant3 ⊢G∈AbelOp∧S:ℂ×X⟶X∧∀x∈X1Sx=x∧∀y∈ℂ∀z∈XySxGz=ySxGySz∧∀z∈ℂy+zSx=ySxGzSx∧y⁢zSx=ySzSx→G∈V∧S∈V
17 1 isvclem ⊢G∈V∧S∈V→GS∈CVecOLD↔G∈AbelOp∧S:ℂ×X⟶X∧∀x∈X1Sx=x∧∀y∈ℂ∀z∈XySxGz=ySxGySz∧∀z∈ℂy+zSx=ySxGzSx∧y⁢zSx=ySzSx
18 2 16 17 pm5.21nii ⊢GS∈CVecOLD↔G∈AbelOp∧S:ℂ×X⟶X∧∀x∈X1Sx=x∧∀y∈ℂ∀z∈XySxGz=ySxGySz∧∀z∈ℂy+zSx=ySxGzSx∧y⁢zSx=ySzSx