Metamath Proof Explorer


Theorem psrval

Description: Value of the multivariate power series structure. (Contributed by Mario Carneiro, 29-Dec-2014)

Ref Expression
Hypotheses psrval.s S = I mPwSer R
psrval.k K = Base R
psrval.a + ˙ = + R
psrval.m · ˙ = R
psrval.o O = TopOpen R
psrval.d D = h 0 I | h -1 Fin
psrval.b φ B = K D
psrval.p ˙ = f + ˙ B × B
psrval.t × ˙ = f B , g B k D R x y D | y f k f x · ˙ g k f x
psrval.v ˙ = x K , f B D × x · ˙ f f
psrval.j φ J = 𝑡 D × O
psrval.i φ I W
psrval.r φ R X
Assertion psrval φ S = Base ndx B + ndx ˙ ndx × ˙ Scalar ndx R ndx ˙ TopSet ndx J

Proof

Step Hyp Ref Expression
1 psrval.s S = I mPwSer R
2 psrval.k K = Base R
3 psrval.a + ˙ = + R
4 psrval.m · ˙ = R
5 psrval.o O = TopOpen R
6 psrval.d D = h 0 I | h -1 Fin
7 psrval.b φ B = K D
8 psrval.p ˙ = f + ˙ B × B
9 psrval.t × ˙ = f B , g B k D R x y D | y f k f x · ˙ g k f x
10 psrval.v ˙ = x K , f B D × x · ˙ f f
11 psrval.j φ J = 𝑡 D × O
12 psrval.i φ I W
13 psrval.r φ R X
14 df-psr mPwSer = i V , r V h 0 i | h -1 Fin / d Base r d / b Base ndx b + ndx f + r b × b ndx f b , g b k d r x y d | y f k f x r g k f x Scalar ndx r ndx x Base r , f b d × x r f f TopSet ndx 𝑡 d × TopOpen r
15 14 a1i φ mPwSer = i V , r V h 0 i | h -1 Fin / d Base r d / b Base ndx b + ndx f + r b × b ndx f b , g b k d r x y d | y f k f x r g k f x Scalar ndx r ndx x Base r , f b d × x r f f TopSet ndx 𝑡 d × TopOpen r
16 simprl φ i = I r = R i = I
17 16 oveq2d φ i = I r = R 0 i = 0 I
18 rabeq 0 i = 0 I h 0 i | h -1 Fin = h 0 I | h -1 Fin
19 17 18 syl φ i = I r = R h 0 i | h -1 Fin = h 0 I | h -1 Fin
20 19 6 eqtr4di φ i = I r = R h 0 i | h -1 Fin = D
21 20 csbeq1d φ i = I r = R h 0 i | h -1 Fin / d Base r d / b Base ndx b + ndx f + r b × b ndx f b , g b k d r x y d | y f k f x r g k f x Scalar ndx r ndx x Base r , f b d × x r f f TopSet ndx 𝑡 d × TopOpen r = D / d Base r d / b Base ndx b + ndx f + r b × b ndx f b , g b k d r x y d | y f k f x r g k f x Scalar ndx r ndx x Base r , f b d × x r f f TopSet ndx 𝑡 d × TopOpen r
22 ovex 0 i V
23 22 rabex h 0 i | h -1 Fin V
24 20 23 eqeltrrdi φ i = I r = R D V
25 simplrr φ i = I r = R d = D r = R
26 25 fveq2d φ i = I r = R d = D Base r = Base R
27 26 2 eqtr4di φ i = I r = R d = D Base r = K
28 simpr φ i = I r = R d = D d = D
29 27 28 oveq12d φ i = I r = R d = D Base r d = K D
30 7 ad2antrr φ i = I r = R d = D B = K D
31 29 30 eqtr4d φ i = I r = R d = D Base r d = B
32 31 csbeq1d φ i = I r = R d = D Base r d / b Base ndx b + ndx f + r b × b ndx f b , g b k d r x y d | y f k f x r g k f x Scalar ndx r ndx x Base r , f b d × x r f f TopSet ndx 𝑡 d × TopOpen r = B / b Base ndx b + ndx f + r b × b ndx f b , g b k d r x y d | y f k f x r g k f x Scalar ndx r ndx x Base r , f b d × x r f f TopSet ndx 𝑡 d × TopOpen r
33 ovex Base r d V
34 31 33 eqeltrrdi φ i = I r = R d = D B V
35 simpr φ i = I r = R d = D b = B b = B
36 35 opeq2d φ i = I r = R d = D b = B Base ndx b = Base ndx B
37 25 adantr φ i = I r = R d = D b = B r = R
38 37 fveq2d φ i = I r = R d = D b = B + r = + R
39 38 3 eqtr4di φ i = I r = R d = D b = B + r = + ˙
40 ofeq + r = + ˙ f + r = f + ˙
41 39 40 syl φ i = I r = R d = D b = B f + r = f + ˙
42 35 35 xpeq12d φ i = I r = R d = D b = B b × b = B × B
43 41 42 reseq12d φ i = I r = R d = D b = B f + r b × b = f + ˙ B × B
44 43 8 eqtr4di φ i = I r = R d = D b = B f + r b × b = ˙
45 44 opeq2d φ i = I r = R d = D b = B + ndx f + r b × b = + ndx ˙
46 28 adantr φ i = I r = R d = D b = B d = D
47 rabeq d = D y d | y f k = y D | y f k
48 46 47 syl φ i = I r = R d = D b = B y d | y f k = y D | y f k
49 37 fveq2d φ i = I r = R d = D b = B r = R
50 49 4 eqtr4di φ i = I r = R d = D b = B r = · ˙
51 50 oveqd φ i = I r = R d = D b = B f x r g k f x = f x · ˙ g k f x
52 48 51 mpteq12dv φ i = I r = R d = D b = B x y d | y f k f x r g k f x = x y D | y f k f x · ˙ g k f x
53 37 52 oveq12d φ i = I r = R d = D b = B r x y d | y f k f x r g k f x = R x y D | y f k f x · ˙ g k f x
54 46 53 mpteq12dv φ i = I r = R d = D b = B k d r x y d | y f k f x r g k f x = k D R x y D | y f k f x · ˙ g k f x
55 35 35 54 mpoeq123dv φ i = I r = R d = D b = B f b , g b k d r x y d | y f k f x r g k f x = f B , g B k D R x y D | y f k f x · ˙ g k f x
56 55 9 eqtr4di φ i = I r = R d = D b = B f b , g b k d r x y d | y f k f x r g k f x = × ˙
57 56 opeq2d φ i = I r = R d = D b = B ndx f b , g b k d r x y d | y f k f x r g k f x = ndx × ˙
58 36 45 57 tpeq123d φ i = I r = R d = D b = B Base ndx b + ndx f + r b × b ndx f b , g b k d r x y d | y f k f x r g k f x = Base ndx B + ndx ˙ ndx × ˙
59 37 opeq2d φ i = I r = R d = D b = B Scalar ndx r = Scalar ndx R
60 27 adantr φ i = I r = R d = D b = B Base r = K
61 ofeq r = · ˙ f r = f · ˙
62 50 61 syl φ i = I r = R d = D b = B f r = f · ˙
63 46 xpeq1d φ i = I r = R d = D b = B d × x = D × x
64 eqidd φ i = I r = R d = D b = B f = f
65 62 63 64 oveq123d φ i = I r = R d = D b = B d × x r f f = D × x · ˙ f f
66 60 35 65 mpoeq123dv φ i = I r = R d = D b = B x Base r , f b d × x r f f = x K , f B D × x · ˙ f f
67 66 10 eqtr4di φ i = I r = R d = D b = B x Base r , f b d × x r f f = ˙
68 67 opeq2d φ i = I r = R d = D b = B ndx x Base r , f b d × x r f f = ndx ˙
69 37 fveq2d φ i = I r = R d = D b = B TopOpen r = TopOpen R
70 69 5 eqtr4di φ i = I r = R d = D b = B TopOpen r = O
71 70 sneqd φ i = I r = R d = D b = B TopOpen r = O
72 46 71 xpeq12d φ i = I r = R d = D b = B d × TopOpen r = D × O
73 72 fveq2d φ i = I r = R d = D b = B 𝑡 d × TopOpen r = 𝑡 D × O
74 11 ad3antrrr φ i = I r = R d = D b = B J = 𝑡 D × O
75 73 74 eqtr4d φ i = I r = R d = D b = B 𝑡 d × TopOpen r = J
76 75 opeq2d φ i = I r = R d = D b = B TopSet ndx 𝑡 d × TopOpen r = TopSet ndx J
77 59 68 76 tpeq123d φ i = I r = R d = D b = B Scalar ndx r ndx x Base r , f b d × x r f f TopSet ndx 𝑡 d × TopOpen r = Scalar ndx R ndx ˙ TopSet ndx J
78 58 77 uneq12d φ i = I r = R d = D b = B Base ndx b + ndx f + r b × b ndx f b , g b k d r x y d | y f k f x r g k f x Scalar ndx r ndx x Base r , f b d × x r f f TopSet ndx 𝑡 d × TopOpen r = Base ndx B + ndx ˙ ndx × ˙ Scalar ndx R ndx ˙ TopSet ndx J
79 34 78 csbied φ i = I r = R d = D B / b Base ndx b + ndx f + r b × b ndx f b , g b k d r x y d | y f k f x r g k f x Scalar ndx r ndx x Base r , f b d × x r f f TopSet ndx 𝑡 d × TopOpen r = Base ndx B + ndx ˙ ndx × ˙ Scalar ndx R ndx ˙ TopSet ndx J
80 32 79 eqtrd φ i = I r = R d = D Base r d / b Base ndx b + ndx f + r b × b ndx f b , g b k d r x y d | y f k f x r g k f x Scalar ndx r ndx x Base r , f b d × x r f f TopSet ndx 𝑡 d × TopOpen r = Base ndx B + ndx ˙ ndx × ˙ Scalar ndx R ndx ˙ TopSet ndx J
81 24 80 csbied φ i = I r = R D / d Base r d / b Base ndx b + ndx f + r b × b ndx f b , g b k d r x y d | y f k f x r g k f x Scalar ndx r ndx x Base r , f b d × x r f f TopSet ndx 𝑡 d × TopOpen r = Base ndx B + ndx ˙ ndx × ˙ Scalar ndx R ndx ˙ TopSet ndx J
82 21 81 eqtrd φ i = I r = R h 0 i | h -1 Fin / d Base r d / b Base ndx b + ndx f + r b × b ndx f b , g b k d r x y d | y f k f x r g k f x Scalar ndx r ndx x Base r , f b d × x r f f TopSet ndx 𝑡 d × TopOpen r = Base ndx B + ndx ˙ ndx × ˙ Scalar ndx R ndx ˙ TopSet ndx J
83 12 elexd φ I V
84 13 elexd φ R V
85 tpex Base ndx B + ndx ˙ ndx × ˙ V
86 tpex Scalar ndx R ndx ˙ TopSet ndx J V
87 85 86 unex Base ndx B + ndx ˙ ndx × ˙ Scalar ndx R ndx ˙ TopSet ndx J V
88 87 a1i φ Base ndx B + ndx ˙ ndx × ˙ Scalar ndx R ndx ˙ TopSet ndx J V
89 15 82 83 84 88 ovmpod φ I mPwSer R = Base ndx B + ndx ˙ ndx × ˙ Scalar ndx R ndx ˙ TopSet ndx J
90 1 89 syl5eq φ S = Base ndx B + ndx ˙ ndx × ˙ Scalar ndx R ndx ˙ TopSet ndx J