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 = ( R freeLMod I )
frlm0.z 
|- .0. = ( 0g ` R )
Assertion frlm0 
|- ( ( R e. Ring /\ I e. W ) -> ( I X. { .0. } ) = ( 0g ` F ) )

Proof

Step Hyp Ref Expression
1 frlmval.f 
 |-  F = ( R freeLMod I )
2 frlm0.z 
 |-  .0. = ( 0g ` R )
3 rlmlmod 
 |-  ( R e. Ring -> ( ringLMod ` R ) e. LMod )
4 eqid 
 |-  ( ( ringLMod ` R ) ^s I ) = ( ( ringLMod ` R ) ^s I )
5 4 pwslmod 
 |-  ( ( ( ringLMod ` R ) e. LMod /\ I e. W ) -> ( ( ringLMod ` R ) ^s I ) e. LMod )
6 3 5 sylan 
 |-  ( ( R e. Ring /\ I e. W ) -> ( ( ringLMod ` R ) ^s I ) e. LMod )
7 eqid 
 |-  ( Base ` F ) = ( Base ` F )
8 eqid 
 |-  ( LSubSp ` ( ( ringLMod ` R ) ^s I ) ) = ( LSubSp ` ( ( ringLMod ` R ) ^s I ) )
9 1 7 8 frlmlss 
 |-  ( ( R e. Ring /\ I e. W ) -> ( Base ` F ) e. ( LSubSp ` ( ( ringLMod ` R ) ^s I ) ) )
10 8 lsssubg 
 |-  ( ( ( ( ringLMod ` R ) ^s I ) e. LMod /\ ( Base ` F ) e. ( LSubSp ` ( ( ringLMod ` R ) ^s I ) ) ) -> ( Base ` F ) e. ( SubGrp ` ( ( ringLMod ` R ) ^s I ) ) )
11 6 9 10 syl2anc 
 |-  ( ( R e. Ring /\ I e. W ) -> ( Base ` F ) e. ( SubGrp ` ( ( ringLMod ` R ) ^s I ) ) )
12 eqid 
 |-  ( ( ( ringLMod ` R ) ^s I ) |`s ( Base ` F ) ) = ( ( ( ringLMod ` R ) ^s I ) |`s ( Base ` F ) )
13 eqid 
 |-  ( 0g ` ( ( ringLMod ` R ) ^s I ) ) = ( 0g ` ( ( ringLMod ` R ) ^s I ) )
14 12 13 subg0 
 |-  ( ( Base ` F ) e. ( SubGrp ` ( ( ringLMod ` R ) ^s I ) ) -> ( 0g ` ( ( ringLMod ` R ) ^s I ) ) = ( 0g ` ( ( ( ringLMod ` R ) ^s I ) |`s ( Base ` F ) ) ) )
15 11 14 syl 
 |-  ( ( R e. Ring /\ I e. W ) -> ( 0g ` ( ( ringLMod ` R ) ^s I ) ) = ( 0g ` ( ( ( ringLMod ` R ) ^s I ) |`s ( Base ` F ) ) ) )
16 lmodgrp 
 |-  ( ( ringLMod ` R ) e. LMod -> ( ringLMod ` R ) e. Grp )
17 grpmnd 
 |-  ( ( ringLMod ` R ) e. Grp -> ( ringLMod ` R ) e. Mnd )
18 3 16 17 3syl 
 |-  ( R e. Ring -> ( ringLMod ` R ) e. Mnd )
19 rlm0 
 |-  ( 0g ` R ) = ( 0g ` ( ringLMod ` R ) )
20 2 19 eqtri 
 |-  .0. = ( 0g ` ( ringLMod ` R ) )
21 4 20 pws0g 
 |-  ( ( ( ringLMod ` R ) e. Mnd /\ I e. W ) -> ( I X. { .0. } ) = ( 0g ` ( ( ringLMod ` R ) ^s I ) ) )
22 18 21 sylan 
 |-  ( ( R e. Ring /\ I e. W ) -> ( I X. { .0. } ) = ( 0g ` ( ( ringLMod ` R ) ^s I ) ) )
23 1 7 frlmpws 
 |-  ( ( R e. Ring /\ I e. W ) -> F = ( ( ( ringLMod ` R ) ^s I ) |`s ( Base ` F ) ) )
24 23 fveq2d 
 |-  ( ( R e. Ring /\ I e. W ) -> ( 0g ` F ) = ( 0g ` ( ( ( ringLMod ` R ) ^s I ) |`s ( Base ` F ) ) ) )
25 15 22 24 3eqtr4d 
 |-  ( ( R e. Ring /\ I e. W ) -> ( I X. { .0. } ) = ( 0g ` F ) )