Definition df-vc 28822

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

Step	Hyp	Ref	Expression
1		cvc 28821	. 2 class CVecOLD
2		vg	. . . . . 6 setvar 𝑔
3	2	cv 1538	. . . . 5 class 𝑔
4		cablo 28807	. . . . 5 class AbelOp
5	3, 4	wcel 2108	. . . 4 wff 𝑔 ∈ AbelOp
6		cc 10800	. . . . . 6 class ℂ
7	3	crn 5581	. . . . . 6 class ran 𝑔
8	6, 7	cxp 5578	. . . . 5 class (ℂ × ran 𝑔)
9		vs	. . . . . 6 setvar 𝑠
10	9	cv 1538	. . . . 5 class 𝑠
11	8, 7, 10	wf 6414	. . . 4 wff 𝑠:(ℂ × ran 𝑔)⟶ran 𝑔
12		c1 10803	. . . . . . . 8 class 1
13		vx	. . . . . . . . 9 setvar 𝑥
14	13	cv 1538	. . . . . . . 8 class 𝑥
15	12, 14, 10	co 7255	. . . . . . 7 class (1𝑠𝑥)
16	15, 14	wceq 1539	. . . . . 6 wff (1𝑠𝑥) = 𝑥
17		vy	. . . . . . . . . . . 12 setvar 𝑦
18	17	cv 1538	. . . . . . . . . . 11 class 𝑦
19		vz	. . . . . . . . . . . . 13 setvar 𝑧
20	19	cv 1538	. . . . . . . . . . . 12 class 𝑧
21	14, 20, 3	co 7255	. . . . . . . . . . 11 class (𝑥𝑔𝑧)
22	18, 21, 10	co 7255	. . . . . . . . . 10 class (𝑦𝑠(𝑥𝑔𝑧))
23	18, 14, 10	co 7255	. . . . . . . . . . 11 class (𝑦𝑠𝑥)
24	18, 20, 10	co 7255	. . . . . . . . . . 11 class (𝑦𝑠𝑧)
25	23, 24, 3	co 7255	. . . . . . . . . 10 class ((𝑦𝑠𝑥)𝑔(𝑦𝑠𝑧))
26	22, 25	wceq 1539	. . . . . . . . 9 wff (𝑦𝑠(𝑥𝑔𝑧)) = ((𝑦𝑠𝑥)𝑔(𝑦𝑠𝑧))
27	26, 19, 7	wral 3063	. . . . . . . 8 wff ∀𝑧 ∈ ran 𝑔(𝑦𝑠(𝑥𝑔𝑧)) = ((𝑦𝑠𝑥)𝑔(𝑦𝑠𝑧))
28		caddc 10805	. . . . . . . . . . . . 13 class +
29	18, 20, 28	co 7255	. . . . . . . . . . . 12 class (𝑦 + 𝑧)
30	29, 14, 10	co 7255	. . . . . . . . . . 11 class ((𝑦 + 𝑧)𝑠𝑥)
31	20, 14, 10	co 7255	. . . . . . . . . . . 12 class (𝑧𝑠𝑥)
32	23, 31, 3	co 7255	. . . . . . . . . . 11 class ((𝑦𝑠𝑥)𝑔(𝑧𝑠𝑥))
33	30, 32	wceq 1539	. . . . . . . . . 10 wff ((𝑦 + 𝑧)𝑠𝑥) = ((𝑦𝑠𝑥)𝑔(𝑧𝑠𝑥))
34		cmul 10807	. . . . . . . . . . . . 13 class ·
35	18, 20, 34	co 7255	. . . . . . . . . . . 12 class (𝑦 · 𝑧)
36	35, 14, 10	co 7255	. . . . . . . . . . 11 class ((𝑦 · 𝑧)𝑠𝑥)
37	18, 31, 10	co 7255	. . . . . . . . . . 11 class (𝑦𝑠(𝑧𝑠𝑥))
38	36, 37	wceq 1539	. . . . . . . . . 10 wff ((𝑦 · 𝑧)𝑠𝑥) = (𝑦𝑠(𝑧𝑠𝑥))
39	33, 38	wa 395	. . . . . . . . 9 wff (((𝑦 + 𝑧)𝑠𝑥) = ((𝑦𝑠𝑥)𝑔(𝑧𝑠𝑥)) ∧ ((𝑦 · 𝑧)𝑠𝑥) = (𝑦𝑠(𝑧𝑠𝑥)))
40	39, 19, 6	wral 3063	. . . . . . . 8 wff ∀𝑧 ∈ ℂ (((𝑦 + 𝑧)𝑠𝑥) = ((𝑦𝑠𝑥)𝑔(𝑧𝑠𝑥)) ∧ ((𝑦 · 𝑧)𝑠𝑥) = (𝑦𝑠(𝑧𝑠𝑥)))
41	27, 40	wa 395	. . . . . . 7 wff (∀𝑧 ∈ ran 𝑔(𝑦𝑠(𝑥𝑔𝑧)) = ((𝑦𝑠𝑥)𝑔(𝑦𝑠𝑧)) ∧ ∀𝑧 ∈ ℂ (((𝑦 + 𝑧)𝑠𝑥) = ((𝑦𝑠𝑥)𝑔(𝑧𝑠𝑥)) ∧ ((𝑦 · 𝑧)𝑠𝑥) = (𝑦𝑠(𝑧𝑠𝑥))))
42	41, 17, 6	wral 3063	. . . . . 6 wff ∀𝑦 ∈ ℂ (∀𝑧 ∈ ran 𝑔(𝑦𝑠(𝑥𝑔𝑧)) = ((𝑦𝑠𝑥)𝑔(𝑦𝑠𝑧)) ∧ ∀𝑧 ∈ ℂ (((𝑦 + 𝑧)𝑠𝑥) = ((𝑦𝑠𝑥)𝑔(𝑧𝑠𝑥)) ∧ ((𝑦 · 𝑧)𝑠𝑥) = (𝑦𝑠(𝑧𝑠𝑥))))
43	16, 42	wa 395	. . . . 5 wff ((1𝑠𝑥) = 𝑥 ∧ ∀𝑦 ∈ ℂ (∀𝑧 ∈ ran 𝑔(𝑦𝑠(𝑥𝑔𝑧)) = ((𝑦𝑠𝑥)𝑔(𝑦𝑠𝑧)) ∧ ∀𝑧 ∈ ℂ (((𝑦 + 𝑧)𝑠𝑥) = ((𝑦𝑠𝑥)𝑔(𝑧𝑠𝑥)) ∧ ((𝑦 · 𝑧)𝑠𝑥) = (𝑦𝑠(𝑧𝑠𝑥)))))
44	43, 13, 7	wral 3063	. . . 4 wff ∀𝑥 ∈ ran 𝑔((1𝑠𝑥) = 𝑥 ∧ ∀𝑦 ∈ ℂ (∀𝑧 ∈ ran 𝑔(𝑦𝑠(𝑥𝑔𝑧)) = ((𝑦𝑠𝑥)𝑔(𝑦𝑠𝑧)) ∧ ∀𝑧 ∈ ℂ (((𝑦 + 𝑧)𝑠𝑥) = ((𝑦𝑠𝑥)𝑔(𝑧𝑠𝑥)) ∧ ((𝑦 · 𝑧)𝑠𝑥) = (𝑦𝑠(𝑧𝑠𝑥)))))
45	5, 11, 44	w3a 1085	. . 3 wff (𝑔 ∈ AbelOp ∧ 𝑠:(ℂ × ran 𝑔)⟶ran 𝑔 ∧ ∀𝑥 ∈ ran 𝑔((1𝑠𝑥) = 𝑥 ∧ ∀𝑦 ∈ ℂ (∀𝑧 ∈ ran 𝑔(𝑦𝑠(𝑥𝑔𝑧)) = ((𝑦𝑠𝑥)𝑔(𝑦𝑠𝑧)) ∧ ∀𝑧 ∈ ℂ (((𝑦 + 𝑧)𝑠𝑥) = ((𝑦𝑠𝑥)𝑔(𝑧𝑠𝑥)) ∧ ((𝑦 · 𝑧)𝑠𝑥) = (𝑦𝑠(𝑧𝑠𝑥))))))
46	45, 2, 9	copab 5132	. 2 class {⟨𝑔, 𝑠⟩ ∣ (𝑔 ∈ AbelOp ∧ 𝑠:(ℂ × ran 𝑔)⟶ran 𝑔 ∧ ∀𝑥 ∈ ran 𝑔((1𝑠𝑥) = 𝑥 ∧ ∀𝑦 ∈ ℂ (∀𝑧 ∈ ran 𝑔(𝑦𝑠(𝑥𝑔𝑧)) = ((𝑦𝑠𝑥)𝑔(𝑦𝑠𝑧)) ∧ ∀𝑧 ∈ ℂ (((𝑦 + 𝑧)𝑠𝑥) = ((𝑦𝑠𝑥)𝑔(𝑧𝑠𝑥)) ∧ ((𝑦 · 𝑧)𝑠𝑥) = (𝑦𝑠(𝑧𝑠𝑥))))))}
47	1, 46	wceq 1539	1 wff CVecOLD = {⟨𝑔, 𝑠⟩ ∣ (𝑔 ∈ AbelOp ∧ 𝑠:(ℂ × ran 𝑔)⟶ran 𝑔 ∧ ∀𝑥 ∈ ran 𝑔((1𝑠𝑥) = 𝑥 ∧ ∀𝑦 ∈ ℂ (∀𝑧 ∈ ran 𝑔(𝑦𝑠(𝑥𝑔𝑧)) = ((𝑦𝑠𝑥)𝑔(𝑦𝑠𝑧)) ∧ ∀𝑧 ∈ ℂ (((𝑦 + 𝑧)𝑠𝑥) = ((𝑦𝑠𝑥)𝑔(𝑧𝑠𝑥)) ∧ ((𝑦 · 𝑧)𝑠𝑥) = (𝑦𝑠(𝑧𝑠𝑥))))))}

This definition is referenced by:  vcrel  28823  vciOLD  28824  isvclem  28840