Theorem isvclem

Description: Lemma for isvcOLD . (Contributed by NM, 31-May-2008) (New usage is discouraged.)

	Ref	Expression
Hypothesis	isvclem.1	⊢ 𝑋 = ran 𝐺
Assertion	isvclem	⊢ ( ( 𝐺 ∈ V ∧ 𝑆 ∈ V ) → ( ⟨ 𝐺 , 𝑆 ⟩ ∈ CVecOLD ↔ ( 𝐺 ∈ AbelOp ∧ 𝑆 : ( ℂ × 𝑋 ) ⟶ 𝑋 ∧ ∀ 𝑥 ∈ 𝑋 ( ( 1 𝑆 𝑥 ) = 𝑥 ∧ ∀ 𝑦 ∈ ℂ ( ∀ 𝑧 ∈ 𝑋 ( 𝑦 𝑆 ( 𝑥 𝐺 𝑧 ) ) = ( ( 𝑦 𝑆 𝑥 ) 𝐺 ( 𝑦 𝑆 𝑧 ) ) ∧ ∀ 𝑧 ∈ ℂ ( ( ( 𝑦 + 𝑧 ) 𝑆 𝑥 ) = ( ( 𝑦 𝑆 𝑥 ) 𝐺 ( 𝑧 𝑆 𝑥 ) ) ∧ ( ( 𝑦 · 𝑧 ) 𝑆 𝑥 ) = ( 𝑦 𝑆 ( 𝑧 𝑆 𝑥 ) ) ) ) ) ) ) )

Proof

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