Metamath Proof Explorer


Theorem lmodfopnelem1

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

Ref Expression
Hypotheses lmodfopne.t ·˙=𝑠𝑓W
lmodfopne.a +˙=+𝑓W
lmodfopne.v V=BaseW
lmodfopne.s S=ScalarW
lmodfopne.k K=BaseS
Assertion lmodfopnelem1 WLMod+˙=·˙V=K

Proof

Step Hyp Ref Expression
1 lmodfopne.t ·˙=𝑠𝑓W
2 lmodfopne.a +˙=+𝑓W
3 lmodfopne.v V=BaseW
4 lmodfopne.s S=ScalarW
5 lmodfopne.k K=BaseS
6 3 4 5 1 lmodscaf WLMod·˙:K×VV
7 6 ffnd WLMod·˙FnK×V
8 3 2 plusffn +˙FnV×V
9 fneq1 +˙=·˙+˙FnV×V·˙FnV×V
10 fndmu ·˙FnV×V·˙FnK×VV×V=K×V
11 10 ex ·˙FnV×V·˙FnK×VV×V=K×V
12 9 11 syl6bi +˙=·˙+˙FnV×V·˙FnK×VV×V=K×V
13 12 com13 ·˙FnK×V+˙FnV×V+˙=·˙V×V=K×V
14 13 impcom +˙FnV×V·˙FnK×V+˙=·˙V×V=K×V
15 3 lmodbn0 WLModV
16 xp11 VVV×V=K×VV=KV=V
17 15 15 16 syl2anc WLModV×V=K×VV=KV=V
18 17 simprbda WLModV×V=K×VV=K
19 18 expcom V×V=K×VWLModV=K
20 14 19 syl6 +˙FnV×V·˙FnK×V+˙=·˙WLModV=K
21 20 com23 +˙FnV×V·˙FnK×VWLMod+˙=·˙V=K
22 21 ex +˙FnV×V·˙FnK×VWLMod+˙=·˙V=K
23 22 com23 +˙FnV×VWLMod·˙FnK×V+˙=·˙V=K
24 8 23 ax-mp WLMod·˙FnK×V+˙=·˙V=K
25 7 24 mpd WLMod+˙=·˙V=K
26 25 imp WLMod+˙=·˙V=K