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 ‘ 𝐹 ) )