Theorem ply1frcl

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

	Ref	Expression
Hypothesis	ply1frcl.q	⊢ 𝑄 = ran ( 𝑆 evalSub1 𝑅 )
Assertion	ply1frcl	⊢ ( 𝑋 ∈ 𝑄 → ( 𝑆 ∈ V ∧ 𝑅 ∈ 𝒫 ( Base ‘ 𝑆 ) ) )

Proof

Step	Hyp	Ref	Expression
1		ply1frcl.q	⊢ 𝑄 = ran ( 𝑆 evalSub1 𝑅 )
2		ne0i	⊢ ( 𝑋 ∈ ran ( 𝑆 evalSub1 𝑅 ) → ran ( 𝑆 evalSub1 𝑅 ) ≠ ∅ )
3	2 1	eleq2s	⊢ ( 𝑋 ∈ 𝑄 → ran ( 𝑆 evalSub1 𝑅 ) ≠ ∅ )
4		rneq	⊢ ( ( 𝑆 evalSub1 𝑅 ) = ∅ → ran ( 𝑆 evalSub1 𝑅 ) = ran ∅ )
5		rn0	⊢ ran ∅ = ∅
6	4 5	eqtrdi	⊢ ( ( 𝑆 evalSub1 𝑅 ) = ∅ → ran ( 𝑆 evalSub1 𝑅 ) = ∅ )
7	6	necon3i	⊢ ( ran ( 𝑆 evalSub1 𝑅 ) ≠ ∅ → ( 𝑆 evalSub1 𝑅 ) ≠ ∅ )
8		n0	⊢ ( ( 𝑆 evalSub1 𝑅 ) ≠ ∅ ↔ ∃ 𝑒 𝑒 ∈ ( 𝑆 evalSub1 𝑅 ) )
9		df-evls1	⊢ evalSub1 = ( 𝑠 ∈ V , 𝑟 ∈ 𝒫 ( Base ‘ 𝑠 ) ↦ ⦋ ( Base ‘ 𝑠 ) / 𝑏 ⦌ ( ( 𝑥 ∈ ( 𝑏 ↑m ( 𝑏 ↑m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦 ∈ 𝑏 ↦ ( 1o × { 𝑦 } ) ) ) ) ∘ ( ( 1o evalSub 𝑠 ) ‘ 𝑟 ) ) )
10	9	dmmpossx	⊢ dom evalSub1 ⊆ ∪ 𝑠 ∈ V ( { 𝑠 } × 𝒫 ( Base ‘ 𝑠 ) )
11		elfvdm	⊢ ( 𝑒 ∈ ( evalSub1 ‘ ⟨ 𝑆 , 𝑅 ⟩ ) → ⟨ 𝑆 , 𝑅 ⟩ ∈ dom evalSub1 )
12		df-ov	⊢ ( 𝑆 evalSub1 𝑅 ) = ( evalSub1 ‘ ⟨ 𝑆 , 𝑅 ⟩ )
13	11 12	eleq2s	⊢ ( 𝑒 ∈ ( 𝑆 evalSub1 𝑅 ) → ⟨ 𝑆 , 𝑅 ⟩ ∈ dom evalSub1 )
14	10 13	sselid	⊢ ( 𝑒 ∈ ( 𝑆 evalSub1 𝑅 ) → ⟨ 𝑆 , 𝑅 ⟩ ∈ ∪ 𝑠 ∈ V ( { 𝑠 } × 𝒫 ( Base ‘ 𝑠 ) ) )
15		fveq2	⊢ ( 𝑠 = 𝑆 → ( Base ‘ 𝑠 ) = ( Base ‘ 𝑆 ) )
16	15	pweqd	⊢ ( 𝑠 = 𝑆 → 𝒫 ( Base ‘ 𝑠 ) = 𝒫 ( Base ‘ 𝑆 ) )
17	16	opeliunxp2	⊢ ( ⟨ 𝑆 , 𝑅 ⟩ ∈ ∪ 𝑠 ∈ V ( { 𝑠 } × 𝒫 ( Base ‘ 𝑠 ) ) ↔ ( 𝑆 ∈ V ∧ 𝑅 ∈ 𝒫 ( Base ‘ 𝑆 ) ) )
18	14 17	sylib	⊢ ( 𝑒 ∈ ( 𝑆 evalSub1 𝑅 ) → ( 𝑆 ∈ V ∧ 𝑅 ∈ 𝒫 ( Base ‘ 𝑆 ) ) )
19	18	exlimiv	⊢ ( ∃ 𝑒 𝑒 ∈ ( 𝑆 evalSub1 𝑅 ) → ( 𝑆 ∈ V ∧ 𝑅 ∈ 𝒫 ( Base ‘ 𝑆 ) ) )
20	8 19	sylbi	⊢ ( ( 𝑆 evalSub1 𝑅 ) ≠ ∅ → ( 𝑆 ∈ V ∧ 𝑅 ∈ 𝒫 ( Base ‘ 𝑆 ) ) )
21	3 7 20	3syl	⊢ ( 𝑋 ∈ 𝑄 → ( 𝑆 ∈ V ∧ 𝑅 ∈ 𝒫 ( Base ‘ 𝑆 ) ) )