Metamath Proof Explorer

Theorem ply1frcl

Description: Reverse closure for the set of univariate polynomial functions. (Contributed by AV, 9-Sep-2019)

Ref Expression
Hypothesis ply1frcl.q 
|- Q = ran ( S evalSub1 R )
Assertion ply1frcl 
|- ( X e. Q -> ( S e. _V /\ R e. ~P ( Base ` S ) ) )

Proof

Step Hyp Ref Expression
1 ply1frcl.q 
 |-  Q = ran ( S evalSub1 R )
2 ne0i 
 |-  ( X e. ran ( S evalSub1 R ) -> ran ( S evalSub1 R ) =/= (/) )
3 2 1 eleq2s 
 |-  ( X e. Q -> ran ( S evalSub1 R ) =/= (/) )
4 rneq 
 |-  ( ( S evalSub1 R ) = (/) -> ran ( S evalSub1 R ) = ran (/) )
5 rn0 
 |-  ran (/) = (/)
6 4 5 eqtrdi 
 |-  ( ( S evalSub1 R ) = (/) -> ran ( S evalSub1 R ) = (/) )
7 6 necon3i 
 |-  ( ran ( S evalSub1 R ) =/= (/) -> ( S evalSub1 R ) =/= (/) )
8 n0 
 |-  ( ( S evalSub1 R ) =/= (/) <-> E. e e e. ( S evalSub1 R ) )
9 df-evls1 
 |-  evalSub1 = ( s e. _V , r e. ~P ( Base ` s ) |-> [_ ( Base ` s ) / b ]_ ( ( x e. ( b ^m ( b ^m 1o ) ) |-> ( x o. ( y e. b |-> ( 1o X. { y } ) ) ) ) o. ( ( 1o evalSub s ) ` r ) ) )
10 9 dmmpossx 
 |-  dom evalSub1 C_ U_ s e. _V ( { s } X. ~P ( Base ` s ) )
11 elfvdm 
 |-  ( e e. ( evalSub1 ` <. S , R >. ) -> <. S , R >. e. dom evalSub1 )
12 df-ov 
 |-  ( S evalSub1 R ) = ( evalSub1 ` <. S , R >. )
13 11 12 eleq2s 
 |-  ( e e. ( S evalSub1 R ) -> <. S , R >. e. dom evalSub1 )
14 10 13 sseldi 
 |-  ( e e. ( S evalSub1 R ) -> <. S , R >. e. U_ s e. _V ( { s } X. ~P ( Base ` s ) ) )
15 fveq2 
 |-  ( s = S -> ( Base ` s ) = ( Base ` S ) )
16 15 pweqd 
 |-  ( s = S -> ~P ( Base ` s ) = ~P ( Base ` S ) )
17 16 opeliunxp2 
 |-  ( <. S , R >. e. U_ s e. _V ( { s } X. ~P ( Base ` s ) ) <-> ( S e. _V /\ R e. ~P ( Base ` S ) ) )
18 14 17 sylib 
 |-  ( e e. ( S evalSub1 R ) -> ( S e. _V /\ R e. ~P ( Base ` S ) ) )
19 18 exlimiv 
 |-  ( E. e e e. ( S evalSub1 R ) -> ( S e. _V /\ R e. ~P ( Base ` S ) ) )
20 8 19 sylbi 
 |-  ( ( S evalSub1 R ) =/= (/) -> ( S e. _V /\ R e. ~P ( Base ` S ) ) )
21 3 7 20 3syl 
 |-  ( X e. Q -> ( S e. _V /\ R e. ~P ( Base ` S ) ) )