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⊆BaseW→subringAlg⁡W⁡S=WsSetScalar⁡ndxW↾𝑠SsSet⋅ndx⋅WsSet⋅𝑖⁡ndx⋅W

Proof

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