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