Theorem uc1pval

Description: Value of the set of unitic polynomials. (Contributed by Stefan O'Rear, 28-Mar-2015)

	Ref	Expression
Hypotheses	uc1pval.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
	uc1pval.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
	uc1pval.z	⊢ 0 = ( 0g ‘ 𝑃 )
	uc1pval.d	⊢ 𝐷 = ( deg1 ‘ 𝑅 )
	uc1pval.c	⊢ 𝐶 = ( Unic1p ‘ 𝑅 )
	uc1pval.u	⊢ 𝑈 = ( Unit ‘ 𝑅 )
Assertion	uc1pval	⊢ 𝐶 = { 𝑓 ∈ 𝐵 ∣ ( 𝑓 ≠ 0 ∧ ( ( coe1 ‘ 𝑓 ) ‘ ( 𝐷 ‘ 𝑓 ) ) ∈ 𝑈 ) }

Proof

Step	Hyp	Ref	Expression
1		uc1pval.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
2		uc1pval.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
3		uc1pval.z	⊢ 0 = ( 0g ‘ 𝑃 )
4		uc1pval.d	⊢ 𝐷 = ( deg1 ‘ 𝑅 )
5		uc1pval.c	⊢ 𝐶 = ( Unic1p ‘ 𝑅 )
6		uc1pval.u	⊢ 𝑈 = ( Unit ‘ 𝑅 )
7		fveq2	⊢ ( 𝑟 = 𝑅 → ( Poly1 ‘ 𝑟 ) = ( Poly1 ‘ 𝑅 ) )
8	7 1	eqtr4di	⊢ ( 𝑟 = 𝑅 → ( Poly1 ‘ 𝑟 ) = 𝑃 )
9	8	fveq2d	⊢ ( 𝑟 = 𝑅 → ( Base ‘ ( Poly1 ‘ 𝑟 ) ) = ( Base ‘ 𝑃 ) )
10	9 2	eqtr4di	⊢ ( 𝑟 = 𝑅 → ( Base ‘ ( Poly1 ‘ 𝑟 ) ) = 𝐵 )
11	8	fveq2d	⊢ ( 𝑟 = 𝑅 → ( 0g ‘ ( Poly1 ‘ 𝑟 ) ) = ( 0g ‘ 𝑃 ) )
12	11 3	eqtr4di	⊢ ( 𝑟 = 𝑅 → ( 0g ‘ ( Poly1 ‘ 𝑟 ) ) = 0 )
13	12	neeq2d	⊢ ( 𝑟 = 𝑅 → ( 𝑓 ≠ ( 0g ‘ ( Poly1 ‘ 𝑟 ) ) ↔ 𝑓 ≠ 0 ) )
14		fveq2	⊢ ( 𝑟 = 𝑅 → ( deg1 ‘ 𝑟 ) = ( deg1 ‘ 𝑅 ) )
15	14 4	eqtr4di	⊢ ( 𝑟 = 𝑅 → ( deg1 ‘ 𝑟 ) = 𝐷 )
16	15	fveq1d	⊢ ( 𝑟 = 𝑅 → ( ( deg1 ‘ 𝑟 ) ‘ 𝑓 ) = ( 𝐷 ‘ 𝑓 ) )
17	16	fveq2d	⊢ ( 𝑟 = 𝑅 → ( ( coe1 ‘ 𝑓 ) ‘ ( ( deg1 ‘ 𝑟 ) ‘ 𝑓 ) ) = ( ( coe1 ‘ 𝑓 ) ‘ ( 𝐷 ‘ 𝑓 ) ) )
18		fveq2	⊢ ( 𝑟 = 𝑅 → ( Unit ‘ 𝑟 ) = ( Unit ‘ 𝑅 ) )
19	18 6	eqtr4di	⊢ ( 𝑟 = 𝑅 → ( Unit ‘ 𝑟 ) = 𝑈 )
20	17 19	eleq12d	⊢ ( 𝑟 = 𝑅 → ( ( ( coe1 ‘ 𝑓 ) ‘ ( ( deg1 ‘ 𝑟 ) ‘ 𝑓 ) ) ∈ ( Unit ‘ 𝑟 ) ↔ ( ( coe1 ‘ 𝑓 ) ‘ ( 𝐷 ‘ 𝑓 ) ) ∈ 𝑈 ) )
21	13 20	anbi12d	⊢ ( 𝑟 = 𝑅 → ( ( 𝑓 ≠ ( 0g ‘ ( Poly1 ‘ 𝑟 ) ) ∧ ( ( coe1 ‘ 𝑓 ) ‘ ( ( deg1 ‘ 𝑟 ) ‘ 𝑓 ) ) ∈ ( Unit ‘ 𝑟 ) ) ↔ ( 𝑓 ≠ 0 ∧ ( ( coe1 ‘ 𝑓 ) ‘ ( 𝐷 ‘ 𝑓 ) ) ∈ 𝑈 ) ) )
22	10 21	rabeqbidv	⊢ ( 𝑟 = 𝑅 → { 𝑓 ∈ ( Base ‘ ( Poly1 ‘ 𝑟 ) ) ∣ ( 𝑓 ≠ ( 0g ‘ ( Poly1 ‘ 𝑟 ) ) ∧ ( ( coe1 ‘ 𝑓 ) ‘ ( ( deg1 ‘ 𝑟 ) ‘ 𝑓 ) ) ∈ ( Unit ‘ 𝑟 ) ) } = { 𝑓 ∈ 𝐵 ∣ ( 𝑓 ≠ 0 ∧ ( ( coe1 ‘ 𝑓 ) ‘ ( 𝐷 ‘ 𝑓 ) ) ∈ 𝑈 ) } )
23		df-uc1p	⊢ Unic1p = ( 𝑟 ∈ V ↦ { 𝑓 ∈ ( Base ‘ ( Poly1 ‘ 𝑟 ) ) ∣ ( 𝑓 ≠ ( 0g ‘ ( Poly1 ‘ 𝑟 ) ) ∧ ( ( coe1 ‘ 𝑓 ) ‘ ( ( deg1 ‘ 𝑟 ) ‘ 𝑓 ) ) ∈ ( Unit ‘ 𝑟 ) ) } )
24	2	fvexi	⊢ 𝐵 ∈ V
25	24	rabex	⊢ { 𝑓 ∈ 𝐵 ∣ ( 𝑓 ≠ 0 ∧ ( ( coe1 ‘ 𝑓 ) ‘ ( 𝐷 ‘ 𝑓 ) ) ∈ 𝑈 ) } ∈ V
26	22 23 25	fvmpt	⊢ ( 𝑅 ∈ V → ( Unic1p ‘ 𝑅 ) = { 𝑓 ∈ 𝐵 ∣ ( 𝑓 ≠ 0 ∧ ( ( coe1 ‘ 𝑓 ) ‘ ( 𝐷 ‘ 𝑓 ) ) ∈ 𝑈 ) } )
27		fvprc	⊢ ( ¬ 𝑅 ∈ V → ( Unic1p ‘ 𝑅 ) = ∅ )
28		ssrab2	⊢ { 𝑓 ∈ 𝐵 ∣ ( 𝑓 ≠ 0 ∧ ( ( coe1 ‘ 𝑓 ) ‘ ( 𝐷 ‘ 𝑓 ) ) ∈ 𝑈 ) } ⊆ 𝐵
29		fvprc	⊢ ( ¬ 𝑅 ∈ V → ( Poly1 ‘ 𝑅 ) = ∅ )
30	1 29	syl5eq	⊢ ( ¬ 𝑅 ∈ V → 𝑃 = ∅ )
31	30	fveq2d	⊢ ( ¬ 𝑅 ∈ V → ( Base ‘ 𝑃 ) = ( Base ‘ ∅ ) )
32		base0	⊢ ∅ = ( Base ‘ ∅ )
33	31 32	eqtr4di	⊢ ( ¬ 𝑅 ∈ V → ( Base ‘ 𝑃 ) = ∅ )
34	2 33	syl5eq	⊢ ( ¬ 𝑅 ∈ V → 𝐵 = ∅ )
35	28 34	sseqtrid	⊢ ( ¬ 𝑅 ∈ V → { 𝑓 ∈ 𝐵 ∣ ( 𝑓 ≠ 0 ∧ ( ( coe1 ‘ 𝑓 ) ‘ ( 𝐷 ‘ 𝑓 ) ) ∈ 𝑈 ) } ⊆ ∅ )
36		ss0	⊢ ( { 𝑓 ∈ 𝐵 ∣ ( 𝑓 ≠ 0 ∧ ( ( coe1 ‘ 𝑓 ) ‘ ( 𝐷 ‘ 𝑓 ) ) ∈ 𝑈 ) } ⊆ ∅ → { 𝑓 ∈ 𝐵 ∣ ( 𝑓 ≠ 0 ∧ ( ( coe1 ‘ 𝑓 ) ‘ ( 𝐷 ‘ 𝑓 ) ) ∈ 𝑈 ) } = ∅ )
37	35 36	syl	⊢ ( ¬ 𝑅 ∈ V → { 𝑓 ∈ 𝐵 ∣ ( 𝑓 ≠ 0 ∧ ( ( coe1 ‘ 𝑓 ) ‘ ( 𝐷 ‘ 𝑓 ) ) ∈ 𝑈 ) } = ∅ )
38	27 37	eqtr4d	⊢ ( ¬ 𝑅 ∈ V → ( Unic1p ‘ 𝑅 ) = { 𝑓 ∈ 𝐵 ∣ ( 𝑓 ≠ 0 ∧ ( ( coe1 ‘ 𝑓 ) ‘ ( 𝐷 ‘ 𝑓 ) ) ∈ 𝑈 ) } )
39	26 38	pm2.61i	⊢ ( Unic1p ‘ 𝑅 ) = { 𝑓 ∈ 𝐵 ∣ ( 𝑓 ≠ 0 ∧ ( ( coe1 ‘ 𝑓 ) ‘ ( 𝐷 ‘ 𝑓 ) ) ∈ 𝑈 ) }
40	5 39	eqtri	⊢ 𝐶 = { 𝑓 ∈ 𝐵 ∣ ( 𝑓 ≠ 0 ∧ ( ( coe1 ‘ 𝑓 ) ‘ ( 𝐷 ‘ 𝑓 ) ) ∈ 𝑈 ) }