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 \in LMod \land F = ℂ_{fld} ↾_{𝑠} K \land K \in SubRing (ℂ_{fld})) \to W \in CMod$

Proof

Step	Hyp	Ref	Expression
1		clm0.f	$⊢ F = Scalar (W)$
2		simp1	$⊢ (W \in LMod \land F = ℂ_{fld} ↾_{𝑠} K \land K \in SubRing (ℂ_{fld})) \to W \in LMod$
3		simp2	$⊢ (W \in LMod \land F = ℂ_{fld} ↾_{𝑠} K \land K \in SubRing (ℂ_{fld})) \to F = ℂ_{fld} ↾_{𝑠} K$
4		eqid	$⊢ ℂ_{fld} ↾_{𝑠} K = ℂ_{fld} ↾_{𝑠} K$
5	4	subrgbas	$⊢ K \in SubRing (ℂ_{fld}) \to K = {Base}_{(ℂ_{fld} ↾_{𝑠} K)}$
6	5	3ad2ant3	$⊢ (W \in LMod \land F = ℂ_{fld} ↾_{𝑠} K \land K \in SubRing (ℂ_{fld})) \to K = {Base}_{(ℂ_{fld} ↾_{𝑠} K)}$
7	3	fveq2d	$⊢ (W \in LMod \land F = ℂ_{fld} ↾_{𝑠} K \land K \in SubRing (ℂ_{fld})) \to {Base}_{F} = {Base}_{(ℂ_{fld} ↾_{𝑠} K)}$
8	6 7	eqtr4d	$⊢ (W \in LMod \land F = ℂ_{fld} ↾_{𝑠} K \land K \in SubRing (ℂ_{fld})) \to K = {Base}_{F}$
9	8	oveq2d	$⊢ (W \in LMod \land F = ℂ_{fld} ↾_{𝑠} K \land K \in SubRing (ℂ_{fld})) \to ℂ_{fld} ↾_{𝑠} K = ℂ_{fld} ↾_{𝑠} {Base}_{F}$
10	3 9	eqtrd	$⊢ (W \in LMod \land F = ℂ_{fld} ↾_{𝑠} K \land K \in SubRing (ℂ_{fld})) \to F = ℂ_{fld} ↾_{𝑠} {Base}_{F}$
11		simp3	$⊢ (W \in LMod \land F = ℂ_{fld} ↾_{𝑠} K \land K \in SubRing (ℂ_{fld})) \to K \in SubRing (ℂ_{fld})$
12	8 11	eqeltrrd	$⊢ (W \in LMod \land F = ℂ_{fld} ↾_{𝑠} K \land K \in SubRing (ℂ_{fld})) \to {Base}_{F} \in SubRing (ℂ_{fld})$
13		eqid	$⊢ {Base}_{F} = {Base}_{F}$
14	1 13	isclm	$⊢ W \in CMod \leftrightarrow (W \in LMod \land F = ℂ_{fld} ↾_{𝑠} {Base}_{F} \land {Base}_{F} \in SubRing (ℂ_{fld}))$
15	2 10 12 14	syl3anbrc	$⊢ (W \in LMod \land F = ℂ_{fld} ↾_{𝑠} K \land K \in SubRing (ℂ_{fld})) \to W \in CMod$