This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem rlmval2

Description: Value of the ring module extended. (Contributed by AV, 2-Dec-2018) (Revised by Thierry Arnoux, 16-Jun-2019)

Ref Expression
Assertion rlmval2 ⊢ W ∈ X → ringLMod ⁡ W = W sSet Scalar ⁡ ndx W sSet ⋅ ndx ⋅ W sSet ⋅ 𝑖 ⁡ ndx ⋅ W

Proof

Step Hyp Ref Expression
1 rlmval ⊢ ringLMod ⁡ W = subringAlg ⁡ W ⁡ Base W
2 1 a1i ⊢ W ∈ X → ringLMod ⁡ W = subringAlg ⁡ W ⁡ Base W
3 ssid ⊢ Base W ⊆ Base W
4 sraval ⊢ W ∈ X ∧ Base W ⊆ Base W → subringAlg ⁡ W ⁡ Base W = W sSet Scalar ⁡ ndx W ↾ 𝑠 Base W sSet ⋅ ndx ⋅ W sSet ⋅ 𝑖 ⁡ ndx ⋅ W
5 3 4 mpan2 ⊢ W ∈ X → subringAlg ⁡ W ⁡ Base W = W sSet Scalar ⁡ ndx W ↾ 𝑠 Base W sSet ⋅ ndx ⋅ W sSet ⋅ 𝑖 ⁡ ndx ⋅ W
6 eqid ⊢ Base W = Base W
7 6 ressid ⊢ W ∈ X → W ↾ 𝑠 Base W = W
8 7 opeq2d ⊢ W ∈ X → Scalar ⁡ ndx W ↾ 𝑠 Base W = Scalar ⁡ ndx W
9 8 oveq2d ⊢ W ∈ X → W sSet Scalar ⁡ ndx W ↾ 𝑠 Base W = W sSet Scalar ⁡ ndx W
10 9 oveq1d ⊢ W ∈ X → W sSet Scalar ⁡ ndx W ↾ 𝑠 Base W sSet ⋅ ndx ⋅ W = W sSet Scalar ⁡ ndx W sSet ⋅ ndx ⋅ W
11 10 oveq1d ⊢ W ∈ X → W sSet Scalar ⁡ ndx W ↾ 𝑠 Base W sSet ⋅ ndx ⋅ W sSet ⋅ 𝑖 ⁡ ndx ⋅ W = W sSet Scalar ⁡ ndx W sSet ⋅ ndx ⋅ W sSet ⋅ 𝑖 ⁡ ndx ⋅ W
12 2 5 11 3eqtrd ⊢ W ∈ X → ringLMod ⁡ W = W sSet Scalar ⁡ ndx W sSet ⋅ ndx ⋅ W sSet ⋅ 𝑖 ⁡ ndx ⋅ W