Theorem lmodfopnelem1

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

	Ref	Expression
Hypotheses	lmodfopne.t	|- .x. = ( .sf ` W )
	lmodfopne.a	|- .+ = ( +f ` W )
	lmodfopne.v	|- V = ( Base ` W )
	lmodfopne.s	|- S = ( Scalar ` W )
	lmodfopne.k	|- K = ( Base ` S )
Assertion	lmodfopnelem1	|- ( ( W e. LMod /\ .+ = .x. ) -> V = K )

Proof

Step	Hyp	Ref	Expression
1		lmodfopne.t	|- .x. = ( .sf ` W )
2		lmodfopne.a	|- .+ = ( +f ` 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 e. LMod -> .x. : ( K X. V ) --> V )
7	6	ffnd	|- ( W e. LMod -> .x. Fn ( K X. V ) )
8	3 2	plusffn	|- .+ Fn ( V X. V )
9		fneq1	|- ( .+ = .x. -> ( .+ Fn ( V X. V ) <-> .x. Fn ( V X. V ) ) )
10		fndmu	|- ( ( .x. Fn ( V X. V ) /\ .x. Fn ( K X. V ) ) -> ( V X. V ) = ( K X. V ) )
11	10	ex	|- ( .x. Fn ( V X. V ) -> ( .x. Fn ( K X. V ) -> ( V X. V ) = ( K X. V ) ) )
12	9 11	biimtrdi	|- ( .+ = .x. -> ( .+ Fn ( V X. V ) -> ( .x. Fn ( K X. V ) -> ( V X. V ) = ( K X. V ) ) ) )
13	12	com13	|- ( .x. Fn ( K X. V ) -> ( .+ Fn ( V X. V ) -> ( .+ = .x. -> ( V X. V ) = ( K X. V ) ) ) )
14	13	impcom	|- ( ( .+ Fn ( V X. V ) /\ .x. Fn ( K X. V ) ) -> ( .+ = .x. -> ( V X. V ) = ( K X. V ) ) )
15	3	lmodbn0	|- ( W e. LMod -> V =/= (/) )
16		xp11	|- ( ( V =/= (/) /\ V =/= (/) ) -> ( ( V X. V ) = ( K X. V ) <-> ( V = K /\ V = V ) ) )
17	15 15 16	syl2anc	|- ( W e. LMod -> ( ( V X. V ) = ( K X. V ) <-> ( V = K /\ V = V ) ) )
18	17	simprbda	|- ( ( W e. LMod /\ ( V X. V ) = ( K X. V ) ) -> V = K )
19	18	expcom	|- ( ( V X. V ) = ( K X. V ) -> ( W e. LMod -> V = K ) )
20	14 19	syl6	|- ( ( .+ Fn ( V X. V ) /\ .x. Fn ( K X. V ) ) -> ( .+ = .x. -> ( W e. LMod -> V = K ) ) )
21	20	com23	|- ( ( .+ Fn ( V X. V ) /\ .x. Fn ( K X. V ) ) -> ( W e. LMod -> ( .+ = .x. -> V = K ) ) )
22	21	ex	|- ( .+ Fn ( V X. V ) -> ( .x. Fn ( K X. V ) -> ( W e. LMod -> ( .+ = .x. -> V = K ) ) ) )
23	22	com23	|- ( .+ Fn ( V X. V ) -> ( W e. LMod -> ( .x. Fn ( K X. V ) -> ( .+ = .x. -> V = K ) ) ) )
24	8 23	ax-mp	|- ( W e. LMod -> ( .x. Fn ( K X. V ) -> ( .+ = .x. -> V = K ) ) )
25	7 24	mpd	|- ( W e. LMod -> ( .+ = .x. -> V = K ) )
26	25	imp	|- ( ( W e. LMod /\ .+ = .x. ) -> V = K )