Metamath Proof Explorer

Definition df-vc

Description: Define the class of all complex vector spaces. (Contributed by NM, 3-Nov-2006) (New usage is discouraged.)

Ref Expression
Assertion 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

Detailed syntax breakdown

Step Hyp Ref Expression
0 cvc class CVec OLD
1 vg setvar g
2 vs setvar s
3 1 cv setvar g
4 cablo class AbelOp
5 3 4 wcel wff g ∈ AbelOp
6 2 cv setvar s
7 cc class ℂ
8 3 crn class ran ⁡ g
9 7 8 cxp class ℂ × ran ⁡ g
10 9 8 6 wf wff s : ℂ × ran ⁡ g ⟶ ran ⁡ g
11 vx setvar x
12 c1 class 1
13 11 cv setvar x
14 12 13 6 co class 1 s x
15 14 13 wceq wff 1 s x = x
16 vy setvar y
17 vz setvar z
18 16 cv setvar y
19 17 cv setvar z
20 13 19 3 co class x g z
21 18 20 6 co class y s x g z
22 18 13 6 co class y s x
23 18 19 6 co class y s z
24 22 23 3 co class y s x g y s z
25 21 24 wceq wff y s x g z = y s x g y s z
26 25 17 8 wral wff ∀ z ∈ ran ⁡ g y s x g z = y s x g y s z
27 caddc class +
28 18 19 27 co class y + z
29 28 13 6 co class y + z s x
30 19 13 6 co class z s x
31 22 30 3 co class y s x g z s x
32 29 31 wceq wff y + z s x = y s x g z s x
33 cmul class ×
34 18 19 33 co class y ⁢ z
35 34 13 6 co class y ⁢ z s x
36 18 30 6 co class y s z s x
37 35 36 wceq wff y ⁢ z s x = y s z s x
38 32 37 wa wff y + z s x = y s x g z s x ∧ y ⁢ z s x = y s z s x
39 38 17 7 wral wff ∀ z ∈ ℂ y + z s x = y s x g z s x ∧ y ⁢ z s x = y s z s x
40 26 39 wa wff ∀ 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
41 40 16 7 wral wff ∀ 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
42 15 41 wa wff 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
43 42 11 8 wral wff ∀ 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
44 5 10 43 w3a wff 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
45 44 1 2 copab class 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
46 0 45 wceq wff 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