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 \in AbelOp \land s : ℂ \times ran g ⟶ ran g \land \forall x \in ran g (1 s x = x \land \forall y \in ℂ (\forall z \in ran g y s (x g z) = (y s x) g (y s z) \land \forall z \in ℂ ((y + z) s x = (y s x) g (z s x) \land 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 \in AbelOp$
6	2	cv	$setvar s$
7		cc	$class ℂ$
8	3	crn	$class ran g$
9	7 8	cxp	$class (ℂ \times ran g)$
10	9 8 6	wf	$wff s : ℂ \times 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 \forall z \in 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 \times$
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) \land y z s x = y s (z s x))$
39	38 17 7	wral	$wff \forall z \in ℂ ((y + z) s x = (y s x) g (z s x) \land y z s x = y s (z s x))$
40	26 39	wa	$wff (\forall z \in ran g y s (x g z) = (y s x) g (y s z) \land \forall z \in ℂ ((y + z) s x = (y s x) g (z s x) \land y z s x = y s (z s x)))$
41	40 16 7	wral	$wff \forall y \in ℂ (\forall z \in ran g y s (x g z) = (y s x) g (y s z) \land \forall z \in ℂ ((y + z) s x = (y s x) g (z s x) \land y z s x = y s (z s x)))$
42	15 41	wa	$wff (1 s x = x \land \forall y \in ℂ (\forall z \in ran g y s (x g z) = (y s x) g (y s z) \land \forall z \in ℂ ((y + z) s x = (y s x) g (z s x) \land y z s x = y s (z s x))))$
43	42 11 8	wral	$wff \forall x \in ran g (1 s x = x \land \forall y \in ℂ (\forall z \in ran g y s (x g z) = (y s x) g (y s z) \land \forall z \in ℂ ((y + z) s x = (y s x) g (z s x) \land y z s x = y s (z s x))))$
44	5 10 43	w3a	$wff (g \in AbelOp \land s : ℂ \times ran g ⟶ ran g \land \forall x \in ran g (1 s x = x \land \forall y \in ℂ (\forall z \in ran g y s (x g z) = (y s x) g (y s z) \land \forall z \in ℂ ((y + z) s x = (y s x) g (z s x) \land y z s x = y s (z s x)))))$
45	44 1 2	copab	$class \{⟨g, s⟩ \| (g \in AbelOp \land s : ℂ \times ran g ⟶ ran g \land \forall x \in ran g (1 s x = x \land \forall y \in ℂ (\forall z \in ran g y s (x g z) = (y s x) g (y s z) \land \forall z \in ℂ ((y + z) s x = (y s x) g (z s x) \land y z s x = y s (z s x)))))\}$
46	0 45	wceq	$wff {CVec}_{OLD} = \{⟨g, s⟩ \| (g \in AbelOp \land s : ℂ \times ran g ⟶ ran g \land \forall x \in ran g (1 s x = x \land \forall y \in ℂ (\forall z \in ran g y s (x g z) = (y s x) g (y s z) \land \forall z \in ℂ ((y + z) s x = (y s x) g (z s x) \land y z s x = y s (z s x)))))\}$

Metamath Proof Explorer

Definition df-vc

Detailed syntax breakdown