This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )