Metamath Proof Explorer

Theorem pf1rcl

Description: Reverse closure for the set of polynomial functions. (Contributed by Mario Carneiro, 12-Jun-2015)

Ref Expression
Hypothesis pf1rcl.q 
|- Q = ran ( eval1 ` R )
Assertion pf1rcl 
|- ( X e. Q -> R e. CRing )

Proof

Step Hyp Ref Expression
1 pf1rcl.q 
 |-  Q = ran ( eval1 ` R )
2 n0i 
 |-  ( X e. Q -> -. Q = (/) )
3 eqid 
 |-  ( eval1 ` R ) = ( eval1 ` R )
4 eqid 
 |-  ( 1o eval R ) = ( 1o eval R )
5 eqid 
 |-  ( Base ` R ) = ( Base ` R )
6 3 4 5 evl1fval 
 |-  ( eval1 ` R ) = ( ( x e. ( ( Base ` R ) ^m ( ( Base ` R ) ^m 1o ) ) |-> ( x o. ( y e. ( Base ` R ) |-> ( 1o X. { y } ) ) ) ) o. ( 1o eval R ) )
7 6 rneqi 
 |-  ran ( eval1 ` R ) = ran ( ( x e. ( ( Base ` R ) ^m ( ( Base ` R ) ^m 1o ) ) |-> ( x o. ( y e. ( Base ` R ) |-> ( 1o X. { y } ) ) ) ) o. ( 1o eval R ) )
8 rnco2 
 |-  ran ( ( x e. ( ( Base ` R ) ^m ( ( Base ` R ) ^m 1o ) ) |-> ( x o. ( y e. ( Base ` R ) |-> ( 1o X. { y } ) ) ) ) o. ( 1o eval R ) ) = ( ( x e. ( ( Base ` R ) ^m ( ( Base ` R ) ^m 1o ) ) |-> ( x o. ( y e. ( Base ` R ) |-> ( 1o X. { y } ) ) ) ) " ran ( 1o eval R ) )
9 1 7 8 3eqtri 
 |-  Q = ( ( x e. ( ( Base ` R ) ^m ( ( Base ` R ) ^m 1o ) ) |-> ( x o. ( y e. ( Base ` R ) |-> ( 1o X. { y } ) ) ) ) " ran ( 1o eval R ) )
10 inss2 
 |-  ( dom ( x e. ( ( Base ` R ) ^m ( ( Base ` R ) ^m 1o ) ) |-> ( x o. ( y e. ( Base ` R ) |-> ( 1o X. { y } ) ) ) ) i^i ran ( 1o eval R ) ) C_ ran ( 1o eval R )
11 neq0 
 |-  ( -. ran ( 1o eval R ) = (/) <-> E. x x e. ran ( 1o eval R ) )
12 4 5 evlval 
 |-  ( 1o eval R ) = ( ( 1o evalSub R ) ` ( Base ` R ) )
13 12 rneqi 
 |-  ran ( 1o eval R ) = ran ( ( 1o evalSub R ) ` ( Base ` R ) )
14 13 mpfrcl 
 |-  ( x e. ran ( 1o eval R ) -> ( 1o e. _V /\ R e. CRing /\ ( Base ` R ) e. ( SubRing ` R ) ) )
15 14 simp2d 
 |-  ( x e. ran ( 1o eval R ) -> R e. CRing )
16 15 exlimiv 
 |-  ( E. x x e. ran ( 1o eval R ) -> R e. CRing )
17 11 16 sylbi 
 |-  ( -. ran ( 1o eval R ) = (/) -> R e. CRing )
18 17 con1i 
 |-  ( -. R e. CRing -> ran ( 1o eval R ) = (/) )
19 sseq0 
 |-  ( ( ( dom ( x e. ( ( Base ` R ) ^m ( ( Base ` R ) ^m 1o ) ) |-> ( x o. ( y e. ( Base ` R ) |-> ( 1o X. { y } ) ) ) ) i^i ran ( 1o eval R ) ) C_ ran ( 1o eval R ) /\ ran ( 1o eval R ) = (/) ) -> ( dom ( x e. ( ( Base ` R ) ^m ( ( Base ` R ) ^m 1o ) ) |-> ( x o. ( y e. ( Base ` R ) |-> ( 1o X. { y } ) ) ) ) i^i ran ( 1o eval R ) ) = (/) )
20 10 18 19 sylancr 
 |-  ( -. R e. CRing -> ( dom ( x e. ( ( Base ` R ) ^m ( ( Base ` R ) ^m 1o ) ) |-> ( x o. ( y e. ( Base ` R ) |-> ( 1o X. { y } ) ) ) ) i^i ran ( 1o eval R ) ) = (/) )
21 imadisj 
 |-  ( ( ( x e. ( ( Base ` R ) ^m ( ( Base ` R ) ^m 1o ) ) |-> ( x o. ( y e. ( Base ` R ) |-> ( 1o X. { y } ) ) ) ) " ran ( 1o eval R ) ) = (/) <-> ( dom ( x e. ( ( Base ` R ) ^m ( ( Base ` R ) ^m 1o ) ) |-> ( x o. ( y e. ( Base ` R ) |-> ( 1o X. { y } ) ) ) ) i^i ran ( 1o eval R ) ) = (/) )
22 20 21 sylibr 
 |-  ( -. R e. CRing -> ( ( x e. ( ( Base ` R ) ^m ( ( Base ` R ) ^m 1o ) ) |-> ( x o. ( y e. ( Base ` R ) |-> ( 1o X. { y } ) ) ) ) " ran ( 1o eval R ) ) = (/) )
23 9 22 syl5eq 
 |-  ( -. R e. CRing -> Q = (/) )
24 2 23 nsyl2 
 |-  ( X e. Q -> R e. CRing )