Metamath Proof Explorer

Theorem frlmsslss

Description: A subset of a free module obtained by restricting the support set is a submodule. J is the set of forbidden unit vectors. (Contributed by Stefan O'Rear, 4-Feb-2015)

Ref Expression
Hypotheses frlmsslss.y ⊢ Y = R freeLMod I
frlmsslss.u ⊢ U = LSubSp ⁡ Y
frlmsslss.b ⊢ B = Base Y
frlmsslss.z ⊢ 0 ˙ = 0 R
frlmsslss.c ⊢ C = x ∈ B | x ↾ J = J × 0 ˙
Assertion frlmsslss ⊢ R ∈ Ring ∧ I ∈ V ∧ J ⊆ I → C ∈ U

Proof

Step Hyp Ref Expression
1 frlmsslss.y ⊢ Y = R freeLMod I
2 frlmsslss.u ⊢ U = LSubSp ⁡ Y
3 frlmsslss.b ⊢ B = Base Y
4 frlmsslss.z ⊢ 0 ˙ = 0 R
5 frlmsslss.c ⊢ C = x ∈ B | x ↾ J = J × 0 ˙
6 simp1 ⊢ R ∈ Ring ∧ I ∈ V ∧ J ⊆ I → R ∈ Ring
7 simp2 ⊢ R ∈ Ring ∧ I ∈ V ∧ J ⊆ I → I ∈ V
8 simp3 ⊢ R ∈ Ring ∧ I ∈ V ∧ J ⊆ I → J ⊆ I
9 7 8 ssexd ⊢ R ∈ Ring ∧ I ∈ V ∧ J ⊆ I → J ∈ V
10 eqid ⊢ R freeLMod J = R freeLMod J
11 10 4 frlm0 ⊢ R ∈ Ring ∧ J ∈ V → J × 0 ˙ = 0 R freeLMod J
12 6 9 11 syl2anc ⊢ R ∈ Ring ∧ I ∈ V ∧ J ⊆ I → J × 0 ˙ = 0 R freeLMod J
13 12 eqeq2d ⊢ R ∈ Ring ∧ I ∈ V ∧ J ⊆ I → x ↾ J = J × 0 ˙ ↔ x ↾ J = 0 R freeLMod J
14 13 rabbidv ⊢ R ∈ Ring ∧ I ∈ V ∧ J ⊆ I → x ∈ B | x ↾ J = J × 0 ˙ = x ∈ B | x ↾ J = 0 R freeLMod J
15 5 14 syl5eq ⊢ R ∈ Ring ∧ I ∈ V ∧ J ⊆ I → C = x ∈ B | x ↾ J = 0 R freeLMod J
16 eqid ⊢ Base R freeLMod J = Base R freeLMod J
17 eqid ⊢ x ∈ B ⟼ x ↾ J = x ∈ B ⟼ x ↾ J
18 1 10 3 16 17 frlmsplit2 ⊢ R ∈ Ring ∧ I ∈ V ∧ J ⊆ I → x ∈ B ⟼ x ↾ J ∈ Y LMHom R freeLMod J
19 fvex ⊢ 0 R freeLMod J ∈ V
20 17 mptiniseg ⊢ 0 R freeLMod J ∈ V → x ∈ B ⟼ x ↾ J -1 0 R freeLMod J = x ∈ B | x ↾ J = 0 R freeLMod J
21 19 20 ax-mp ⊢ x ∈ B ⟼ x ↾ J -1 0 R freeLMod J = x ∈ B | x ↾ J = 0 R freeLMod J
22 21 eqcomi ⊢ x ∈ B | x ↾ J = 0 R freeLMod J = x ∈ B ⟼ x ↾ J -1 0 R freeLMod J
23 eqid ⊢ 0 R freeLMod J = 0 R freeLMod J
24 22 23 2 lmhmkerlss ⊢ x ∈ B ⟼ x ↾ J ∈ Y LMHom R freeLMod J → x ∈ B | x ↾ J = 0 R freeLMod J ∈ U
25 18 24 syl ⊢ R ∈ Ring ∧ I ∈ V ∧ J ⊆ I → x ∈ B | x ↾ J = 0 R freeLMod J ∈ U
26 15 25 eqeltrd ⊢ R ∈ Ring ∧ I ∈ V ∧ J ⊆ I → C ∈ U