# 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 𝑄 = ran ( eval1𝑅 )
Assertion pf1rcl ( 𝑋𝑄𝑅 ∈ CRing )

### Proof

Step Hyp Ref Expression
1 pf1rcl.q 𝑄 = ran ( eval1𝑅 )
2 n0i ( 𝑋𝑄 → ¬ 𝑄 = ∅ )
3 eqid ( eval1𝑅 ) = ( eval1𝑅 )
4 eqid ( 1o eval 𝑅 ) = ( 1o eval 𝑅 )
5 eqid ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
6 3 4 5 evl1fval ( eval1𝑅 ) = ( ( 𝑥 ∈ ( ( Base ‘ 𝑅 ) ↑m ( ( Base ‘ 𝑅 ) ↑m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦 ∈ ( Base ‘ 𝑅 ) ↦ ( 1o × { 𝑦 } ) ) ) ) ∘ ( 1o eval 𝑅 ) )
7 6 rneqi ran ( eval1𝑅 ) = ran ( ( 𝑥 ∈ ( ( Base ‘ 𝑅 ) ↑m ( ( Base ‘ 𝑅 ) ↑m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦 ∈ ( Base ‘ 𝑅 ) ↦ ( 1o × { 𝑦 } ) ) ) ) ∘ ( 1o eval 𝑅 ) )
8 rnco2 ran ( ( 𝑥 ∈ ( ( Base ‘ 𝑅 ) ↑m ( ( Base ‘ 𝑅 ) ↑m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦 ∈ ( Base ‘ 𝑅 ) ↦ ( 1o × { 𝑦 } ) ) ) ) ∘ ( 1o eval 𝑅 ) ) = ( ( 𝑥 ∈ ( ( Base ‘ 𝑅 ) ↑m ( ( Base ‘ 𝑅 ) ↑m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦 ∈ ( Base ‘ 𝑅 ) ↦ ( 1o × { 𝑦 } ) ) ) ) “ ran ( 1o eval 𝑅 ) )
9 1 7 8 3eqtri 𝑄 = ( ( 𝑥 ∈ ( ( Base ‘ 𝑅 ) ↑m ( ( Base ‘ 𝑅 ) ↑m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦 ∈ ( Base ‘ 𝑅 ) ↦ ( 1o × { 𝑦 } ) ) ) ) “ ran ( 1o eval 𝑅 ) )
10 inss2 ( dom ( 𝑥 ∈ ( ( Base ‘ 𝑅 ) ↑m ( ( Base ‘ 𝑅 ) ↑m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦 ∈ ( Base ‘ 𝑅 ) ↦ ( 1o × { 𝑦 } ) ) ) ) ∩ ran ( 1o eval 𝑅 ) ) ⊆ ran ( 1o eval 𝑅 )
11 neq0 ( ¬ ran ( 1o eval 𝑅 ) = ∅ ↔ ∃ 𝑥 𝑥 ∈ ran ( 1o eval 𝑅 ) )
12 4 5 evlval ( 1o eval 𝑅 ) = ( ( 1o evalSub 𝑅 ) ‘ ( Base ‘ 𝑅 ) )
13 12 rneqi ran ( 1o eval 𝑅 ) = ran ( ( 1o evalSub 𝑅 ) ‘ ( Base ‘ 𝑅 ) )
14 13 mpfrcl ( 𝑥 ∈ ran ( 1o eval 𝑅 ) → ( 1o ∈ V ∧ 𝑅 ∈ CRing ∧ ( Base ‘ 𝑅 ) ∈ ( SubRing ‘ 𝑅 ) ) )
15 14 simp2d ( 𝑥 ∈ ran ( 1o eval 𝑅 ) → 𝑅 ∈ CRing )
16 15 exlimiv ( ∃ 𝑥 𝑥 ∈ ran ( 1o eval 𝑅 ) → 𝑅 ∈ CRing )
17 11 16 sylbi ( ¬ ran ( 1o eval 𝑅 ) = ∅ → 𝑅 ∈ CRing )
18 17 con1i ( ¬ 𝑅 ∈ CRing → ran ( 1o eval 𝑅 ) = ∅ )
19 sseq0 ( ( ( dom ( 𝑥 ∈ ( ( Base ‘ 𝑅 ) ↑m ( ( Base ‘ 𝑅 ) ↑m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦 ∈ ( Base ‘ 𝑅 ) ↦ ( 1o × { 𝑦 } ) ) ) ) ∩ ran ( 1o eval 𝑅 ) ) ⊆ ran ( 1o eval 𝑅 ) ∧ ran ( 1o eval 𝑅 ) = ∅ ) → ( dom ( 𝑥 ∈ ( ( Base ‘ 𝑅 ) ↑m ( ( Base ‘ 𝑅 ) ↑m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦 ∈ ( Base ‘ 𝑅 ) ↦ ( 1o × { 𝑦 } ) ) ) ) ∩ ran ( 1o eval 𝑅 ) ) = ∅ )
20 10 18 19 sylancr ( ¬ 𝑅 ∈ CRing → ( dom ( 𝑥 ∈ ( ( Base ‘ 𝑅 ) ↑m ( ( Base ‘ 𝑅 ) ↑m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦 ∈ ( Base ‘ 𝑅 ) ↦ ( 1o × { 𝑦 } ) ) ) ) ∩ ran ( 1o eval 𝑅 ) ) = ∅ )
21 imadisj ( ( ( 𝑥 ∈ ( ( Base ‘ 𝑅 ) ↑m ( ( Base ‘ 𝑅 ) ↑m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦 ∈ ( Base ‘ 𝑅 ) ↦ ( 1o × { 𝑦 } ) ) ) ) “ ran ( 1o eval 𝑅 ) ) = ∅ ↔ ( dom ( 𝑥 ∈ ( ( Base ‘ 𝑅 ) ↑m ( ( Base ‘ 𝑅 ) ↑m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦 ∈ ( Base ‘ 𝑅 ) ↦ ( 1o × { 𝑦 } ) ) ) ) ∩ ran ( 1o eval 𝑅 ) ) = ∅ )
22 20 21 sylibr ( ¬ 𝑅 ∈ CRing → ( ( 𝑥 ∈ ( ( Base ‘ 𝑅 ) ↑m ( ( Base ‘ 𝑅 ) ↑m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦 ∈ ( Base ‘ 𝑅 ) ↦ ( 1o × { 𝑦 } ) ) ) ) “ ran ( 1o eval 𝑅 ) ) = ∅ )
23 9 22 syl5eq ( ¬ 𝑅 ∈ CRing → 𝑄 = ∅ )
24 2 23 nsyl2 ( 𝑋𝑄𝑅 ∈ CRing )