Theorem isclmi

Description: Reverse direction of isclm . (Contributed by Mario Carneiro, 30-Oct-2015)

	Ref	Expression
Hypothesis	clm0.f	⊢ 𝐹 = ( Scalar ‘ 𝑊 )
Assertion	isclmi	⊢ ( ( 𝑊 ∈ LMod ∧ 𝐹 = ( ℂfld ↾s 𝐾 ) ∧ 𝐾 ∈ ( SubRing ‘ ℂfld ) ) → 𝑊 ∈ ℂMod )

Proof

Step	Hyp	Ref	Expression
1		clm0.f	⊢ 𝐹 = ( Scalar ‘ 𝑊 )
2		simp1	⊢ ( ( 𝑊 ∈ LMod ∧ 𝐹 = ( ℂfld ↾s 𝐾 ) ∧ 𝐾 ∈ ( SubRing ‘ ℂfld ) ) → 𝑊 ∈ LMod )
3		simp2	⊢ ( ( 𝑊 ∈ LMod ∧ 𝐹 = ( ℂfld ↾s 𝐾 ) ∧ 𝐾 ∈ ( SubRing ‘ ℂfld ) ) → 𝐹 = ( ℂfld ↾s 𝐾 ) )
4		eqid	⊢ ( ℂfld ↾s 𝐾 ) = ( ℂfld ↾s 𝐾 )
5	4	subrgbas	⊢ ( 𝐾 ∈ ( SubRing ‘ ℂfld ) → 𝐾 = ( Base ‘ ( ℂfld ↾s 𝐾 ) ) )
6	5	3ad2ant3	⊢ ( ( 𝑊 ∈ LMod ∧ 𝐹 = ( ℂfld ↾s 𝐾 ) ∧ 𝐾 ∈ ( SubRing ‘ ℂfld ) ) → 𝐾 = ( Base ‘ ( ℂfld ↾s 𝐾 ) ) )
7	3	fveq2d	⊢ ( ( 𝑊 ∈ LMod ∧ 𝐹 = ( ℂfld ↾s 𝐾 ) ∧ 𝐾 ∈ ( SubRing ‘ ℂfld ) ) → ( Base ‘ 𝐹 ) = ( Base ‘ ( ℂfld ↾s 𝐾 ) ) )
8	6 7	eqtr4d	⊢ ( ( 𝑊 ∈ LMod ∧ 𝐹 = ( ℂfld ↾s 𝐾 ) ∧ 𝐾 ∈ ( SubRing ‘ ℂfld ) ) → 𝐾 = ( Base ‘ 𝐹 ) )
9	8	oveq2d	⊢ ( ( 𝑊 ∈ LMod ∧ 𝐹 = ( ℂfld ↾s 𝐾 ) ∧ 𝐾 ∈ ( SubRing ‘ ℂfld ) ) → ( ℂfld ↾s 𝐾 ) = ( ℂfld ↾s ( Base ‘ 𝐹 ) ) )
10	3 9	eqtrd	⊢ ( ( 𝑊 ∈ LMod ∧ 𝐹 = ( ℂfld ↾s 𝐾 ) ∧ 𝐾 ∈ ( SubRing ‘ ℂfld ) ) → 𝐹 = ( ℂfld ↾s ( Base ‘ 𝐹 ) ) )
11		simp3	⊢ ( ( 𝑊 ∈ LMod ∧ 𝐹 = ( ℂfld ↾s 𝐾 ) ∧ 𝐾 ∈ ( SubRing ‘ ℂfld ) ) → 𝐾 ∈ ( SubRing ‘ ℂfld ) )
12	8 11	eqeltrrd	⊢ ( ( 𝑊 ∈ LMod ∧ 𝐹 = ( ℂfld ↾s 𝐾 ) ∧ 𝐾 ∈ ( SubRing ‘ ℂfld ) ) → ( Base ‘ 𝐹 ) ∈ ( SubRing ‘ ℂfld ) )
13		eqid	⊢ ( Base ‘ 𝐹 ) = ( Base ‘ 𝐹 )
14	1 13	isclm	⊢ ( 𝑊 ∈ ℂMod ↔ ( 𝑊 ∈ LMod ∧ 𝐹 = ( ℂfld ↾s ( Base ‘ 𝐹 ) ) ∧ ( Base ‘ 𝐹 ) ∈ ( SubRing ‘ ℂfld ) ) )
15	2 10 12 14	syl3anbrc	⊢ ( ( 𝑊 ∈ LMod ∧ 𝐹 = ( ℂfld ↾s 𝐾 ) ∧ 𝐾 ∈ ( SubRing ‘ ℂfld ) ) → 𝑊 ∈ ℂMod )