isvciOLD

Description: Properties that determine a complex vector space. (Contributed by NM, 5-Nov-2006) Obsolete version of iscvsi . (New usage is discouraged.) (Proof modification is discouraged.)

	Ref	Expression
Hypotheses	isvciOLD.1	$⊢ G \in AbelOp$
	isvciOLD.2	$⊢ dom G = X \times X$
	isvciOLD.3	$⊢ S : ℂ \times X ⟶ X$
	isvciOLD.4	$⊢ x \in X \to 1 S x = x$
	isvciOLD.5	$⊢ (y \in ℂ \land x \in X \land z \in X) \to y S (x G z) = (y S x) G (y S z)$
	isvciOLD.6	$⊢ (y \in ℂ \land z \in ℂ \land x \in X) \to (y + z) S x = (y S x) G (z S x)$
	isvciOLD.7	$⊢ (y \in ℂ \land z \in ℂ \land x \in X) \to y z S x = y S (z S x)$
	isvciOLD.8	$⊢ W = ⟨G, S⟩$
Assertion	isvciOLD	$⊢ W \in {CVec}_{OLD}$

Proof

Step	Hyp	Ref	Expression
1		isvciOLD.1	$⊢ G \in AbelOp$
2		isvciOLD.2	$⊢ dom G = X \times X$
3		isvciOLD.3	$⊢ S : ℂ \times X ⟶ X$
4		isvciOLD.4	$⊢ x \in X \to 1 S x = x$
5		isvciOLD.5	$⊢ (y \in ℂ \land x \in X \land z \in X) \to y S (x G z) = (y S x) G (y S z)$
6		isvciOLD.6	$⊢ (y \in ℂ \land z \in ℂ \land x \in X) \to (y + z) S x = (y S x) G (z S x)$
7		isvciOLD.7	$⊢ (y \in ℂ \land z \in ℂ \land x \in X) \to y z S x = y S (z S x)$
8		isvciOLD.8	$⊢ W = ⟨G, S⟩$
9	5	3com12	$⊢ (x \in X \land y \in ℂ \land z \in X) \to y S (x G z) = (y S x) G (y S z)$
10	9	3expa	$⊢ ((x \in X \land y \in ℂ) \land z \in X) \to y S (x G z) = (y S x) G (y S z)$
11	10	ralrimiva	$⊢ (x \in X \land y \in ℂ) \to \forall z \in X y S (x G z) = (y S x) G (y S z)$
12	6 7	jca	$⊢ (y \in ℂ \land z \in ℂ \land x \in X) \to ((y + z) S x = (y S x) G (z S x) \land y z S x = y S (z S x))$
13	12	3comr	$⊢ (x \in X \land y \in ℂ \land z \in ℂ) \to ((y + z) S x = (y S x) G (z S x) \land y z S x = y S (z S x))$
14	13	3expa	$⊢ ((x \in X \land y \in ℂ) \land z \in ℂ) \to ((y + z) S x = (y S x) G (z S x) \land y z S x = y S (z S x))$
15	14	ralrimiva	$⊢ (x \in X \land y \in ℂ) \to \forall z \in ℂ ((y + z) S x = (y S x) G (z S x) \land y z S x = y S (z S x))$
16	11 15	jca	$⊢ (x \in X \land y \in ℂ) \to (\forall z \in X 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)))$
17	16	ralrimiva	$⊢ x \in X \to \forall y \in ℂ (\forall z \in X 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)))$
18	4 17	jca	$⊢ x \in X \to (1 S x = x \land \forall y \in ℂ (\forall z \in X 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))))$
19	18	rgen	$⊢ \forall x \in X (1 S x = x \land \forall y \in ℂ (\forall z \in X 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))))$
20		ablogrpo	$⊢ G \in AbelOp \to G \in GrpOp$
21	1 20	ax-mp	$⊢ G \in GrpOp$
22	21 2	grporn	$⊢ X = ran G$
23	22	isvcOLD	$⊢ ⟨G, S⟩ \in {CVec}_{OLD} \leftrightarrow (G \in AbelOp \land S : ℂ \times X ⟶ X \land \forall x \in X (1 S x = x \land \forall y \in ℂ (\forall z \in X 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)))))$
24	1 3 19 23	mpbir3an	$⊢ ⟨G, S⟩ \in {CVec}_{OLD}$
25	8 24	eqeltri	$⊢ W \in {CVec}_{OLD}$

Metamath Proof Explorer

Theorem isvciOLD

Proof