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 𝐹 = ( 𝑅 freeLMod 𝐼 )
frlm0.z 0 = ( 0g𝑅 )
Assertion frlm0 ( ( 𝑅 ∈ Ring ∧ 𝐼𝑊 ) → ( 𝐼 × { 0 } ) = ( 0g𝐹 ) )

Proof

Step Hyp Ref Expression
1 frlmval.f 𝐹 = ( 𝑅 freeLMod 𝐼 )
2 frlm0.z 0 = ( 0g𝑅 )
3 rlmlmod ( 𝑅 ∈ Ring → ( ringLMod ‘ 𝑅 ) ∈ LMod )
4 eqid ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) = ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 )
5 4 pwslmod ( ( ( ringLMod ‘ 𝑅 ) ∈ LMod ∧ 𝐼𝑊 ) → ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ∈ LMod )
6 3 5 sylan ( ( 𝑅 ∈ Ring ∧ 𝐼𝑊 ) → ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ∈ LMod )
7 eqid ( Base ‘ 𝐹 ) = ( Base ‘ 𝐹 )
8 eqid ( LSubSp ‘ ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ) = ( LSubSp ‘ ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) )
9 1 7 8 frlmlss ( ( 𝑅 ∈ Ring ∧ 𝐼𝑊 ) → ( Base ‘ 𝐹 ) ∈ ( LSubSp ‘ ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ) )
10 8 lsssubg ( ( ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ∈ LMod ∧ ( Base ‘ 𝐹 ) ∈ ( LSubSp ‘ ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ) ) → ( Base ‘ 𝐹 ) ∈ ( SubGrp ‘ ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ) )
11 6 9 10 syl2anc ( ( 𝑅 ∈ Ring ∧ 𝐼𝑊 ) → ( Base ‘ 𝐹 ) ∈ ( SubGrp ‘ ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ) )
12 eqid ( ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ↾s ( Base ‘ 𝐹 ) ) = ( ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ↾s ( Base ‘ 𝐹 ) )
13 eqid ( 0g ‘ ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ) = ( 0g ‘ ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) )
14 12 13 subg0 ( ( Base ‘ 𝐹 ) ∈ ( SubGrp ‘ ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ) → ( 0g ‘ ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ) = ( 0g ‘ ( ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ↾s ( Base ‘ 𝐹 ) ) ) )
15 11 14 syl ( ( 𝑅 ∈ Ring ∧ 𝐼𝑊 ) → ( 0g ‘ ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ) = ( 0g ‘ ( ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ↾s ( Base ‘ 𝐹 ) ) ) )
16 lmodgrp ( ( ringLMod ‘ 𝑅 ) ∈ LMod → ( ringLMod ‘ 𝑅 ) ∈ Grp )
17 grpmnd ( ( ringLMod ‘ 𝑅 ) ∈ Grp → ( ringLMod ‘ 𝑅 ) ∈ Mnd )
18 3 16 17 3syl ( 𝑅 ∈ Ring → ( ringLMod ‘ 𝑅 ) ∈ Mnd )
19 rlm0 ( 0g𝑅 ) = ( 0g ‘ ( ringLMod ‘ 𝑅 ) )
20 2 19 eqtri 0 = ( 0g ‘ ( ringLMod ‘ 𝑅 ) )
21 4 20 pws0g ( ( ( ringLMod ‘ 𝑅 ) ∈ Mnd ∧ 𝐼𝑊 ) → ( 𝐼 × { 0 } ) = ( 0g ‘ ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ) )
22 18 21 sylan ( ( 𝑅 ∈ Ring ∧ 𝐼𝑊 ) → ( 𝐼 × { 0 } ) = ( 0g ‘ ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ) )
23 1 7 frlmpws ( ( 𝑅 ∈ Ring ∧ 𝐼𝑊 ) → 𝐹 = ( ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ↾s ( Base ‘ 𝐹 ) ) )
24 23 fveq2d ( ( 𝑅 ∈ Ring ∧ 𝐼𝑊 ) → ( 0g𝐹 ) = ( 0g ‘ ( ( ( ringLMod ‘ 𝑅 ) ↑s 𝐼 ) ↾s ( Base ‘ 𝐹 ) ) ) )
25 15 22 24 3eqtr4d ( ( 𝑅 ∈ Ring ∧ 𝐼𝑊 ) → ( 𝐼 × { 0 } ) = ( 0g𝐹 ) )