lmodfopnelem2

	Ref	Expression
Hypotheses	lmodfopne.t	$⊢ \underset{˙}{\cdot} = \cdot_{𝑠𝑓} (W)$
	lmodfopne.a	$⊢ \underset{˙}{+} = +_{𝑓} (W)$
	lmodfopne.v	$⊢ V = {Base}_{W}$
	lmodfopne.s	$⊢ S = Scalar (W)$
	lmodfopne.k	$⊢ K = {Base}_{S}$
	lmodfopne.0	$⊢ \underset{˙}{0} = 0_{S}$
	lmodfopne.1	$⊢ \underset{˙}{1} = 1_{S}$
Assertion	lmodfopnelem2	$⊢ (W \in LMod \land \underset{˙}{+} = \underset{˙}{\cdot}) \to (\underset{˙}{0} \in V \land \underset{˙}{1} \in V)$

Step	Hyp	Ref	Expression
1		lmodfopne.t	$⊢ \underset{˙}{\cdot} = \cdot_{𝑠𝑓} (W)$
2		lmodfopne.a	$⊢ \underset{˙}{+} = +_{𝑓} (W)$
3		lmodfopne.v	$⊢ V = {Base}_{W}$
4		lmodfopne.s	$⊢ S = Scalar (W)$
5		lmodfopne.k	$⊢ K = {Base}_{S}$
6		lmodfopne.0	$⊢ \underset{˙}{0} = 0_{S}$
7		lmodfopne.1	$⊢ \underset{˙}{1} = 1_{S}$
8	1 2 3 4 5	lmodfopnelem1	$⊢ (W \in LMod \land \underset{˙}{+} = \underset{˙}{\cdot}) \to V = K$
9	8	ex	$⊢ W \in LMod \to (\underset{˙}{+} = \underset{˙}{\cdot} \to V = K)$
10	4 5 6	lmod0cl	$⊢ W \in LMod \to \underset{˙}{0} \in K$
11	4 5 7	lmod1cl	$⊢ W \in LMod \to \underset{˙}{1} \in K$
12	10 11	jca	$⊢ W \in LMod \to (\underset{˙}{0} \in K \land \underset{˙}{1} \in K)$
13		eleq2	$⊢ V = K \to (\underset{˙}{0} \in V \leftrightarrow \underset{˙}{0} \in K)$
14		eleq2	$⊢ V = K \to (\underset{˙}{1} \in V \leftrightarrow \underset{˙}{1} \in K)$
15	13 14	anbi12d	$⊢ V = K \to ((\underset{˙}{0} \in V \land \underset{˙}{1} \in V) \leftrightarrow (\underset{˙}{0} \in K \land \underset{˙}{1} \in K))$
16	12 15	syl5ibrcom	$⊢ W \in LMod \to (V = K \to (\underset{˙}{0} \in V \land \underset{˙}{1} \in V))$
17	9 16	syld	$⊢ W \in LMod \to (\underset{˙}{+} = \underset{˙}{\cdot} \to (\underset{˙}{0} \in V \land \underset{˙}{1} \in V))$
18	17	imp	$⊢ (W \in LMod \land \underset{˙}{+} = \underset{˙}{\cdot}) \to (\underset{˙}{0} \in V \land \underset{˙}{1} \in V)$

Metamath Proof Explorer