Metamath Proof Explorer

Theorem sraval

Description: Lemma for srabase through sravsca . (Contributed by Mario Carneiro, 27-Nov-2014) (Revised by Thierry Arnoux, 16-Jun-2019)

Ref Expression
Assertion sraval ( ( 𝑊 ∈ 𝑉 ∧ 𝑆 ⊆ ( Base ‘ 𝑊 ) ) → ( ( subringAlg ‘ 𝑊 ) ‘ 𝑆 ) = ( ( ( 𝑊 sSet ⟨ ( Scalar ‘ ndx ) , ( 𝑊 ↾s 𝑆 ) ⟩ ) sSet ⟨ ( ·𝑠 ‘ ndx ) , ( .r ‘ 𝑊 ) ⟩ ) sSet ⟨ ( ·𝑖 ‘ ndx ) , ( .r ‘ 𝑊 ) ⟩ ) )

Proof

Step Hyp Ref Expression
1 elex ⊢ ( 𝑊 ∈ 𝑉 → 𝑊 ∈ V )
2 1 adantr ⊢ ( ( 𝑊 ∈ 𝑉 ∧ 𝑆 ⊆ ( Base ‘ 𝑊 ) ) → 𝑊 ∈ V )
3 fveq2 ⊢ ( 𝑤 = 𝑊 → ( Base ‘ 𝑤 ) = ( Base ‘ 𝑊 ) )
4 3 pweqd ⊢ ( 𝑤 = 𝑊 → 𝒫 ( Base ‘ 𝑤 ) = 𝒫 ( Base ‘ 𝑊 ) )
5 id ⊢ ( 𝑤 = 𝑊 → 𝑤 = 𝑊 )
6 oveq1 ⊢ ( 𝑤 = 𝑊 → ( 𝑤 ↾s 𝑠 ) = ( 𝑊 ↾s 𝑠 ) )
7 6 opeq2d ⊢ ( 𝑤 = 𝑊 → ⟨ ( Scalar ‘ ndx ) , ( 𝑤 ↾s 𝑠 ) ⟩ = ⟨ ( Scalar ‘ ndx ) , ( 𝑊 ↾s 𝑠 ) ⟩ )
8 5 7 oveq12d ⊢ ( 𝑤 = 𝑊 → ( 𝑤 sSet ⟨ ( Scalar ‘ ndx ) , ( 𝑤 ↾s 𝑠 ) ⟩ ) = ( 𝑊 sSet ⟨ ( Scalar ‘ ndx ) , ( 𝑊 ↾s 𝑠 ) ⟩ ) )
9 fveq2 ⊢ ( 𝑤 = 𝑊 → ( .r ‘ 𝑤 ) = ( .r ‘ 𝑊 ) )
10 9 opeq2d ⊢ ( 𝑤 = 𝑊 → ⟨ ( ·𝑠 ‘ ndx ) , ( .r ‘ 𝑤 ) ⟩ = ⟨ ( ·𝑠 ‘ ndx ) , ( .r ‘ 𝑊 ) ⟩ )
11 8 10 oveq12d ⊢ ( 𝑤 = 𝑊 → ( ( 𝑤 sSet ⟨ ( Scalar ‘ ndx ) , ( 𝑤 ↾s 𝑠 ) ⟩ ) sSet ⟨ ( ·𝑠 ‘ ndx ) , ( .r ‘ 𝑤 ) ⟩ ) = ( ( 𝑊 sSet ⟨ ( Scalar ‘ ndx ) , ( 𝑊 ↾s 𝑠 ) ⟩ ) sSet ⟨ ( ·𝑠 ‘ ndx ) , ( .r ‘ 𝑊 ) ⟩ ) )
12 9 opeq2d ⊢ ( 𝑤 = 𝑊 → ⟨ ( ·𝑖 ‘ ndx ) , ( .r ‘ 𝑤 ) ⟩ = ⟨ ( ·𝑖 ‘ ndx ) , ( .r ‘ 𝑊 ) ⟩ )
13 11 12 oveq12d ⊢ ( 𝑤 = 𝑊 → ( ( ( 𝑤 sSet ⟨ ( Scalar ‘ ndx ) , ( 𝑤 ↾s 𝑠 ) ⟩ ) sSet ⟨ ( ·𝑠 ‘ ndx ) , ( .r ‘ 𝑤 ) ⟩ ) sSet ⟨ ( ·𝑖 ‘ ndx ) , ( .r ‘ 𝑤 ) ⟩ ) = ( ( ( 𝑊 sSet ⟨ ( Scalar ‘ ndx ) , ( 𝑊 ↾s 𝑠 ) ⟩ ) sSet ⟨ ( ·𝑠 ‘ ndx ) , ( .r ‘ 𝑊 ) ⟩ ) sSet ⟨ ( ·𝑖 ‘ ndx ) , ( .r ‘ 𝑊 ) ⟩ ) )
14 4 13 mpteq12dv ⊢ ( 𝑤 = 𝑊 → ( 𝑠 ∈ 𝒫 ( Base ‘ 𝑤 ) ↦ ( ( ( 𝑤 sSet ⟨ ( Scalar ‘ ndx ) , ( 𝑤 ↾s 𝑠 ) ⟩ ) sSet ⟨ ( ·𝑠 ‘ ndx ) , ( .r ‘ 𝑤 ) ⟩ ) sSet ⟨ ( ·𝑖 ‘ ndx ) , ( .r ‘ 𝑤 ) ⟩ ) ) = ( 𝑠 ∈ 𝒫 ( Base ‘ 𝑊 ) ↦ ( ( ( 𝑊 sSet ⟨ ( Scalar ‘ ndx ) , ( 𝑊 ↾s 𝑠 ) ⟩ ) sSet ⟨ ( ·𝑠 ‘ ndx ) , ( .r ‘ 𝑊 ) ⟩ ) sSet ⟨ ( ·𝑖 ‘ ndx ) , ( .r ‘ 𝑊 ) ⟩ ) ) )
15 df-sra ⊢ subringAlg = ( 𝑤 ∈ V ↦ ( 𝑠 ∈ 𝒫 ( Base ‘ 𝑤 ) ↦ ( ( ( 𝑤 sSet ⟨ ( Scalar ‘ ndx ) , ( 𝑤 ↾s 𝑠 ) ⟩ ) sSet ⟨ ( ·𝑠 ‘ ndx ) , ( .r ‘ 𝑤 ) ⟩ ) sSet ⟨ ( ·𝑖 ‘ ndx ) , ( .r ‘ 𝑤 ) ⟩ ) ) )
16 fvex ⊢ ( Base ‘ 𝑊 ) ∈ V
17 16 pwex ⊢ 𝒫 ( Base ‘ 𝑊 ) ∈ V
18 17 mptex ⊢ ( 𝑠 ∈ 𝒫 ( Base ‘ 𝑊 ) ↦ ( ( ( 𝑊 sSet ⟨ ( Scalar ‘ ndx ) , ( 𝑊 ↾s 𝑠 ) ⟩ ) sSet ⟨ ( ·𝑠 ‘ ndx ) , ( .r ‘ 𝑊 ) ⟩ ) sSet ⟨ ( ·𝑖 ‘ ndx ) , ( .r ‘ 𝑊 ) ⟩ ) ) ∈ V
19 14 15 18 fvmpt ⊢ ( 𝑊 ∈ V → ( subringAlg ‘ 𝑊 ) = ( 𝑠 ∈ 𝒫 ( Base ‘ 𝑊 ) ↦ ( ( ( 𝑊 sSet ⟨ ( Scalar ‘ ndx ) , ( 𝑊 ↾s 𝑠 ) ⟩ ) sSet ⟨ ( ·𝑠 ‘ ndx ) , ( .r ‘ 𝑊 ) ⟩ ) sSet ⟨ ( ·𝑖 ‘ ndx ) , ( .r ‘ 𝑊 ) ⟩ ) ) )
20 2 19 syl ⊢ ( ( 𝑊 ∈ 𝑉 ∧ 𝑆 ⊆ ( Base ‘ 𝑊 ) ) → ( subringAlg ‘ 𝑊 ) = ( 𝑠 ∈ 𝒫 ( Base ‘ 𝑊 ) ↦ ( ( ( 𝑊 sSet ⟨ ( Scalar ‘ ndx ) , ( 𝑊 ↾s 𝑠 ) ⟩ ) sSet ⟨ ( ·𝑠 ‘ ndx ) , ( .r ‘ 𝑊 ) ⟩ ) sSet ⟨ ( ·𝑖 ‘ ndx ) , ( .r ‘ 𝑊 ) ⟩ ) ) )
21 simpr ⊢ ( ( ( 𝑊 ∈ 𝑉 ∧ 𝑆 ⊆ ( Base ‘ 𝑊 ) ) ∧ 𝑠 = 𝑆 ) → 𝑠 = 𝑆 )
22 21 oveq2d ⊢ ( ( ( 𝑊 ∈ 𝑉 ∧ 𝑆 ⊆ ( Base ‘ 𝑊 ) ) ∧ 𝑠 = 𝑆 ) → ( 𝑊 ↾s 𝑠 ) = ( 𝑊 ↾s 𝑆 ) )
23 22 opeq2d ⊢ ( ( ( 𝑊 ∈ 𝑉 ∧ 𝑆 ⊆ ( Base ‘ 𝑊 ) ) ∧ 𝑠 = 𝑆 ) → ⟨ ( Scalar ‘ ndx ) , ( 𝑊 ↾s 𝑠 ) ⟩ = ⟨ ( Scalar ‘ ndx ) , ( 𝑊 ↾s 𝑆 ) ⟩ )
24 23 oveq2d ⊢ ( ( ( 𝑊 ∈ 𝑉 ∧ 𝑆 ⊆ ( Base ‘ 𝑊 ) ) ∧ 𝑠 = 𝑆 ) → ( 𝑊 sSet ⟨ ( Scalar ‘ ndx ) , ( 𝑊 ↾s 𝑠 ) ⟩ ) = ( 𝑊 sSet ⟨ ( Scalar ‘ ndx ) , ( 𝑊 ↾s 𝑆 ) ⟩ ) )
25 24 oveq1d ⊢ ( ( ( 𝑊 ∈ 𝑉 ∧ 𝑆 ⊆ ( Base ‘ 𝑊 ) ) ∧ 𝑠 = 𝑆 ) → ( ( 𝑊 sSet ⟨ ( Scalar ‘ ndx ) , ( 𝑊 ↾s 𝑠 ) ⟩ ) sSet ⟨ ( ·𝑠 ‘ ndx ) , ( .r ‘ 𝑊 ) ⟩ ) = ( ( 𝑊 sSet ⟨ ( Scalar ‘ ndx ) , ( 𝑊 ↾s 𝑆 ) ⟩ ) sSet ⟨ ( ·𝑠 ‘ ndx ) , ( .r ‘ 𝑊 ) ⟩ ) )
26 25 oveq1d ⊢ ( ( ( 𝑊 ∈ 𝑉 ∧ 𝑆 ⊆ ( Base ‘ 𝑊 ) ) ∧ 𝑠 = 𝑆 ) → ( ( ( 𝑊 sSet ⟨ ( Scalar ‘ ndx ) , ( 𝑊 ↾s 𝑠 ) ⟩ ) sSet ⟨ ( ·𝑠 ‘ ndx ) , ( .r ‘ 𝑊 ) ⟩ ) sSet ⟨ ( ·𝑖 ‘ ndx ) , ( .r ‘ 𝑊 ) ⟩ ) = ( ( ( 𝑊 sSet ⟨ ( Scalar ‘ ndx ) , ( 𝑊 ↾s 𝑆 ) ⟩ ) sSet ⟨ ( ·𝑠 ‘ ndx ) , ( .r ‘ 𝑊 ) ⟩ ) sSet ⟨ ( ·𝑖 ‘ ndx ) , ( .r ‘ 𝑊 ) ⟩ ) )
27 16 elpw2 ⊢ ( 𝑆 ∈ 𝒫 ( Base ‘ 𝑊 ) ↔ 𝑆 ⊆ ( Base ‘ 𝑊 ) )
28 27 bilanri ⊢ ( ( 𝑊 ∈ 𝑉 ∧ 𝑆 ⊆ ( Base ‘ 𝑊 ) ) → 𝑆 ∈ 𝒫 ( Base ‘ 𝑊 ) )
29 ovexd ⊢ ( ( 𝑊 ∈ 𝑉 ∧ 𝑆 ⊆ ( Base ‘ 𝑊 ) ) → ( ( ( 𝑊 sSet ⟨ ( Scalar ‘ ndx ) , ( 𝑊 ↾s 𝑆 ) ⟩ ) sSet ⟨ ( ·𝑠 ‘ ndx ) , ( .r ‘ 𝑊 ) ⟩ ) sSet ⟨ ( ·𝑖 ‘ ndx ) , ( .r ‘ 𝑊 ) ⟩ ) ∈ V )
30 20 26 28 29 fvmptd ⊢ ( ( 𝑊 ∈ 𝑉 ∧ 𝑆 ⊆ ( Base ‘ 𝑊 ) ) → ( ( subringAlg ‘ 𝑊 ) ‘ 𝑆 ) = ( ( ( 𝑊 sSet ⟨ ( Scalar ‘ ndx ) , ( 𝑊 ↾s 𝑆 ) ⟩ ) sSet ⟨ ( ·𝑠 ‘ ndx ) , ( .r ‘ 𝑊 ) ⟩ ) sSet ⟨ ( ·𝑖 ‘ ndx ) , ( .r ‘ 𝑊 ) ⟩ ) )