| Step | Hyp | Ref
| Expression |
| 1 | | fta1glem.5 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝑇 ∈ (◡(𝑂‘𝐹) “ {𝑊})) |
| 2 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑅 ↑s 𝐾) = (𝑅 ↑s 𝐾) |
| 3 | | fta1glem.k |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 𝐾 = (Base‘𝑅) |
| 4 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(Base‘(𝑅
↑s 𝐾)) = (Base‘(𝑅 ↑s 𝐾)) |
| 5 | | fta1g.1 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 𝑅 ∈ IDomn) |
| 6 | 3 | fvexi 6920 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 𝐾 ∈ V |
| 7 | 6 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 𝐾 ∈ V) |
| 8 | | isidom 20725 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑅 ∈ IDomn ↔ (𝑅 ∈ CRing ∧ 𝑅 ∈ Domn)) |
| 9 | 8 | simplbi 497 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑅 ∈ IDomn → 𝑅 ∈ CRing) |
| 10 | 5, 9 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → 𝑅 ∈ CRing) |
| 11 | | fta1g.o |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ 𝑂 = (eval1‘𝑅) |
| 12 | | fta1g.p |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ 𝑃 = (Poly1‘𝑅) |
| 13 | 11, 12, 2, 3 | evl1rhm 22336 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑅 ∈ CRing → 𝑂 ∈ (𝑃 RingHom (𝑅 ↑s 𝐾))) |
| 14 | 10, 13 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → 𝑂 ∈ (𝑃 RingHom (𝑅 ↑s 𝐾))) |
| 15 | | fta1g.b |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ 𝐵 = (Base‘𝑃) |
| 16 | 15, 4 | rhmf 20485 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑂 ∈ (𝑃 RingHom (𝑅 ↑s 𝐾)) → 𝑂:𝐵⟶(Base‘(𝑅 ↑s 𝐾))) |
| 17 | 14, 16 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → 𝑂:𝐵⟶(Base‘(𝑅 ↑s 𝐾))) |
| 18 | | fta1g.2 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → 𝐹 ∈ 𝐵) |
| 19 | 17, 18 | ffvelcdmd 7105 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (𝑂‘𝐹) ∈ (Base‘(𝑅 ↑s 𝐾))) |
| 20 | 2, 3, 4, 5, 7, 19 | pwselbas 17534 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝑂‘𝐹):𝐾⟶𝐾) |
| 21 | 20 | ffnd 6737 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝑂‘𝐹) Fn 𝐾) |
| 22 | | fniniseg 7080 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑂‘𝐹) Fn 𝐾 → (𝑇 ∈ (◡(𝑂‘𝐹) “ {𝑊}) ↔ (𝑇 ∈ 𝐾 ∧ ((𝑂‘𝐹)‘𝑇) = 𝑊))) |
| 23 | 21, 22 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝑇 ∈ (◡(𝑂‘𝐹) “ {𝑊}) ↔ (𝑇 ∈ 𝐾 ∧ ((𝑂‘𝐹)‘𝑇) = 𝑊))) |
| 24 | 1, 23 | mpbid 232 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑇 ∈ 𝐾 ∧ ((𝑂‘𝐹)‘𝑇) = 𝑊)) |
| 25 | 24 | simprd 495 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((𝑂‘𝐹)‘𝑇) = 𝑊) |
| 26 | | fta1glem.x |
. . . . . . . . . . . . . . . . 17
⊢ 𝑋 = (var1‘𝑅) |
| 27 | | fta1glem.m |
. . . . . . . . . . . . . . . . 17
⊢ − =
(-g‘𝑃) |
| 28 | | fta1glem.a |
. . . . . . . . . . . . . . . . 17
⊢ 𝐴 = (algSc‘𝑃) |
| 29 | | fta1glem.g |
. . . . . . . . . . . . . . . . 17
⊢ 𝐺 = (𝑋 − (𝐴‘𝑇)) |
| 30 | 8 | simprbi 496 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑅 ∈ IDomn → 𝑅 ∈ Domn) |
| 31 | | domnnzr 20706 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑅 ∈ Domn → 𝑅 ∈ NzRing) |
| 32 | 30, 31 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑅 ∈ IDomn → 𝑅 ∈ NzRing) |
| 33 | 5, 32 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑅 ∈ NzRing) |
| 34 | 24 | simpld 494 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑇 ∈ 𝐾) |
| 35 | | fta1g.w |
. . . . . . . . . . . . . . . . 17
⊢ 𝑊 = (0g‘𝑅) |
| 36 | | eqid 2737 |
. . . . . . . . . . . . . . . . 17
⊢
(∥r‘𝑃) = (∥r‘𝑃) |
| 37 | 12, 15, 3, 26, 27, 28, 29, 11, 33, 10, 34, 18, 35, 36 | facth1 26206 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝐺(∥r‘𝑃)𝐹 ↔ ((𝑂‘𝐹)‘𝑇) = 𝑊)) |
| 38 | 25, 37 | mpbird 257 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐺(∥r‘𝑃)𝐹) |
| 39 | | nzrring 20516 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑅 ∈ NzRing → 𝑅 ∈ Ring) |
| 40 | 33, 39 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑅 ∈ Ring) |
| 41 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . 19
⊢
(Monic1p‘𝑅) = (Monic1p‘𝑅) |
| 42 | | fta1g.d |
. . . . . . . . . . . . . . . . . . 19
⊢ 𝐷 = (deg1‘𝑅) |
| 43 | 12, 15, 3, 26, 27, 28, 29, 11, 33, 10, 34, 41, 42, 35 | ply1remlem 26204 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝐺 ∈ (Monic1p‘𝑅) ∧ (𝐷‘𝐺) = 1 ∧ (◡(𝑂‘𝐺) “ {𝑊}) = {𝑇})) |
| 44 | 43 | simp1d 1143 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐺 ∈ (Monic1p‘𝑅)) |
| 45 | | eqid 2737 |
. . . . . . . . . . . . . . . . . 18
⊢
(Unic1p‘𝑅) = (Unic1p‘𝑅) |
| 46 | 45, 41 | mon1puc1p 26190 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑅 ∈ Ring ∧ 𝐺 ∈
(Monic1p‘𝑅)) → 𝐺 ∈ (Unic1p‘𝑅)) |
| 47 | 40, 44, 46 | syl2anc 584 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐺 ∈ (Unic1p‘𝑅)) |
| 48 | | eqid 2737 |
. . . . . . . . . . . . . . . . 17
⊢
(.r‘𝑃) = (.r‘𝑃) |
| 49 | | eqid 2737 |
. . . . . . . . . . . . . . . . 17
⊢
(quot1p‘𝑅) = (quot1p‘𝑅) |
| 50 | 12, 36, 15, 45, 48, 49 | dvdsq1p 26202 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ (Unic1p‘𝑅)) → (𝐺(∥r‘𝑃)𝐹 ↔ 𝐹 = ((𝐹(quot1p‘𝑅)𝐺)(.r‘𝑃)𝐺))) |
| 51 | 40, 18, 47, 50 | syl3anc 1373 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐺(∥r‘𝑃)𝐹 ↔ 𝐹 = ((𝐹(quot1p‘𝑅)𝐺)(.r‘𝑃)𝐺))) |
| 52 | 38, 51 | mpbid 232 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐹 = ((𝐹(quot1p‘𝑅)𝐺)(.r‘𝑃)𝐺)) |
| 53 | 52 | fveq2d 6910 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑂‘𝐹) = (𝑂‘((𝐹(quot1p‘𝑅)𝐺)(.r‘𝑃)𝐺))) |
| 54 | 49, 12, 15, 45 | q1pcl 26196 |
. . . . . . . . . . . . . . 15
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ (Unic1p‘𝑅)) → (𝐹(quot1p‘𝑅)𝐺) ∈ 𝐵) |
| 55 | 40, 18, 47, 54 | syl3anc 1373 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐹(quot1p‘𝑅)𝐺) ∈ 𝐵) |
| 56 | 12, 15, 41 | mon1pcl 26184 |
. . . . . . . . . . . . . . 15
⊢ (𝐺 ∈
(Monic1p‘𝑅) → 𝐺 ∈ 𝐵) |
| 57 | 44, 56 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐺 ∈ 𝐵) |
| 58 | | eqid 2737 |
. . . . . . . . . . . . . . 15
⊢
(.r‘(𝑅 ↑s 𝐾)) = (.r‘(𝑅 ↑s 𝐾)) |
| 59 | 15, 48, 58 | rhmmul 20486 |
. . . . . . . . . . . . . 14
⊢ ((𝑂 ∈ (𝑃 RingHom (𝑅 ↑s 𝐾)) ∧ (𝐹(quot1p‘𝑅)𝐺) ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → (𝑂‘((𝐹(quot1p‘𝑅)𝐺)(.r‘𝑃)𝐺)) = ((𝑂‘(𝐹(quot1p‘𝑅)𝐺))(.r‘(𝑅 ↑s 𝐾))(𝑂‘𝐺))) |
| 60 | 14, 55, 57, 59 | syl3anc 1373 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑂‘((𝐹(quot1p‘𝑅)𝐺)(.r‘𝑃)𝐺)) = ((𝑂‘(𝐹(quot1p‘𝑅)𝐺))(.r‘(𝑅 ↑s 𝐾))(𝑂‘𝐺))) |
| 61 | 17, 55 | ffvelcdmd 7105 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑂‘(𝐹(quot1p‘𝑅)𝐺)) ∈ (Base‘(𝑅 ↑s 𝐾))) |
| 62 | 17, 57 | ffvelcdmd 7105 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑂‘𝐺) ∈ (Base‘(𝑅 ↑s 𝐾))) |
| 63 | | eqid 2737 |
. . . . . . . . . . . . . 14
⊢
(.r‘𝑅) = (.r‘𝑅) |
| 64 | 2, 4, 5, 7, 61, 62, 63, 58 | pwsmulrval 17536 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑂‘(𝐹(quot1p‘𝑅)𝐺))(.r‘(𝑅 ↑s 𝐾))(𝑂‘𝐺)) = ((𝑂‘(𝐹(quot1p‘𝑅)𝐺)) ∘f
(.r‘𝑅)(𝑂‘𝐺))) |
| 65 | 53, 60, 64 | 3eqtrd 2781 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑂‘𝐹) = ((𝑂‘(𝐹(quot1p‘𝑅)𝐺)) ∘f
(.r‘𝑅)(𝑂‘𝐺))) |
| 66 | 65 | fveq1d 6908 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑂‘𝐹)‘𝑥) = (((𝑂‘(𝐹(quot1p‘𝑅)𝐺)) ∘f
(.r‘𝑅)(𝑂‘𝐺))‘𝑥)) |
| 67 | 66 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐾) → ((𝑂‘𝐹)‘𝑥) = (((𝑂‘(𝐹(quot1p‘𝑅)𝐺)) ∘f
(.r‘𝑅)(𝑂‘𝐺))‘𝑥)) |
| 68 | 2, 3, 4, 5, 7, 61 | pwselbas 17534 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑂‘(𝐹(quot1p‘𝑅)𝐺)):𝐾⟶𝐾) |
| 69 | 68 | ffnd 6737 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑂‘(𝐹(quot1p‘𝑅)𝐺)) Fn 𝐾) |
| 70 | 69 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐾) → (𝑂‘(𝐹(quot1p‘𝑅)𝐺)) Fn 𝐾) |
| 71 | 2, 3, 4, 5, 7, 62 | pwselbas 17534 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑂‘𝐺):𝐾⟶𝐾) |
| 72 | 71 | ffnd 6737 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑂‘𝐺) Fn 𝐾) |
| 73 | 72 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐾) → (𝑂‘𝐺) Fn 𝐾) |
| 74 | 6 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐾) → 𝐾 ∈ V) |
| 75 | | simpr 484 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐾) → 𝑥 ∈ 𝐾) |
| 76 | | fnfvof 7714 |
. . . . . . . . . . 11
⊢ ((((𝑂‘(𝐹(quot1p‘𝑅)𝐺)) Fn 𝐾 ∧ (𝑂‘𝐺) Fn 𝐾) ∧ (𝐾 ∈ V ∧ 𝑥 ∈ 𝐾)) → (((𝑂‘(𝐹(quot1p‘𝑅)𝐺)) ∘f
(.r‘𝑅)(𝑂‘𝐺))‘𝑥) = (((𝑂‘(𝐹(quot1p‘𝑅)𝐺))‘𝑥)(.r‘𝑅)((𝑂‘𝐺)‘𝑥))) |
| 77 | 70, 73, 74, 75, 76 | syl22anc 839 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐾) → (((𝑂‘(𝐹(quot1p‘𝑅)𝐺)) ∘f
(.r‘𝑅)(𝑂‘𝐺))‘𝑥) = (((𝑂‘(𝐹(quot1p‘𝑅)𝐺))‘𝑥)(.r‘𝑅)((𝑂‘𝐺)‘𝑥))) |
| 78 | 67, 77 | eqtrd 2777 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐾) → ((𝑂‘𝐹)‘𝑥) = (((𝑂‘(𝐹(quot1p‘𝑅)𝐺))‘𝑥)(.r‘𝑅)((𝑂‘𝐺)‘𝑥))) |
| 79 | 78 | eqeq1d 2739 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐾) → (((𝑂‘𝐹)‘𝑥) = 𝑊 ↔ (((𝑂‘(𝐹(quot1p‘𝑅)𝐺))‘𝑥)(.r‘𝑅)((𝑂‘𝐺)‘𝑥)) = 𝑊)) |
| 80 | 5, 30 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑅 ∈ Domn) |
| 81 | 80 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐾) → 𝑅 ∈ Domn) |
| 82 | 68 | ffvelcdmda 7104 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐾) → ((𝑂‘(𝐹(quot1p‘𝑅)𝐺))‘𝑥) ∈ 𝐾) |
| 83 | 71 | ffvelcdmda 7104 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐾) → ((𝑂‘𝐺)‘𝑥) ∈ 𝐾) |
| 84 | 3, 63, 35 | domneq0 20708 |
. . . . . . . . 9
⊢ ((𝑅 ∈ Domn ∧ ((𝑂‘(𝐹(quot1p‘𝑅)𝐺))‘𝑥) ∈ 𝐾 ∧ ((𝑂‘𝐺)‘𝑥) ∈ 𝐾) → ((((𝑂‘(𝐹(quot1p‘𝑅)𝐺))‘𝑥)(.r‘𝑅)((𝑂‘𝐺)‘𝑥)) = 𝑊 ↔ (((𝑂‘(𝐹(quot1p‘𝑅)𝐺))‘𝑥) = 𝑊 ∨ ((𝑂‘𝐺)‘𝑥) = 𝑊))) |
| 85 | 81, 82, 83, 84 | syl3anc 1373 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐾) → ((((𝑂‘(𝐹(quot1p‘𝑅)𝐺))‘𝑥)(.r‘𝑅)((𝑂‘𝐺)‘𝑥)) = 𝑊 ↔ (((𝑂‘(𝐹(quot1p‘𝑅)𝐺))‘𝑥) = 𝑊 ∨ ((𝑂‘𝐺)‘𝑥) = 𝑊))) |
| 86 | 79, 85 | bitrd 279 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐾) → (((𝑂‘𝐹)‘𝑥) = 𝑊 ↔ (((𝑂‘(𝐹(quot1p‘𝑅)𝐺))‘𝑥) = 𝑊 ∨ ((𝑂‘𝐺)‘𝑥) = 𝑊))) |
| 87 | 86 | pm5.32da 579 |
. . . . . 6
⊢ (𝜑 → ((𝑥 ∈ 𝐾 ∧ ((𝑂‘𝐹)‘𝑥) = 𝑊) ↔ (𝑥 ∈ 𝐾 ∧ (((𝑂‘(𝐹(quot1p‘𝑅)𝐺))‘𝑥) = 𝑊 ∨ ((𝑂‘𝐺)‘𝑥) = 𝑊)))) |
| 88 | | andi 1010 |
. . . . . 6
⊢ ((𝑥 ∈ 𝐾 ∧ (((𝑂‘(𝐹(quot1p‘𝑅)𝐺))‘𝑥) = 𝑊 ∨ ((𝑂‘𝐺)‘𝑥) = 𝑊)) ↔ ((𝑥 ∈ 𝐾 ∧ ((𝑂‘(𝐹(quot1p‘𝑅)𝐺))‘𝑥) = 𝑊) ∨ (𝑥 ∈ 𝐾 ∧ ((𝑂‘𝐺)‘𝑥) = 𝑊))) |
| 89 | 87, 88 | bitrdi 287 |
. . . . 5
⊢ (𝜑 → ((𝑥 ∈ 𝐾 ∧ ((𝑂‘𝐹)‘𝑥) = 𝑊) ↔ ((𝑥 ∈ 𝐾 ∧ ((𝑂‘(𝐹(quot1p‘𝑅)𝐺))‘𝑥) = 𝑊) ∨ (𝑥 ∈ 𝐾 ∧ ((𝑂‘𝐺)‘𝑥) = 𝑊)))) |
| 90 | | fniniseg 7080 |
. . . . . 6
⊢ ((𝑂‘𝐹) Fn 𝐾 → (𝑥 ∈ (◡(𝑂‘𝐹) “ {𝑊}) ↔ (𝑥 ∈ 𝐾 ∧ ((𝑂‘𝐹)‘𝑥) = 𝑊))) |
| 91 | 21, 90 | syl 17 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ (◡(𝑂‘𝐹) “ {𝑊}) ↔ (𝑥 ∈ 𝐾 ∧ ((𝑂‘𝐹)‘𝑥) = 𝑊))) |
| 92 | | elun 4153 |
. . . . . 6
⊢ (𝑥 ∈ ((◡(𝑂‘(𝐹(quot1p‘𝑅)𝐺)) “ {𝑊}) ∪ {𝑇}) ↔ (𝑥 ∈ (◡(𝑂‘(𝐹(quot1p‘𝑅)𝐺)) “ {𝑊}) ∨ 𝑥 ∈ {𝑇})) |
| 93 | | fniniseg 7080 |
. . . . . . . 8
⊢ ((𝑂‘(𝐹(quot1p‘𝑅)𝐺)) Fn 𝐾 → (𝑥 ∈ (◡(𝑂‘(𝐹(quot1p‘𝑅)𝐺)) “ {𝑊}) ↔ (𝑥 ∈ 𝐾 ∧ ((𝑂‘(𝐹(quot1p‘𝑅)𝐺))‘𝑥) = 𝑊))) |
| 94 | 69, 93 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ (◡(𝑂‘(𝐹(quot1p‘𝑅)𝐺)) “ {𝑊}) ↔ (𝑥 ∈ 𝐾 ∧ ((𝑂‘(𝐹(quot1p‘𝑅)𝐺))‘𝑥) = 𝑊))) |
| 95 | 43 | simp3d 1145 |
. . . . . . . . 9
⊢ (𝜑 → (◡(𝑂‘𝐺) “ {𝑊}) = {𝑇}) |
| 96 | 95 | eleq2d 2827 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ (◡(𝑂‘𝐺) “ {𝑊}) ↔ 𝑥 ∈ {𝑇})) |
| 97 | | fniniseg 7080 |
. . . . . . . . 9
⊢ ((𝑂‘𝐺) Fn 𝐾 → (𝑥 ∈ (◡(𝑂‘𝐺) “ {𝑊}) ↔ (𝑥 ∈ 𝐾 ∧ ((𝑂‘𝐺)‘𝑥) = 𝑊))) |
| 98 | 72, 97 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ (◡(𝑂‘𝐺) “ {𝑊}) ↔ (𝑥 ∈ 𝐾 ∧ ((𝑂‘𝐺)‘𝑥) = 𝑊))) |
| 99 | 96, 98 | bitr3d 281 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ {𝑇} ↔ (𝑥 ∈ 𝐾 ∧ ((𝑂‘𝐺)‘𝑥) = 𝑊))) |
| 100 | 94, 99 | orbi12d 919 |
. . . . . 6
⊢ (𝜑 → ((𝑥 ∈ (◡(𝑂‘(𝐹(quot1p‘𝑅)𝐺)) “ {𝑊}) ∨ 𝑥 ∈ {𝑇}) ↔ ((𝑥 ∈ 𝐾 ∧ ((𝑂‘(𝐹(quot1p‘𝑅)𝐺))‘𝑥) = 𝑊) ∨ (𝑥 ∈ 𝐾 ∧ ((𝑂‘𝐺)‘𝑥) = 𝑊)))) |
| 101 | 92, 100 | bitrid 283 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ ((◡(𝑂‘(𝐹(quot1p‘𝑅)𝐺)) “ {𝑊}) ∪ {𝑇}) ↔ ((𝑥 ∈ 𝐾 ∧ ((𝑂‘(𝐹(quot1p‘𝑅)𝐺))‘𝑥) = 𝑊) ∨ (𝑥 ∈ 𝐾 ∧ ((𝑂‘𝐺)‘𝑥) = 𝑊)))) |
| 102 | 89, 91, 101 | 3bitr4d 311 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ (◡(𝑂‘𝐹) “ {𝑊}) ↔ 𝑥 ∈ ((◡(𝑂‘(𝐹(quot1p‘𝑅)𝐺)) “ {𝑊}) ∪ {𝑇}))) |
| 103 | 102 | eqrdv 2735 |
. . 3
⊢ (𝜑 → (◡(𝑂‘𝐹) “ {𝑊}) = ((◡(𝑂‘(𝐹(quot1p‘𝑅)𝐺)) “ {𝑊}) ∪ {𝑇})) |
| 104 | 103 | fveq2d 6910 |
. 2
⊢ (𝜑 → (♯‘(◡(𝑂‘𝐹) “ {𝑊})) = (♯‘((◡(𝑂‘(𝐹(quot1p‘𝑅)𝐺)) “ {𝑊}) ∪ {𝑇}))) |
| 105 | | fvex 6919 |
. . . . . . . . . 10
⊢ (𝑂‘(𝐹(quot1p‘𝑅)𝐺)) ∈ V |
| 106 | 105 | cnvex 7947 |
. . . . . . . . 9
⊢ ◡(𝑂‘(𝐹(quot1p‘𝑅)𝐺)) ∈ V |
| 107 | 106 | imaex 7936 |
. . . . . . . 8
⊢ (◡(𝑂‘(𝐹(quot1p‘𝑅)𝐺)) “ {𝑊}) ∈ V |
| 108 | 107 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → (◡(𝑂‘(𝐹(quot1p‘𝑅)𝐺)) “ {𝑊}) ∈ V) |
| 109 | | fta1glem.3 |
. . . . . . 7
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
| 110 | | fta1g.z |
. . . . . . . . . 10
⊢ 0 =
(0g‘𝑃) |
| 111 | | fta1glem.4 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐷‘𝐹) = (𝑁 + 1)) |
| 112 | 12, 15, 42, 11, 35, 110, 5, 18, 3, 26, 27, 28, 29, 109, 111, 1 | fta1glem1 26207 |
. . . . . . . . 9
⊢ (𝜑 → (𝐷‘(𝐹(quot1p‘𝑅)𝐺)) = 𝑁) |
| 113 | | fveq2 6906 |
. . . . . . . . . . . 12
⊢ (𝑔 = (𝐹(quot1p‘𝑅)𝐺) → (𝐷‘𝑔) = (𝐷‘(𝐹(quot1p‘𝑅)𝐺))) |
| 114 | 113 | eqeq1d 2739 |
. . . . . . . . . . 11
⊢ (𝑔 = (𝐹(quot1p‘𝑅)𝐺) → ((𝐷‘𝑔) = 𝑁 ↔ (𝐷‘(𝐹(quot1p‘𝑅)𝐺)) = 𝑁)) |
| 115 | | fveq2 6906 |
. . . . . . . . . . . . . . 15
⊢ (𝑔 = (𝐹(quot1p‘𝑅)𝐺) → (𝑂‘𝑔) = (𝑂‘(𝐹(quot1p‘𝑅)𝐺))) |
| 116 | 115 | cnveqd 5886 |
. . . . . . . . . . . . . 14
⊢ (𝑔 = (𝐹(quot1p‘𝑅)𝐺) → ◡(𝑂‘𝑔) = ◡(𝑂‘(𝐹(quot1p‘𝑅)𝐺))) |
| 117 | 116 | imaeq1d 6077 |
. . . . . . . . . . . . 13
⊢ (𝑔 = (𝐹(quot1p‘𝑅)𝐺) → (◡(𝑂‘𝑔) “ {𝑊}) = (◡(𝑂‘(𝐹(quot1p‘𝑅)𝐺)) “ {𝑊})) |
| 118 | 117 | fveq2d 6910 |
. . . . . . . . . . . 12
⊢ (𝑔 = (𝐹(quot1p‘𝑅)𝐺) → (♯‘(◡(𝑂‘𝑔) “ {𝑊})) = (♯‘(◡(𝑂‘(𝐹(quot1p‘𝑅)𝐺)) “ {𝑊}))) |
| 119 | 118, 113 | breq12d 5156 |
. . . . . . . . . . 11
⊢ (𝑔 = (𝐹(quot1p‘𝑅)𝐺) → ((♯‘(◡(𝑂‘𝑔) “ {𝑊})) ≤ (𝐷‘𝑔) ↔ (♯‘(◡(𝑂‘(𝐹(quot1p‘𝑅)𝐺)) “ {𝑊})) ≤ (𝐷‘(𝐹(quot1p‘𝑅)𝐺)))) |
| 120 | 114, 119 | imbi12d 344 |
. . . . . . . . . 10
⊢ (𝑔 = (𝐹(quot1p‘𝑅)𝐺) → (((𝐷‘𝑔) = 𝑁 → (♯‘(◡(𝑂‘𝑔) “ {𝑊})) ≤ (𝐷‘𝑔)) ↔ ((𝐷‘(𝐹(quot1p‘𝑅)𝐺)) = 𝑁 → (♯‘(◡(𝑂‘(𝐹(quot1p‘𝑅)𝐺)) “ {𝑊})) ≤ (𝐷‘(𝐹(quot1p‘𝑅)𝐺))))) |
| 121 | | fta1glem.6 |
. . . . . . . . . 10
⊢ (𝜑 → ∀𝑔 ∈ 𝐵 ((𝐷‘𝑔) = 𝑁 → (♯‘(◡(𝑂‘𝑔) “ {𝑊})) ≤ (𝐷‘𝑔))) |
| 122 | 120, 121,
55 | rspcdva 3623 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐷‘(𝐹(quot1p‘𝑅)𝐺)) = 𝑁 → (♯‘(◡(𝑂‘(𝐹(quot1p‘𝑅)𝐺)) “ {𝑊})) ≤ (𝐷‘(𝐹(quot1p‘𝑅)𝐺)))) |
| 123 | 112, 122 | mpd 15 |
. . . . . . . 8
⊢ (𝜑 → (♯‘(◡(𝑂‘(𝐹(quot1p‘𝑅)𝐺)) “ {𝑊})) ≤ (𝐷‘(𝐹(quot1p‘𝑅)𝐺))) |
| 124 | 123, 112 | breqtrd 5169 |
. . . . . . 7
⊢ (𝜑 → (♯‘(◡(𝑂‘(𝐹(quot1p‘𝑅)𝐺)) “ {𝑊})) ≤ 𝑁) |
| 125 | | hashbnd 14375 |
. . . . . . 7
⊢ (((◡(𝑂‘(𝐹(quot1p‘𝑅)𝐺)) “ {𝑊}) ∈ V ∧ 𝑁 ∈ ℕ0 ∧
(♯‘(◡(𝑂‘(𝐹(quot1p‘𝑅)𝐺)) “ {𝑊})) ≤ 𝑁) → (◡(𝑂‘(𝐹(quot1p‘𝑅)𝐺)) “ {𝑊}) ∈ Fin) |
| 126 | 108, 109,
124, 125 | syl3anc 1373 |
. . . . . 6
⊢ (𝜑 → (◡(𝑂‘(𝐹(quot1p‘𝑅)𝐺)) “ {𝑊}) ∈ Fin) |
| 127 | | snfi 9083 |
. . . . . 6
⊢ {𝑇} ∈ Fin |
| 128 | | unfi 9211 |
. . . . . 6
⊢ (((◡(𝑂‘(𝐹(quot1p‘𝑅)𝐺)) “ {𝑊}) ∈ Fin ∧ {𝑇} ∈ Fin) → ((◡(𝑂‘(𝐹(quot1p‘𝑅)𝐺)) “ {𝑊}) ∪ {𝑇}) ∈ Fin) |
| 129 | 126, 127,
128 | sylancl 586 |
. . . . 5
⊢ (𝜑 → ((◡(𝑂‘(𝐹(quot1p‘𝑅)𝐺)) “ {𝑊}) ∪ {𝑇}) ∈ Fin) |
| 130 | | hashcl 14395 |
. . . . 5
⊢ (((◡(𝑂‘(𝐹(quot1p‘𝑅)𝐺)) “ {𝑊}) ∪ {𝑇}) ∈ Fin → (♯‘((◡(𝑂‘(𝐹(quot1p‘𝑅)𝐺)) “ {𝑊}) ∪ {𝑇})) ∈
ℕ0) |
| 131 | 129, 130 | syl 17 |
. . . 4
⊢ (𝜑 → (♯‘((◡(𝑂‘(𝐹(quot1p‘𝑅)𝐺)) “ {𝑊}) ∪ {𝑇})) ∈
ℕ0) |
| 132 | 131 | nn0red 12588 |
. . 3
⊢ (𝜑 → (♯‘((◡(𝑂‘(𝐹(quot1p‘𝑅)𝐺)) “ {𝑊}) ∪ {𝑇})) ∈ ℝ) |
| 133 | | hashcl 14395 |
. . . . . 6
⊢ ((◡(𝑂‘(𝐹(quot1p‘𝑅)𝐺)) “ {𝑊}) ∈ Fin → (♯‘(◡(𝑂‘(𝐹(quot1p‘𝑅)𝐺)) “ {𝑊})) ∈
ℕ0) |
| 134 | 126, 133 | syl 17 |
. . . . 5
⊢ (𝜑 → (♯‘(◡(𝑂‘(𝐹(quot1p‘𝑅)𝐺)) “ {𝑊})) ∈
ℕ0) |
| 135 | 134 | nn0red 12588 |
. . . 4
⊢ (𝜑 → (♯‘(◡(𝑂‘(𝐹(quot1p‘𝑅)𝐺)) “ {𝑊})) ∈ ℝ) |
| 136 | | peano2re 11434 |
. . . 4
⊢
((♯‘(◡(𝑂‘(𝐹(quot1p‘𝑅)𝐺)) “ {𝑊})) ∈ ℝ →
((♯‘(◡(𝑂‘(𝐹(quot1p‘𝑅)𝐺)) “ {𝑊})) + 1) ∈ ℝ) |
| 137 | 135, 136 | syl 17 |
. . 3
⊢ (𝜑 → ((♯‘(◡(𝑂‘(𝐹(quot1p‘𝑅)𝐺)) “ {𝑊})) + 1) ∈ ℝ) |
| 138 | | peano2nn0 12566 |
. . . . . 6
⊢ (𝑁 ∈ ℕ0
→ (𝑁 + 1) ∈
ℕ0) |
| 139 | 109, 138 | syl 17 |
. . . . 5
⊢ (𝜑 → (𝑁 + 1) ∈
ℕ0) |
| 140 | 111, 139 | eqeltrd 2841 |
. . . 4
⊢ (𝜑 → (𝐷‘𝐹) ∈
ℕ0) |
| 141 | 140 | nn0red 12588 |
. . 3
⊢ (𝜑 → (𝐷‘𝐹) ∈ ℝ) |
| 142 | | hashun2 14422 |
. . . . 5
⊢ (((◡(𝑂‘(𝐹(quot1p‘𝑅)𝐺)) “ {𝑊}) ∈ Fin ∧ {𝑇} ∈ Fin) → (♯‘((◡(𝑂‘(𝐹(quot1p‘𝑅)𝐺)) “ {𝑊}) ∪ {𝑇})) ≤ ((♯‘(◡(𝑂‘(𝐹(quot1p‘𝑅)𝐺)) “ {𝑊})) + (♯‘{𝑇}))) |
| 143 | 126, 127,
142 | sylancl 586 |
. . . 4
⊢ (𝜑 → (♯‘((◡(𝑂‘(𝐹(quot1p‘𝑅)𝐺)) “ {𝑊}) ∪ {𝑇})) ≤ ((♯‘(◡(𝑂‘(𝐹(quot1p‘𝑅)𝐺)) “ {𝑊})) + (♯‘{𝑇}))) |
| 144 | | hashsng 14408 |
. . . . . 6
⊢ (𝑇 ∈ (◡(𝑂‘𝐹) “ {𝑊}) → (♯‘{𝑇}) = 1) |
| 145 | 1, 144 | syl 17 |
. . . . 5
⊢ (𝜑 → (♯‘{𝑇}) = 1) |
| 146 | 145 | oveq2d 7447 |
. . . 4
⊢ (𝜑 → ((♯‘(◡(𝑂‘(𝐹(quot1p‘𝑅)𝐺)) “ {𝑊})) + (♯‘{𝑇})) = ((♯‘(◡(𝑂‘(𝐹(quot1p‘𝑅)𝐺)) “ {𝑊})) + 1)) |
| 147 | 143, 146 | breqtrd 5169 |
. . 3
⊢ (𝜑 → (♯‘((◡(𝑂‘(𝐹(quot1p‘𝑅)𝐺)) “ {𝑊}) ∪ {𝑇})) ≤ ((♯‘(◡(𝑂‘(𝐹(quot1p‘𝑅)𝐺)) “ {𝑊})) + 1)) |
| 148 | 109 | nn0red 12588 |
. . . . 5
⊢ (𝜑 → 𝑁 ∈ ℝ) |
| 149 | | 1red 11262 |
. . . . 5
⊢ (𝜑 → 1 ∈
ℝ) |
| 150 | 135, 148,
149, 124 | leadd1dd 11877 |
. . . 4
⊢ (𝜑 → ((♯‘(◡(𝑂‘(𝐹(quot1p‘𝑅)𝐺)) “ {𝑊})) + 1) ≤ (𝑁 + 1)) |
| 151 | 150, 111 | breqtrrd 5171 |
. . 3
⊢ (𝜑 → ((♯‘(◡(𝑂‘(𝐹(quot1p‘𝑅)𝐺)) “ {𝑊})) + 1) ≤ (𝐷‘𝐹)) |
| 152 | 132, 137,
141, 147, 151 | letrd 11418 |
. 2
⊢ (𝜑 → (♯‘((◡(𝑂‘(𝐹(quot1p‘𝑅)𝐺)) “ {𝑊}) ∪ {𝑇})) ≤ (𝐷‘𝐹)) |
| 153 | 104, 152 | eqbrtrd 5165 |
1
⊢ (𝜑 → (♯‘(◡(𝑂‘𝐹) “ {𝑊})) ≤ (𝐷‘𝐹)) |