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 eqtrid ⊢ ( ¬ 𝑅 ∈ CRing → 𝑄 = ∅ )
24 2 23 nsyl2 ⊢ ( 𝑋 ∈ 𝑄 → 𝑅 ∈ CRing )