Metamath Proof Explorer

Theorem frlm0

Description: Zero in a free module (ring constraint is stronger than necessary, but allows use of frlmlss ). (Contributed by Stefan O'Rear, 4-Feb-2015)

Ref Expression
Hypotheses frlmval.f ⊢F=RfreeLModI
frlm0.z ⊢0˙=0R
Assertion frlm0 ⊢R∈Ring∧I∈W→I×0˙=0F

Proof

Step Hyp Ref Expression
1 frlmval.f ⊢F=RfreeLModI
2 frlm0.z ⊢0˙=0R
3 rlmlmod ⊢R∈Ring→ringLMod⁡R∈LMod
4 eqid ⊢ringLMod⁡R↑𝑠I=ringLMod⁡R↑𝑠I
5 4 pwslmod ⊢ringLMod⁡R∈LMod∧I∈W→ringLMod⁡R↑𝑠I∈LMod
6 3 5 sylan ⊢R∈Ring∧I∈W→ringLMod⁡R↑𝑠I∈LMod
7 eqid ⊢BaseF=BaseF
8 eqid ⊢LSubSp⁡ringLMod⁡R↑𝑠I=LSubSp⁡ringLMod⁡R↑𝑠I
9 1 7 8 frlmlss ⊢R∈Ring∧I∈W→BaseF∈LSubSp⁡ringLMod⁡R↑𝑠I
10 8 lsssubg ⊢ringLMod⁡R↑𝑠I∈LMod∧BaseF∈LSubSp⁡ringLMod⁡R↑𝑠I→BaseF∈SubGrp⁡ringLMod⁡R↑𝑠I
11 6 9 10 syl2anc ⊢R∈Ring∧I∈W→BaseF∈SubGrp⁡ringLMod⁡R↑𝑠I
12 eqid ⊢ringLMod⁡R↑𝑠I↾𝑠BaseF=ringLMod⁡R↑𝑠I↾𝑠BaseF
13 eqid ⊢0ringLMod⁡R↑𝑠I=0ringLMod⁡R↑𝑠I
14 12 13 subg0 ⊢BaseF∈SubGrp⁡ringLMod⁡R↑𝑠I→0ringLMod⁡R↑𝑠I=0ringLMod⁡R↑𝑠I↾𝑠BaseF
15 11 14 syl ⊢R∈Ring∧I∈W→0ringLMod⁡R↑𝑠I=0ringLMod⁡R↑𝑠I↾𝑠BaseF
16 lmodgrp ⊢ringLMod⁡R∈LMod→ringLMod⁡R∈Grp
17 grpmnd ⊢ringLMod⁡R∈Grp→ringLMod⁡R∈Mnd
18 3 16 17 3syl ⊢R∈Ring→ringLMod⁡R∈Mnd
19 rlm0 ⊢0R=0ringLMod⁡R
20 2 19 eqtri ⊢0˙=0ringLMod⁡R
21 4 20 pws0g ⊢ringLMod⁡R∈Mnd∧I∈W→I×0˙=0ringLMod⁡R↑𝑠I
22 18 21 sylan ⊢R∈Ring∧I∈W→I×0˙=0ringLMod⁡R↑𝑠I
23 1 7 frlmpws ⊢R∈Ring∧I∈W→F=ringLMod⁡R↑𝑠I↾𝑠BaseF
24 23 fveq2d ⊢R∈Ring∧I∈W→0F=0ringLMod⁡R↑𝑠I↾𝑠BaseF
25 15 22 24 3eqtr4d ⊢R∈Ring∧I∈W→I×0˙=0F