lmodfopnelem1

	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}$
Assertion	lmodfopnelem1	$⊢ (W \in LMod \land \underset{˙}{+} = \underset{˙}{\cdot}) \to V = K$

Proof

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

Metamath Proof Explorer

Theorem lmodfopnelem1

Proof