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 ⊢ W ∈ V ∧ S ⊆ Base W → subringAlg ⁡ W ⁡ S = W sSet Scalar ⁡ ndx W ↾ 𝑠 S sSet ⋅ ndx ⋅ W sSet ⋅ 𝑖 ⁡ ndx ⋅ W

Proof

Step Hyp Ref Expression
1 elex ⊢ W ∈ V → W ∈ V
2 1 adantr ⊢ W ∈ V ∧ S ⊆ Base W → W ∈ V
3 fveq2 ⊢ w = W → Base w = Base W
4 3 pweqd ⊢ w = W → 𝒫 Base w = 𝒫 Base W
5 id ⊢ w = W → w = W
6 oveq1 ⊢ w = W → w ↾ 𝑠 s = W ↾ 𝑠 s
7 6 opeq2d ⊢ w = W → Scalar ⁡ ndx w ↾ 𝑠 s = Scalar ⁡ ndx W ↾ 𝑠 s
8 5 7 oveq12d ⊢ w = W → w sSet Scalar ⁡ ndx w ↾ 𝑠 s = W sSet Scalar ⁡ ndx W ↾ 𝑠 s
9 fveq2 ⊢ w = W → ⋅ w = ⋅ W
10 9 opeq2d ⊢ w = W → ⋅ ndx ⋅ w = ⋅ ndx ⋅ W
11 8 10 oveq12d ⊢ w = W → w sSet Scalar ⁡ ndx w ↾ 𝑠 s sSet ⋅ ndx ⋅ w = W sSet Scalar ⁡ ndx W ↾ 𝑠 s sSet ⋅ ndx ⋅ W
12 9 opeq2d ⊢ w = W → ⋅ 𝑖 ⁡ ndx ⋅ w = ⋅ 𝑖 ⁡ ndx ⋅ W
13 11 12 oveq12d ⊢ w = W → w sSet Scalar ⁡ ndx w ↾ 𝑠 s sSet ⋅ ndx ⋅ w sSet ⋅ 𝑖 ⁡ ndx ⋅ w = W sSet Scalar ⁡ ndx W ↾ 𝑠 s sSet ⋅ ndx ⋅ W sSet ⋅ 𝑖 ⁡ ndx ⋅ W
14 4 13 mpteq12dv ⊢ w = W → s ∈ 𝒫 Base w ⟼ w sSet Scalar ⁡ ndx w ↾ 𝑠 s sSet ⋅ ndx ⋅ w sSet ⋅ 𝑖 ⁡ ndx ⋅ w = s ∈ 𝒫 Base W ⟼ W sSet Scalar ⁡ ndx W ↾ 𝑠 s sSet ⋅ ndx ⋅ W sSet ⋅ 𝑖 ⁡ ndx ⋅ W
15 df-sra ⊢ subringAlg = w ∈ V ⟼ s ∈ 𝒫 Base w ⟼ w sSet Scalar ⁡ ndx w ↾ 𝑠 s sSet ⋅ ndx ⋅ w sSet ⋅ 𝑖 ⁡ ndx ⋅ w
16 fvex ⊢ Base W ∈ V
17 16 pwex ⊢ 𝒫 Base W ∈ V
18 17 mptex ⊢ s ∈ 𝒫 Base W ⟼ W sSet Scalar ⁡ ndx W ↾ 𝑠 s sSet ⋅ ndx ⋅ W sSet ⋅ 𝑖 ⁡ ndx ⋅ W ∈ V
19 14 15 18 fvmpt ⊢ W ∈ V → subringAlg ⁡ W = s ∈ 𝒫 Base W ⟼ W sSet Scalar ⁡ ndx W ↾ 𝑠 s sSet ⋅ ndx ⋅ W sSet ⋅ 𝑖 ⁡ ndx ⋅ W
20 2 19 syl ⊢ W ∈ V ∧ S ⊆ Base W → subringAlg ⁡ W = s ∈ 𝒫 Base W ⟼ W sSet Scalar ⁡ ndx W ↾ 𝑠 s sSet ⋅ ndx ⋅ W sSet ⋅ 𝑖 ⁡ ndx ⋅ W
21 simpr ⊢ W ∈ V ∧ S ⊆ Base W ∧ s = S → s = S
22 21 oveq2d ⊢ W ∈ V ∧ S ⊆ Base W ∧ s = S → W ↾ 𝑠 s = W ↾ 𝑠 S
23 22 opeq2d ⊢ W ∈ V ∧ S ⊆ Base W ∧ s = S → Scalar ⁡ ndx W ↾ 𝑠 s = Scalar ⁡ ndx W ↾ 𝑠 S
24 23 oveq2d ⊢ W ∈ V ∧ S ⊆ Base W ∧ s = S → W sSet Scalar ⁡ ndx W ↾ 𝑠 s = W sSet Scalar ⁡ ndx W ↾ 𝑠 S
25 24 oveq1d ⊢ W ∈ V ∧ S ⊆ Base W ∧ s = S → W sSet Scalar ⁡ ndx W ↾ 𝑠 s sSet ⋅ ndx ⋅ W = W sSet Scalar ⁡ ndx W ↾ 𝑠 S sSet ⋅ ndx ⋅ W
26 25 oveq1d ⊢ W ∈ V ∧ S ⊆ Base W ∧ s = S → W sSet Scalar ⁡ ndx W ↾ 𝑠 s sSet ⋅ ndx ⋅ W sSet ⋅ 𝑖 ⁡ ndx ⋅ W = W sSet Scalar ⁡ ndx W ↾ 𝑠 S sSet ⋅ ndx ⋅ W sSet ⋅ 𝑖 ⁡ ndx ⋅ W
27 16 elpw2 ⊢ S ∈ 𝒫 Base W ↔ S ⊆ Base W
28 27 bilanri ⊢ W ∈ V ∧ S ⊆ Base W → S ∈ 𝒫 Base W
29 ovexd ⊢ W ∈ V ∧ S ⊆ Base W → W sSet Scalar ⁡ ndx W ↾ 𝑠 S sSet ⋅ ndx ⋅ W sSet ⋅ 𝑖 ⁡ ndx ⋅ W ∈ V
30 20 26 28 29 fvmptd ⊢ W ∈ V ∧ S ⊆ Base W → subringAlg ⁡ W ⁡ S = W sSet Scalar ⁡ ndx W ↾ 𝑠 S sSet ⋅ ndx ⋅ W sSet ⋅ 𝑖 ⁡ ndx ⋅ W