MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-vc Structured version   Visualization version   GIF version

Definition df-vc 26563
Description: Define the class of all complex vector spaces. (Contributed by NM, 3-Nov-2006.) (New usage is discouraged.)
Assertion
Ref Expression
df-vc CVecOLD = {⟨𝑔, 𝑠⟩ ∣ (𝑔 ∈ AbelOp ∧ 𝑠:(ℂ × ran 𝑔)⟶ran 𝑔 ∧ ∀𝑥 ∈ ran 𝑔((1𝑠𝑥) = 𝑥 ∧ ∀𝑦 ∈ ℂ (∀𝑧 ∈ ran 𝑔(𝑦𝑠(𝑥𝑔𝑧)) = ((𝑦𝑠𝑥)𝑔(𝑦𝑠𝑧)) ∧ ∀𝑧 ∈ ℂ (((𝑦 + 𝑧)𝑠𝑥) = ((𝑦𝑠𝑥)𝑔(𝑧𝑠𝑥)) ∧ ((𝑦 · 𝑧)𝑠𝑥) = (𝑦𝑠(𝑧𝑠𝑥))))))}
Distinct variable group:   𝑔,𝑠,𝑥,𝑦,𝑧

Detailed syntax breakdown of Definition df-vc
StepHypRef Expression
1 cvc 26562 . 2 class CVecOLD
2 vg . . . . . 6 setvar 𝑔
32cv 1473 . . . . 5 class 𝑔
4 cablo 26547 . . . . 5 class AbelOp
53, 4wcel 1975 . . . 4 wff 𝑔 ∈ AbelOp
6 cc 9786 . . . . . 6 class
73crn 5025 . . . . . 6 class ran 𝑔
86, 7cxp 5022 . . . . 5 class (ℂ × ran 𝑔)
9 vs . . . . . 6 setvar 𝑠
109cv 1473 . . . . 5 class 𝑠
118, 7, 10wf 5782 . . . 4 wff 𝑠:(ℂ × ran 𝑔)⟶ran 𝑔
12 c1 9789 . . . . . . . 8 class 1
13 vx . . . . . . . . 9 setvar 𝑥
1413cv 1473 . . . . . . . 8 class 𝑥
1512, 14, 10co 6523 . . . . . . 7 class (1𝑠𝑥)
1615, 14wceq 1474 . . . . . 6 wff (1𝑠𝑥) = 𝑥
17 vy . . . . . . . . . . . 12 setvar 𝑦
1817cv 1473 . . . . . . . . . . 11 class 𝑦
19 vz . . . . . . . . . . . . 13 setvar 𝑧
2019cv 1473 . . . . . . . . . . . 12 class 𝑧
2114, 20, 3co 6523 . . . . . . . . . . 11 class (𝑥𝑔𝑧)
2218, 21, 10co 6523 . . . . . . . . . 10 class (𝑦𝑠(𝑥𝑔𝑧))
2318, 14, 10co 6523 . . . . . . . . . . 11 class (𝑦𝑠𝑥)
2418, 20, 10co 6523 . . . . . . . . . . 11 class (𝑦𝑠𝑧)
2523, 24, 3co 6523 . . . . . . . . . 10 class ((𝑦𝑠𝑥)𝑔(𝑦𝑠𝑧))
2622, 25wceq 1474 . . . . . . . . 9 wff (𝑦𝑠(𝑥𝑔𝑧)) = ((𝑦𝑠𝑥)𝑔(𝑦𝑠𝑧))
2726, 19, 7wral 2891 . . . . . . . 8 wff 𝑧 ∈ ran 𝑔(𝑦𝑠(𝑥𝑔𝑧)) = ((𝑦𝑠𝑥)𝑔(𝑦𝑠𝑧))
28 caddc 9791 . . . . . . . . . . . . 13 class +
2918, 20, 28co 6523 . . . . . . . . . . . 12 class (𝑦 + 𝑧)
3029, 14, 10co 6523 . . . . . . . . . . 11 class ((𝑦 + 𝑧)𝑠𝑥)
3120, 14, 10co 6523 . . . . . . . . . . . 12 class (𝑧𝑠𝑥)
3223, 31, 3co 6523 . . . . . . . . . . 11 class ((𝑦𝑠𝑥)𝑔(𝑧𝑠𝑥))
3330, 32wceq 1474 . . . . . . . . . 10 wff ((𝑦 + 𝑧)𝑠𝑥) = ((𝑦𝑠𝑥)𝑔(𝑧𝑠𝑥))
34 cmul 9793 . . . . . . . . . . . . 13 class ·
3518, 20, 34co 6523 . . . . . . . . . . . 12 class (𝑦 · 𝑧)
3635, 14, 10co 6523 . . . . . . . . . . 11 class ((𝑦 · 𝑧)𝑠𝑥)
3718, 31, 10co 6523 . . . . . . . . . . 11 class (𝑦𝑠(𝑧𝑠𝑥))
3836, 37wceq 1474 . . . . . . . . . 10 wff ((𝑦 · 𝑧)𝑠𝑥) = (𝑦𝑠(𝑧𝑠𝑥))
3933, 38wa 382 . . . . . . . . 9 wff (((𝑦 + 𝑧)𝑠𝑥) = ((𝑦𝑠𝑥)𝑔(𝑧𝑠𝑥)) ∧ ((𝑦 · 𝑧)𝑠𝑥) = (𝑦𝑠(𝑧𝑠𝑥)))
4039, 19, 6wral 2891 . . . . . . . 8 wff 𝑧 ∈ ℂ (((𝑦 + 𝑧)𝑠𝑥) = ((𝑦𝑠𝑥)𝑔(𝑧𝑠𝑥)) ∧ ((𝑦 · 𝑧)𝑠𝑥) = (𝑦𝑠(𝑧𝑠𝑥)))
4127, 40wa 382 . . . . . . 7 wff (∀𝑧 ∈ ran 𝑔(𝑦𝑠(𝑥𝑔𝑧)) = ((𝑦𝑠𝑥)𝑔(𝑦𝑠𝑧)) ∧ ∀𝑧 ∈ ℂ (((𝑦 + 𝑧)𝑠𝑥) = ((𝑦𝑠𝑥)𝑔(𝑧𝑠𝑥)) ∧ ((𝑦 · 𝑧)𝑠𝑥) = (𝑦𝑠(𝑧𝑠𝑥))))
4241, 17, 6wral 2891 . . . . . 6 wff 𝑦 ∈ ℂ (∀𝑧 ∈ ran 𝑔(𝑦𝑠(𝑥𝑔𝑧)) = ((𝑦𝑠𝑥)𝑔(𝑦𝑠𝑧)) ∧ ∀𝑧 ∈ ℂ (((𝑦 + 𝑧)𝑠𝑥) = ((𝑦𝑠𝑥)𝑔(𝑧𝑠𝑥)) ∧ ((𝑦 · 𝑧)𝑠𝑥) = (𝑦𝑠(𝑧𝑠𝑥))))
4316, 42wa 382 . . . . 5 wff ((1𝑠𝑥) = 𝑥 ∧ ∀𝑦 ∈ ℂ (∀𝑧 ∈ ran 𝑔(𝑦𝑠(𝑥𝑔𝑧)) = ((𝑦𝑠𝑥)𝑔(𝑦𝑠𝑧)) ∧ ∀𝑧 ∈ ℂ (((𝑦 + 𝑧)𝑠𝑥) = ((𝑦𝑠𝑥)𝑔(𝑧𝑠𝑥)) ∧ ((𝑦 · 𝑧)𝑠𝑥) = (𝑦𝑠(𝑧𝑠𝑥)))))
4443, 13, 7wral 2891 . . . 4 wff 𝑥 ∈ ran 𝑔((1𝑠𝑥) = 𝑥 ∧ ∀𝑦 ∈ ℂ (∀𝑧 ∈ ran 𝑔(𝑦𝑠(𝑥𝑔𝑧)) = ((𝑦𝑠𝑥)𝑔(𝑦𝑠𝑧)) ∧ ∀𝑧 ∈ ℂ (((𝑦 + 𝑧)𝑠𝑥) = ((𝑦𝑠𝑥)𝑔(𝑧𝑠𝑥)) ∧ ((𝑦 · 𝑧)𝑠𝑥) = (𝑦𝑠(𝑧𝑠𝑥)))))
455, 11, 44w3a 1030 . . 3 wff (𝑔 ∈ AbelOp ∧ 𝑠:(ℂ × ran 𝑔)⟶ran 𝑔 ∧ ∀𝑥 ∈ ran 𝑔((1𝑠𝑥) = 𝑥 ∧ ∀𝑦 ∈ ℂ (∀𝑧 ∈ ran 𝑔(𝑦𝑠(𝑥𝑔𝑧)) = ((𝑦𝑠𝑥)𝑔(𝑦𝑠𝑧)) ∧ ∀𝑧 ∈ ℂ (((𝑦 + 𝑧)𝑠𝑥) = ((𝑦𝑠𝑥)𝑔(𝑧𝑠𝑥)) ∧ ((𝑦 · 𝑧)𝑠𝑥) = (𝑦𝑠(𝑧𝑠𝑥))))))
4645, 2, 9copab 4632 . 2 class {⟨𝑔, 𝑠⟩ ∣ (𝑔 ∈ AbelOp ∧ 𝑠:(ℂ × ran 𝑔)⟶ran 𝑔 ∧ ∀𝑥 ∈ ran 𝑔((1𝑠𝑥) = 𝑥 ∧ ∀𝑦 ∈ ℂ (∀𝑧 ∈ ran 𝑔(𝑦𝑠(𝑥𝑔𝑧)) = ((𝑦𝑠𝑥)𝑔(𝑦𝑠𝑧)) ∧ ∀𝑧 ∈ ℂ (((𝑦 + 𝑧)𝑠𝑥) = ((𝑦𝑠𝑥)𝑔(𝑧𝑠𝑥)) ∧ ((𝑦 · 𝑧)𝑠𝑥) = (𝑦𝑠(𝑧𝑠𝑥))))))}
471, 46wceq 1474 1 wff CVecOLD = {⟨𝑔, 𝑠⟩ ∣ (𝑔 ∈ AbelOp ∧ 𝑠:(ℂ × ran 𝑔)⟶ran 𝑔 ∧ ∀𝑥 ∈ ran 𝑔((1𝑠𝑥) = 𝑥 ∧ ∀𝑦 ∈ ℂ (∀𝑧 ∈ ran 𝑔(𝑦𝑠(𝑥𝑔𝑧)) = ((𝑦𝑠𝑥)𝑔(𝑦𝑠𝑧)) ∧ ∀𝑧 ∈ ℂ (((𝑦 + 𝑧)𝑠𝑥) = ((𝑦𝑠𝑥)𝑔(𝑧𝑠𝑥)) ∧ ((𝑦 · 𝑧)𝑠𝑥) = (𝑦𝑠(𝑧𝑠𝑥))))))}
Colors of variables: wff setvar class
This definition is referenced by:  vcrel  26564  vciOLD  26565  isvclem  26594
  Copyright terms: Public domain W3C validator