Step | Hyp | Ref
| Expression |
1 | | fta1glem.5 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝑇 ∈ (◡(𝑂‘𝐹) “ {𝑊})) |
2 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑅 ↑s 𝐾) = (𝑅 ↑s 𝐾) |
3 | | fta1glem.k |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 𝐾 = (Base‘𝑅) |
4 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(Base‘(𝑅
↑s 𝐾)) = (Base‘(𝑅 ↑s 𝐾)) |
5 | | fta1g.1 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 𝑅 ∈ IDomn) |
6 | | fvex 6201 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(Base‘𝑅)
∈ V |
7 | 3, 6 | eqeltri 2697 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 𝐾 ∈ V |
8 | 7 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 𝐾 ∈ V) |
9 | | isidom 19304 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑅 ∈ IDomn ↔ (𝑅 ∈ CRing ∧ 𝑅 ∈ Domn)) |
10 | 9 | simplbi 476 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑅 ∈ IDomn → 𝑅 ∈ CRing) |
11 | 5, 10 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → 𝑅 ∈ CRing) |
12 | | fta1g.o |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ 𝑂 = (eval1‘𝑅) |
13 | | fta1g.p |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ 𝑃 = (Poly1‘𝑅) |
14 | 12, 13, 2, 3 | evl1rhm 19696 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑅 ∈ CRing → 𝑂 ∈ (𝑃 RingHom (𝑅 ↑s 𝐾))) |
15 | 11, 14 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → 𝑂 ∈ (𝑃 RingHom (𝑅 ↑s 𝐾))) |
16 | | fta1g.b |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ 𝐵 = (Base‘𝑃) |
17 | 16, 4 | rhmf 18726 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑂 ∈ (𝑃 RingHom (𝑅 ↑s 𝐾)) → 𝑂:𝐵⟶(Base‘(𝑅 ↑s 𝐾))) |
18 | 15, 17 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → 𝑂:𝐵⟶(Base‘(𝑅 ↑s 𝐾))) |
19 | | fta1g.2 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → 𝐹 ∈ 𝐵) |
20 | 18, 19 | ffvelrnd 6360 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (𝑂‘𝐹) ∈ (Base‘(𝑅 ↑s 𝐾))) |
21 | 2, 3, 4, 5, 8, 20 | pwselbas 16149 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝑂‘𝐹):𝐾⟶𝐾) |
22 | 21 | ffnd 6046 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝑂‘𝐹) Fn 𝐾) |
23 | | fniniseg 6338 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑂‘𝐹) Fn 𝐾 → (𝑇 ∈ (◡(𝑂‘𝐹) “ {𝑊}) ↔ (𝑇 ∈ 𝐾 ∧ ((𝑂‘𝐹)‘𝑇) = 𝑊))) |
24 | 22, 23 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝑇 ∈ (◡(𝑂‘𝐹) “ {𝑊}) ↔ (𝑇 ∈ 𝐾 ∧ ((𝑂‘𝐹)‘𝑇) = 𝑊))) |
25 | 1, 24 | mpbid 222 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑇 ∈ 𝐾 ∧ ((𝑂‘𝐹)‘𝑇) = 𝑊)) |
26 | 25 | simprd 479 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((𝑂‘𝐹)‘𝑇) = 𝑊) |
27 | | fta1glem.x |
. . . . . . . . . . . . . . . . 17
⊢ 𝑋 = (var1‘𝑅) |
28 | | fta1glem.m |
. . . . . . . . . . . . . . . . 17
⊢ − =
(-g‘𝑃) |
29 | | fta1glem.a |
. . . . . . . . . . . . . . . . 17
⊢ 𝐴 = (algSc‘𝑃) |
30 | | fta1glem.g |
. . . . . . . . . . . . . . . . 17
⊢ 𝐺 = (𝑋 − (𝐴‘𝑇)) |
31 | 9 | simprbi 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑅 ∈ IDomn → 𝑅 ∈ Domn) |
32 | | domnnzr 19295 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑅 ∈ Domn → 𝑅 ∈ NzRing) |
33 | 31, 32 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑅 ∈ IDomn → 𝑅 ∈ NzRing) |
34 | 5, 33 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑅 ∈ NzRing) |
35 | 25 | simpld 475 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑇 ∈ 𝐾) |
36 | | fta1g.w |
. . . . . . . . . . . . . . . . 17
⊢ 𝑊 = (0g‘𝑅) |
37 | | eqid 2622 |
. . . . . . . . . . . . . . . . 17
⊢
(∥r‘𝑃) = (∥r‘𝑃) |
38 | 13, 16, 3, 27, 28, 29, 30, 12, 34, 11, 35, 19, 36, 37 | facth1 23924 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝐺(∥r‘𝑃)𝐹 ↔ ((𝑂‘𝐹)‘𝑇) = 𝑊)) |
39 | 26, 38 | mpbird 247 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐺(∥r‘𝑃)𝐹) |
40 | | nzrring 19261 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑅 ∈ NzRing → 𝑅 ∈ Ring) |
41 | 34, 40 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑅 ∈ Ring) |
42 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . 19
⊢
(Monic1p‘𝑅) = (Monic1p‘𝑅) |
43 | | fta1g.d |
. . . . . . . . . . . . . . . . . . 19
⊢ 𝐷 = ( deg1
‘𝑅) |
44 | 13, 16, 3, 27, 28, 29, 30, 12, 34, 11, 35, 42, 43, 36 | ply1remlem 23922 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝐺 ∈ (Monic1p‘𝑅) ∧ (𝐷‘𝐺) = 1 ∧ (◡(𝑂‘𝐺) “ {𝑊}) = {𝑇})) |
45 | 44 | simp1d 1073 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐺 ∈ (Monic1p‘𝑅)) |
46 | | eqid 2622 |
. . . . . . . . . . . . . . . . . 18
⊢
(Unic1p‘𝑅) = (Unic1p‘𝑅) |
47 | 46, 42 | mon1puc1p 23910 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑅 ∈ Ring ∧ 𝐺 ∈
(Monic1p‘𝑅)) → 𝐺 ∈ (Unic1p‘𝑅)) |
48 | 41, 45, 47 | syl2anc 693 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐺 ∈ (Unic1p‘𝑅)) |
49 | | eqid 2622 |
. . . . . . . . . . . . . . . . 17
⊢
(.r‘𝑃) = (.r‘𝑃) |
50 | | eqid 2622 |
. . . . . . . . . . . . . . . . 17
⊢
(quot1p‘𝑅) = (quot1p‘𝑅) |
51 | 13, 37, 16, 46, 49, 50 | dvdsq1p 23920 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ (Unic1p‘𝑅)) → (𝐺(∥r‘𝑃)𝐹 ↔ 𝐹 = ((𝐹(quot1p‘𝑅)𝐺)(.r‘𝑃)𝐺))) |
52 | 41, 19, 48, 51 | syl3anc 1326 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐺(∥r‘𝑃)𝐹 ↔ 𝐹 = ((𝐹(quot1p‘𝑅)𝐺)(.r‘𝑃)𝐺))) |
53 | 39, 52 | mpbid 222 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐹 = ((𝐹(quot1p‘𝑅)𝐺)(.r‘𝑃)𝐺)) |
54 | 53 | fveq2d 6195 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑂‘𝐹) = (𝑂‘((𝐹(quot1p‘𝑅)𝐺)(.r‘𝑃)𝐺))) |
55 | 50, 13, 16, 46 | q1pcl 23915 |
. . . . . . . . . . . . . . 15
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ (Unic1p‘𝑅)) → (𝐹(quot1p‘𝑅)𝐺) ∈ 𝐵) |
56 | 41, 19, 48, 55 | syl3anc 1326 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐹(quot1p‘𝑅)𝐺) ∈ 𝐵) |
57 | 13, 16, 42 | mon1pcl 23904 |
. . . . . . . . . . . . . . 15
⊢ (𝐺 ∈
(Monic1p‘𝑅) → 𝐺 ∈ 𝐵) |
58 | 45, 57 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐺 ∈ 𝐵) |
59 | | eqid 2622 |
. . . . . . . . . . . . . . 15
⊢
(.r‘(𝑅 ↑s 𝐾)) = (.r‘(𝑅 ↑s 𝐾)) |
60 | 16, 49, 59 | rhmmul 18727 |
. . . . . . . . . . . . . 14
⊢ ((𝑂 ∈ (𝑃 RingHom (𝑅 ↑s 𝐾)) ∧ (𝐹(quot1p‘𝑅)𝐺) ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → (𝑂‘((𝐹(quot1p‘𝑅)𝐺)(.r‘𝑃)𝐺)) = ((𝑂‘(𝐹(quot1p‘𝑅)𝐺))(.r‘(𝑅 ↑s 𝐾))(𝑂‘𝐺))) |
61 | 15, 56, 58, 60 | syl3anc 1326 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑂‘((𝐹(quot1p‘𝑅)𝐺)(.r‘𝑃)𝐺)) = ((𝑂‘(𝐹(quot1p‘𝑅)𝐺))(.r‘(𝑅 ↑s 𝐾))(𝑂‘𝐺))) |
62 | 18, 56 | ffvelrnd 6360 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑂‘(𝐹(quot1p‘𝑅)𝐺)) ∈ (Base‘(𝑅 ↑s 𝐾))) |
63 | 18, 58 | ffvelrnd 6360 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑂‘𝐺) ∈ (Base‘(𝑅 ↑s 𝐾))) |
64 | | eqid 2622 |
. . . . . . . . . . . . . 14
⊢
(.r‘𝑅) = (.r‘𝑅) |
65 | 2, 4, 5, 8, 62, 63, 64, 59 | pwsmulrval 16151 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑂‘(𝐹(quot1p‘𝑅)𝐺))(.r‘(𝑅 ↑s 𝐾))(𝑂‘𝐺)) = ((𝑂‘(𝐹(quot1p‘𝑅)𝐺)) ∘𝑓
(.r‘𝑅)(𝑂‘𝐺))) |
66 | 54, 61, 65 | 3eqtrd 2660 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑂‘𝐹) = ((𝑂‘(𝐹(quot1p‘𝑅)𝐺)) ∘𝑓
(.r‘𝑅)(𝑂‘𝐺))) |
67 | 66 | fveq1d 6193 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑂‘𝐹)‘𝑥) = (((𝑂‘(𝐹(quot1p‘𝑅)𝐺)) ∘𝑓
(.r‘𝑅)(𝑂‘𝐺))‘𝑥)) |
68 | 67 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐾) → ((𝑂‘𝐹)‘𝑥) = (((𝑂‘(𝐹(quot1p‘𝑅)𝐺)) ∘𝑓
(.r‘𝑅)(𝑂‘𝐺))‘𝑥)) |
69 | 2, 3, 4, 5, 8, 62 | pwselbas 16149 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑂‘(𝐹(quot1p‘𝑅)𝐺)):𝐾⟶𝐾) |
70 | 69 | ffnd 6046 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑂‘(𝐹(quot1p‘𝑅)𝐺)) Fn 𝐾) |
71 | 70 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐾) → (𝑂‘(𝐹(quot1p‘𝑅)𝐺)) Fn 𝐾) |
72 | 2, 3, 4, 5, 8, 63 | pwselbas 16149 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑂‘𝐺):𝐾⟶𝐾) |
73 | 72 | ffnd 6046 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑂‘𝐺) Fn 𝐾) |
74 | 73 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐾) → (𝑂‘𝐺) Fn 𝐾) |
75 | 7 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐾) → 𝐾 ∈ V) |
76 | | simpr 477 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐾) → 𝑥 ∈ 𝐾) |
77 | | fnfvof 6911 |
. . . . . . . . . . 11
⊢ ((((𝑂‘(𝐹(quot1p‘𝑅)𝐺)) Fn 𝐾 ∧ (𝑂‘𝐺) Fn 𝐾) ∧ (𝐾 ∈ V ∧ 𝑥 ∈ 𝐾)) → (((𝑂‘(𝐹(quot1p‘𝑅)𝐺)) ∘𝑓
(.r‘𝑅)(𝑂‘𝐺))‘𝑥) = (((𝑂‘(𝐹(quot1p‘𝑅)𝐺))‘𝑥)(.r‘𝑅)((𝑂‘𝐺)‘𝑥))) |
78 | 71, 74, 75, 76, 77 | syl22anc 1327 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐾) → (((𝑂‘(𝐹(quot1p‘𝑅)𝐺)) ∘𝑓
(.r‘𝑅)(𝑂‘𝐺))‘𝑥) = (((𝑂‘(𝐹(quot1p‘𝑅)𝐺))‘𝑥)(.r‘𝑅)((𝑂‘𝐺)‘𝑥))) |
79 | 68, 78 | eqtrd 2656 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐾) → ((𝑂‘𝐹)‘𝑥) = (((𝑂‘(𝐹(quot1p‘𝑅)𝐺))‘𝑥)(.r‘𝑅)((𝑂‘𝐺)‘𝑥))) |
80 | 79 | eqeq1d 2624 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐾) → (((𝑂‘𝐹)‘𝑥) = 𝑊 ↔ (((𝑂‘(𝐹(quot1p‘𝑅)𝐺))‘𝑥)(.r‘𝑅)((𝑂‘𝐺)‘𝑥)) = 𝑊)) |
81 | 5, 31 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑅 ∈ Domn) |
82 | 81 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐾) → 𝑅 ∈ Domn) |
83 | 69 | ffvelrnda 6359 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐾) → ((𝑂‘(𝐹(quot1p‘𝑅)𝐺))‘𝑥) ∈ 𝐾) |
84 | 72 | ffvelrnda 6359 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐾) → ((𝑂‘𝐺)‘𝑥) ∈ 𝐾) |
85 | 3, 64, 36 | domneq0 19297 |
. . . . . . . . 9
⊢ ((𝑅 ∈ Domn ∧ ((𝑂‘(𝐹(quot1p‘𝑅)𝐺))‘𝑥) ∈ 𝐾 ∧ ((𝑂‘𝐺)‘𝑥) ∈ 𝐾) → ((((𝑂‘(𝐹(quot1p‘𝑅)𝐺))‘𝑥)(.r‘𝑅)((𝑂‘𝐺)‘𝑥)) = 𝑊 ↔ (((𝑂‘(𝐹(quot1p‘𝑅)𝐺))‘𝑥) = 𝑊 ∨ ((𝑂‘𝐺)‘𝑥) = 𝑊))) |
86 | 82, 83, 84, 85 | syl3anc 1326 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐾) → ((((𝑂‘(𝐹(quot1p‘𝑅)𝐺))‘𝑥)(.r‘𝑅)((𝑂‘𝐺)‘𝑥)) = 𝑊 ↔ (((𝑂‘(𝐹(quot1p‘𝑅)𝐺))‘𝑥) = 𝑊 ∨ ((𝑂‘𝐺)‘𝑥) = 𝑊))) |
87 | 80, 86 | bitrd 268 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐾) → (((𝑂‘𝐹)‘𝑥) = 𝑊 ↔ (((𝑂‘(𝐹(quot1p‘𝑅)𝐺))‘𝑥) = 𝑊 ∨ ((𝑂‘𝐺)‘𝑥) = 𝑊))) |
88 | 87 | pm5.32da 673 |
. . . . . 6
⊢ (𝜑 → ((𝑥 ∈ 𝐾 ∧ ((𝑂‘𝐹)‘𝑥) = 𝑊) ↔ (𝑥 ∈ 𝐾 ∧ (((𝑂‘(𝐹(quot1p‘𝑅)𝐺))‘𝑥) = 𝑊 ∨ ((𝑂‘𝐺)‘𝑥) = 𝑊)))) |
89 | | andi 911 |
. . . . . 6
⊢ ((𝑥 ∈ 𝐾 ∧ (((𝑂‘(𝐹(quot1p‘𝑅)𝐺))‘𝑥) = 𝑊 ∨ ((𝑂‘𝐺)‘𝑥) = 𝑊)) ↔ ((𝑥 ∈ 𝐾 ∧ ((𝑂‘(𝐹(quot1p‘𝑅)𝐺))‘𝑥) = 𝑊) ∨ (𝑥 ∈ 𝐾 ∧ ((𝑂‘𝐺)‘𝑥) = 𝑊))) |
90 | 88, 89 | syl6bb 276 |
. . . . 5
⊢ (𝜑 → ((𝑥 ∈ 𝐾 ∧ ((𝑂‘𝐹)‘𝑥) = 𝑊) ↔ ((𝑥 ∈ 𝐾 ∧ ((𝑂‘(𝐹(quot1p‘𝑅)𝐺))‘𝑥) = 𝑊) ∨ (𝑥 ∈ 𝐾 ∧ ((𝑂‘𝐺)‘𝑥) = 𝑊)))) |
91 | | fniniseg 6338 |
. . . . . 6
⊢ ((𝑂‘𝐹) Fn 𝐾 → (𝑥 ∈ (◡(𝑂‘𝐹) “ {𝑊}) ↔ (𝑥 ∈ 𝐾 ∧ ((𝑂‘𝐹)‘𝑥) = 𝑊))) |
92 | 22, 91 | syl 17 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ (◡(𝑂‘𝐹) “ {𝑊}) ↔ (𝑥 ∈ 𝐾 ∧ ((𝑂‘𝐹)‘𝑥) = 𝑊))) |
93 | | elun 3753 |
. . . . . 6
⊢ (𝑥 ∈ ((◡(𝑂‘(𝐹(quot1p‘𝑅)𝐺)) “ {𝑊}) ∪ {𝑇}) ↔ (𝑥 ∈ (◡(𝑂‘(𝐹(quot1p‘𝑅)𝐺)) “ {𝑊}) ∨ 𝑥 ∈ {𝑇})) |
94 | | fniniseg 6338 |
. . . . . . . 8
⊢ ((𝑂‘(𝐹(quot1p‘𝑅)𝐺)) Fn 𝐾 → (𝑥 ∈ (◡(𝑂‘(𝐹(quot1p‘𝑅)𝐺)) “ {𝑊}) ↔ (𝑥 ∈ 𝐾 ∧ ((𝑂‘(𝐹(quot1p‘𝑅)𝐺))‘𝑥) = 𝑊))) |
95 | 70, 94 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ (◡(𝑂‘(𝐹(quot1p‘𝑅)𝐺)) “ {𝑊}) ↔ (𝑥 ∈ 𝐾 ∧ ((𝑂‘(𝐹(quot1p‘𝑅)𝐺))‘𝑥) = 𝑊))) |
96 | 44 | simp3d 1075 |
. . . . . . . . 9
⊢ (𝜑 → (◡(𝑂‘𝐺) “ {𝑊}) = {𝑇}) |
97 | 96 | eleq2d 2687 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ (◡(𝑂‘𝐺) “ {𝑊}) ↔ 𝑥 ∈ {𝑇})) |
98 | | fniniseg 6338 |
. . . . . . . . 9
⊢ ((𝑂‘𝐺) Fn 𝐾 → (𝑥 ∈ (◡(𝑂‘𝐺) “ {𝑊}) ↔ (𝑥 ∈ 𝐾 ∧ ((𝑂‘𝐺)‘𝑥) = 𝑊))) |
99 | 73, 98 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ (◡(𝑂‘𝐺) “ {𝑊}) ↔ (𝑥 ∈ 𝐾 ∧ ((𝑂‘𝐺)‘𝑥) = 𝑊))) |
100 | 97, 99 | bitr3d 270 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ {𝑇} ↔ (𝑥 ∈ 𝐾 ∧ ((𝑂‘𝐺)‘𝑥) = 𝑊))) |
101 | 95, 100 | orbi12d 746 |
. . . . . 6
⊢ (𝜑 → ((𝑥 ∈ (◡(𝑂‘(𝐹(quot1p‘𝑅)𝐺)) “ {𝑊}) ∨ 𝑥 ∈ {𝑇}) ↔ ((𝑥 ∈ 𝐾 ∧ ((𝑂‘(𝐹(quot1p‘𝑅)𝐺))‘𝑥) = 𝑊) ∨ (𝑥 ∈ 𝐾 ∧ ((𝑂‘𝐺)‘𝑥) = 𝑊)))) |
102 | 93, 101 | syl5bb 272 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ ((◡(𝑂‘(𝐹(quot1p‘𝑅)𝐺)) “ {𝑊}) ∪ {𝑇}) ↔ ((𝑥 ∈ 𝐾 ∧ ((𝑂‘(𝐹(quot1p‘𝑅)𝐺))‘𝑥) = 𝑊) ∨ (𝑥 ∈ 𝐾 ∧ ((𝑂‘𝐺)‘𝑥) = 𝑊)))) |
103 | 90, 92, 102 | 3bitr4d 300 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ (◡(𝑂‘𝐹) “ {𝑊}) ↔ 𝑥 ∈ ((◡(𝑂‘(𝐹(quot1p‘𝑅)𝐺)) “ {𝑊}) ∪ {𝑇}))) |
104 | 103 | eqrdv 2620 |
. . 3
⊢ (𝜑 → (◡(𝑂‘𝐹) “ {𝑊}) = ((◡(𝑂‘(𝐹(quot1p‘𝑅)𝐺)) “ {𝑊}) ∪ {𝑇})) |
105 | 104 | fveq2d 6195 |
. 2
⊢ (𝜑 → (#‘(◡(𝑂‘𝐹) “ {𝑊})) = (#‘((◡(𝑂‘(𝐹(quot1p‘𝑅)𝐺)) “ {𝑊}) ∪ {𝑇}))) |
106 | | fvex 6201 |
. . . . . . . . . 10
⊢ (𝑂‘(𝐹(quot1p‘𝑅)𝐺)) ∈ V |
107 | 106 | cnvex 7113 |
. . . . . . . . 9
⊢ ◡(𝑂‘(𝐹(quot1p‘𝑅)𝐺)) ∈ V |
108 | 107 | imaex 7104 |
. . . . . . . 8
⊢ (◡(𝑂‘(𝐹(quot1p‘𝑅)𝐺)) “ {𝑊}) ∈ V |
109 | 108 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → (◡(𝑂‘(𝐹(quot1p‘𝑅)𝐺)) “ {𝑊}) ∈ V) |
110 | | fta1glem.3 |
. . . . . . 7
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
111 | | fta1glem.6 |
. . . . . . . . 9
⊢ (𝜑 → ∀𝑔 ∈ 𝐵 ((𝐷‘𝑔) = 𝑁 → (#‘(◡(𝑂‘𝑔) “ {𝑊})) ≤ (𝐷‘𝑔))) |
112 | | fta1g.z |
. . . . . . . . . 10
⊢ 0 =
(0g‘𝑃) |
113 | | fta1glem.4 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐷‘𝐹) = (𝑁 + 1)) |
114 | 13, 16, 43, 12, 36, 112, 5, 19, 3, 27, 28, 29, 30, 110, 113, 1 | fta1glem1 23925 |
. . . . . . . . 9
⊢ (𝜑 → (𝐷‘(𝐹(quot1p‘𝑅)𝐺)) = 𝑁) |
115 | | fveq2 6191 |
. . . . . . . . . . . 12
⊢ (𝑔 = (𝐹(quot1p‘𝑅)𝐺) → (𝐷‘𝑔) = (𝐷‘(𝐹(quot1p‘𝑅)𝐺))) |
116 | 115 | eqeq1d 2624 |
. . . . . . . . . . 11
⊢ (𝑔 = (𝐹(quot1p‘𝑅)𝐺) → ((𝐷‘𝑔) = 𝑁 ↔ (𝐷‘(𝐹(quot1p‘𝑅)𝐺)) = 𝑁)) |
117 | | fveq2 6191 |
. . . . . . . . . . . . . . 15
⊢ (𝑔 = (𝐹(quot1p‘𝑅)𝐺) → (𝑂‘𝑔) = (𝑂‘(𝐹(quot1p‘𝑅)𝐺))) |
118 | 117 | cnveqd 5298 |
. . . . . . . . . . . . . 14
⊢ (𝑔 = (𝐹(quot1p‘𝑅)𝐺) → ◡(𝑂‘𝑔) = ◡(𝑂‘(𝐹(quot1p‘𝑅)𝐺))) |
119 | 118 | imaeq1d 5465 |
. . . . . . . . . . . . 13
⊢ (𝑔 = (𝐹(quot1p‘𝑅)𝐺) → (◡(𝑂‘𝑔) “ {𝑊}) = (◡(𝑂‘(𝐹(quot1p‘𝑅)𝐺)) “ {𝑊})) |
120 | 119 | fveq2d 6195 |
. . . . . . . . . . . 12
⊢ (𝑔 = (𝐹(quot1p‘𝑅)𝐺) → (#‘(◡(𝑂‘𝑔) “ {𝑊})) = (#‘(◡(𝑂‘(𝐹(quot1p‘𝑅)𝐺)) “ {𝑊}))) |
121 | 120, 115 | breq12d 4666 |
. . . . . . . . . . 11
⊢ (𝑔 = (𝐹(quot1p‘𝑅)𝐺) → ((#‘(◡(𝑂‘𝑔) “ {𝑊})) ≤ (𝐷‘𝑔) ↔ (#‘(◡(𝑂‘(𝐹(quot1p‘𝑅)𝐺)) “ {𝑊})) ≤ (𝐷‘(𝐹(quot1p‘𝑅)𝐺)))) |
122 | 116, 121 | imbi12d 334 |
. . . . . . . . . 10
⊢ (𝑔 = (𝐹(quot1p‘𝑅)𝐺) → (((𝐷‘𝑔) = 𝑁 → (#‘(◡(𝑂‘𝑔) “ {𝑊})) ≤ (𝐷‘𝑔)) ↔ ((𝐷‘(𝐹(quot1p‘𝑅)𝐺)) = 𝑁 → (#‘(◡(𝑂‘(𝐹(quot1p‘𝑅)𝐺)) “ {𝑊})) ≤ (𝐷‘(𝐹(quot1p‘𝑅)𝐺))))) |
123 | 122 | rspcv 3305 |
. . . . . . . . 9
⊢ ((𝐹(quot1p‘𝑅)𝐺) ∈ 𝐵 → (∀𝑔 ∈ 𝐵 ((𝐷‘𝑔) = 𝑁 → (#‘(◡(𝑂‘𝑔) “ {𝑊})) ≤ (𝐷‘𝑔)) → ((𝐷‘(𝐹(quot1p‘𝑅)𝐺)) = 𝑁 → (#‘(◡(𝑂‘(𝐹(quot1p‘𝑅)𝐺)) “ {𝑊})) ≤ (𝐷‘(𝐹(quot1p‘𝑅)𝐺))))) |
124 | 56, 111, 114, 123 | syl3c 66 |
. . . . . . . 8
⊢ (𝜑 → (#‘(◡(𝑂‘(𝐹(quot1p‘𝑅)𝐺)) “ {𝑊})) ≤ (𝐷‘(𝐹(quot1p‘𝑅)𝐺))) |
125 | 124, 114 | breqtrd 4679 |
. . . . . . 7
⊢ (𝜑 → (#‘(◡(𝑂‘(𝐹(quot1p‘𝑅)𝐺)) “ {𝑊})) ≤ 𝑁) |
126 | | hashbnd 13123 |
. . . . . . 7
⊢ (((◡(𝑂‘(𝐹(quot1p‘𝑅)𝐺)) “ {𝑊}) ∈ V ∧ 𝑁 ∈ ℕ0 ∧
(#‘(◡(𝑂‘(𝐹(quot1p‘𝑅)𝐺)) “ {𝑊})) ≤ 𝑁) → (◡(𝑂‘(𝐹(quot1p‘𝑅)𝐺)) “ {𝑊}) ∈ Fin) |
127 | 109, 110,
125, 126 | syl3anc 1326 |
. . . . . 6
⊢ (𝜑 → (◡(𝑂‘(𝐹(quot1p‘𝑅)𝐺)) “ {𝑊}) ∈ Fin) |
128 | | snfi 8038 |
. . . . . 6
⊢ {𝑇} ∈ Fin |
129 | | unfi 8227 |
. . . . . 6
⊢ (((◡(𝑂‘(𝐹(quot1p‘𝑅)𝐺)) “ {𝑊}) ∈ Fin ∧ {𝑇} ∈ Fin) → ((◡(𝑂‘(𝐹(quot1p‘𝑅)𝐺)) “ {𝑊}) ∪ {𝑇}) ∈ Fin) |
130 | 127, 128,
129 | sylancl 694 |
. . . . 5
⊢ (𝜑 → ((◡(𝑂‘(𝐹(quot1p‘𝑅)𝐺)) “ {𝑊}) ∪ {𝑇}) ∈ Fin) |
131 | | hashcl 13147 |
. . . . 5
⊢ (((◡(𝑂‘(𝐹(quot1p‘𝑅)𝐺)) “ {𝑊}) ∪ {𝑇}) ∈ Fin → (#‘((◡(𝑂‘(𝐹(quot1p‘𝑅)𝐺)) “ {𝑊}) ∪ {𝑇})) ∈
ℕ0) |
132 | 130, 131 | syl 17 |
. . . 4
⊢ (𝜑 → (#‘((◡(𝑂‘(𝐹(quot1p‘𝑅)𝐺)) “ {𝑊}) ∪ {𝑇})) ∈
ℕ0) |
133 | 132 | nn0red 11352 |
. . 3
⊢ (𝜑 → (#‘((◡(𝑂‘(𝐹(quot1p‘𝑅)𝐺)) “ {𝑊}) ∪ {𝑇})) ∈ ℝ) |
134 | | hashcl 13147 |
. . . . . 6
⊢ ((◡(𝑂‘(𝐹(quot1p‘𝑅)𝐺)) “ {𝑊}) ∈ Fin → (#‘(◡(𝑂‘(𝐹(quot1p‘𝑅)𝐺)) “ {𝑊})) ∈
ℕ0) |
135 | 127, 134 | syl 17 |
. . . . 5
⊢ (𝜑 → (#‘(◡(𝑂‘(𝐹(quot1p‘𝑅)𝐺)) “ {𝑊})) ∈
ℕ0) |
136 | 135 | nn0red 11352 |
. . . 4
⊢ (𝜑 → (#‘(◡(𝑂‘(𝐹(quot1p‘𝑅)𝐺)) “ {𝑊})) ∈ ℝ) |
137 | | peano2re 10209 |
. . . 4
⊢
((#‘(◡(𝑂‘(𝐹(quot1p‘𝑅)𝐺)) “ {𝑊})) ∈ ℝ → ((#‘(◡(𝑂‘(𝐹(quot1p‘𝑅)𝐺)) “ {𝑊})) + 1) ∈ ℝ) |
138 | 136, 137 | syl 17 |
. . 3
⊢ (𝜑 → ((#‘(◡(𝑂‘(𝐹(quot1p‘𝑅)𝐺)) “ {𝑊})) + 1) ∈ ℝ) |
139 | | peano2nn0 11333 |
. . . . . 6
⊢ (𝑁 ∈ ℕ0
→ (𝑁 + 1) ∈
ℕ0) |
140 | 110, 139 | syl 17 |
. . . . 5
⊢ (𝜑 → (𝑁 + 1) ∈
ℕ0) |
141 | 113, 140 | eqeltrd 2701 |
. . . 4
⊢ (𝜑 → (𝐷‘𝐹) ∈
ℕ0) |
142 | 141 | nn0red 11352 |
. . 3
⊢ (𝜑 → (𝐷‘𝐹) ∈ ℝ) |
143 | | hashun2 13172 |
. . . . 5
⊢ (((◡(𝑂‘(𝐹(quot1p‘𝑅)𝐺)) “ {𝑊}) ∈ Fin ∧ {𝑇} ∈ Fin) → (#‘((◡(𝑂‘(𝐹(quot1p‘𝑅)𝐺)) “ {𝑊}) ∪ {𝑇})) ≤ ((#‘(◡(𝑂‘(𝐹(quot1p‘𝑅)𝐺)) “ {𝑊})) + (#‘{𝑇}))) |
144 | 127, 128,
143 | sylancl 694 |
. . . 4
⊢ (𝜑 → (#‘((◡(𝑂‘(𝐹(quot1p‘𝑅)𝐺)) “ {𝑊}) ∪ {𝑇})) ≤ ((#‘(◡(𝑂‘(𝐹(quot1p‘𝑅)𝐺)) “ {𝑊})) + (#‘{𝑇}))) |
145 | | hashsng 13159 |
. . . . . 6
⊢ (𝑇 ∈ (◡(𝑂‘𝐹) “ {𝑊}) → (#‘{𝑇}) = 1) |
146 | 1, 145 | syl 17 |
. . . . 5
⊢ (𝜑 → (#‘{𝑇}) = 1) |
147 | 146 | oveq2d 6666 |
. . . 4
⊢ (𝜑 → ((#‘(◡(𝑂‘(𝐹(quot1p‘𝑅)𝐺)) “ {𝑊})) + (#‘{𝑇})) = ((#‘(◡(𝑂‘(𝐹(quot1p‘𝑅)𝐺)) “ {𝑊})) + 1)) |
148 | 144, 147 | breqtrd 4679 |
. . 3
⊢ (𝜑 → (#‘((◡(𝑂‘(𝐹(quot1p‘𝑅)𝐺)) “ {𝑊}) ∪ {𝑇})) ≤ ((#‘(◡(𝑂‘(𝐹(quot1p‘𝑅)𝐺)) “ {𝑊})) + 1)) |
149 | 110 | nn0red 11352 |
. . . . 5
⊢ (𝜑 → 𝑁 ∈ ℝ) |
150 | | 1red 10055 |
. . . . 5
⊢ (𝜑 → 1 ∈
ℝ) |
151 | 136, 149,
150, 125 | leadd1dd 10641 |
. . . 4
⊢ (𝜑 → ((#‘(◡(𝑂‘(𝐹(quot1p‘𝑅)𝐺)) “ {𝑊})) + 1) ≤ (𝑁 + 1)) |
152 | 151, 113 | breqtrrd 4681 |
. . 3
⊢ (𝜑 → ((#‘(◡(𝑂‘(𝐹(quot1p‘𝑅)𝐺)) “ {𝑊})) + 1) ≤ (𝐷‘𝐹)) |
153 | 133, 138,
142, 148, 152 | letrd 10194 |
. 2
⊢ (𝜑 → (#‘((◡(𝑂‘(𝐹(quot1p‘𝑅)𝐺)) “ {𝑊}) ∪ {𝑇})) ≤ (𝐷‘𝐹)) |
154 | 105, 153 | eqbrtrd 4675 |
1
⊢ (𝜑 → (#‘(◡(𝑂‘𝐹) “ {𝑊})) ≤ (𝐷‘𝐹)) |