Theorem lmodfopnelem1

Description: Lemma 1 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$$
Assertion	lmodfopnelem1	$$⊢\left(W\in \mathrm{LMod}\wedge \underset{\dot{}}{+}=\underset{\dot{}}{·}\right)\to V=K$$

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	3 4 5 1	lmodscaf	$$⊢W\in \mathrm{LMod}\to \underset{\dot{}}{·}:K\times V⟶V$$
7	6	ffnd	$$⊢W\in \mathrm{LMod}\to \underset{\dot{}}{·}Fn\left(K\times V\right)$$
8	3 2	plusffn	$$⊢\underset{\dot{}}{+}Fn\left(V\times V\right)$$
9		fneq1	$$⊢\underset{\dot{}}{+}=\underset{\dot{}}{·}\to \left(\underset{\dot{}}{+}Fn\left(V\times V\right)\leftrightarrow \underset{\dot{}}{·}Fn\left(V\times V\right)\right)$$
10		fndmu	$$⊢\left(\underset{\dot{}}{·}Fn\left(V\times V\right)\wedge \underset{\dot{}}{·}Fn\left(K\times V\right)\right)\to V\times V=K\times V$$
11	10	ex	$$⊢\underset{\dot{}}{·}Fn\left(V\times V\right)\to \left(\underset{\dot{}}{·}Fn\left(K\times V\right)\to V\times V=K\times V\right)$$
12	9 11	biimtrdi	$$⊢\underset{\dot{}}{+}=\underset{\dot{}}{·}\to \left(\underset{\dot{}}{+}Fn\left(V\times V\right)\to \left(\underset{\dot{}}{·}Fn\left(K\times V\right)\to V\times V=K\times V\right)\right)$$
13	12	com13	$$⊢\underset{\dot{}}{·}Fn\left(K\times V\right)\to \left(\underset{\dot{}}{+}Fn\left(V\times V\right)\to \left(\underset{\dot{}}{+}=\underset{\dot{}}{·}\to V\times V=K\times V\right)\right)$$
14	13	impcom	$$⊢\left(\underset{\dot{}}{+}Fn\left(V\times V\right)\wedge \underset{\dot{}}{·}Fn\left(K\times V\right)\right)\to \left(\underset{\dot{}}{+}=\underset{\dot{}}{·}\to V\times V=K\times V\right)$$
15	3	lmodbn0	$$⊢W\in \mathrm{LMod}\to V\ne \varnothing$$
16		xp11	$$⊢\left(V\ne \varnothing \wedge V\ne \varnothing \right)\to \left(V\times V=K\times V\leftrightarrow \left(V=K\wedge V=V\right)\right)$$
17	15 15 16	syl2anc	$$⊢W\in \mathrm{LMod}\to \left(V\times V=K\times V\leftrightarrow \left(V=K\wedge V=V\right)\right)$$
18	17	simprbda	$$⊢\left(W\in \mathrm{LMod}\wedge V\times V=K\times V\right)\to V=K$$
19	18	expcom	$$⊢V\times V=K\times V\to \left(W\in \mathrm{LMod}\to V=K\right)$$
20	14 19	syl6	$$⊢\left(\underset{\dot{}}{+}Fn\left(V\times V\right)\wedge \underset{\dot{}}{·}Fn\left(K\times V\right)\right)\to \left(\underset{\dot{}}{+}=\underset{\dot{}}{·}\to \left(W\in \mathrm{LMod}\to V=K\right)\right)$$
21	20	com23	$$⊢\left(\underset{\dot{}}{+}Fn\left(V\times V\right)\wedge \underset{\dot{}}{·}Fn\left(K\times V\right)\right)\to \left(W\in \mathrm{LMod}\to \left(\underset{\dot{}}{+}=\underset{\dot{}}{·}\to V=K\right)\right)$$
22	21	ex	$$⊢\underset{\dot{}}{+}Fn\left(V\times V\right)\to \left(\underset{\dot{}}{·}Fn\left(K\times V\right)\to \left(W\in \mathrm{LMod}\to \left(\underset{\dot{}}{+}=\underset{\dot{}}{·}\to V=K\right)\right)\right)$$
23	22	com23	$$⊢\underset{\dot{}}{+}Fn\left(V\times V\right)\to \left(W\in \mathrm{LMod}\to \left(\underset{\dot{}}{·}Fn\left(K\times V\right)\to \left(\underset{\dot{}}{+}=\underset{\dot{}}{·}\to V=K\right)\right)\right)$$
24	8 23	ax-mp	$$⊢W\in \mathrm{LMod}\to \left(\underset{\dot{}}{·}Fn\left(K\times V\right)\to \left(\underset{\dot{}}{+}=\underset{\dot{}}{·}\to V=K\right)\right)$$
25	7 24	mpd	$$⊢W\in \mathrm{LMod}\to \left(\underset{\dot{}}{+}=\underset{\dot{}}{·}\to V=K\right)$$
26	25	imp	$$⊢\left(W\in \mathrm{LMod}\wedge \underset{\dot{}}{+}=\underset{\dot{}}{·}\right)\to V=K$$