This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )