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 
|- .< = ( lt ` R )
opsrle.c 
|- C = ( T
opsrle.d 
|- D = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin }
opsrle.l 
|- .<_ = ( le ` O )
opsrle.t 
|- ( ph -> T C_ ( I X. I ) )
Assertion opsrle 
|- ( ph -> .<_ = { <. x , y >. | ( { x , y } C_ B /\ ( E. z e. D ( ( x ` z ) .< ( y ` z ) /\ A. w e. 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 
 |-  .< = ( lt ` R )
5 opsrle.c 
 |-  C = ( T
6 opsrle.d 
 |-  D = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin }
7 opsrle.l 
 |-  .<_ = ( le ` O )
8 opsrle.t 
 |-  ( ph -> T C_ ( I X. I ) )
9 eqid 
 |-  { <. x , y >. | ( { x , y } C_ B /\ ( E. z e. D ( ( x ` z ) .< ( y ` z ) /\ A. w e. D ( w C z -> ( x ` w ) = ( y ` w ) ) ) \/ x = y ) ) } = { <. x , y >. | ( { x , y } C_ B /\ ( E. z e. D ( ( x ` z ) .< ( y ` z ) /\ A. w e. D ( w C z -> ( x ` w ) = ( y ` w ) ) ) \/ x = y ) ) }
10 simprl 
 |-  ( ( ph /\ ( I e. _V /\ R e. _V ) ) -> I e. _V )
11 simprr 
 |-  ( ( ph /\ ( I e. _V /\ R e. _V ) ) -> R e. _V )
12 8 adantr 
 |-  ( ( ph /\ ( I e. _V /\ R e. _V ) ) -> T C_ ( I X. I ) )
13 1 2 3 4 5 6 9 10 11 12 opsrval 
 |-  ( ( ph /\ ( I e. _V /\ R e. _V ) ) -> O = ( S sSet <. ( le ` ndx ) , { <. x , y >. | ( { x , y } C_ B /\ ( E. z e. D ( ( x ` z ) .< ( y ` z ) /\ A. w e. D ( w C z -> ( x ` w ) = ( y ` w ) ) ) \/ x = y ) ) } >. ) )
14 13 fveq2d 
 |-  ( ( ph /\ ( I e. _V /\ R e. _V ) ) -> ( le ` O ) = ( le ` ( S sSet <. ( le ` ndx ) , { <. x , y >. | ( { x , y } C_ B /\ ( E. z e. D ( ( x ` z ) .< ( y ` z ) /\ A. w e. D ( w C z -> ( x ` w ) = ( y ` w ) ) ) \/ x = y ) ) } >. ) ) )
15 1 ovexi 
 |-  S e. _V
16 3 fvexi 
 |-  B e. _V
17 16 16 xpex 
 |-  ( B X. B ) e. _V
18 vex 
 |-  x e. _V
19 vex 
 |-  y e. _V
20 18 19 prss 
 |-  ( ( x e. B /\ y e. B ) <-> { x , y } C_ B )
21 20 anbi1i 
 |-  ( ( ( x e. B /\ y e. B ) /\ ( E. z e. D ( ( x ` z ) .< ( y ` z ) /\ A. w e. D ( w C z -> ( x ` w ) = ( y ` w ) ) ) \/ x = y ) ) <-> ( { x , y } C_ B /\ ( E. z e. D ( ( x ` z ) .< ( y ` z ) /\ A. w e. D ( w C z -> ( x ` w ) = ( y ` w ) ) ) \/ x = y ) ) )
22 21 opabbii 
 |-  { <. x , y >. | ( ( x e. B /\ y e. B ) /\ ( E. z e. D ( ( x ` z ) .< ( y ` z ) /\ A. w e. D ( w C z -> ( x ` w ) = ( y ` w ) ) ) \/ x = y ) ) } = { <. x , y >. | ( { x , y } C_ B /\ ( E. z e. D ( ( x ` z ) .< ( y ` z ) /\ A. w e. D ( w C z -> ( x ` w ) = ( y ` w ) ) ) \/ x = y ) ) }
23 opabssxp 
 |-  { <. x , y >. | ( ( x e. B /\ y e. B ) /\ ( E. z e. D ( ( x ` z ) .< ( y ` z ) /\ A. w e. D ( w C z -> ( x ` w ) = ( y ` w ) ) ) \/ x = y ) ) } C_ ( B X. B )
24 22 23 eqsstrri 
 |-  { <. x , y >. | ( { x , y } C_ B /\ ( E. z e. D ( ( x ` z ) .< ( y ` z ) /\ A. w e. D ( w C z -> ( x ` w ) = ( y ` w ) ) ) \/ x = y ) ) } C_ ( B X. B )
25 17 24 ssexi 
 |-  { <. x , y >. | ( { x , y } C_ B /\ ( E. z e. D ( ( x ` z ) .< ( y ` z ) /\ A. w e. D ( w C z -> ( x ` w ) = ( y ` w ) ) ) \/ x = y ) ) } e. _V
26 pleid 
 |-  le = Slot ( le ` ndx )
27 26 setsid 
 |-  ( ( S e. _V /\ { <. x , y >. | ( { x , y } C_ B /\ ( E. z e. D ( ( x ` z ) .< ( y ` z ) /\ A. w e. D ( w C z -> ( x ` w ) = ( y ` w ) ) ) \/ x = y ) ) } e. _V ) -> { <. x , y >. | ( { x , y } C_ B /\ ( E. z e. D ( ( x ` z ) .< ( y ` z ) /\ A. w e. D ( w C z -> ( x ` w ) = ( y ` w ) ) ) \/ x = y ) ) } = ( le ` ( S sSet <. ( le ` ndx ) , { <. x , y >. | ( { x , y } C_ B /\ ( E. z e. D ( ( x ` z ) .< ( y ` z ) /\ A. w e. D ( w C z -> ( x ` w ) = ( y ` w ) ) ) \/ x = y ) ) } >. ) ) )
28 15 25 27 mp2an 
 |-  { <. x , y >. | ( { x , y } C_ B /\ ( E. z e. D ( ( x ` z ) .< ( y ` z ) /\ A. w e. D ( w C z -> ( x ` w ) = ( y ` w ) ) ) \/ x = y ) ) } = ( le ` ( S sSet <. ( le ` ndx ) , { <. x , y >. | ( { x , y } C_ B /\ ( E. z e. D ( ( x ` z ) .< ( y ` z ) /\ A. w e. D ( w C z -> ( x ` w ) = ( y ` w ) ) ) \/ x = y ) ) } >. ) )
29 14 7 28 3eqtr4g 
 |-  ( ( ph /\ ( I e. _V /\ R e. _V ) ) -> .<_ = { <. x , y >. | ( { x , y } C_ B /\ ( E. z e. D ( ( x ` z ) .< ( y ` z ) /\ A. w e. D ( w C z -> ( x ` w ) = ( y ` w ) ) ) \/ x = y ) ) } )
30 reldmopsr 
 |-  Rel dom ordPwSer
31 30 ovprc 
 |-  ( -. ( I e. _V /\ R e. _V ) -> ( I ordPwSer R ) = (/) )
32 31 adantl 
 |-  ( ( ph /\ -. ( I e. _V /\ R e. _V ) ) -> ( I ordPwSer R ) = (/) )
33 32 fveq1d 
 |-  ( ( ph /\ -. ( I e. _V /\ R e. _V ) ) -> ( ( I ordPwSer R ) ` T ) = ( (/) ` T ) )
34 2 33 syl5eq 
 |-  ( ( ph /\ -. ( I e. _V /\ R e. _V ) ) -> O = ( (/) ` T ) )
35 0fv 
 |-  ( (/) ` T ) = (/)
36 34 35 eqtrdi 
 |-  ( ( ph /\ -. ( I e. _V /\ R e. _V ) ) -> O = (/) )
37 36 fveq2d 
 |-  ( ( ph /\ -. ( I e. _V /\ R e. _V ) ) -> ( le ` O ) = ( le ` (/) ) )
38 26 str0 
 |-  (/) = ( le ` (/) )
39 37 7 38 3eqtr4g 
 |-  ( ( ph /\ -. ( I e. _V /\ R e. _V ) ) -> .<_ = (/) )
40 reldmpsr 
 |-  Rel dom mPwSer
41 40 ovprc 
 |-  ( -. ( I e. _V /\ R e. _V ) -> ( I mPwSer R ) = (/) )
42 41 adantl 
 |-  ( ( ph /\ -. ( I e. _V /\ R e. _V ) ) -> ( I mPwSer R ) = (/) )
43 1 42 syl5eq 
 |-  ( ( ph /\ -. ( I e. _V /\ R e. _V ) ) -> S = (/) )
44 43 fveq2d 
 |-  ( ( ph /\ -. ( I e. _V /\ R e. _V ) ) -> ( Base ` S ) = ( Base ` (/) ) )
45 base0 
 |-  (/) = ( Base ` (/) )
46 44 3 45 3eqtr4g 
 |-  ( ( ph /\ -. ( I e. _V /\ R e. _V ) ) -> B = (/) )
47 46 xpeq2d 
 |-  ( ( ph /\ -. ( I e. _V /\ R e. _V ) ) -> ( B X. B ) = ( B X. (/) ) )
48 xp0 
 |-  ( B X. (/) ) = (/)
49 47 48 eqtrdi 
 |-  ( ( ph /\ -. ( I e. _V /\ R e. _V ) ) -> ( B X. B ) = (/) )
50 sseq0 
 |-  ( ( { <. x , y >. | ( { x , y } C_ B /\ ( E. z e. D ( ( x ` z ) .< ( y ` z ) /\ A. w e. D ( w C z -> ( x ` w ) = ( y ` w ) ) ) \/ x = y ) ) } C_ ( B X. B ) /\ ( B X. B ) = (/) ) -> { <. x , y >. | ( { x , y } C_ B /\ ( E. z e. D ( ( x ` z ) .< ( y ` z ) /\ A. w e. D ( w C z -> ( x ` w ) = ( y ` w ) ) ) \/ x = y ) ) } = (/) )
51 24 49 50 sylancr 
 |-  ( ( ph /\ -. ( I e. _V /\ R e. _V ) ) -> { <. x , y >. | ( { x , y } C_ B /\ ( E. z e. D ( ( x ` z ) .< ( y ` z ) /\ A. w e. D ( w C z -> ( x ` w ) = ( y ` w ) ) ) \/ x = y ) ) } = (/) )
52 39 51 eqtr4d 
 |-  ( ( ph /\ -. ( I e. _V /\ R e. _V ) ) -> .<_ = { <. x , y >. | ( { x , y } C_ B /\ ( E. z e. D ( ( x ` z ) .< ( y ` z ) /\ A. w e. D ( w C z -> ( x ` w ) = ( y ` w ) ) ) \/ x = y ) ) } )
53 29 52 pm2.61dan 
 |-  ( ph -> .<_ = { <. x , y >. | ( { x , y } C_ B /\ ( E. z e. D ( ( x ` z ) .< ( y ` z ) /\ A. w e. D ( w C z -> ( x ` w ) = ( y ` w ) ) ) \/ x = y ) ) } )