Metamath Proof Explorer

Theorem isclmi

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

Ref Expression
Hypothesis clm0.f ⊢ F = Scalar ⁡ W
Assertion isclmi ⊢ W ∈ LMod ∧ F = ℂ fld ↾ 𝑠 K ∧ K ∈ SubRing ⁡ ℂ fld → W ∈ CMod

Proof

Step Hyp Ref Expression
1 clm0.f ⊢ F = Scalar ⁡ W
2 simp1 ⊢ W ∈ LMod ∧ F = ℂ fld ↾ 𝑠 K ∧ K ∈ SubRing ⁡ ℂ fld → W ∈ LMod
3 simp2 ⊢ W ∈ LMod ∧ F = ℂ fld ↾ 𝑠 K ∧ K ∈ SubRing ⁡ ℂ fld → F = ℂ fld ↾ 𝑠 K
4 eqid ⊢ ℂ fld ↾ 𝑠 K = ℂ fld ↾ 𝑠 K
5 4 subrgbas ⊢ K ∈ SubRing ⁡ ℂ fld → K = Base ℂ fld ↾ 𝑠 K
6 5 3ad2ant3 ⊢ W ∈ LMod ∧ F = ℂ fld ↾ 𝑠 K ∧ K ∈ SubRing ⁡ ℂ fld → K = Base ℂ fld ↾ 𝑠 K
7 3 fveq2d ⊢ W ∈ LMod ∧ F = ℂ fld ↾ 𝑠 K ∧ K ∈ SubRing ⁡ ℂ fld → Base F = Base ℂ fld ↾ 𝑠 K
8 6 7 eqtr4d ⊢ W ∈ LMod ∧ F = ℂ fld ↾ 𝑠 K ∧ K ∈ SubRing ⁡ ℂ fld → K = Base F
9 8 oveq2d ⊢ W ∈ LMod ∧ F = ℂ fld ↾ 𝑠 K ∧ K ∈ SubRing ⁡ ℂ fld → ℂ fld ↾ 𝑠 K = ℂ fld ↾ 𝑠 Base F
10 3 9 eqtrd ⊢ W ∈ LMod ∧ F = ℂ fld ↾ 𝑠 K ∧ K ∈ SubRing ⁡ ℂ fld → F = ℂ fld ↾ 𝑠 Base F
11 simp3 ⊢ W ∈ LMod ∧ F = ℂ fld ↾ 𝑠 K ∧ K ∈ SubRing ⁡ ℂ fld → K ∈ SubRing ⁡ ℂ fld
12 8 11 eqeltrrd ⊢ W ∈ LMod ∧ F = ℂ fld ↾ 𝑠 K ∧ K ∈ SubRing ⁡ ℂ fld → Base F ∈ SubRing ⁡ ℂ fld
13 eqid ⊢ Base F = Base F
14 1 13 isclm ⊢ W ∈ CMod ↔ W ∈ LMod ∧ F = ℂ fld ↾ 𝑠 Base F ∧ Base F ∈ SubRing ⁡ ℂ fld
15 2 10 12 14 syl3anbrc ⊢ W ∈ LMod ∧ F = ℂ fld ↾ 𝑠 K ∧ K ∈ SubRing ⁡ ℂ fld → W ∈ CMod