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 simpr W V S Base W S Base W
28 16 elpw2 S 𝒫 Base W S Base W
29 27 28 sylibr W V S Base W S 𝒫 Base W
30 ovexd W V S Base W W sSet Scalar ndx W 𝑠 S sSet ndx W sSet 𝑖 ndx W V
31 20 26 29 30 fvmptd W V S Base W subringAlg W S = W sSet Scalar ndx W 𝑠 S sSet ndx W sSet 𝑖 ndx W