Metamath Proof Explorer


Theorem opsrle

Description: An alternative expression for the set of polynomials, as the smallest subalgebra of the set of power series that contains all the variable generators. (Contributed by Mario Carneiro, 8-Feb-2015) (Revised by Mario Carneiro, 2-Oct-2015)

Ref Expression
Hypotheses opsrle.s S = I mPwSer R
opsrle.o O = I ordPwSer R T
opsrle.b B = Base S
opsrle.q < ˙ = < R
opsrle.c C = T < bag I
opsrle.d D = h 0 I | h -1 Fin
opsrle.l ˙ = O
opsrle.t φ T I × I
Assertion opsrle φ ˙ = x y | x y B z D x z < ˙ y z w D w C z x w = y w x = y

Proof

Step Hyp Ref Expression
1 opsrle.s S = I mPwSer R
2 opsrle.o O = I ordPwSer R T
3 opsrle.b B = Base S
4 opsrle.q < ˙ = < R
5 opsrle.c C = T < bag I
6 opsrle.d D = h 0 I | h -1 Fin
7 opsrle.l ˙ = O
8 opsrle.t φ T I × I
9 eqid x y | x y B z D x z < ˙ y z w D w C z x w = y w x = y = x y | x y B z D x z < ˙ y z w D w C z x w = y w x = y
10 simprl φ I V R V I V
11 simprr φ I V R V R V
12 8 adantr φ I V R V T I × I
13 1 2 3 4 5 6 9 10 11 12 opsrval φ I V R V O = S sSet ndx x y | x y B z D x z < ˙ y z w D w C z x w = y w x = y
14 13 fveq2d φ I V R V O = S sSet ndx x y | x y B z D x z < ˙ y z w D w C z x w = y w x = y
15 1 ovexi S V
16 3 fvexi B V
17 16 16 xpex B × B V
18 vex x V
19 vex y V
20 18 19 prss x B y B x y B
21 20 anbi1i x B y B z D x z < ˙ y z w D w C z x w = y w x = y x y B z D x z < ˙ y z w D w C z x w = y w x = y
22 21 opabbii x y | x B y B z D x z < ˙ y z w D w C z x w = y w x = y = x y | x y B z D x z < ˙ y z w D w C z x w = y w x = y
23 opabssxp x y | x B y B z D x z < ˙ y z w D w C z x w = y w x = y B × B
24 22 23 eqsstrri x y | x y B z D x z < ˙ y z w D w C z x w = y w x = y B × B
25 17 24 ssexi x y | x y B z D x z < ˙ y z w D w C z x w = y w x = y V
26 pleid le = Slot ndx
27 26 setsid S V x y | x y B z D x z < ˙ y z w D w C z x w = y w x = y V x y | x y B z D x z < ˙ y z w D w C z x w = y w x = y = S sSet ndx x y | x y B z D x z < ˙ y z w D w C z x w = y w x = y
28 15 25 27 mp2an x y | x y B z D x z < ˙ y z w D w C z x w = y w x = y = S sSet ndx x y | x y B z D x z < ˙ y z w D w C z x w = y w x = y
29 14 7 28 3eqtr4g φ I V R V ˙ = x y | x y B z D x z < ˙ y z w D w C z x w = y w x = y
30 reldmopsr Rel dom ordPwSer
31 30 ovprc ¬ I V R V I ordPwSer R =
32 31 adantl φ ¬ I V R V I ordPwSer R =
33 32 fveq1d φ ¬ I V R V I ordPwSer R T = T
34 2 33 eqtrid φ ¬ I V R V O = T
35 0fv T =
36 34 35 eqtrdi φ ¬ I V R V O =
37 36 fveq2d φ ¬ I V R V O =
38 26 str0 =
39 37 7 38 3eqtr4g φ ¬ I V R V ˙ =
40 reldmpsr Rel dom mPwSer
41 40 ovprc ¬ I V R V I mPwSer R =
42 41 adantl φ ¬ I V R V I mPwSer R =
43 1 42 eqtrid φ ¬ I V R V S =
44 43 fveq2d φ ¬ I V R V Base S = Base
45 base0 = Base
46 44 3 45 3eqtr4g φ ¬ I V R V B =
47 46 xpeq2d φ ¬ I V R V B × B = B ×
48 xp0 B × =
49 47 48 eqtrdi φ ¬ I V R V B × B =
50 sseq0 x y | x y B z D x z < ˙ y z w D w C z x w = y w x = y B × B B × B = x y | x y B z D x z < ˙ y z w D w C z x w = y w x = y =
51 24 49 50 sylancr φ ¬ I V R V x y | x y B z D x z < ˙ y z w D w C z x w = y w x = y =
52 39 51 eqtr4d φ ¬ I V R V ˙ = x y | x y B z D x z < ˙ y z w D w C z x w = y w x = y
53 29 52 pm2.61dan φ ˙ = x y | x y B z D x z < ˙ y z w D w C z x w = y w x = y