Step | Hyp | Ref
| Expression |
1 | | eqid 2738 |
. 2
⊢ (𝐷‘𝐹) = (𝐷‘𝐹) |
2 | | fveqeq2 6683 |
. . . 4
⊢ (𝑓 = 𝐹 → ((𝐷‘𝑓) = (𝐷‘𝐹) ↔ (𝐷‘𝐹) = (𝐷‘𝐹))) |
3 | | fveq2 6674 |
. . . . . . . 8
⊢ (𝑓 = 𝐹 → (𝑂‘𝑓) = (𝑂‘𝐹)) |
4 | 3 | cnveqd 5718 |
. . . . . . 7
⊢ (𝑓 = 𝐹 → ◡(𝑂‘𝑓) = ◡(𝑂‘𝐹)) |
5 | 4 | imaeq1d 5902 |
. . . . . 6
⊢ (𝑓 = 𝐹 → (◡(𝑂‘𝑓) “ {𝑊}) = (◡(𝑂‘𝐹) “ {𝑊})) |
6 | 5 | fveq2d 6678 |
. . . . 5
⊢ (𝑓 = 𝐹 → (♯‘(◡(𝑂‘𝑓) “ {𝑊})) = (♯‘(◡(𝑂‘𝐹) “ {𝑊}))) |
7 | | fveq2 6674 |
. . . . 5
⊢ (𝑓 = 𝐹 → (𝐷‘𝑓) = (𝐷‘𝐹)) |
8 | 6, 7 | breq12d 5043 |
. . . 4
⊢ (𝑓 = 𝐹 → ((♯‘(◡(𝑂‘𝑓) “ {𝑊})) ≤ (𝐷‘𝑓) ↔ (♯‘(◡(𝑂‘𝐹) “ {𝑊})) ≤ (𝐷‘𝐹))) |
9 | 2, 8 | imbi12d 348 |
. . 3
⊢ (𝑓 = 𝐹 → (((𝐷‘𝑓) = (𝐷‘𝐹) → (♯‘(◡(𝑂‘𝑓) “ {𝑊})) ≤ (𝐷‘𝑓)) ↔ ((𝐷‘𝐹) = (𝐷‘𝐹) → (♯‘(◡(𝑂‘𝐹) “ {𝑊})) ≤ (𝐷‘𝐹)))) |
10 | | fta1g.1 |
. . . . . 6
⊢ (𝜑 → 𝑅 ∈ IDomn) |
11 | | isidom 20196 |
. . . . . . 7
⊢ (𝑅 ∈ IDomn ↔ (𝑅 ∈ CRing ∧ 𝑅 ∈ Domn)) |
12 | 11 | simplbi 501 |
. . . . . 6
⊢ (𝑅 ∈ IDomn → 𝑅 ∈ CRing) |
13 | | crngring 19428 |
. . . . . 6
⊢ (𝑅 ∈ CRing → 𝑅 ∈ Ring) |
14 | 10, 12, 13 | 3syl 18 |
. . . . 5
⊢ (𝜑 → 𝑅 ∈ Ring) |
15 | | fta1g.2 |
. . . . 5
⊢ (𝜑 → 𝐹 ∈ 𝐵) |
16 | | fta1g.3 |
. . . . 5
⊢ (𝜑 → 𝐹 ≠ 0 ) |
17 | | fta1g.d |
. . . . . 6
⊢ 𝐷 = ( deg1
‘𝑅) |
18 | | fta1g.p |
. . . . . 6
⊢ 𝑃 = (Poly1‘𝑅) |
19 | | fta1g.z |
. . . . . 6
⊢ 0 =
(0g‘𝑃) |
20 | | fta1g.b |
. . . . . 6
⊢ 𝐵 = (Base‘𝑃) |
21 | 17, 18, 19, 20 | deg1nn0cl 24841 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 0 ) → (𝐷‘𝐹) ∈
ℕ0) |
22 | 14, 15, 16, 21 | syl3anc 1372 |
. . . 4
⊢ (𝜑 → (𝐷‘𝐹) ∈
ℕ0) |
23 | | eqeq2 2750 |
. . . . . . . 8
⊢ (𝑥 = 0 → ((𝐷‘𝑓) = 𝑥 ↔ (𝐷‘𝑓) = 0)) |
24 | 23 | imbi1d 345 |
. . . . . . 7
⊢ (𝑥 = 0 → (((𝐷‘𝑓) = 𝑥 → (♯‘(◡(𝑂‘𝑓) “ {𝑊})) ≤ (𝐷‘𝑓)) ↔ ((𝐷‘𝑓) = 0 → (♯‘(◡(𝑂‘𝑓) “ {𝑊})) ≤ (𝐷‘𝑓)))) |
25 | 24 | ralbidv 3109 |
. . . . . 6
⊢ (𝑥 = 0 → (∀𝑓 ∈ 𝐵 ((𝐷‘𝑓) = 𝑥 → (♯‘(◡(𝑂‘𝑓) “ {𝑊})) ≤ (𝐷‘𝑓)) ↔ ∀𝑓 ∈ 𝐵 ((𝐷‘𝑓) = 0 → (♯‘(◡(𝑂‘𝑓) “ {𝑊})) ≤ (𝐷‘𝑓)))) |
26 | 25 | imbi2d 344 |
. . . . 5
⊢ (𝑥 = 0 → ((𝑅 ∈ IDomn → ∀𝑓 ∈ 𝐵 ((𝐷‘𝑓) = 𝑥 → (♯‘(◡(𝑂‘𝑓) “ {𝑊})) ≤ (𝐷‘𝑓))) ↔ (𝑅 ∈ IDomn → ∀𝑓 ∈ 𝐵 ((𝐷‘𝑓) = 0 → (♯‘(◡(𝑂‘𝑓) “ {𝑊})) ≤ (𝐷‘𝑓))))) |
27 | | eqeq2 2750 |
. . . . . . . 8
⊢ (𝑥 = 𝑑 → ((𝐷‘𝑓) = 𝑥 ↔ (𝐷‘𝑓) = 𝑑)) |
28 | 27 | imbi1d 345 |
. . . . . . 7
⊢ (𝑥 = 𝑑 → (((𝐷‘𝑓) = 𝑥 → (♯‘(◡(𝑂‘𝑓) “ {𝑊})) ≤ (𝐷‘𝑓)) ↔ ((𝐷‘𝑓) = 𝑑 → (♯‘(◡(𝑂‘𝑓) “ {𝑊})) ≤ (𝐷‘𝑓)))) |
29 | 28 | ralbidv 3109 |
. . . . . 6
⊢ (𝑥 = 𝑑 → (∀𝑓 ∈ 𝐵 ((𝐷‘𝑓) = 𝑥 → (♯‘(◡(𝑂‘𝑓) “ {𝑊})) ≤ (𝐷‘𝑓)) ↔ ∀𝑓 ∈ 𝐵 ((𝐷‘𝑓) = 𝑑 → (♯‘(◡(𝑂‘𝑓) “ {𝑊})) ≤ (𝐷‘𝑓)))) |
30 | 29 | imbi2d 344 |
. . . . 5
⊢ (𝑥 = 𝑑 → ((𝑅 ∈ IDomn → ∀𝑓 ∈ 𝐵 ((𝐷‘𝑓) = 𝑥 → (♯‘(◡(𝑂‘𝑓) “ {𝑊})) ≤ (𝐷‘𝑓))) ↔ (𝑅 ∈ IDomn → ∀𝑓 ∈ 𝐵 ((𝐷‘𝑓) = 𝑑 → (♯‘(◡(𝑂‘𝑓) “ {𝑊})) ≤ (𝐷‘𝑓))))) |
31 | | eqeq2 2750 |
. . . . . . . 8
⊢ (𝑥 = (𝑑 + 1) → ((𝐷‘𝑓) = 𝑥 ↔ (𝐷‘𝑓) = (𝑑 + 1))) |
32 | 31 | imbi1d 345 |
. . . . . . 7
⊢ (𝑥 = (𝑑 + 1) → (((𝐷‘𝑓) = 𝑥 → (♯‘(◡(𝑂‘𝑓) “ {𝑊})) ≤ (𝐷‘𝑓)) ↔ ((𝐷‘𝑓) = (𝑑 + 1) → (♯‘(◡(𝑂‘𝑓) “ {𝑊})) ≤ (𝐷‘𝑓)))) |
33 | 32 | ralbidv 3109 |
. . . . . 6
⊢ (𝑥 = (𝑑 + 1) → (∀𝑓 ∈ 𝐵 ((𝐷‘𝑓) = 𝑥 → (♯‘(◡(𝑂‘𝑓) “ {𝑊})) ≤ (𝐷‘𝑓)) ↔ ∀𝑓 ∈ 𝐵 ((𝐷‘𝑓) = (𝑑 + 1) → (♯‘(◡(𝑂‘𝑓) “ {𝑊})) ≤ (𝐷‘𝑓)))) |
34 | 33 | imbi2d 344 |
. . . . 5
⊢ (𝑥 = (𝑑 + 1) → ((𝑅 ∈ IDomn → ∀𝑓 ∈ 𝐵 ((𝐷‘𝑓) = 𝑥 → (♯‘(◡(𝑂‘𝑓) “ {𝑊})) ≤ (𝐷‘𝑓))) ↔ (𝑅 ∈ IDomn → ∀𝑓 ∈ 𝐵 ((𝐷‘𝑓) = (𝑑 + 1) → (♯‘(◡(𝑂‘𝑓) “ {𝑊})) ≤ (𝐷‘𝑓))))) |
35 | | eqeq2 2750 |
. . . . . . . 8
⊢ (𝑥 = (𝐷‘𝐹) → ((𝐷‘𝑓) = 𝑥 ↔ (𝐷‘𝑓) = (𝐷‘𝐹))) |
36 | 35 | imbi1d 345 |
. . . . . . 7
⊢ (𝑥 = (𝐷‘𝐹) → (((𝐷‘𝑓) = 𝑥 → (♯‘(◡(𝑂‘𝑓) “ {𝑊})) ≤ (𝐷‘𝑓)) ↔ ((𝐷‘𝑓) = (𝐷‘𝐹) → (♯‘(◡(𝑂‘𝑓) “ {𝑊})) ≤ (𝐷‘𝑓)))) |
37 | 36 | ralbidv 3109 |
. . . . . 6
⊢ (𝑥 = (𝐷‘𝐹) → (∀𝑓 ∈ 𝐵 ((𝐷‘𝑓) = 𝑥 → (♯‘(◡(𝑂‘𝑓) “ {𝑊})) ≤ (𝐷‘𝑓)) ↔ ∀𝑓 ∈ 𝐵 ((𝐷‘𝑓) = (𝐷‘𝐹) → (♯‘(◡(𝑂‘𝑓) “ {𝑊})) ≤ (𝐷‘𝑓)))) |
38 | 37 | imbi2d 344 |
. . . . 5
⊢ (𝑥 = (𝐷‘𝐹) → ((𝑅 ∈ IDomn → ∀𝑓 ∈ 𝐵 ((𝐷‘𝑓) = 𝑥 → (♯‘(◡(𝑂‘𝑓) “ {𝑊})) ≤ (𝐷‘𝑓))) ↔ (𝑅 ∈ IDomn → ∀𝑓 ∈ 𝐵 ((𝐷‘𝑓) = (𝐷‘𝐹) → (♯‘(◡(𝑂‘𝑓) “ {𝑊})) ≤ (𝐷‘𝑓))))) |
39 | | simprr 773 |
. . . . . . . . . . . . . 14
⊢ ((𝑅 ∈ IDomn ∧ (𝑓 ∈ 𝐵 ∧ (𝐷‘𝑓) = 0)) → (𝐷‘𝑓) = 0) |
40 | | 0nn0 11991 |
. . . . . . . . . . . . . 14
⊢ 0 ∈
ℕ0 |
41 | 39, 40 | eqeltrdi 2841 |
. . . . . . . . . . . . 13
⊢ ((𝑅 ∈ IDomn ∧ (𝑓 ∈ 𝐵 ∧ (𝐷‘𝑓) = 0)) → (𝐷‘𝑓) ∈
ℕ0) |
42 | 12, 13 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝑅 ∈ IDomn → 𝑅 ∈ Ring) |
43 | | simpl 486 |
. . . . . . . . . . . . . 14
⊢ ((𝑓 ∈ 𝐵 ∧ (𝐷‘𝑓) = 0) → 𝑓 ∈ 𝐵) |
44 | 17, 18, 19, 20 | deg1nn0clb 24843 |
. . . . . . . . . . . . . 14
⊢ ((𝑅 ∈ Ring ∧ 𝑓 ∈ 𝐵) → (𝑓 ≠ 0 ↔ (𝐷‘𝑓) ∈
ℕ0)) |
45 | 42, 43, 44 | syl2an 599 |
. . . . . . . . . . . . 13
⊢ ((𝑅 ∈ IDomn ∧ (𝑓 ∈ 𝐵 ∧ (𝐷‘𝑓) = 0)) → (𝑓 ≠ 0 ↔ (𝐷‘𝑓) ∈
ℕ0)) |
46 | 41, 45 | mpbird 260 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ IDomn ∧ (𝑓 ∈ 𝐵 ∧ (𝐷‘𝑓) = 0)) → 𝑓 ≠ 0 ) |
47 | | simplrr 778 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑅 ∈ IDomn ∧ (𝑓 ∈ 𝐵 ∧ (𝐷‘𝑓) = 0)) ∧ 𝑥 ∈ (◡(𝑂‘𝑓) “ {𝑊})) → (𝐷‘𝑓) = 0) |
48 | | 0le0 11817 |
. . . . . . . . . . . . . . . . 17
⊢ 0 ≤
0 |
49 | 47, 48 | eqbrtrdi 5069 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑅 ∈ IDomn ∧ (𝑓 ∈ 𝐵 ∧ (𝐷‘𝑓) = 0)) ∧ 𝑥 ∈ (◡(𝑂‘𝑓) “ {𝑊})) → (𝐷‘𝑓) ≤ 0) |
50 | 42 | ad2antrr 726 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑅 ∈ IDomn ∧ (𝑓 ∈ 𝐵 ∧ (𝐷‘𝑓) = 0)) ∧ 𝑥 ∈ (◡(𝑂‘𝑓) “ {𝑊})) → 𝑅 ∈ Ring) |
51 | | simplrl 777 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑅 ∈ IDomn ∧ (𝑓 ∈ 𝐵 ∧ (𝐷‘𝑓) = 0)) ∧ 𝑥 ∈ (◡(𝑂‘𝑓) “ {𝑊})) → 𝑓 ∈ 𝐵) |
52 | | eqid 2738 |
. . . . . . . . . . . . . . . . . 18
⊢
(algSc‘𝑃) =
(algSc‘𝑃) |
53 | 17, 18, 20, 52 | deg1le0 24864 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑅 ∈ Ring ∧ 𝑓 ∈ 𝐵) → ((𝐷‘𝑓) ≤ 0 ↔ 𝑓 = ((algSc‘𝑃)‘((coe1‘𝑓)‘0)))) |
54 | 50, 51, 53 | syl2anc 587 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑅 ∈ IDomn ∧ (𝑓 ∈ 𝐵 ∧ (𝐷‘𝑓) = 0)) ∧ 𝑥 ∈ (◡(𝑂‘𝑓) “ {𝑊})) → ((𝐷‘𝑓) ≤ 0 ↔ 𝑓 = ((algSc‘𝑃)‘((coe1‘𝑓)‘0)))) |
55 | 49, 54 | mpbid 235 |
. . . . . . . . . . . . . . 15
⊢ (((𝑅 ∈ IDomn ∧ (𝑓 ∈ 𝐵 ∧ (𝐷‘𝑓) = 0)) ∧ 𝑥 ∈ (◡(𝑂‘𝑓) “ {𝑊})) → 𝑓 = ((algSc‘𝑃)‘((coe1‘𝑓)‘0))) |
56 | 55 | fveq2d 6678 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑅 ∈ IDomn ∧ (𝑓 ∈ 𝐵 ∧ (𝐷‘𝑓) = 0)) ∧ 𝑥 ∈ (◡(𝑂‘𝑓) “ {𝑊})) → (𝑂‘𝑓) = (𝑂‘((algSc‘𝑃)‘((coe1‘𝑓)‘0)))) |
57 | 12 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑅 ∈ IDomn ∧ (𝑓 ∈ 𝐵 ∧ (𝐷‘𝑓) = 0)) → 𝑅 ∈ CRing) |
58 | 57 | adantr 484 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑅 ∈ IDomn ∧ (𝑓 ∈ 𝐵 ∧ (𝐷‘𝑓) = 0)) ∧ 𝑥 ∈ (◡(𝑂‘𝑓) “ {𝑊})) → 𝑅 ∈ CRing) |
59 | | eqid 2738 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(coe1‘𝑓) = (coe1‘𝑓) |
60 | | eqid 2738 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(Base‘𝑅) =
(Base‘𝑅) |
61 | 59, 20, 18, 60 | coe1f 20986 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑓 ∈ 𝐵 → (coe1‘𝑓):ℕ0⟶(Base‘𝑅)) |
62 | 51, 61 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑅 ∈ IDomn ∧ (𝑓 ∈ 𝐵 ∧ (𝐷‘𝑓) = 0)) ∧ 𝑥 ∈ (◡(𝑂‘𝑓) “ {𝑊})) → (coe1‘𝑓):ℕ0⟶(Base‘𝑅)) |
63 | | ffvelrn 6859 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((coe1‘𝑓):ℕ0⟶(Base‘𝑅) ∧ 0 ∈
ℕ0) → ((coe1‘𝑓)‘0) ∈ (Base‘𝑅)) |
64 | 62, 40, 63 | sylancl 589 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑅 ∈ IDomn ∧ (𝑓 ∈ 𝐵 ∧ (𝐷‘𝑓) = 0)) ∧ 𝑥 ∈ (◡(𝑂‘𝑓) “ {𝑊})) → ((coe1‘𝑓)‘0) ∈
(Base‘𝑅)) |
65 | | fta1g.o |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 𝑂 = (eval1‘𝑅) |
66 | 65, 18, 60, 52 | evl1sca 21104 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑅 ∈ CRing ∧
((coe1‘𝑓)‘0) ∈ (Base‘𝑅)) → (𝑂‘((algSc‘𝑃)‘((coe1‘𝑓)‘0))) =
((Base‘𝑅) ×
{((coe1‘𝑓)‘0)})) |
67 | 58, 64, 66 | syl2anc 587 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑅 ∈ IDomn ∧ (𝑓 ∈ 𝐵 ∧ (𝐷‘𝑓) = 0)) ∧ 𝑥 ∈ (◡(𝑂‘𝑓) “ {𝑊})) → (𝑂‘((algSc‘𝑃)‘((coe1‘𝑓)‘0))) =
((Base‘𝑅) ×
{((coe1‘𝑓)‘0)})) |
68 | 56, 67 | eqtrd 2773 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑅 ∈ IDomn ∧ (𝑓 ∈ 𝐵 ∧ (𝐷‘𝑓) = 0)) ∧ 𝑥 ∈ (◡(𝑂‘𝑓) “ {𝑊})) → (𝑂‘𝑓) = ((Base‘𝑅) × {((coe1‘𝑓)‘0)})) |
69 | 68 | fveq1d 6676 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑅 ∈ IDomn ∧ (𝑓 ∈ 𝐵 ∧ (𝐷‘𝑓) = 0)) ∧ 𝑥 ∈ (◡(𝑂‘𝑓) “ {𝑊})) → ((𝑂‘𝑓)‘𝑥) = (((Base‘𝑅) × {((coe1‘𝑓)‘0)})‘𝑥)) |
70 | | eqid 2738 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑅 ↑s
(Base‘𝑅)) = (𝑅 ↑s
(Base‘𝑅)) |
71 | | eqid 2738 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(Base‘(𝑅
↑s (Base‘𝑅))) = (Base‘(𝑅 ↑s (Base‘𝑅))) |
72 | | simpl 486 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑅 ∈ IDomn ∧ (𝑓 ∈ 𝐵 ∧ (𝐷‘𝑓) = 0)) → 𝑅 ∈ IDomn) |
73 | | fvexd 6689 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑅 ∈ IDomn ∧ (𝑓 ∈ 𝐵 ∧ (𝐷‘𝑓) = 0)) → (Base‘𝑅) ∈ V) |
74 | 65, 18, 70, 60 | evl1rhm 21102 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑅 ∈ CRing → 𝑂 ∈ (𝑃 RingHom (𝑅 ↑s (Base‘𝑅)))) |
75 | 20, 71 | rhmf 19600 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑂 ∈ (𝑃 RingHom (𝑅 ↑s (Base‘𝑅))) → 𝑂:𝐵⟶(Base‘(𝑅 ↑s (Base‘𝑅)))) |
76 | 57, 74, 75 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑅 ∈ IDomn ∧ (𝑓 ∈ 𝐵 ∧ (𝐷‘𝑓) = 0)) → 𝑂:𝐵⟶(Base‘(𝑅 ↑s (Base‘𝑅)))) |
77 | | simprl 771 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑅 ∈ IDomn ∧ (𝑓 ∈ 𝐵 ∧ (𝐷‘𝑓) = 0)) → 𝑓 ∈ 𝐵) |
78 | 76, 77 | ffvelrnd 6862 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑅 ∈ IDomn ∧ (𝑓 ∈ 𝐵 ∧ (𝐷‘𝑓) = 0)) → (𝑂‘𝑓) ∈ (Base‘(𝑅 ↑s (Base‘𝑅)))) |
79 | 70, 60, 71, 72, 73, 78 | pwselbas 16865 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑅 ∈ IDomn ∧ (𝑓 ∈ 𝐵 ∧ (𝐷‘𝑓) = 0)) → (𝑂‘𝑓):(Base‘𝑅)⟶(Base‘𝑅)) |
80 | | ffn 6504 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑂‘𝑓):(Base‘𝑅)⟶(Base‘𝑅) → (𝑂‘𝑓) Fn (Base‘𝑅)) |
81 | | fniniseg 6837 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑂‘𝑓) Fn (Base‘𝑅) → (𝑥 ∈ (◡(𝑂‘𝑓) “ {𝑊}) ↔ (𝑥 ∈ (Base‘𝑅) ∧ ((𝑂‘𝑓)‘𝑥) = 𝑊))) |
82 | 79, 80, 81 | 3syl 18 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑅 ∈ IDomn ∧ (𝑓 ∈ 𝐵 ∧ (𝐷‘𝑓) = 0)) → (𝑥 ∈ (◡(𝑂‘𝑓) “ {𝑊}) ↔ (𝑥 ∈ (Base‘𝑅) ∧ ((𝑂‘𝑓)‘𝑥) = 𝑊))) |
83 | 82 | simplbda 503 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑅 ∈ IDomn ∧ (𝑓 ∈ 𝐵 ∧ (𝐷‘𝑓) = 0)) ∧ 𝑥 ∈ (◡(𝑂‘𝑓) “ {𝑊})) → ((𝑂‘𝑓)‘𝑥) = 𝑊) |
84 | 82 | simprbda 502 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑅 ∈ IDomn ∧ (𝑓 ∈ 𝐵 ∧ (𝐷‘𝑓) = 0)) ∧ 𝑥 ∈ (◡(𝑂‘𝑓) “ {𝑊})) → 𝑥 ∈ (Base‘𝑅)) |
85 | | fvex 6687 |
. . . . . . . . . . . . . . . . . . 19
⊢
((coe1‘𝑓)‘0) ∈ V |
86 | 85 | fvconst2 6976 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ (Base‘𝑅) → (((Base‘𝑅) ×
{((coe1‘𝑓)‘0)})‘𝑥) = ((coe1‘𝑓)‘0)) |
87 | 84, 86 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑅 ∈ IDomn ∧ (𝑓 ∈ 𝐵 ∧ (𝐷‘𝑓) = 0)) ∧ 𝑥 ∈ (◡(𝑂‘𝑓) “ {𝑊})) → (((Base‘𝑅) × {((coe1‘𝑓)‘0)})‘𝑥) =
((coe1‘𝑓)‘0)) |
88 | 69, 83, 87 | 3eqtr3rd 2782 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑅 ∈ IDomn ∧ (𝑓 ∈ 𝐵 ∧ (𝐷‘𝑓) = 0)) ∧ 𝑥 ∈ (◡(𝑂‘𝑓) “ {𝑊})) → ((coe1‘𝑓)‘0) = 𝑊) |
89 | 88 | fveq2d 6678 |
. . . . . . . . . . . . . . 15
⊢ (((𝑅 ∈ IDomn ∧ (𝑓 ∈ 𝐵 ∧ (𝐷‘𝑓) = 0)) ∧ 𝑥 ∈ (◡(𝑂‘𝑓) “ {𝑊})) → ((algSc‘𝑃)‘((coe1‘𝑓)‘0)) =
((algSc‘𝑃)‘𝑊)) |
90 | | fta1g.w |
. . . . . . . . . . . . . . . . 17
⊢ 𝑊 = (0g‘𝑅) |
91 | 18, 52, 90, 19 | ply1scl0 21065 |
. . . . . . . . . . . . . . . 16
⊢ (𝑅 ∈ Ring →
((algSc‘𝑃)‘𝑊) = 0 ) |
92 | 50, 91 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (((𝑅 ∈ IDomn ∧ (𝑓 ∈ 𝐵 ∧ (𝐷‘𝑓) = 0)) ∧ 𝑥 ∈ (◡(𝑂‘𝑓) “ {𝑊})) → ((algSc‘𝑃)‘𝑊) = 0 ) |
93 | 55, 89, 92 | 3eqtrd 2777 |
. . . . . . . . . . . . . 14
⊢ (((𝑅 ∈ IDomn ∧ (𝑓 ∈ 𝐵 ∧ (𝐷‘𝑓) = 0)) ∧ 𝑥 ∈ (◡(𝑂‘𝑓) “ {𝑊})) → 𝑓 = 0 ) |
94 | 93 | ex 416 |
. . . . . . . . . . . . 13
⊢ ((𝑅 ∈ IDomn ∧ (𝑓 ∈ 𝐵 ∧ (𝐷‘𝑓) = 0)) → (𝑥 ∈ (◡(𝑂‘𝑓) “ {𝑊}) → 𝑓 = 0 )) |
95 | 94 | necon3ad 2947 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ IDomn ∧ (𝑓 ∈ 𝐵 ∧ (𝐷‘𝑓) = 0)) → (𝑓 ≠ 0 → ¬ 𝑥 ∈ (◡(𝑂‘𝑓) “ {𝑊}))) |
96 | 46, 95 | mpd 15 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ IDomn ∧ (𝑓 ∈ 𝐵 ∧ (𝐷‘𝑓) = 0)) → ¬ 𝑥 ∈ (◡(𝑂‘𝑓) “ {𝑊})) |
97 | 96 | eq0rdv 4293 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ IDomn ∧ (𝑓 ∈ 𝐵 ∧ (𝐷‘𝑓) = 0)) → (◡(𝑂‘𝑓) “ {𝑊}) = ∅) |
98 | 97 | fveq2d 6678 |
. . . . . . . . 9
⊢ ((𝑅 ∈ IDomn ∧ (𝑓 ∈ 𝐵 ∧ (𝐷‘𝑓) = 0)) → (♯‘(◡(𝑂‘𝑓) “ {𝑊})) =
(♯‘∅)) |
99 | | hash0 13820 |
. . . . . . . . 9
⊢
(♯‘∅) = 0 |
100 | 98, 99 | eqtrdi 2789 |
. . . . . . . 8
⊢ ((𝑅 ∈ IDomn ∧ (𝑓 ∈ 𝐵 ∧ (𝐷‘𝑓) = 0)) → (♯‘(◡(𝑂‘𝑓) “ {𝑊})) = 0) |
101 | 48, 39 | breqtrrid 5068 |
. . . . . . . 8
⊢ ((𝑅 ∈ IDomn ∧ (𝑓 ∈ 𝐵 ∧ (𝐷‘𝑓) = 0)) → 0 ≤ (𝐷‘𝑓)) |
102 | 100, 101 | eqbrtrd 5052 |
. . . . . . 7
⊢ ((𝑅 ∈ IDomn ∧ (𝑓 ∈ 𝐵 ∧ (𝐷‘𝑓) = 0)) → (♯‘(◡(𝑂‘𝑓) “ {𝑊})) ≤ (𝐷‘𝑓)) |
103 | 102 | expr 460 |
. . . . . 6
⊢ ((𝑅 ∈ IDomn ∧ 𝑓 ∈ 𝐵) → ((𝐷‘𝑓) = 0 → (♯‘(◡(𝑂‘𝑓) “ {𝑊})) ≤ (𝐷‘𝑓))) |
104 | 103 | ralrimiva 3096 |
. . . . 5
⊢ (𝑅 ∈ IDomn →
∀𝑓 ∈ 𝐵 ((𝐷‘𝑓) = 0 → (♯‘(◡(𝑂‘𝑓) “ {𝑊})) ≤ (𝐷‘𝑓))) |
105 | | fveqeq2 6683 |
. . . . . . . . . 10
⊢ (𝑓 = 𝑔 → ((𝐷‘𝑓) = 𝑑 ↔ (𝐷‘𝑔) = 𝑑)) |
106 | | fveq2 6674 |
. . . . . . . . . . . . . 14
⊢ (𝑓 = 𝑔 → (𝑂‘𝑓) = (𝑂‘𝑔)) |
107 | 106 | cnveqd 5718 |
. . . . . . . . . . . . 13
⊢ (𝑓 = 𝑔 → ◡(𝑂‘𝑓) = ◡(𝑂‘𝑔)) |
108 | 107 | imaeq1d 5902 |
. . . . . . . . . . . 12
⊢ (𝑓 = 𝑔 → (◡(𝑂‘𝑓) “ {𝑊}) = (◡(𝑂‘𝑔) “ {𝑊})) |
109 | 108 | fveq2d 6678 |
. . . . . . . . . . 11
⊢ (𝑓 = 𝑔 → (♯‘(◡(𝑂‘𝑓) “ {𝑊})) = (♯‘(◡(𝑂‘𝑔) “ {𝑊}))) |
110 | | fveq2 6674 |
. . . . . . . . . . 11
⊢ (𝑓 = 𝑔 → (𝐷‘𝑓) = (𝐷‘𝑔)) |
111 | 109, 110 | breq12d 5043 |
. . . . . . . . . 10
⊢ (𝑓 = 𝑔 → ((♯‘(◡(𝑂‘𝑓) “ {𝑊})) ≤ (𝐷‘𝑓) ↔ (♯‘(◡(𝑂‘𝑔) “ {𝑊})) ≤ (𝐷‘𝑔))) |
112 | 105, 111 | imbi12d 348 |
. . . . . . . . 9
⊢ (𝑓 = 𝑔 → (((𝐷‘𝑓) = 𝑑 → (♯‘(◡(𝑂‘𝑓) “ {𝑊})) ≤ (𝐷‘𝑓)) ↔ ((𝐷‘𝑔) = 𝑑 → (♯‘(◡(𝑂‘𝑔) “ {𝑊})) ≤ (𝐷‘𝑔)))) |
113 | 112 | cbvralvw 3349 |
. . . . . . . 8
⊢
(∀𝑓 ∈
𝐵 ((𝐷‘𝑓) = 𝑑 → (♯‘(◡(𝑂‘𝑓) “ {𝑊})) ≤ (𝐷‘𝑓)) ↔ ∀𝑔 ∈ 𝐵 ((𝐷‘𝑔) = 𝑑 → (♯‘(◡(𝑂‘𝑔) “ {𝑊})) ≤ (𝐷‘𝑔))) |
114 | | simprr 773 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑅 ∈ IDomn ∧ 𝑑 ∈ ℕ0)
∧ (𝑓 ∈ 𝐵 ∧ (𝐷‘𝑓) = (𝑑 + 1))) → (𝐷‘𝑓) = (𝑑 + 1)) |
115 | | peano2nn0 12016 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑑 ∈ ℕ0
→ (𝑑 + 1) ∈
ℕ0) |
116 | 115 | ad2antlr 727 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑅 ∈ IDomn ∧ 𝑑 ∈ ℕ0)
∧ (𝑓 ∈ 𝐵 ∧ (𝐷‘𝑓) = (𝑑 + 1))) → (𝑑 + 1) ∈
ℕ0) |
117 | 114, 116 | eqeltrd 2833 |
. . . . . . . . . . . . . . 15
⊢ (((𝑅 ∈ IDomn ∧ 𝑑 ∈ ℕ0)
∧ (𝑓 ∈ 𝐵 ∧ (𝐷‘𝑓) = (𝑑 + 1))) → (𝐷‘𝑓) ∈
ℕ0) |
118 | 117 | nn0ge0d 12039 |
. . . . . . . . . . . . . 14
⊢ (((𝑅 ∈ IDomn ∧ 𝑑 ∈ ℕ0)
∧ (𝑓 ∈ 𝐵 ∧ (𝐷‘𝑓) = (𝑑 + 1))) → 0 ≤ (𝐷‘𝑓)) |
119 | | fveq2 6674 |
. . . . . . . . . . . . . . . 16
⊢ ((◡(𝑂‘𝑓) “ {𝑊}) = ∅ → (♯‘(◡(𝑂‘𝑓) “ {𝑊})) =
(♯‘∅)) |
120 | 119, 99 | eqtrdi 2789 |
. . . . . . . . . . . . . . 15
⊢ ((◡(𝑂‘𝑓) “ {𝑊}) = ∅ → (♯‘(◡(𝑂‘𝑓) “ {𝑊})) = 0) |
121 | 120 | breq1d 5040 |
. . . . . . . . . . . . . 14
⊢ ((◡(𝑂‘𝑓) “ {𝑊}) = ∅ → ((♯‘(◡(𝑂‘𝑓) “ {𝑊})) ≤ (𝐷‘𝑓) ↔ 0 ≤ (𝐷‘𝑓))) |
122 | 118, 121 | syl5ibrcom 250 |
. . . . . . . . . . . . 13
⊢ (((𝑅 ∈ IDomn ∧ 𝑑 ∈ ℕ0)
∧ (𝑓 ∈ 𝐵 ∧ (𝐷‘𝑓) = (𝑑 + 1))) → ((◡(𝑂‘𝑓) “ {𝑊}) = ∅ → (♯‘(◡(𝑂‘𝑓) “ {𝑊})) ≤ (𝐷‘𝑓))) |
123 | 122 | a1dd 50 |
. . . . . . . . . . . 12
⊢ (((𝑅 ∈ IDomn ∧ 𝑑 ∈ ℕ0)
∧ (𝑓 ∈ 𝐵 ∧ (𝐷‘𝑓) = (𝑑 + 1))) → ((◡(𝑂‘𝑓) “ {𝑊}) = ∅ → (∀𝑔 ∈ 𝐵 ((𝐷‘𝑔) = 𝑑 → (♯‘(◡(𝑂‘𝑔) “ {𝑊})) ≤ (𝐷‘𝑔)) → (♯‘(◡(𝑂‘𝑓) “ {𝑊})) ≤ (𝐷‘𝑓)))) |
124 | | n0 4235 |
. . . . . . . . . . . . 13
⊢ ((◡(𝑂‘𝑓) “ {𝑊}) ≠ ∅ ↔ ∃𝑥 𝑥 ∈ (◡(𝑂‘𝑓) “ {𝑊})) |
125 | | simplll 775 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑅 ∈ IDomn ∧ 𝑑 ∈ ℕ0)
∧ (𝑓 ∈ 𝐵 ∧ (𝐷‘𝑓) = (𝑑 + 1))) ∧ (𝑥 ∈ (◡(𝑂‘𝑓) “ {𝑊}) ∧ ∀𝑔 ∈ 𝐵 ((𝐷‘𝑔) = 𝑑 → (♯‘(◡(𝑂‘𝑔) “ {𝑊})) ≤ (𝐷‘𝑔)))) → 𝑅 ∈ IDomn) |
126 | | simplrl 777 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑅 ∈ IDomn ∧ 𝑑 ∈ ℕ0)
∧ (𝑓 ∈ 𝐵 ∧ (𝐷‘𝑓) = (𝑑 + 1))) ∧ (𝑥 ∈ (◡(𝑂‘𝑓) “ {𝑊}) ∧ ∀𝑔 ∈ 𝐵 ((𝐷‘𝑔) = 𝑑 → (♯‘(◡(𝑂‘𝑔) “ {𝑊})) ≤ (𝐷‘𝑔)))) → 𝑓 ∈ 𝐵) |
127 | | eqid 2738 |
. . . . . . . . . . . . . . . 16
⊢
(var1‘𝑅) = (var1‘𝑅) |
128 | | eqid 2738 |
. . . . . . . . . . . . . . . 16
⊢
(-g‘𝑃) = (-g‘𝑃) |
129 | | eqid 2738 |
. . . . . . . . . . . . . . . 16
⊢
((var1‘𝑅)(-g‘𝑃)((algSc‘𝑃)‘𝑥)) = ((var1‘𝑅)(-g‘𝑃)((algSc‘𝑃)‘𝑥)) |
130 | | simpllr 776 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑅 ∈ IDomn ∧ 𝑑 ∈ ℕ0)
∧ (𝑓 ∈ 𝐵 ∧ (𝐷‘𝑓) = (𝑑 + 1))) ∧ (𝑥 ∈ (◡(𝑂‘𝑓) “ {𝑊}) ∧ ∀𝑔 ∈ 𝐵 ((𝐷‘𝑔) = 𝑑 → (♯‘(◡(𝑂‘𝑔) “ {𝑊})) ≤ (𝐷‘𝑔)))) → 𝑑 ∈ ℕ0) |
131 | | simplrr 778 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑅 ∈ IDomn ∧ 𝑑 ∈ ℕ0)
∧ (𝑓 ∈ 𝐵 ∧ (𝐷‘𝑓) = (𝑑 + 1))) ∧ (𝑥 ∈ (◡(𝑂‘𝑓) “ {𝑊}) ∧ ∀𝑔 ∈ 𝐵 ((𝐷‘𝑔) = 𝑑 → (♯‘(◡(𝑂‘𝑔) “ {𝑊})) ≤ (𝐷‘𝑔)))) → (𝐷‘𝑓) = (𝑑 + 1)) |
132 | | simprl 771 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑅 ∈ IDomn ∧ 𝑑 ∈ ℕ0)
∧ (𝑓 ∈ 𝐵 ∧ (𝐷‘𝑓) = (𝑑 + 1))) ∧ (𝑥 ∈ (◡(𝑂‘𝑓) “ {𝑊}) ∧ ∀𝑔 ∈ 𝐵 ((𝐷‘𝑔) = 𝑑 → (♯‘(◡(𝑂‘𝑔) “ {𝑊})) ≤ (𝐷‘𝑔)))) → 𝑥 ∈ (◡(𝑂‘𝑓) “ {𝑊})) |
133 | | simprr 773 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑅 ∈ IDomn ∧ 𝑑 ∈ ℕ0)
∧ (𝑓 ∈ 𝐵 ∧ (𝐷‘𝑓) = (𝑑 + 1))) ∧ (𝑥 ∈ (◡(𝑂‘𝑓) “ {𝑊}) ∧ ∀𝑔 ∈ 𝐵 ((𝐷‘𝑔) = 𝑑 → (♯‘(◡(𝑂‘𝑔) “ {𝑊})) ≤ (𝐷‘𝑔)))) → ∀𝑔 ∈ 𝐵 ((𝐷‘𝑔) = 𝑑 → (♯‘(◡(𝑂‘𝑔) “ {𝑊})) ≤ (𝐷‘𝑔))) |
134 | 18, 20, 17, 65, 90, 19, 125, 126, 60, 127, 128, 52, 129, 130, 131, 132, 133 | fta1glem2 24919 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑅 ∈ IDomn ∧ 𝑑 ∈ ℕ0)
∧ (𝑓 ∈ 𝐵 ∧ (𝐷‘𝑓) = (𝑑 + 1))) ∧ (𝑥 ∈ (◡(𝑂‘𝑓) “ {𝑊}) ∧ ∀𝑔 ∈ 𝐵 ((𝐷‘𝑔) = 𝑑 → (♯‘(◡(𝑂‘𝑔) “ {𝑊})) ≤ (𝐷‘𝑔)))) → (♯‘(◡(𝑂‘𝑓) “ {𝑊})) ≤ (𝐷‘𝑓)) |
135 | 134 | exp32 424 |
. . . . . . . . . . . . . 14
⊢ (((𝑅 ∈ IDomn ∧ 𝑑 ∈ ℕ0)
∧ (𝑓 ∈ 𝐵 ∧ (𝐷‘𝑓) = (𝑑 + 1))) → (𝑥 ∈ (◡(𝑂‘𝑓) “ {𝑊}) → (∀𝑔 ∈ 𝐵 ((𝐷‘𝑔) = 𝑑 → (♯‘(◡(𝑂‘𝑔) “ {𝑊})) ≤ (𝐷‘𝑔)) → (♯‘(◡(𝑂‘𝑓) “ {𝑊})) ≤ (𝐷‘𝑓)))) |
136 | 135 | exlimdv 1940 |
. . . . . . . . . . . . 13
⊢ (((𝑅 ∈ IDomn ∧ 𝑑 ∈ ℕ0)
∧ (𝑓 ∈ 𝐵 ∧ (𝐷‘𝑓) = (𝑑 + 1))) → (∃𝑥 𝑥 ∈ (◡(𝑂‘𝑓) “ {𝑊}) → (∀𝑔 ∈ 𝐵 ((𝐷‘𝑔) = 𝑑 → (♯‘(◡(𝑂‘𝑔) “ {𝑊})) ≤ (𝐷‘𝑔)) → (♯‘(◡(𝑂‘𝑓) “ {𝑊})) ≤ (𝐷‘𝑓)))) |
137 | 124, 136 | syl5bi 245 |
. . . . . . . . . . . 12
⊢ (((𝑅 ∈ IDomn ∧ 𝑑 ∈ ℕ0)
∧ (𝑓 ∈ 𝐵 ∧ (𝐷‘𝑓) = (𝑑 + 1))) → ((◡(𝑂‘𝑓) “ {𝑊}) ≠ ∅ → (∀𝑔 ∈ 𝐵 ((𝐷‘𝑔) = 𝑑 → (♯‘(◡(𝑂‘𝑔) “ {𝑊})) ≤ (𝐷‘𝑔)) → (♯‘(◡(𝑂‘𝑓) “ {𝑊})) ≤ (𝐷‘𝑓)))) |
138 | 123, 137 | pm2.61dne 3020 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ IDomn ∧ 𝑑 ∈ ℕ0)
∧ (𝑓 ∈ 𝐵 ∧ (𝐷‘𝑓) = (𝑑 + 1))) → (∀𝑔 ∈ 𝐵 ((𝐷‘𝑔) = 𝑑 → (♯‘(◡(𝑂‘𝑔) “ {𝑊})) ≤ (𝐷‘𝑔)) → (♯‘(◡(𝑂‘𝑓) “ {𝑊})) ≤ (𝐷‘𝑓))) |
139 | 138 | expr 460 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ IDomn ∧ 𝑑 ∈ ℕ0)
∧ 𝑓 ∈ 𝐵) → ((𝐷‘𝑓) = (𝑑 + 1) → (∀𝑔 ∈ 𝐵 ((𝐷‘𝑔) = 𝑑 → (♯‘(◡(𝑂‘𝑔) “ {𝑊})) ≤ (𝐷‘𝑔)) → (♯‘(◡(𝑂‘𝑓) “ {𝑊})) ≤ (𝐷‘𝑓)))) |
140 | 139 | com23 86 |
. . . . . . . . 9
⊢ (((𝑅 ∈ IDomn ∧ 𝑑 ∈ ℕ0)
∧ 𝑓 ∈ 𝐵) → (∀𝑔 ∈ 𝐵 ((𝐷‘𝑔) = 𝑑 → (♯‘(◡(𝑂‘𝑔) “ {𝑊})) ≤ (𝐷‘𝑔)) → ((𝐷‘𝑓) = (𝑑 + 1) → (♯‘(◡(𝑂‘𝑓) “ {𝑊})) ≤ (𝐷‘𝑓)))) |
141 | 140 | ralrimdva 3101 |
. . . . . . . 8
⊢ ((𝑅 ∈ IDomn ∧ 𝑑 ∈ ℕ0)
→ (∀𝑔 ∈
𝐵 ((𝐷‘𝑔) = 𝑑 → (♯‘(◡(𝑂‘𝑔) “ {𝑊})) ≤ (𝐷‘𝑔)) → ∀𝑓 ∈ 𝐵 ((𝐷‘𝑓) = (𝑑 + 1) → (♯‘(◡(𝑂‘𝑓) “ {𝑊})) ≤ (𝐷‘𝑓)))) |
142 | 113, 141 | syl5bi 245 |
. . . . . . 7
⊢ ((𝑅 ∈ IDomn ∧ 𝑑 ∈ ℕ0)
→ (∀𝑓 ∈
𝐵 ((𝐷‘𝑓) = 𝑑 → (♯‘(◡(𝑂‘𝑓) “ {𝑊})) ≤ (𝐷‘𝑓)) → ∀𝑓 ∈ 𝐵 ((𝐷‘𝑓) = (𝑑 + 1) → (♯‘(◡(𝑂‘𝑓) “ {𝑊})) ≤ (𝐷‘𝑓)))) |
143 | 142 | expcom 417 |
. . . . . 6
⊢ (𝑑 ∈ ℕ0
→ (𝑅 ∈ IDomn
→ (∀𝑓 ∈
𝐵 ((𝐷‘𝑓) = 𝑑 → (♯‘(◡(𝑂‘𝑓) “ {𝑊})) ≤ (𝐷‘𝑓)) → ∀𝑓 ∈ 𝐵 ((𝐷‘𝑓) = (𝑑 + 1) → (♯‘(◡(𝑂‘𝑓) “ {𝑊})) ≤ (𝐷‘𝑓))))) |
144 | 143 | a2d 29 |
. . . . 5
⊢ (𝑑 ∈ ℕ0
→ ((𝑅 ∈ IDomn
→ ∀𝑓 ∈
𝐵 ((𝐷‘𝑓) = 𝑑 → (♯‘(◡(𝑂‘𝑓) “ {𝑊})) ≤ (𝐷‘𝑓))) → (𝑅 ∈ IDomn → ∀𝑓 ∈ 𝐵 ((𝐷‘𝑓) = (𝑑 + 1) → (♯‘(◡(𝑂‘𝑓) “ {𝑊})) ≤ (𝐷‘𝑓))))) |
145 | 26, 30, 34, 38, 104, 144 | nn0ind 12158 |
. . . 4
⊢ ((𝐷‘𝐹) ∈ ℕ0 → (𝑅 ∈ IDomn →
∀𝑓 ∈ 𝐵 ((𝐷‘𝑓) = (𝐷‘𝐹) → (♯‘(◡(𝑂‘𝑓) “ {𝑊})) ≤ (𝐷‘𝑓)))) |
146 | 22, 10, 145 | sylc 65 |
. . 3
⊢ (𝜑 → ∀𝑓 ∈ 𝐵 ((𝐷‘𝑓) = (𝐷‘𝐹) → (♯‘(◡(𝑂‘𝑓) “ {𝑊})) ≤ (𝐷‘𝑓))) |
147 | 9, 146, 15 | rspcdva 3528 |
. 2
⊢ (𝜑 → ((𝐷‘𝐹) = (𝐷‘𝐹) → (♯‘(◡(𝑂‘𝐹) “ {𝑊})) ≤ (𝐷‘𝐹))) |
148 | 1, 147 | mpi 20 |
1
⊢ (𝜑 → (♯‘(◡(𝑂‘𝐹) “ {𝑊})) ≤ (𝐷‘𝐹)) |