Metamath Proof Explorer

Theorem vciOLD

Description: Obsolete version of cvsi . The properties of a complex vector space, which is an Abelian group (i.e. the vectors, with the operation of vector addition) accompanied by a scalar multiplication operation on the field of complex numbers. The variable W was chosen because _V is already used for the universal class. (Contributed by NM, 3-Nov-2006) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Hypotheses vciOLD.1 ⊢ G = 1 st ⁡ W
vciOLD.2 ⊢ S = 2 nd ⁡ W
vciOLD.3 ⊢ X = ran ⁡ G
Assertion vciOLD ⊢ W ∈ 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 vciOLD.1 ⊢ G = 1 st ⁡ W
2 vciOLD.2 ⊢ S = 2 nd ⁡ W
3 vciOLD.3 ⊢ X = ran ⁡ G
4 1 eqeq2i ⊢ g = G ↔ g = 1 st ⁡ W
5 eleq1 ⊢ g = G → g ∈ AbelOp ↔ G ∈ AbelOp
6 rneq ⊢ g = G → ran ⁡ g = ran ⁡ G
7 6 3 eqtr4di ⊢ g = G → ran ⁡ g = X
8 xpeq2 ⊢ ran ⁡ g = X → ℂ × ran ⁡ g = ℂ × X
9 8 feq2d ⊢ ran ⁡ g = X → s : ℂ × ran ⁡ g ⟶ ran ⁡ g ↔ s : ℂ × X ⟶ ran ⁡ g
10 feq3 ⊢ ran ⁡ g = X → s : ℂ × X ⟶ ran ⁡ g ↔ s : ℂ × X ⟶ X
11 9 10 bitrd ⊢ ran ⁡ g = X → s : ℂ × ran ⁡ g ⟶ ran ⁡ g ↔ s : ℂ × X ⟶ X
12 7 11 syl ⊢ g = G → s : ℂ × ran ⁡ g ⟶ ran ⁡ g ↔ s : ℂ × X ⟶ X
13 oveq ⊢ g = G → x g z = x G z
14 13 oveq2d ⊢ g = G → y s x g z = y s x G z
15 oveq ⊢ g = G → y s x g y s z = y s x G y s z
16 14 15 eqeq12d ⊢ g = G → y s x g z = y s x g y s z ↔ y s x G z = y s x G y s z
17 7 16 raleqbidv ⊢ g = G → ∀ z ∈ ran ⁡ g y s x g z = y s x g y s z ↔ ∀ z ∈ X y s x G z = y s x G y s z
18 oveq ⊢ g = G → y s x g z s x = y s x G z s x
19 18 eqeq2d ⊢ g = G → y + z s x = y s x g z s x ↔ y + z s x = y s x G z s x
20 19 anbi1d ⊢ g = G → y + z s x = y s x g z s x ∧ y ⁢ z s x = y s z s x ↔ y + z s x = y s x G z s x ∧ y ⁢ z s x = y s z s x
21 20 ralbidv ⊢ g = G → ∀ z ∈ ℂ y + z s x = y s x g z s x ∧ y ⁢ z s x = y s z s x ↔ ∀ z ∈ ℂ y + z s x = y s x G z s x ∧ y ⁢ z s x = y s z s x
22 17 21 anbi12d ⊢ g = G → ∀ z ∈ ran ⁡ g 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 ↔ ∀ 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
23 22 ralbidv ⊢ g = G → ∀ y ∈ ℂ ∀ z ∈ ran ⁡ g 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 ↔ ∀ 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
24 23 anbi2d ⊢ g = G → 1 s x = x ∧ ∀ y ∈ ℂ ∀ z ∈ ran ⁡ g 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 ↔ 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
25 7 24 raleqbidv ⊢ g = G → ∀ x ∈ ran ⁡ g 1 s x = x ∧ ∀ y ∈ ℂ ∀ z ∈ ran ⁡ g 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 ↔ ∀ 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
26 5 12 25 3anbi123d ⊢ g = G → g ∈ AbelOp ∧ s : ℂ × ran ⁡ g ⟶ ran ⁡ g ∧ ∀ x ∈ ran ⁡ g 1 s x = x ∧ ∀ y ∈ ℂ ∀ z ∈ ran ⁡ g 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 ∈ 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
27 4 26 sylbir ⊢ g = 1 st ⁡ W → g ∈ AbelOp ∧ s : ℂ × ran ⁡ g ⟶ ran ⁡ g ∧ ∀ x ∈ ran ⁡ g 1 s x = x ∧ ∀ y ∈ ℂ ∀ z ∈ ran ⁡ g 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 ∈ 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
28 2 eqeq2i ⊢ s = S ↔ s = 2 nd ⁡ W
29 feq1 ⊢ s = S → s : ℂ × X ⟶ X ↔ S : ℂ × X ⟶ X
30 oveq ⊢ s = S → 1 s x = 1 S x
31 30 eqeq1d ⊢ s = S → 1 s x = x ↔ 1 S x = x
32 oveq ⊢ s = S → y s x G z = y S x G z
33 oveq ⊢ s = S → y s x = y S x
34 oveq ⊢ s = S → y s z = y S z
35 33 34 oveq12d ⊢ s = S → y s x G y s z = y S x G y S z
36 32 35 eqeq12d ⊢ s = S → y s x G z = y s x G y s z ↔ y S x G z = y S x G y S z
37 36 ralbidv ⊢ s = S → ∀ z ∈ X y s x G z = y s x G y s z ↔ ∀ z ∈ X y S x G z = y S x G y S z
38 oveq ⊢ s = S → y + z s x = y + z S x
39 oveq ⊢ s = S → z s x = z S x
40 33 39 oveq12d ⊢ s = S → y s x G z s x = y S x G z S x
41 38 40 eqeq12d ⊢ s = S → y + z s x = y s x G z s x ↔ y + z S x = y S x G z S x
42 oveq ⊢ s = S → y ⁢ z s x = y ⁢ z S x
43 39 oveq2d ⊢ s = S → y s z s x = y s z S x
44 oveq ⊢ s = S → y s z S x = y S z S x
45 43 44 eqtrd ⊢ s = S → y s z s x = y S z S x
46 42 45 eqeq12d ⊢ s = S → y ⁢ z s x = y s z s x ↔ y ⁢ z S x = y S z S x
47 41 46 anbi12d ⊢ s = S → y + z s x = y s x G z s x ∧ y ⁢ z s x = y s z s x ↔ y + z S x = y S x G z S x ∧ y ⁢ z S x = y S z S x
48 47 ralbidv ⊢ s = S → ∀ z ∈ ℂ y + z s x = y s x G z s x ∧ y ⁢ z s x = y s z s x ↔ ∀ z ∈ ℂ y + z S x = y S x G z S x ∧ y ⁢ z S x = y S z S x
49 37 48 anbi12d ⊢ s = S → ∀ 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 ↔ ∀ 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
50 49 ralbidv ⊢ s = S → ∀ 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 ↔ ∀ 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
51 31 50 anbi12d ⊢ s = S → 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 ↔ 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
52 51 ralbidv ⊢ s = S → ∀ 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 ↔ ∀ 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
53 29 52 3anbi23d ⊢ s = S → 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 ∈ 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
54 28 53 sylbir ⊢ s = 2 nd ⁡ W → 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 ∈ 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
55 27 54 elopabi ⊢ W ∈ g s | g ∈ AbelOp ∧ s : ℂ × ran ⁡ g ⟶ ran ⁡ g ∧ ∀ x ∈ ran ⁡ g 1 s x = x ∧ ∀ y ∈ ℂ ∀ z ∈ ran ⁡ g 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 ∈ 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
56 df-vc ⊢ CVec OLD = g s | g ∈ AbelOp ∧ s : ℂ × ran ⁡ g ⟶ ran ⁡ g ∧ ∀ x ∈ ran ⁡ g 1 s x = x ∧ ∀ y ∈ ℂ ∀ z ∈ ran ⁡ g 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
57 55 56 eleq2s ⊢ W ∈ 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