Metamath Proof Explorer

Theorem lmod1lem1

Description: Lemma 1 for lmod1 . (Contributed by AV, 28-Apr-2019)

Ref Expression
Hypothesis lmod1.m ⊢ M = Base ndx I + ndx I I I Scalar ⁡ ndx R ∪ ⋅ ndx x ∈ Base R , y ∈ I ⟼ y
Assertion lmod1lem1 ⊢ I ∈ V ∧ R ∈ Ring ∧ r ∈ Base R → r ⋅ M I ∈ I

Proof

Step Hyp Ref Expression
1 lmod1.m ⊢ M = Base ndx I + ndx I I I Scalar ⁡ ndx R ∪ ⋅ ndx x ∈ Base R , y ∈ I ⟼ y
2 fvex ⊢ Base R ∈ V
3 snex ⊢ I ∈ V
4 3 a1i ⊢ I ∈ V ∧ R ∈ Ring ∧ r ∈ Base R → I ∈ V
5 mpoexga ⊢ Base R ∈ V ∧ I ∈ V → x ∈ Base R , y ∈ I ⟼ y ∈ V
6 2 4 5 sylancr ⊢ I ∈ V ∧ R ∈ Ring ∧ r ∈ Base R → x ∈ Base R , y ∈ I ⟼ y ∈ V
7 1 lmodvsca ⊢ x ∈ Base R , y ∈ I ⟼ y ∈ V → x ∈ Base R , y ∈ I ⟼ y = ⋅ M
8 6 7 syl ⊢ I ∈ V ∧ R ∈ Ring ∧ r ∈ Base R → x ∈ Base R , y ∈ I ⟼ y = ⋅ M
9 8 eqcomd ⊢ I ∈ V ∧ R ∈ Ring ∧ r ∈ Base R → ⋅ M = x ∈ Base R , y ∈ I ⟼ y
10 simprr ⊢ I ∈ V ∧ R ∈ Ring ∧ r ∈ Base R ∧ x = r ∧ y = I → y = I
11 simp3 ⊢ I ∈ V ∧ R ∈ Ring ∧ r ∈ Base R → r ∈ Base R
12 snidg ⊢ I ∈ V → I ∈ I
13 12 3ad2ant1 ⊢ I ∈ V ∧ R ∈ Ring ∧ r ∈ Base R → I ∈ I
14 9 10 11 13 13 ovmpod ⊢ I ∈ V ∧ R ∈ Ring ∧ r ∈ Base R → r ⋅ M I = I
15 14 13 eqeltrd ⊢ I ∈ V ∧ R ∈ Ring ∧ r ∈ Base R → r ⋅ M I ∈ I