Theorem vciOLD

Description: Obsolete version of cvsi . The properties of a complex vector space, which is an Abelian group (i.e. the vectors, with the operation of vector addition) accompanied by a scalar multiplication operation on the field of complex numbers. The variable W was chosen because _V is already used for the universal class. (Contributed by NM, 3-Nov-2006) (New usage is discouraged.) (Proof modification is discouraged.)

	Ref	Expression
Hypotheses	vciOLD.1	⊢ 𝐺 = ( 1st ‘ 𝑊 )
	vciOLD.2	⊢ 𝑆 = ( 2nd ‘ 𝑊 )
	vciOLD.3	⊢ 𝑋 = ran 𝐺
Assertion	vciOLD	⊢ ( 𝑊 ∈ CVecOLD → ( 𝐺 ∈ AbelOp ∧ 𝑆 : ( ℂ × 𝑋 ) ⟶ 𝑋 ∧ ∀ 𝑥 ∈ 𝑋 ( ( 1 𝑆 𝑥 ) = 𝑥 ∧ ∀ 𝑦 ∈ ℂ ( ∀ 𝑧 ∈ 𝑋 ( 𝑦 𝑆 ( 𝑥 𝐺 𝑧 ) ) = ( ( 𝑦 𝑆 𝑥 ) 𝐺 ( 𝑦 𝑆 𝑧 ) ) ∧ ∀ 𝑧 ∈ ℂ ( ( ( 𝑦 + 𝑧 ) 𝑆 𝑥 ) = ( ( 𝑦 𝑆 𝑥 ) 𝐺 ( 𝑧 𝑆 𝑥 ) ) ∧ ( ( 𝑦 · 𝑧 ) 𝑆 𝑥 ) = ( 𝑦 𝑆 ( 𝑧 𝑆 𝑥 ) ) ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		vciOLD.1	⊢ 𝐺 = ( 1st ‘ 𝑊 )
2		vciOLD.2	⊢ 𝑆 = ( 2nd ‘ 𝑊 )
3		vciOLD.3	⊢ 𝑋 = ran 𝐺
4	1	eqeq2i	⊢ ( 𝑔 = 𝐺 ↔ 𝑔 = ( 1st ‘ 𝑊 ) )
5		eleq1	⊢ ( 𝑔 = 𝐺 → ( 𝑔 ∈ AbelOp ↔ 𝐺 ∈ AbelOp ) )
6		rneq	⊢ ( 𝑔 = 𝐺 → ran 𝑔 = ran 𝐺 )
7	6 3	eqtr4di	⊢ ( 𝑔 = 𝐺 → ran 𝑔 = 𝑋 )
8		xpeq2	⊢ ( ran 𝑔 = 𝑋 → ( ℂ × ran 𝑔 ) = ( ℂ × 𝑋 ) )
9	8	feq2d	⊢ ( ran 𝑔 = 𝑋 → ( 𝑠 : ( ℂ × ran 𝑔 ) ⟶ ran 𝑔 ↔ 𝑠 : ( ℂ × 𝑋 ) ⟶ ran 𝑔 ) )
10		feq3	⊢ ( ran 𝑔 = 𝑋 → ( 𝑠 : ( ℂ × 𝑋 ) ⟶ ran 𝑔 ↔ 𝑠 : ( ℂ × 𝑋 ) ⟶ 𝑋 ) )
11	9 10	bitrd	⊢ ( ran 𝑔 = 𝑋 → ( 𝑠 : ( ℂ × ran 𝑔 ) ⟶ ran 𝑔 ↔ 𝑠 : ( ℂ × 𝑋 ) ⟶ 𝑋 ) )
12	7 11	syl	⊢ ( 𝑔 = 𝐺 → ( 𝑠 : ( ℂ × ran 𝑔 ) ⟶ ran 𝑔 ↔ 𝑠 : ( ℂ × 𝑋 ) ⟶ 𝑋 ) )
13		oveq	⊢ ( 𝑔 = 𝐺 → ( 𝑥 𝑔 𝑧 ) = ( 𝑥 𝐺 𝑧 ) )
14	13	oveq2d	⊢ ( 𝑔 = 𝐺 → ( 𝑦 𝑠 ( 𝑥 𝑔 𝑧 ) ) = ( 𝑦 𝑠 ( 𝑥 𝐺 𝑧 ) ) )
15		oveq	⊢ ( 𝑔 = 𝐺 → ( ( 𝑦 𝑠 𝑥 ) 𝑔 ( 𝑦 𝑠 𝑧 ) ) = ( ( 𝑦 𝑠 𝑥 ) 𝐺 ( 𝑦 𝑠 𝑧 ) ) )
16	14 15	eqeq12d	⊢ ( 𝑔 = 𝐺 → ( ( 𝑦 𝑠 ( 𝑥 𝑔 𝑧 ) ) = ( ( 𝑦 𝑠 𝑥 ) 𝑔 ( 𝑦 𝑠 𝑧 ) ) ↔ ( 𝑦 𝑠 ( 𝑥 𝐺 𝑧 ) ) = ( ( 𝑦 𝑠 𝑥 ) 𝐺 ( 𝑦 𝑠 𝑧 ) ) ) )
17	7 16	raleqbidv	⊢ ( 𝑔 = 𝐺 → ( ∀ 𝑧 ∈ ran 𝑔 ( 𝑦 𝑠 ( 𝑥 𝑔 𝑧 ) ) = ( ( 𝑦 𝑠 𝑥 ) 𝑔 ( 𝑦 𝑠 𝑧 ) ) ↔ ∀ 𝑧 ∈ 𝑋 ( 𝑦 𝑠 ( 𝑥 𝐺 𝑧 ) ) = ( ( 𝑦 𝑠 𝑥 ) 𝐺 ( 𝑦 𝑠 𝑧 ) ) ) )
18		oveq	⊢ ( 𝑔 = 𝐺 → ( ( 𝑦 𝑠 𝑥 ) 𝑔 ( 𝑧 𝑠 𝑥 ) ) = ( ( 𝑦 𝑠 𝑥 ) 𝐺 ( 𝑧 𝑠 𝑥 ) ) )
19	18	eqeq2d	⊢ ( 𝑔 = 𝐺 → ( ( ( 𝑦 + 𝑧 ) 𝑠 𝑥 ) = ( ( 𝑦 𝑠 𝑥 ) 𝑔 ( 𝑧 𝑠 𝑥 ) ) ↔ ( ( 𝑦 + 𝑧 ) 𝑠 𝑥 ) = ( ( 𝑦 𝑠 𝑥 ) 𝐺 ( 𝑧 𝑠 𝑥 ) ) ) )
20	19	anbi1d	⊢ ( 𝑔 = 𝐺 → ( ( ( ( 𝑦 + 𝑧 ) 𝑠 𝑥 ) = ( ( 𝑦 𝑠 𝑥 ) 𝑔 ( 𝑧 𝑠 𝑥 ) ) ∧ ( ( 𝑦 · 𝑧 ) 𝑠 𝑥 ) = ( 𝑦 𝑠 ( 𝑧 𝑠 𝑥 ) ) ) ↔ ( ( ( 𝑦 + 𝑧 ) 𝑠 𝑥 ) = ( ( 𝑦 𝑠 𝑥 ) 𝐺 ( 𝑧 𝑠 𝑥 ) ) ∧ ( ( 𝑦 · 𝑧 ) 𝑠 𝑥 ) = ( 𝑦 𝑠 ( 𝑧 𝑠 𝑥 ) ) ) ) )
21	20	ralbidv	⊢ ( 𝑔 = 𝐺 → ( ∀ 𝑧 ∈ ℂ ( ( ( 𝑦 + 𝑧 ) 𝑠 𝑥 ) = ( ( 𝑦 𝑠 𝑥 ) 𝑔 ( 𝑧 𝑠 𝑥 ) ) ∧ ( ( 𝑦 · 𝑧 ) 𝑠 𝑥 ) = ( 𝑦 𝑠 ( 𝑧 𝑠 𝑥 ) ) ) ↔ ∀ 𝑧 ∈ ℂ ( ( ( 𝑦 + 𝑧 ) 𝑠 𝑥 ) = ( ( 𝑦 𝑠 𝑥 ) 𝐺 ( 𝑧 𝑠 𝑥 ) ) ∧ ( ( 𝑦 · 𝑧 ) 𝑠 𝑥 ) = ( 𝑦 𝑠 ( 𝑧 𝑠 𝑥 ) ) ) ) )
22	17 21	anbi12d	⊢ ( 𝑔 = 𝐺 → ( ( ∀ 𝑧 ∈ ran 𝑔 ( 𝑦 𝑠 ( 𝑥 𝑔 𝑧 ) ) = ( ( 𝑦 𝑠 𝑥 ) 𝑔 ( 𝑦 𝑠 𝑧 ) ) ∧ ∀ 𝑧 ∈ ℂ ( ( ( 𝑦 + 𝑧 ) 𝑠 𝑥 ) = ( ( 𝑦 𝑠 𝑥 ) 𝑔 ( 𝑧 𝑠 𝑥 ) ) ∧ ( ( 𝑦 · 𝑧 ) 𝑠 𝑥 ) = ( 𝑦 𝑠 ( 𝑧 𝑠 𝑥 ) ) ) ) ↔ ( ∀ 𝑧 ∈ 𝑋 ( 𝑦 𝑠 ( 𝑥 𝐺 𝑧 ) ) = ( ( 𝑦 𝑠 𝑥 ) 𝐺 ( 𝑦 𝑠 𝑧 ) ) ∧ ∀ 𝑧 ∈ ℂ ( ( ( 𝑦 + 𝑧 ) 𝑠 𝑥 ) = ( ( 𝑦 𝑠 𝑥 ) 𝐺 ( 𝑧 𝑠 𝑥 ) ) ∧ ( ( 𝑦 · 𝑧 ) 𝑠 𝑥 ) = ( 𝑦 𝑠 ( 𝑧 𝑠 𝑥 ) ) ) ) ) )
23	22	ralbidv	⊢ ( 𝑔 = 𝐺 → ( ∀ 𝑦 ∈ ℂ ( ∀ 𝑧 ∈ ran 𝑔 ( 𝑦 𝑠 ( 𝑥 𝑔 𝑧 ) ) = ( ( 𝑦 𝑠 𝑥 ) 𝑔 ( 𝑦 𝑠 𝑧 ) ) ∧ ∀ 𝑧 ∈ ℂ ( ( ( 𝑦 + 𝑧 ) 𝑠 𝑥 ) = ( ( 𝑦 𝑠 𝑥 ) 𝑔 ( 𝑧 𝑠 𝑥 ) ) ∧ ( ( 𝑦 · 𝑧 ) 𝑠 𝑥 ) = ( 𝑦 𝑠 ( 𝑧 𝑠 𝑥 ) ) ) ) ↔ ∀ 𝑦 ∈ ℂ ( ∀ 𝑧 ∈ 𝑋 ( 𝑦 𝑠 ( 𝑥 𝐺 𝑧 ) ) = ( ( 𝑦 𝑠 𝑥 ) 𝐺 ( 𝑦 𝑠 𝑧 ) ) ∧ ∀ 𝑧 ∈ ℂ ( ( ( 𝑦 + 𝑧 ) 𝑠 𝑥 ) = ( ( 𝑦 𝑠 𝑥 ) 𝐺 ( 𝑧 𝑠 𝑥 ) ) ∧ ( ( 𝑦 · 𝑧 ) 𝑠 𝑥 ) = ( 𝑦 𝑠 ( 𝑧 𝑠 𝑥 ) ) ) ) ) )
24	23	anbi2d	⊢ ( 𝑔 = 𝐺 → ( ( ( 1 𝑠 𝑥 ) = 𝑥 ∧ ∀ 𝑦 ∈ ℂ ( ∀ 𝑧 ∈ ran 𝑔 ( 𝑦 𝑠 ( 𝑥 𝑔 𝑧 ) ) = ( ( 𝑦 𝑠 𝑥 ) 𝑔 ( 𝑦 𝑠 𝑧 ) ) ∧ ∀ 𝑧 ∈ ℂ ( ( ( 𝑦 + 𝑧 ) 𝑠 𝑥 ) = ( ( 𝑦 𝑠 𝑥 ) 𝑔 ( 𝑧 𝑠 𝑥 ) ) ∧ ( ( 𝑦 · 𝑧 ) 𝑠 𝑥 ) = ( 𝑦 𝑠 ( 𝑧 𝑠 𝑥 ) ) ) ) ) ↔ ( ( 1 𝑠 𝑥 ) = 𝑥 ∧ ∀ 𝑦 ∈ ℂ ( ∀ 𝑧 ∈ 𝑋 ( 𝑦 𝑠 ( 𝑥 𝐺 𝑧 ) ) = ( ( 𝑦 𝑠 𝑥 ) 𝐺 ( 𝑦 𝑠 𝑧 ) ) ∧ ∀ 𝑧 ∈ ℂ ( ( ( 𝑦 + 𝑧 ) 𝑠 𝑥 ) = ( ( 𝑦 𝑠 𝑥 ) 𝐺 ( 𝑧 𝑠 𝑥 ) ) ∧ ( ( 𝑦 · 𝑧 ) 𝑠 𝑥 ) = ( 𝑦 𝑠 ( 𝑧 𝑠 𝑥 ) ) ) ) ) ) )
25	7 24	raleqbidv	⊢ ( 𝑔 = 𝐺 → ( ∀ 𝑥 ∈ ran 𝑔 ( ( 1 𝑠 𝑥 ) = 𝑥 ∧ ∀ 𝑦 ∈ ℂ ( ∀ 𝑧 ∈ ran 𝑔 ( 𝑦 𝑠 ( 𝑥 𝑔 𝑧 ) ) = ( ( 𝑦 𝑠 𝑥 ) 𝑔 ( 𝑦 𝑠 𝑧 ) ) ∧ ∀ 𝑧 ∈ ℂ ( ( ( 𝑦 + 𝑧 ) 𝑠 𝑥 ) = ( ( 𝑦 𝑠 𝑥 ) 𝑔 ( 𝑧 𝑠 𝑥 ) ) ∧ ( ( 𝑦 · 𝑧 ) 𝑠 𝑥 ) = ( 𝑦 𝑠 ( 𝑧 𝑠 𝑥 ) ) ) ) ) ↔ ∀ 𝑥 ∈ 𝑋 ( ( 1 𝑠 𝑥 ) = 𝑥 ∧ ∀ 𝑦 ∈ ℂ ( ∀ 𝑧 ∈ 𝑋 ( 𝑦 𝑠 ( 𝑥 𝐺 𝑧 ) ) = ( ( 𝑦 𝑠 𝑥 ) 𝐺 ( 𝑦 𝑠 𝑧 ) ) ∧ ∀ 𝑧 ∈ ℂ ( ( ( 𝑦 + 𝑧 ) 𝑠 𝑥 ) = ( ( 𝑦 𝑠 𝑥 ) 𝐺 ( 𝑧 𝑠 𝑥 ) ) ∧ ( ( 𝑦 · 𝑧 ) 𝑠 𝑥 ) = ( 𝑦 𝑠 ( 𝑧 𝑠 𝑥 ) ) ) ) ) ) )
26	5 12 25	3anbi123d	⊢ ( 𝑔 = 𝐺 → ( ( 𝑔 ∈ AbelOp ∧ 𝑠 : ( ℂ × ran 𝑔 ) ⟶ ran 𝑔 ∧ ∀ 𝑥 ∈ ran 𝑔 ( ( 1 𝑠 𝑥 ) = 𝑥 ∧ ∀ 𝑦 ∈ ℂ ( ∀ 𝑧 ∈ ran 𝑔 ( 𝑦 𝑠 ( 𝑥 𝑔 𝑧 ) ) = ( ( 𝑦 𝑠 𝑥 ) 𝑔 ( 𝑦 𝑠 𝑧 ) ) ∧ ∀ 𝑧 ∈ ℂ ( ( ( 𝑦 + 𝑧 ) 𝑠 𝑥 ) = ( ( 𝑦 𝑠 𝑥 ) 𝑔 ( 𝑧 𝑠 𝑥 ) ) ∧ ( ( 𝑦 · 𝑧 ) 𝑠 𝑥 ) = ( 𝑦 𝑠 ( 𝑧 𝑠 𝑥 ) ) ) ) ) ) ↔ ( 𝐺 ∈ AbelOp ∧ 𝑠 : ( ℂ × 𝑋 ) ⟶ 𝑋 ∧ ∀ 𝑥 ∈ 𝑋 ( ( 1 𝑠 𝑥 ) = 𝑥 ∧ ∀ 𝑦 ∈ ℂ ( ∀ 𝑧 ∈ 𝑋 ( 𝑦 𝑠 ( 𝑥 𝐺 𝑧 ) ) = ( ( 𝑦 𝑠 𝑥 ) 𝐺 ( 𝑦 𝑠 𝑧 ) ) ∧ ∀ 𝑧 ∈ ℂ ( ( ( 𝑦 + 𝑧 ) 𝑠 𝑥 ) = ( ( 𝑦 𝑠 𝑥 ) 𝐺 ( 𝑧 𝑠 𝑥 ) ) ∧ ( ( 𝑦 · 𝑧 ) 𝑠 𝑥 ) = ( 𝑦 𝑠 ( 𝑧 𝑠 𝑥 ) ) ) ) ) ) ) )
27	4 26	sylbir	⊢ ( 𝑔 = ( 1st ‘ 𝑊 ) → ( ( 𝑔 ∈ AbelOp ∧ 𝑠 : ( ℂ × ran 𝑔 ) ⟶ ran 𝑔 ∧ ∀ 𝑥 ∈ ran 𝑔 ( ( 1 𝑠 𝑥 ) = 𝑥 ∧ ∀ 𝑦 ∈ ℂ ( ∀ 𝑧 ∈ ran 𝑔 ( 𝑦 𝑠 ( 𝑥 𝑔 𝑧 ) ) = ( ( 𝑦 𝑠 𝑥 ) 𝑔 ( 𝑦 𝑠 𝑧 ) ) ∧ ∀ 𝑧 ∈ ℂ ( ( ( 𝑦 + 𝑧 ) 𝑠 𝑥 ) = ( ( 𝑦 𝑠 𝑥 ) 𝑔 ( 𝑧 𝑠 𝑥 ) ) ∧ ( ( 𝑦 · 𝑧 ) 𝑠 𝑥 ) = ( 𝑦 𝑠 ( 𝑧 𝑠 𝑥 ) ) ) ) ) ) ↔ ( 𝐺 ∈ AbelOp ∧ 𝑠 : ( ℂ × 𝑋 ) ⟶ 𝑋 ∧ ∀ 𝑥 ∈ 𝑋 ( ( 1 𝑠 𝑥 ) = 𝑥 ∧ ∀ 𝑦 ∈ ℂ ( ∀ 𝑧 ∈ 𝑋 ( 𝑦 𝑠 ( 𝑥 𝐺 𝑧 ) ) = ( ( 𝑦 𝑠 𝑥 ) 𝐺 ( 𝑦 𝑠 𝑧 ) ) ∧ ∀ 𝑧 ∈ ℂ ( ( ( 𝑦 + 𝑧 ) 𝑠 𝑥 ) = ( ( 𝑦 𝑠 𝑥 ) 𝐺 ( 𝑧 𝑠 𝑥 ) ) ∧ ( ( 𝑦 · 𝑧 ) 𝑠 𝑥 ) = ( 𝑦 𝑠 ( 𝑧 𝑠 𝑥 ) ) ) ) ) ) ) )
28	2	eqeq2i	⊢ ( 𝑠 = 𝑆 ↔ 𝑠 = ( 2nd ‘ 𝑊 ) )
29		feq1	⊢ ( 𝑠 = 𝑆 → ( 𝑠 : ( ℂ × 𝑋 ) ⟶ 𝑋 ↔ 𝑆 : ( ℂ × 𝑋 ) ⟶ 𝑋 ) )
30		oveq	⊢ ( 𝑠 = 𝑆 → ( 1 𝑠 𝑥 ) = ( 1 𝑆 𝑥 ) )
31	30	eqeq1d	⊢ ( 𝑠 = 𝑆 → ( ( 1 𝑠 𝑥 ) = 𝑥 ↔ ( 1 𝑆 𝑥 ) = 𝑥 ) )
32		oveq	⊢ ( 𝑠 = 𝑆 → ( 𝑦 𝑠 ( 𝑥 𝐺 𝑧 ) ) = ( 𝑦 𝑆 ( 𝑥 𝐺 𝑧 ) ) )
33		oveq	⊢ ( 𝑠 = 𝑆 → ( 𝑦 𝑠 𝑥 ) = ( 𝑦 𝑆 𝑥 ) )
34		oveq	⊢ ( 𝑠 = 𝑆 → ( 𝑦 𝑠 𝑧 ) = ( 𝑦 𝑆 𝑧 ) )
35	33 34	oveq12d	⊢ ( 𝑠 = 𝑆 → ( ( 𝑦 𝑠 𝑥 ) 𝐺 ( 𝑦 𝑠 𝑧 ) ) = ( ( 𝑦 𝑆 𝑥 ) 𝐺 ( 𝑦 𝑆 𝑧 ) ) )
36	32 35	eqeq12d	⊢ ( 𝑠 = 𝑆 → ( ( 𝑦 𝑠 ( 𝑥 𝐺 𝑧 ) ) = ( ( 𝑦 𝑠 𝑥 ) 𝐺 ( 𝑦 𝑠 𝑧 ) ) ↔ ( 𝑦 𝑆 ( 𝑥 𝐺 𝑧 ) ) = ( ( 𝑦 𝑆 𝑥 ) 𝐺 ( 𝑦 𝑆 𝑧 ) ) ) )
37	36	ralbidv	⊢ ( 𝑠 = 𝑆 → ( ∀ 𝑧 ∈ 𝑋 ( 𝑦 𝑠 ( 𝑥 𝐺 𝑧 ) ) = ( ( 𝑦 𝑠 𝑥 ) 𝐺 ( 𝑦 𝑠 𝑧 ) ) ↔ ∀ 𝑧 ∈ 𝑋 ( 𝑦 𝑆 ( 𝑥 𝐺 𝑧 ) ) = ( ( 𝑦 𝑆 𝑥 ) 𝐺 ( 𝑦 𝑆 𝑧 ) ) ) )
38		oveq	⊢ ( 𝑠 = 𝑆 → ( ( 𝑦 + 𝑧 ) 𝑠 𝑥 ) = ( ( 𝑦 + 𝑧 ) 𝑆 𝑥 ) )
39		oveq	⊢ ( 𝑠 = 𝑆 → ( 𝑧 𝑠 𝑥 ) = ( 𝑧 𝑆 𝑥 ) )
40	33 39	oveq12d	⊢ ( 𝑠 = 𝑆 → ( ( 𝑦 𝑠 𝑥 ) 𝐺 ( 𝑧 𝑠 𝑥 ) ) = ( ( 𝑦 𝑆 𝑥 ) 𝐺 ( 𝑧 𝑆 𝑥 ) ) )
41	38 40	eqeq12d	⊢ ( 𝑠 = 𝑆 → ( ( ( 𝑦 + 𝑧 ) 𝑠 𝑥 ) = ( ( 𝑦 𝑠 𝑥 ) 𝐺 ( 𝑧 𝑠 𝑥 ) ) ↔ ( ( 𝑦 + 𝑧 ) 𝑆 𝑥 ) = ( ( 𝑦 𝑆 𝑥 ) 𝐺 ( 𝑧 𝑆 𝑥 ) ) ) )
42		oveq	⊢ ( 𝑠 = 𝑆 → ( ( 𝑦 · 𝑧 ) 𝑠 𝑥 ) = ( ( 𝑦 · 𝑧 ) 𝑆 𝑥 ) )
43	39	oveq2d	⊢ ( 𝑠 = 𝑆 → ( 𝑦 𝑠 ( 𝑧 𝑠 𝑥 ) ) = ( 𝑦 𝑠 ( 𝑧 𝑆 𝑥 ) ) )
44		oveq	⊢ ( 𝑠 = 𝑆 → ( 𝑦 𝑠 ( 𝑧 𝑆 𝑥 ) ) = ( 𝑦 𝑆 ( 𝑧 𝑆 𝑥 ) ) )
45	43 44	eqtrd	⊢ ( 𝑠 = 𝑆 → ( 𝑦 𝑠 ( 𝑧 𝑠 𝑥 ) ) = ( 𝑦 𝑆 ( 𝑧 𝑆 𝑥 ) ) )
46	42 45	eqeq12d	⊢ ( 𝑠 = 𝑆 → ( ( ( 𝑦 · 𝑧 ) 𝑠 𝑥 ) = ( 𝑦 𝑠 ( 𝑧 𝑠 𝑥 ) ) ↔ ( ( 𝑦 · 𝑧 ) 𝑆 𝑥 ) = ( 𝑦 𝑆 ( 𝑧 𝑆 𝑥 ) ) ) )
47	41 46	anbi12d	⊢ ( 𝑠 = 𝑆 → ( ( ( ( 𝑦 + 𝑧 ) 𝑠 𝑥 ) = ( ( 𝑦 𝑠 𝑥 ) 𝐺 ( 𝑧 𝑠 𝑥 ) ) ∧ ( ( 𝑦 · 𝑧 ) 𝑠 𝑥 ) = ( 𝑦 𝑠 ( 𝑧 𝑠 𝑥 ) ) ) ↔ ( ( ( 𝑦 + 𝑧 ) 𝑆 𝑥 ) = ( ( 𝑦 𝑆 𝑥 ) 𝐺 ( 𝑧 𝑆 𝑥 ) ) ∧ ( ( 𝑦 · 𝑧 ) 𝑆 𝑥 ) = ( 𝑦 𝑆 ( 𝑧 𝑆 𝑥 ) ) ) ) )
48	47	ralbidv	⊢ ( 𝑠 = 𝑆 → ( ∀ 𝑧 ∈ ℂ ( ( ( 𝑦 + 𝑧 ) 𝑠 𝑥 ) = ( ( 𝑦 𝑠 𝑥 ) 𝐺 ( 𝑧 𝑠 𝑥 ) ) ∧ ( ( 𝑦 · 𝑧 ) 𝑠 𝑥 ) = ( 𝑦 𝑠 ( 𝑧 𝑠 𝑥 ) ) ) ↔ ∀ 𝑧 ∈ ℂ ( ( ( 𝑦 + 𝑧 ) 𝑆 𝑥 ) = ( ( 𝑦 𝑆 𝑥 ) 𝐺 ( 𝑧 𝑆 𝑥 ) ) ∧ ( ( 𝑦 · 𝑧 ) 𝑆 𝑥 ) = ( 𝑦 𝑆 ( 𝑧 𝑆 𝑥 ) ) ) ) )
49	37 48	anbi12d	⊢ ( 𝑠 = 𝑆 → ( ( ∀ 𝑧 ∈ 𝑋 ( 𝑦 𝑠 ( 𝑥 𝐺 𝑧 ) ) = ( ( 𝑦 𝑠 𝑥 ) 𝐺 ( 𝑦 𝑠 𝑧 ) ) ∧ ∀ 𝑧 ∈ ℂ ( ( ( 𝑦 + 𝑧 ) 𝑠 𝑥 ) = ( ( 𝑦 𝑠 𝑥 ) 𝐺 ( 𝑧 𝑠 𝑥 ) ) ∧ ( ( 𝑦 · 𝑧 ) 𝑠 𝑥 ) = ( 𝑦 𝑠 ( 𝑧 𝑠 𝑥 ) ) ) ) ↔ ( ∀ 𝑧 ∈ 𝑋 ( 𝑦 𝑆 ( 𝑥 𝐺 𝑧 ) ) = ( ( 𝑦 𝑆 𝑥 ) 𝐺 ( 𝑦 𝑆 𝑧 ) ) ∧ ∀ 𝑧 ∈ ℂ ( ( ( 𝑦 + 𝑧 ) 𝑆 𝑥 ) = ( ( 𝑦 𝑆 𝑥 ) 𝐺 ( 𝑧 𝑆 𝑥 ) ) ∧ ( ( 𝑦 · 𝑧 ) 𝑆 𝑥 ) = ( 𝑦 𝑆 ( 𝑧 𝑆 𝑥 ) ) ) ) ) )
50	49	ralbidv	⊢ ( 𝑠 = 𝑆 → ( ∀ 𝑦 ∈ ℂ ( ∀ 𝑧 ∈ 𝑋 ( 𝑦 𝑠 ( 𝑥 𝐺 𝑧 ) ) = ( ( 𝑦 𝑠 𝑥 ) 𝐺 ( 𝑦 𝑠 𝑧 ) ) ∧ ∀ 𝑧 ∈ ℂ ( ( ( 𝑦 + 𝑧 ) 𝑠 𝑥 ) = ( ( 𝑦 𝑠 𝑥 ) 𝐺 ( 𝑧 𝑠 𝑥 ) ) ∧ ( ( 𝑦 · 𝑧 ) 𝑠 𝑥 ) = ( 𝑦 𝑠 ( 𝑧 𝑠 𝑥 ) ) ) ) ↔ ∀ 𝑦 ∈ ℂ ( ∀ 𝑧 ∈ 𝑋 ( 𝑦 𝑆 ( 𝑥 𝐺 𝑧 ) ) = ( ( 𝑦 𝑆 𝑥 ) 𝐺 ( 𝑦 𝑆 𝑧 ) ) ∧ ∀ 𝑧 ∈ ℂ ( ( ( 𝑦 + 𝑧 ) 𝑆 𝑥 ) = ( ( 𝑦 𝑆 𝑥 ) 𝐺 ( 𝑧 𝑆 𝑥 ) ) ∧ ( ( 𝑦 · 𝑧 ) 𝑆 𝑥 ) = ( 𝑦 𝑆 ( 𝑧 𝑆 𝑥 ) ) ) ) ) )
51	31 50	anbi12d	⊢ ( 𝑠 = 𝑆 → ( ( ( 1 𝑠 𝑥 ) = 𝑥 ∧ ∀ 𝑦 ∈ ℂ ( ∀ 𝑧 ∈ 𝑋 ( 𝑦 𝑠 ( 𝑥 𝐺 𝑧 ) ) = ( ( 𝑦 𝑠 𝑥 ) 𝐺 ( 𝑦 𝑠 𝑧 ) ) ∧ ∀ 𝑧 ∈ ℂ ( ( ( 𝑦 + 𝑧 ) 𝑠 𝑥 ) = ( ( 𝑦 𝑠 𝑥 ) 𝐺 ( 𝑧 𝑠 𝑥 ) ) ∧ ( ( 𝑦 · 𝑧 ) 𝑠 𝑥 ) = ( 𝑦 𝑠 ( 𝑧 𝑠 𝑥 ) ) ) ) ) ↔ ( ( 1 𝑆 𝑥 ) = 𝑥 ∧ ∀ 𝑦 ∈ ℂ ( ∀ 𝑧 ∈ 𝑋 ( 𝑦 𝑆 ( 𝑥 𝐺 𝑧 ) ) = ( ( 𝑦 𝑆 𝑥 ) 𝐺 ( 𝑦 𝑆 𝑧 ) ) ∧ ∀ 𝑧 ∈ ℂ ( ( ( 𝑦 + 𝑧 ) 𝑆 𝑥 ) = ( ( 𝑦 𝑆 𝑥 ) 𝐺 ( 𝑧 𝑆 𝑥 ) ) ∧ ( ( 𝑦 · 𝑧 ) 𝑆 𝑥 ) = ( 𝑦 𝑆 ( 𝑧 𝑆 𝑥 ) ) ) ) ) ) )
52	51	ralbidv	⊢ ( 𝑠 = 𝑆 → ( ∀ 𝑥 ∈ 𝑋 ( ( 1 𝑠 𝑥 ) = 𝑥 ∧ ∀ 𝑦 ∈ ℂ ( ∀ 𝑧 ∈ 𝑋 ( 𝑦 𝑠 ( 𝑥 𝐺 𝑧 ) ) = ( ( 𝑦 𝑠 𝑥 ) 𝐺 ( 𝑦 𝑠 𝑧 ) ) ∧ ∀ 𝑧 ∈ ℂ ( ( ( 𝑦 + 𝑧 ) 𝑠 𝑥 ) = ( ( 𝑦 𝑠 𝑥 ) 𝐺 ( 𝑧 𝑠 𝑥 ) ) ∧ ( ( 𝑦 · 𝑧 ) 𝑠 𝑥 ) = ( 𝑦 𝑠 ( 𝑧 𝑠 𝑥 ) ) ) ) ) ↔ ∀ 𝑥 ∈ 𝑋 ( ( 1 𝑆 𝑥 ) = 𝑥 ∧ ∀ 𝑦 ∈ ℂ ( ∀ 𝑧 ∈ 𝑋 ( 𝑦 𝑆 ( 𝑥 𝐺 𝑧 ) ) = ( ( 𝑦 𝑆 𝑥 ) 𝐺 ( 𝑦 𝑆 𝑧 ) ) ∧ ∀ 𝑧 ∈ ℂ ( ( ( 𝑦 + 𝑧 ) 𝑆 𝑥 ) = ( ( 𝑦 𝑆 𝑥 ) 𝐺 ( 𝑧 𝑆 𝑥 ) ) ∧ ( ( 𝑦 · 𝑧 ) 𝑆 𝑥 ) = ( 𝑦 𝑆 ( 𝑧 𝑆 𝑥 ) ) ) ) ) ) )
53	29 52	3anbi23d	⊢ ( 𝑠 = 𝑆 → ( ( 𝐺 ∈ AbelOp ∧ 𝑠 : ( ℂ × 𝑋 ) ⟶ 𝑋 ∧ ∀ 𝑥 ∈ 𝑋 ( ( 1 𝑠 𝑥 ) = 𝑥 ∧ ∀ 𝑦 ∈ ℂ ( ∀ 𝑧 ∈ 𝑋 ( 𝑦 𝑠 ( 𝑥 𝐺 𝑧 ) ) = ( ( 𝑦 𝑠 𝑥 ) 𝐺 ( 𝑦 𝑠 𝑧 ) ) ∧ ∀ 𝑧 ∈ ℂ ( ( ( 𝑦 + 𝑧 ) 𝑠 𝑥 ) = ( ( 𝑦 𝑠 𝑥 ) 𝐺 ( 𝑧 𝑠 𝑥 ) ) ∧ ( ( 𝑦 · 𝑧 ) 𝑠 𝑥 ) = ( 𝑦 𝑠 ( 𝑧 𝑠 𝑥 ) ) ) ) ) ) ↔ ( 𝐺 ∈ AbelOp ∧ 𝑆 : ( ℂ × 𝑋 ) ⟶ 𝑋 ∧ ∀ 𝑥 ∈ 𝑋 ( ( 1 𝑆 𝑥 ) = 𝑥 ∧ ∀ 𝑦 ∈ ℂ ( ∀ 𝑧 ∈ 𝑋 ( 𝑦 𝑆 ( 𝑥 𝐺 𝑧 ) ) = ( ( 𝑦 𝑆 𝑥 ) 𝐺 ( 𝑦 𝑆 𝑧 ) ) ∧ ∀ 𝑧 ∈ ℂ ( ( ( 𝑦 + 𝑧 ) 𝑆 𝑥 ) = ( ( 𝑦 𝑆 𝑥 ) 𝐺 ( 𝑧 𝑆 𝑥 ) ) ∧ ( ( 𝑦 · 𝑧 ) 𝑆 𝑥 ) = ( 𝑦 𝑆 ( 𝑧 𝑆 𝑥 ) ) ) ) ) ) ) )
54	28 53	sylbir	⊢ ( 𝑠 = ( 2nd ‘ 𝑊 ) → ( ( 𝐺 ∈ AbelOp ∧ 𝑠 : ( ℂ × 𝑋 ) ⟶ 𝑋 ∧ ∀ 𝑥 ∈ 𝑋 ( ( 1 𝑠 𝑥 ) = 𝑥 ∧ ∀ 𝑦 ∈ ℂ ( ∀ 𝑧 ∈ 𝑋 ( 𝑦 𝑠 ( 𝑥 𝐺 𝑧 ) ) = ( ( 𝑦 𝑠 𝑥 ) 𝐺 ( 𝑦 𝑠 𝑧 ) ) ∧ ∀ 𝑧 ∈ ℂ ( ( ( 𝑦 + 𝑧 ) 𝑠 𝑥 ) = ( ( 𝑦 𝑠 𝑥 ) 𝐺 ( 𝑧 𝑠 𝑥 ) ) ∧ ( ( 𝑦 · 𝑧 ) 𝑠 𝑥 ) = ( 𝑦 𝑠 ( 𝑧 𝑠 𝑥 ) ) ) ) ) ) ↔ ( 𝐺 ∈ AbelOp ∧ 𝑆 : ( ℂ × 𝑋 ) ⟶ 𝑋 ∧ ∀ 𝑥 ∈ 𝑋 ( ( 1 𝑆 𝑥 ) = 𝑥 ∧ ∀ 𝑦 ∈ ℂ ( ∀ 𝑧 ∈ 𝑋 ( 𝑦 𝑆 ( 𝑥 𝐺 𝑧 ) ) = ( ( 𝑦 𝑆 𝑥 ) 𝐺 ( 𝑦 𝑆 𝑧 ) ) ∧ ∀ 𝑧 ∈ ℂ ( ( ( 𝑦 + 𝑧 ) 𝑆 𝑥 ) = ( ( 𝑦 𝑆 𝑥 ) 𝐺 ( 𝑧 𝑆 𝑥 ) ) ∧ ( ( 𝑦 · 𝑧 ) 𝑆 𝑥 ) = ( 𝑦 𝑆 ( 𝑧 𝑆 𝑥 ) ) ) ) ) ) ) )
55	27 54	elopabi	⊢ ( 𝑊 ∈ { ⟨ 𝑔 , 𝑠 ⟩ ∣ ( 𝑔 ∈ AbelOp ∧ 𝑠 : ( ℂ × ran 𝑔 ) ⟶ ran 𝑔 ∧ ∀ 𝑥 ∈ ran 𝑔 ( ( 1 𝑠 𝑥 ) = 𝑥 ∧ ∀ 𝑦 ∈ ℂ ( ∀ 𝑧 ∈ ran 𝑔 ( 𝑦 𝑠 ( 𝑥 𝑔 𝑧 ) ) = ( ( 𝑦 𝑠 𝑥 ) 𝑔 ( 𝑦 𝑠 𝑧 ) ) ∧ ∀ 𝑧 ∈ ℂ ( ( ( 𝑦 + 𝑧 ) 𝑠 𝑥 ) = ( ( 𝑦 𝑠 𝑥 ) 𝑔 ( 𝑧 𝑠 𝑥 ) ) ∧ ( ( 𝑦 · 𝑧 ) 𝑠 𝑥 ) = ( 𝑦 𝑠 ( 𝑧 𝑠 𝑥 ) ) ) ) ) ) } → ( 𝐺 ∈ AbelOp ∧ 𝑆 : ( ℂ × 𝑋 ) ⟶ 𝑋 ∧ ∀ 𝑥 ∈ 𝑋 ( ( 1 𝑆 𝑥 ) = 𝑥 ∧ ∀ 𝑦 ∈ ℂ ( ∀ 𝑧 ∈ 𝑋 ( 𝑦 𝑆 ( 𝑥 𝐺 𝑧 ) ) = ( ( 𝑦 𝑆 𝑥 ) 𝐺 ( 𝑦 𝑆 𝑧 ) ) ∧ ∀ 𝑧 ∈ ℂ ( ( ( 𝑦 + 𝑧 ) 𝑆 𝑥 ) = ( ( 𝑦 𝑆 𝑥 ) 𝐺 ( 𝑧 𝑆 𝑥 ) ) ∧ ( ( 𝑦 · 𝑧 ) 𝑆 𝑥 ) = ( 𝑦 𝑆 ( 𝑧 𝑆 𝑥 ) ) ) ) ) ) )
56		df-vc	⊢ CVecOLD = { ⟨ 𝑔 , 𝑠 ⟩ ∣ ( 𝑔 ∈ AbelOp ∧ 𝑠 : ( ℂ × ran 𝑔 ) ⟶ ran 𝑔 ∧ ∀ 𝑥 ∈ ran 𝑔 ( ( 1 𝑠 𝑥 ) = 𝑥 ∧ ∀ 𝑦 ∈ ℂ ( ∀ 𝑧 ∈ ran 𝑔 ( 𝑦 𝑠 ( 𝑥 𝑔 𝑧 ) ) = ( ( 𝑦 𝑠 𝑥 ) 𝑔 ( 𝑦 𝑠 𝑧 ) ) ∧ ∀ 𝑧 ∈ ℂ ( ( ( 𝑦 + 𝑧 ) 𝑠 𝑥 ) = ( ( 𝑦 𝑠 𝑥 ) 𝑔 ( 𝑧 𝑠 𝑥 ) ) ∧ ( ( 𝑦 · 𝑧 ) 𝑠 𝑥 ) = ( 𝑦 𝑠 ( 𝑧 𝑠 𝑥 ) ) ) ) ) ) }
57	55 56	eleq2s	⊢ ( 𝑊 ∈ CVecOLD → ( 𝐺 ∈ AbelOp ∧ 𝑆 : ( ℂ × 𝑋 ) ⟶ 𝑋 ∧ ∀ 𝑥 ∈ 𝑋 ( ( 1 𝑆 𝑥 ) = 𝑥 ∧ ∀ 𝑦 ∈ ℂ ( ∀ 𝑧 ∈ 𝑋 ( 𝑦 𝑆 ( 𝑥 𝐺 𝑧 ) ) = ( ( 𝑦 𝑆 𝑥 ) 𝐺 ( 𝑦 𝑆 𝑧 ) ) ∧ ∀ 𝑧 ∈ ℂ ( ( ( 𝑦 + 𝑧 ) 𝑆 𝑥 ) = ( ( 𝑦 𝑆 𝑥 ) 𝐺 ( 𝑧 𝑆 𝑥 ) ) ∧ ( ( 𝑦 · 𝑧 ) 𝑆 𝑥 ) = ( 𝑦 𝑆 ( 𝑧 𝑆 𝑥 ) ) ) ) ) ) )