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	⊢ CVecOLD = { ⟨ 𝑔 , 𝑠 ⟩ ∣ ( 𝑔 ∈ AbelOp ∧ 𝑠 : ( ℂ × ran 𝑔 ) ⟶ ran 𝑔 ∧ ∀ 𝑥 ∈ ran 𝑔 ( ( 1 𝑠 𝑥 ) = 𝑥 ∧ ∀ 𝑦 ∈ ℂ ( ∀ 𝑧 ∈ ran 𝑔 ( 𝑦 𝑠 ( 𝑥 𝑔 𝑧 ) ) = ( ( 𝑦 𝑠 𝑥 ) 𝑔 ( 𝑦 𝑠 𝑧 ) ) ∧ ∀ 𝑧 ∈ ℂ ( ( ( 𝑦 + 𝑧 ) 𝑠 𝑥 ) = ( ( 𝑦 𝑠 𝑥 ) 𝑔 ( 𝑧 𝑠 𝑥 ) ) ∧ ( ( 𝑦 · 𝑧 ) 𝑠 𝑥 ) = ( 𝑦 𝑠 ( 𝑧 𝑠 𝑥 ) ) ) ) ) ) }

Detailed syntax breakdown

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