Theorem lmodfopnelem2

Description: Lemma 2 for lmodfopne . (Contributed by AV, 2-Oct-2021)

	Ref	Expression
Hypotheses	lmodfopne.t	$$⊢\underset{\dot{}}{·}={\cdot }_{\mathrm{𝑠𝑓}}\left(W\right)$$
	lmodfopne.a	$$⊢\underset{\dot{}}{+}={+}_{𝑓}\left(W\right)$$
	lmodfopne.v	$$⊢V={\mathrm{Base}}_W$$
	lmodfopne.s	$$⊢S=\mathrm{Scalar}\left(W\right)$$
	lmodfopne.k	$$⊢K={\mathrm{Base}}_S$$
	lmodfopne.0	$$⊢\underset{\dot{}}{0}=0_S$$
	lmodfopne.1	$$⊢\underset{\dot{}}{1}=1_S$$
Assertion	lmodfopnelem2	$$⊢\left(W\in \mathrm{LMod}\wedge \underset{\dot{}}{+}=\underset{\dot{}}{·}\right)\to \left(\underset{\dot{}}{0}\in V\wedge \underset{\dot{}}{1}\in V\right)$$

Proof

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