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 = Base W
lmodfopne.s S = Scalar W
lmodfopne.k K = Base S
Assertion lmodfopnelem1 W LMod + ˙ = · ˙ V = K

Proof

Step Hyp Ref Expression
1 lmodfopne.t · ˙ = 𝑠𝑓 W
2 lmodfopne.a + ˙ = + 𝑓 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 LMod · ˙ : K × V V
7 6 ffnd W LMod · ˙ Fn K × V
8 3 2 plusffn + ˙ Fn V × V
9 fneq1 + ˙ = · ˙ + ˙ Fn V × V · ˙ Fn V × V
10 fndmu · ˙ Fn V × V · ˙ Fn K × V V × V = K × V
11 10 ex · ˙ Fn V × V · ˙ Fn K × V V × V = K × V
12 9 11 syl6bi + ˙ = · ˙ + ˙ Fn V × V · ˙ Fn K × V V × V = K × V
13 12 com13 · ˙ Fn K × V + ˙ Fn V × V + ˙ = · ˙ V × V = K × V
14 13 impcom + ˙ Fn V × V · ˙ Fn K × V + ˙ = · ˙ V × V = K × V
15 3 lmodbn0 W LMod V
16 xp11 V V V × V = K × V V = K V = V
17 15 15 16 syl2anc W LMod V × V = K × V V = K V = V
18 17 simprbda W LMod V × V = K × V V = K
19 18 expcom V × V = K × V W LMod V = K
20 14 19 syl6 + ˙ Fn V × V · ˙ Fn K × V + ˙ = · ˙ W LMod V = K
21 20 com23 + ˙ Fn V × V · ˙ Fn K × V W LMod + ˙ = · ˙ V = K
22 21 ex + ˙ Fn V × V · ˙ Fn K × V W LMod + ˙ = · ˙ V = K
23 22 com23 + ˙ Fn V × V W LMod · ˙ Fn K × V + ˙ = · ˙ V = K
24 8 23 ax-mp W LMod · ˙ Fn K × V + ˙ = · ˙ V = K
25 7 24 mpd W LMod + ˙ = · ˙ V = K
26 25 imp W LMod + ˙ = · ˙ V = K