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 ( 𝑊 ∈ 𝑋 → ( ringLMod ‘ 𝑊 ) = ( ( ( 𝑊 sSet ⟨ ( Scalar ‘ ndx ) , 𝑊 ⟩ ) sSet ⟨ ( ·𝑠 ‘ ndx ) , ( .r ‘ 𝑊 ) ⟩ ) sSet ⟨ ( ·𝑖 ‘ ndx ) , ( .r ‘ 𝑊 ) ⟩ ) )

Proof

Step Hyp Ref Expression
1 rlmval ⊢ ( ringLMod ‘ 𝑊 ) = ( ( subringAlg ‘ 𝑊 ) ‘ ( Base ‘ 𝑊 ) )
2 1 a1i ⊢ ( 𝑊 ∈ 𝑋 → ( ringLMod ‘ 𝑊 ) = ( ( subringAlg ‘ 𝑊 ) ‘ ( Base ‘ 𝑊 ) ) )
3 ssid ⊢ ( Base ‘ 𝑊 ) ⊆ ( Base ‘ 𝑊 )
4 sraval ⊢ ( ( 𝑊 ∈ 𝑋 ∧ ( Base ‘ 𝑊 ) ⊆ ( Base ‘ 𝑊 ) ) → ( ( subringAlg ‘ 𝑊 ) ‘ ( Base ‘ 𝑊 ) ) = ( ( ( 𝑊 sSet ⟨ ( Scalar ‘ ndx ) , ( 𝑊 ↾s ( Base ‘ 𝑊 ) ) ⟩ ) sSet ⟨ ( ·𝑠 ‘ ndx ) , ( .r ‘ 𝑊 ) ⟩ ) sSet ⟨ ( ·𝑖 ‘ ndx ) , ( .r ‘ 𝑊 ) ⟩ ) )
5 3 4 mpan2 ⊢ ( 𝑊 ∈ 𝑋 → ( ( subringAlg ‘ 𝑊 ) ‘ ( Base ‘ 𝑊 ) ) = ( ( ( 𝑊 sSet ⟨ ( Scalar ‘ ndx ) , ( 𝑊 ↾s ( Base ‘ 𝑊 ) ) ⟩ ) sSet ⟨ ( ·𝑠 ‘ ndx ) , ( .r ‘ 𝑊 ) ⟩ ) sSet ⟨ ( ·𝑖 ‘ ndx ) , ( .r ‘ 𝑊 ) ⟩ ) )
6 eqid ⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
7 6 ressid ⊢ ( 𝑊 ∈ 𝑋 → ( 𝑊 ↾s ( Base ‘ 𝑊 ) ) = 𝑊 )
8 7 opeq2d ⊢ ( 𝑊 ∈ 𝑋 → ⟨ ( Scalar ‘ ndx ) , ( 𝑊 ↾s ( Base ‘ 𝑊 ) ) ⟩ = ⟨ ( Scalar ‘ ndx ) , 𝑊 ⟩ )
9 8 oveq2d ⊢ ( 𝑊 ∈ 𝑋 → ( 𝑊 sSet ⟨ ( Scalar ‘ ndx ) , ( 𝑊 ↾s ( Base ‘ 𝑊 ) ) ⟩ ) = ( 𝑊 sSet ⟨ ( Scalar ‘ ndx ) , 𝑊 ⟩ ) )
10 9 oveq1d ⊢ ( 𝑊 ∈ 𝑋 → ( ( 𝑊 sSet ⟨ ( Scalar ‘ ndx ) , ( 𝑊 ↾s ( Base ‘ 𝑊 ) ) ⟩ ) sSet ⟨ ( ·𝑠 ‘ ndx ) , ( .r ‘ 𝑊 ) ⟩ ) = ( ( 𝑊 sSet ⟨ ( Scalar ‘ ndx ) , 𝑊 ⟩ ) sSet ⟨ ( ·𝑠 ‘ ndx ) , ( .r ‘ 𝑊 ) ⟩ ) )
11 10 oveq1d ⊢ ( 𝑊 ∈ 𝑋 → ( ( ( 𝑊 sSet ⟨ ( Scalar ‘ ndx ) , ( 𝑊 ↾s ( Base ‘ 𝑊 ) ) ⟩ ) sSet ⟨ ( ·𝑠 ‘ ndx ) , ( .r ‘ 𝑊 ) ⟩ ) sSet ⟨ ( ·𝑖 ‘ ndx ) , ( .r ‘ 𝑊 ) ⟩ ) = ( ( ( 𝑊 sSet ⟨ ( Scalar ‘ ndx ) , 𝑊 ⟩ ) sSet ⟨ ( ·𝑠 ‘ ndx ) , ( .r ‘ 𝑊 ) ⟩ ) sSet ⟨ ( ·𝑖 ‘ ndx ) , ( .r ‘ 𝑊 ) ⟩ ) )
12 2 5 11 3eqtrd ⊢ ( 𝑊 ∈ 𝑋 → ( ringLMod ‘ 𝑊 ) = ( ( ( 𝑊 sSet ⟨ ( Scalar ‘ ndx ) , 𝑊 ⟩ ) sSet ⟨ ( ·𝑠 ‘ ndx ) , ( .r ‘ 𝑊 ) ⟩ ) sSet ⟨ ( ·𝑖 ‘ ndx ) , ( .r ‘ 𝑊 ) ⟩ ) )