Metamath Proof Explorer

Theorem isvcOLD

Description: The predicate "is a complex vector space." (Contributed by NM, 31-May-2008) Obsolete version of iscvsp . (New usage is discouraged.) (Proof modification is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		isvcOLD.1	⊢ 𝑋 = ran 𝐺
2		vcex	⊢ ( ⟨ 𝐺 , 𝑆 ⟩ ∈ CVec_OLD → ( 𝐺 ∈ V ∧ 𝑆 ∈ V ) )
3		elex	⊢ ( 𝐺 ∈ AbelOp → 𝐺 ∈ V )
4	3	adantr	⊢ ( ( 𝐺 ∈ AbelOp ∧ 𝑆 : ( ℂ × 𝑋 ) ⟶ 𝑋 ) → 𝐺 ∈ V )
5		cnex	⊢ ℂ ∈ V
6		ablogrpo	⊢ ( 𝐺 ∈ AbelOp → 𝐺 ∈ GrpOp )
7		rnexg	⊢ ( 𝐺 ∈ GrpOp → ran 𝐺 ∈ V )
8	1 7	eqeltrid	⊢ ( 𝐺 ∈ GrpOp → 𝑋 ∈ V )
9	6 8	syl	⊢ ( 𝐺 ∈ AbelOp → 𝑋 ∈ V )
10		xpexg	⊢ ( ( ℂ ∈ V ∧ 𝑋 ∈ V ) → ( ℂ × 𝑋 ) ∈ V )
11	5 9 10	sylancr	⊢ ( 𝐺 ∈ AbelOp → ( ℂ × 𝑋 ) ∈ V )
12		fex	⊢ ( ( 𝑆 : ( ℂ × 𝑋 ) ⟶ 𝑋 ∧ ( ℂ × 𝑋 ) ∈ V ) → 𝑆 ∈ V )
13	11 12	sylan2	⊢ ( ( 𝑆 : ( ℂ × 𝑋 ) ⟶ 𝑋 ∧ 𝐺 ∈ AbelOp ) → 𝑆 ∈ V )
14	13	ancoms	⊢ ( ( 𝐺 ∈ AbelOp ∧ 𝑆 : ( ℂ × 𝑋 ) ⟶ 𝑋 ) → 𝑆 ∈ V )
15	4 14	jca	⊢ ( ( 𝐺 ∈ AbelOp ∧ 𝑆 : ( ℂ × 𝑋 ) ⟶ 𝑋 ) → ( 𝐺 ∈ V ∧ 𝑆 ∈ V ) )
16	15	3adant3	⊢ ( ( 𝐺 ∈ AbelOp ∧ 𝑆 : ( ℂ × 𝑋 ) ⟶ 𝑋 ∧ ∀ 𝑥 ∈ 𝑋 ( ( 1 𝑆 𝑥 ) = 𝑥 ∧ ∀ 𝑦 ∈ ℂ ( ∀ 𝑧 ∈ 𝑋 ( 𝑦 𝑆 ( 𝑥 𝐺 𝑧 ) ) = ( ( 𝑦 𝑆 𝑥 ) 𝐺 ( 𝑦 𝑆 𝑧 ) ) ∧ ∀ 𝑧 ∈ ℂ ( ( ( 𝑦 + 𝑧 ) 𝑆 𝑥 ) = ( ( 𝑦 𝑆 𝑥 ) 𝐺 ( 𝑧 𝑆 𝑥 ) ) ∧ ( ( 𝑦 · 𝑧 ) 𝑆 𝑥 ) = ( 𝑦 𝑆 ( 𝑧 𝑆 𝑥 ) ) ) ) ) ) → ( 𝐺 ∈ V ∧ 𝑆 ∈ V ) )
17	1	isvclem	⊢ ( ( 𝐺 ∈ V ∧ 𝑆 ∈ V ) → ( ⟨ 𝐺 , 𝑆 ⟩ ∈ CVec_OLD ↔ ( 𝐺 ∈ AbelOp ∧ 𝑆 : ( ℂ × 𝑋 ) ⟶ 𝑋 ∧ ∀ 𝑥 ∈ 𝑋 ( ( 1 𝑆 𝑥 ) = 𝑥 ∧ ∀ 𝑦 ∈ ℂ ( ∀ 𝑧 ∈ 𝑋 ( 𝑦 𝑆 ( 𝑥 𝐺 𝑧 ) ) = ( ( 𝑦 𝑆 𝑥 ) 𝐺 ( 𝑦 𝑆 𝑧 ) ) ∧ ∀ 𝑧 ∈ ℂ ( ( ( 𝑦 + 𝑧 ) 𝑆 𝑥 ) = ( ( 𝑦 𝑆 𝑥 ) 𝐺 ( 𝑧 𝑆 𝑥 ) ) ∧ ( ( 𝑦 · 𝑧 ) 𝑆 𝑥 ) = ( 𝑦 𝑆 ( 𝑧 𝑆 𝑥 ) ) ) ) ) ) ) )
18	2 16 17	pm5.21nii	⊢ ( ⟨ 𝐺 , 𝑆 ⟩ ∈ CVec_OLD ↔ ( 𝐺 ∈ AbelOp ∧ 𝑆 : ( ℂ × 𝑋 ) ⟶ 𝑋 ∧ ∀ 𝑥 ∈ 𝑋 ( ( 1 𝑆 𝑥 ) = 𝑥 ∧ ∀ 𝑦 ∈ ℂ ( ∀ 𝑧 ∈ 𝑋 ( 𝑦 𝑆 ( 𝑥 𝐺 𝑧 ) ) = ( ( 𝑦 𝑆 𝑥 ) 𝐺 ( 𝑦 𝑆 𝑧 ) ) ∧ ∀ 𝑧 ∈ ℂ ( ( ( 𝑦 + 𝑧 ) 𝑆 𝑥 ) = ( ( 𝑦 𝑆 𝑥 ) 𝐺 ( 𝑧 𝑆 𝑥 ) ) ∧ ( ( 𝑦 · 𝑧 ) 𝑆 𝑥 ) = ( 𝑦 𝑆 ( 𝑧 𝑆 𝑥 ) ) ) ) ) ) )