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 ⊢ G S ∈ 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

Proof

Step Hyp Ref Expression
1 isvcOLD.1 ⊢ X = ran ⁡ G
2 vcex ⊢ G S ∈ CVec OLD → 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 ∈ 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 → G ∈ V ∧ S ∈ V
17 1 isvclem ⊢ G ∈ V ∧ S ∈ V → G S ∈ 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
18 2 16 17 pm5.21nii ⊢ G S ∈ 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