Metamath Proof Explorer


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𝑓 ) ‘ ( 𝐷𝑓 ) ) ∈ 𝑈 ) }