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 ˙ = 0 R
Assertion frlm0 ⊢ R ∈ Ring ∧ I ∈ W → I × 0 ˙ = 0 F

Proof

Step Hyp Ref Expression
1 frlmval.f ⊢ F = R freeLMod I
2 frlm0.z ⊢ 0 ˙ = 0 R
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 ⊢ Base F = Base F
8 eqid ⊢ LSubSp ⁡ ringLMod ⁡ R ↑ 𝑠 I = LSubSp ⁡ ringLMod ⁡ R ↑ 𝑠 I
9 1 7 8 frlmlss ⊢ R ∈ Ring ∧ I ∈ W → Base F ∈ LSubSp ⁡ ringLMod ⁡ R ↑ 𝑠 I
10 8 lsssubg ⊢ ringLMod ⁡ R ↑ 𝑠 I ∈ LMod ∧ Base F ∈ LSubSp ⁡ ringLMod ⁡ R ↑ 𝑠 I → Base F ∈ SubGrp ⁡ ringLMod ⁡ R ↑ 𝑠 I
11 6 9 10 syl2anc ⊢ R ∈ Ring ∧ I ∈ W → Base F ∈ SubGrp ⁡ ringLMod ⁡ R ↑ 𝑠 I
12 eqid ⊢ ringLMod ⁡ R ↑ 𝑠 I ↾ 𝑠 Base F = ringLMod ⁡ R ↑ 𝑠 I ↾ 𝑠 Base F
13 eqid ⊢ 0 ringLMod ⁡ R ↑ 𝑠 I = 0 ringLMod ⁡ R ↑ 𝑠 I
14 12 13 subg0 ⊢ Base F ∈ SubGrp ⁡ ringLMod ⁡ R ↑ 𝑠 I → 0 ringLMod ⁡ R ↑ 𝑠 I = 0 ringLMod ⁡ R ↑ 𝑠 I ↾ 𝑠 Base F
15 11 14 syl ⊢ R ∈ Ring ∧ I ∈ W → 0 ringLMod ⁡ R ↑ 𝑠 I = 0 ringLMod ⁡ R ↑ 𝑠 I ↾ 𝑠 Base F
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 ⊢ 0 R = 0 ringLMod ⁡ R
20 2 19 eqtri ⊢ 0 ˙ = 0 ringLMod ⁡ R
21 4 20 pws0g ⊢ ringLMod ⁡ R ∈ Mnd ∧ I ∈ W → I × 0 ˙ = 0 ringLMod ⁡ R ↑ 𝑠 I
22 18 21 sylan ⊢ R ∈ Ring ∧ I ∈ W → I × 0 ˙ = 0 ringLMod ⁡ R ↑ 𝑠 I
23 1 7 frlmpws ⊢ R ∈ Ring ∧ I ∈ W → F = ringLMod ⁡ R ↑ 𝑠 I ↾ 𝑠 Base F
24 23 fveq2d ⊢ R ∈ Ring ∧ I ∈ W → 0 F = 0 ringLMod ⁡ R ↑ 𝑠 I ↾ 𝑠 Base F
25 15 22 24 3eqtr4d ⊢ R ∈ Ring ∧ I ∈ W → I × 0 ˙ = 0 F