Metamath Proof Explorer


Theorem psrsca

Description: The scalar field of the multivariate power series structure. (Contributed by Mario Carneiro, 28-Dec-2014)

Ref Expression
Hypotheses psrsca.s S = I mPwSer R
psrsca.i φ I V
psrsca.r φ R W
Assertion psrsca φ R = Scalar S

Proof

Step Hyp Ref Expression
1 psrsca.s S = I mPwSer R
2 psrsca.i φ I V
3 psrsca.r φ R W
4 psrvalstr Base ndx Base S + ndx + S ndx S Scalar ndx R ndx x Base R , f Base S h 0 I | h -1 Fin × x R f f TopSet ndx 𝑡 h 0 I | h -1 Fin × TopOpen R Struct 1 9
5 scaid Scalar = Slot Scalar ndx
6 snsstp1 Scalar ndx R Scalar ndx R ndx x Base R , f Base S h 0 I | h -1 Fin × x R f f TopSet ndx 𝑡 h 0 I | h -1 Fin × TopOpen R
7 ssun2 Scalar ndx R ndx x Base R , f Base S h 0 I | h -1 Fin × x R f f TopSet ndx 𝑡 h 0 I | h -1 Fin × TopOpen R Base ndx Base S + ndx + S ndx S Scalar ndx R ndx x Base R , f Base S h 0 I | h -1 Fin × x R f f TopSet ndx 𝑡 h 0 I | h -1 Fin × TopOpen R
8 6 7 sstri Scalar ndx R Base ndx Base S + ndx + S ndx S Scalar ndx R ndx x Base R , f Base S h 0 I | h -1 Fin × x R f f TopSet ndx 𝑡 h 0 I | h -1 Fin × TopOpen R
9 4 5 8 strfv R W R = Scalar Base ndx Base S + ndx + S ndx S Scalar ndx R ndx x Base R , f Base S h 0 I | h -1 Fin × x R f f TopSet ndx 𝑡 h 0 I | h -1 Fin × TopOpen R
10 3 9 syl φ R = Scalar Base ndx Base S + ndx + S ndx S Scalar ndx R ndx x Base R , f Base S h 0 I | h -1 Fin × x R f f TopSet ndx 𝑡 h 0 I | h -1 Fin × TopOpen R
11 eqid Base R = Base R
12 eqid + R = + R
13 eqid R = R
14 eqid TopOpen R = TopOpen R
15 eqid h 0 I | h -1 Fin = h 0 I | h -1 Fin
16 eqid Base S = Base S
17 1 11 15 16 2 psrbas φ Base S = Base R h 0 I | h -1 Fin
18 eqid + S = + S
19 1 16 12 18 psrplusg + S = f + R Base S × Base S
20 eqid S = S
21 1 16 13 20 15 psrmulr S = f Base S , z Base S w h 0 I | h -1 Fin R x y h 0 I | h -1 Fin | y f w f x R z w f x
22 eqid x Base R , f Base S h 0 I | h -1 Fin × x R f f = x Base R , f Base S h 0 I | h -1 Fin × x R f f
23 eqidd φ 𝑡 h 0 I | h -1 Fin × TopOpen R = 𝑡 h 0 I | h -1 Fin × TopOpen R
24 1 11 12 13 14 15 17 19 21 22 23 2 3 psrval φ S = Base ndx Base S + ndx + S ndx S Scalar ndx R ndx x Base R , f Base S h 0 I | h -1 Fin × x R f f TopSet ndx 𝑡 h 0 I | h -1 Fin × TopOpen R
25 24 fveq2d φ Scalar S = Scalar Base ndx Base S + ndx + S ndx S Scalar ndx R ndx x Base R , f Base S h 0 I | h -1 Fin × x R f f TopSet ndx 𝑡 h 0 I | h -1 Fin × TopOpen R
26 10 25 eqtr4d φ R = Scalar S