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 ‘ 𝑊 ) ⟩ ) )