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