Step | Hyp | Ref
| Expression |
1 | | eqid 2610 |
. 2
⊢ (𝐷‘𝐹) = (𝐷‘𝐹) |
2 | | fta1g.2 |
. . 3
⊢ (𝜑 → 𝐹 ∈ 𝐵) |
3 | | fta1g.1 |
. . . . . 6
⊢ (𝜑 → 𝑅 ∈ IDomn) |
4 | | isidom 19125 |
. . . . . . 7
⊢ (𝑅 ∈ IDomn ↔ (𝑅 ∈ CRing ∧ 𝑅 ∈ Domn)) |
5 | 4 | simplbi 475 |
. . . . . 6
⊢ (𝑅 ∈ IDomn → 𝑅 ∈ CRing) |
6 | | crngring 18381 |
. . . . . 6
⊢ (𝑅 ∈ CRing → 𝑅 ∈ Ring) |
7 | 3, 5, 6 | 3syl 18 |
. . . . 5
⊢ (𝜑 → 𝑅 ∈ Ring) |
8 | | fta1g.3 |
. . . . 5
⊢ (𝜑 → 𝐹 ≠ 0 ) |
9 | | fta1g.d |
. . . . . 6
⊢ 𝐷 = ( deg1
‘𝑅) |
10 | | fta1g.p |
. . . . . 6
⊢ 𝑃 = (Poly1‘𝑅) |
11 | | fta1g.z |
. . . . . 6
⊢ 0 =
(0g‘𝑃) |
12 | | fta1g.b |
. . . . . 6
⊢ 𝐵 = (Base‘𝑃) |
13 | 9, 10, 11, 12 | deg1nn0cl 23652 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 0 ) → (𝐷‘𝐹) ∈
ℕ0) |
14 | 7, 2, 8, 13 | syl3anc 1318 |
. . . 4
⊢ (𝜑 → (𝐷‘𝐹) ∈
ℕ0) |
15 | | eqeq2 2621 |
. . . . . . . 8
⊢ (𝑥 = 0 → ((𝐷‘𝑓) = 𝑥 ↔ (𝐷‘𝑓) = 0)) |
16 | 15 | imbi1d 330 |
. . . . . . 7
⊢ (𝑥 = 0 → (((𝐷‘𝑓) = 𝑥 → (#‘(◡(𝑂‘𝑓) “ {𝑊})) ≤ (𝐷‘𝑓)) ↔ ((𝐷‘𝑓) = 0 → (#‘(◡(𝑂‘𝑓) “ {𝑊})) ≤ (𝐷‘𝑓)))) |
17 | 16 | ralbidv 2969 |
. . . . . 6
⊢ (𝑥 = 0 → (∀𝑓 ∈ 𝐵 ((𝐷‘𝑓) = 𝑥 → (#‘(◡(𝑂‘𝑓) “ {𝑊})) ≤ (𝐷‘𝑓)) ↔ ∀𝑓 ∈ 𝐵 ((𝐷‘𝑓) = 0 → (#‘(◡(𝑂‘𝑓) “ {𝑊})) ≤ (𝐷‘𝑓)))) |
18 | 17 | imbi2d 329 |
. . . . 5
⊢ (𝑥 = 0 → ((𝑅 ∈ IDomn → ∀𝑓 ∈ 𝐵 ((𝐷‘𝑓) = 𝑥 → (#‘(◡(𝑂‘𝑓) “ {𝑊})) ≤ (𝐷‘𝑓))) ↔ (𝑅 ∈ IDomn → ∀𝑓 ∈ 𝐵 ((𝐷‘𝑓) = 0 → (#‘(◡(𝑂‘𝑓) “ {𝑊})) ≤ (𝐷‘𝑓))))) |
19 | | eqeq2 2621 |
. . . . . . . 8
⊢ (𝑥 = 𝑑 → ((𝐷‘𝑓) = 𝑥 ↔ (𝐷‘𝑓) = 𝑑)) |
20 | 19 | imbi1d 330 |
. . . . . . 7
⊢ (𝑥 = 𝑑 → (((𝐷‘𝑓) = 𝑥 → (#‘(◡(𝑂‘𝑓) “ {𝑊})) ≤ (𝐷‘𝑓)) ↔ ((𝐷‘𝑓) = 𝑑 → (#‘(◡(𝑂‘𝑓) “ {𝑊})) ≤ (𝐷‘𝑓)))) |
21 | 20 | ralbidv 2969 |
. . . . . 6
⊢ (𝑥 = 𝑑 → (∀𝑓 ∈ 𝐵 ((𝐷‘𝑓) = 𝑥 → (#‘(◡(𝑂‘𝑓) “ {𝑊})) ≤ (𝐷‘𝑓)) ↔ ∀𝑓 ∈ 𝐵 ((𝐷‘𝑓) = 𝑑 → (#‘(◡(𝑂‘𝑓) “ {𝑊})) ≤ (𝐷‘𝑓)))) |
22 | 21 | imbi2d 329 |
. . . . 5
⊢ (𝑥 = 𝑑 → ((𝑅 ∈ IDomn → ∀𝑓 ∈ 𝐵 ((𝐷‘𝑓) = 𝑥 → (#‘(◡(𝑂‘𝑓) “ {𝑊})) ≤ (𝐷‘𝑓))) ↔ (𝑅 ∈ IDomn → ∀𝑓 ∈ 𝐵 ((𝐷‘𝑓) = 𝑑 → (#‘(◡(𝑂‘𝑓) “ {𝑊})) ≤ (𝐷‘𝑓))))) |
23 | | eqeq2 2621 |
. . . . . . . 8
⊢ (𝑥 = (𝑑 + 1) → ((𝐷‘𝑓) = 𝑥 ↔ (𝐷‘𝑓) = (𝑑 + 1))) |
24 | 23 | imbi1d 330 |
. . . . . . 7
⊢ (𝑥 = (𝑑 + 1) → (((𝐷‘𝑓) = 𝑥 → (#‘(◡(𝑂‘𝑓) “ {𝑊})) ≤ (𝐷‘𝑓)) ↔ ((𝐷‘𝑓) = (𝑑 + 1) → (#‘(◡(𝑂‘𝑓) “ {𝑊})) ≤ (𝐷‘𝑓)))) |
25 | 24 | ralbidv 2969 |
. . . . . 6
⊢ (𝑥 = (𝑑 + 1) → (∀𝑓 ∈ 𝐵 ((𝐷‘𝑓) = 𝑥 → (#‘(◡(𝑂‘𝑓) “ {𝑊})) ≤ (𝐷‘𝑓)) ↔ ∀𝑓 ∈ 𝐵 ((𝐷‘𝑓) = (𝑑 + 1) → (#‘(◡(𝑂‘𝑓) “ {𝑊})) ≤ (𝐷‘𝑓)))) |
26 | 25 | imbi2d 329 |
. . . . 5
⊢ (𝑥 = (𝑑 + 1) → ((𝑅 ∈ IDomn → ∀𝑓 ∈ 𝐵 ((𝐷‘𝑓) = 𝑥 → (#‘(◡(𝑂‘𝑓) “ {𝑊})) ≤ (𝐷‘𝑓))) ↔ (𝑅 ∈ IDomn → ∀𝑓 ∈ 𝐵 ((𝐷‘𝑓) = (𝑑 + 1) → (#‘(◡(𝑂‘𝑓) “ {𝑊})) ≤ (𝐷‘𝑓))))) |
27 | | eqeq2 2621 |
. . . . . . . 8
⊢ (𝑥 = (𝐷‘𝐹) → ((𝐷‘𝑓) = 𝑥 ↔ (𝐷‘𝑓) = (𝐷‘𝐹))) |
28 | 27 | imbi1d 330 |
. . . . . . 7
⊢ (𝑥 = (𝐷‘𝐹) → (((𝐷‘𝑓) = 𝑥 → (#‘(◡(𝑂‘𝑓) “ {𝑊})) ≤ (𝐷‘𝑓)) ↔ ((𝐷‘𝑓) = (𝐷‘𝐹) → (#‘(◡(𝑂‘𝑓) “ {𝑊})) ≤ (𝐷‘𝑓)))) |
29 | 28 | ralbidv 2969 |
. . . . . 6
⊢ (𝑥 = (𝐷‘𝐹) → (∀𝑓 ∈ 𝐵 ((𝐷‘𝑓) = 𝑥 → (#‘(◡(𝑂‘𝑓) “ {𝑊})) ≤ (𝐷‘𝑓)) ↔ ∀𝑓 ∈ 𝐵 ((𝐷‘𝑓) = (𝐷‘𝐹) → (#‘(◡(𝑂‘𝑓) “ {𝑊})) ≤ (𝐷‘𝑓)))) |
30 | 29 | imbi2d 329 |
. . . . 5
⊢ (𝑥 = (𝐷‘𝐹) → ((𝑅 ∈ IDomn → ∀𝑓 ∈ 𝐵 ((𝐷‘𝑓) = 𝑥 → (#‘(◡(𝑂‘𝑓) “ {𝑊})) ≤ (𝐷‘𝑓))) ↔ (𝑅 ∈ IDomn → ∀𝑓 ∈ 𝐵 ((𝐷‘𝑓) = (𝐷‘𝐹) → (#‘(◡(𝑂‘𝑓) “ {𝑊})) ≤ (𝐷‘𝑓))))) |
31 | | simprr 792 |
. . . . . . . . . . . . . 14
⊢ ((𝑅 ∈ IDomn ∧ (𝑓 ∈ 𝐵 ∧ (𝐷‘𝑓) = 0)) → (𝐷‘𝑓) = 0) |
32 | | 0nn0 11184 |
. . . . . . . . . . . . . 14
⊢ 0 ∈
ℕ0 |
33 | 31, 32 | syl6eqel 2696 |
. . . . . . . . . . . . 13
⊢ ((𝑅 ∈ IDomn ∧ (𝑓 ∈ 𝐵 ∧ (𝐷‘𝑓) = 0)) → (𝐷‘𝑓) ∈
ℕ0) |
34 | 5, 6 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝑅 ∈ IDomn → 𝑅 ∈ Ring) |
35 | | simpl 472 |
. . . . . . . . . . . . . 14
⊢ ((𝑓 ∈ 𝐵 ∧ (𝐷‘𝑓) = 0) → 𝑓 ∈ 𝐵) |
36 | 9, 10, 11, 12 | deg1nn0clb 23654 |
. . . . . . . . . . . . . 14
⊢ ((𝑅 ∈ Ring ∧ 𝑓 ∈ 𝐵) → (𝑓 ≠ 0 ↔ (𝐷‘𝑓) ∈
ℕ0)) |
37 | 34, 35, 36 | syl2an 493 |
. . . . . . . . . . . . 13
⊢ ((𝑅 ∈ IDomn ∧ (𝑓 ∈ 𝐵 ∧ (𝐷‘𝑓) = 0)) → (𝑓 ≠ 0 ↔ (𝐷‘𝑓) ∈
ℕ0)) |
38 | 33, 37 | mpbird 246 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ IDomn ∧ (𝑓 ∈ 𝐵 ∧ (𝐷‘𝑓) = 0)) → 𝑓 ≠ 0 ) |
39 | | simplrr 797 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑅 ∈ IDomn ∧ (𝑓 ∈ 𝐵 ∧ (𝐷‘𝑓) = 0)) ∧ 𝑥 ∈ (◡(𝑂‘𝑓) “ {𝑊})) → (𝐷‘𝑓) = 0) |
40 | | 0le0 10987 |
. . . . . . . . . . . . . . . . 17
⊢ 0 ≤
0 |
41 | 39, 40 | syl6eqbr 4622 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑅 ∈ IDomn ∧ (𝑓 ∈ 𝐵 ∧ (𝐷‘𝑓) = 0)) ∧ 𝑥 ∈ (◡(𝑂‘𝑓) “ {𝑊})) → (𝐷‘𝑓) ≤ 0) |
42 | 34 | ad2antrr 758 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑅 ∈ IDomn ∧ (𝑓 ∈ 𝐵 ∧ (𝐷‘𝑓) = 0)) ∧ 𝑥 ∈ (◡(𝑂‘𝑓) “ {𝑊})) → 𝑅 ∈ Ring) |
43 | | simplrl 796 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑅 ∈ IDomn ∧ (𝑓 ∈ 𝐵 ∧ (𝐷‘𝑓) = 0)) ∧ 𝑥 ∈ (◡(𝑂‘𝑓) “ {𝑊})) → 𝑓 ∈ 𝐵) |
44 | | eqid 2610 |
. . . . . . . . . . . . . . . . . 18
⊢
(algSc‘𝑃) =
(algSc‘𝑃) |
45 | 9, 10, 12, 44 | deg1le0 23675 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑅 ∈ Ring ∧ 𝑓 ∈ 𝐵) → ((𝐷‘𝑓) ≤ 0 ↔ 𝑓 = ((algSc‘𝑃)‘((coe1‘𝑓)‘0)))) |
46 | 42, 43, 45 | syl2anc 691 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑅 ∈ IDomn ∧ (𝑓 ∈ 𝐵 ∧ (𝐷‘𝑓) = 0)) ∧ 𝑥 ∈ (◡(𝑂‘𝑓) “ {𝑊})) → ((𝐷‘𝑓) ≤ 0 ↔ 𝑓 = ((algSc‘𝑃)‘((coe1‘𝑓)‘0)))) |
47 | 41, 46 | mpbid 221 |
. . . . . . . . . . . . . . 15
⊢ (((𝑅 ∈ IDomn ∧ (𝑓 ∈ 𝐵 ∧ (𝐷‘𝑓) = 0)) ∧ 𝑥 ∈ (◡(𝑂‘𝑓) “ {𝑊})) → 𝑓 = ((algSc‘𝑃)‘((coe1‘𝑓)‘0))) |
48 | 47 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑅 ∈ IDomn ∧ (𝑓 ∈ 𝐵 ∧ (𝐷‘𝑓) = 0)) ∧ 𝑥 ∈ (◡(𝑂‘𝑓) “ {𝑊})) → (𝑂‘𝑓) = (𝑂‘((algSc‘𝑃)‘((coe1‘𝑓)‘0)))) |
49 | 5 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑅 ∈ IDomn ∧ (𝑓 ∈ 𝐵 ∧ (𝐷‘𝑓) = 0)) → 𝑅 ∈ CRing) |
50 | 49 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑅 ∈ IDomn ∧ (𝑓 ∈ 𝐵 ∧ (𝐷‘𝑓) = 0)) ∧ 𝑥 ∈ (◡(𝑂‘𝑓) “ {𝑊})) → 𝑅 ∈ CRing) |
51 | | eqid 2610 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(coe1‘𝑓) = (coe1‘𝑓) |
52 | | eqid 2610 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(Base‘𝑅) =
(Base‘𝑅) |
53 | 51, 12, 10, 52 | coe1f 19402 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑓 ∈ 𝐵 → (coe1‘𝑓):ℕ0⟶(Base‘𝑅)) |
54 | 43, 53 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑅 ∈ IDomn ∧ (𝑓 ∈ 𝐵 ∧ (𝐷‘𝑓) = 0)) ∧ 𝑥 ∈ (◡(𝑂‘𝑓) “ {𝑊})) → (coe1‘𝑓):ℕ0⟶(Base‘𝑅)) |
55 | | ffvelrn 6265 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((coe1‘𝑓):ℕ0⟶(Base‘𝑅) ∧ 0 ∈
ℕ0) → ((coe1‘𝑓)‘0) ∈ (Base‘𝑅)) |
56 | 54, 32, 55 | sylancl 693 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑅 ∈ IDomn ∧ (𝑓 ∈ 𝐵 ∧ (𝐷‘𝑓) = 0)) ∧ 𝑥 ∈ (◡(𝑂‘𝑓) “ {𝑊})) → ((coe1‘𝑓)‘0) ∈
(Base‘𝑅)) |
57 | | fta1g.o |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 𝑂 = (eval1‘𝑅) |
58 | 57, 10, 52, 44 | evl1sca 19519 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑅 ∈ CRing ∧
((coe1‘𝑓)‘0) ∈ (Base‘𝑅)) → (𝑂‘((algSc‘𝑃)‘((coe1‘𝑓)‘0))) =
((Base‘𝑅) ×
{((coe1‘𝑓)‘0)})) |
59 | 50, 56, 58 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑅 ∈ IDomn ∧ (𝑓 ∈ 𝐵 ∧ (𝐷‘𝑓) = 0)) ∧ 𝑥 ∈ (◡(𝑂‘𝑓) “ {𝑊})) → (𝑂‘((algSc‘𝑃)‘((coe1‘𝑓)‘0))) =
((Base‘𝑅) ×
{((coe1‘𝑓)‘0)})) |
60 | 48, 59 | eqtrd 2644 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑅 ∈ IDomn ∧ (𝑓 ∈ 𝐵 ∧ (𝐷‘𝑓) = 0)) ∧ 𝑥 ∈ (◡(𝑂‘𝑓) “ {𝑊})) → (𝑂‘𝑓) = ((Base‘𝑅) × {((coe1‘𝑓)‘0)})) |
61 | 60 | fveq1d 6105 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑅 ∈ IDomn ∧ (𝑓 ∈ 𝐵 ∧ (𝐷‘𝑓) = 0)) ∧ 𝑥 ∈ (◡(𝑂‘𝑓) “ {𝑊})) → ((𝑂‘𝑓)‘𝑥) = (((Base‘𝑅) × {((coe1‘𝑓)‘0)})‘𝑥)) |
62 | | eqid 2610 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑅 ↑s
(Base‘𝑅)) = (𝑅 ↑s
(Base‘𝑅)) |
63 | | eqid 2610 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(Base‘(𝑅
↑s (Base‘𝑅))) = (Base‘(𝑅 ↑s (Base‘𝑅))) |
64 | | simpl 472 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑅 ∈ IDomn ∧ (𝑓 ∈ 𝐵 ∧ (𝐷‘𝑓) = 0)) → 𝑅 ∈ IDomn) |
65 | | fvex 6113 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(Base‘𝑅)
∈ V |
66 | 65 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑅 ∈ IDomn ∧ (𝑓 ∈ 𝐵 ∧ (𝐷‘𝑓) = 0)) → (Base‘𝑅) ∈ V) |
67 | 57, 10, 62, 52 | evl1rhm 19517 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑅 ∈ CRing → 𝑂 ∈ (𝑃 RingHom (𝑅 ↑s (Base‘𝑅)))) |
68 | 12, 63 | rhmf 18549 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑂 ∈ (𝑃 RingHom (𝑅 ↑s (Base‘𝑅))) → 𝑂:𝐵⟶(Base‘(𝑅 ↑s (Base‘𝑅)))) |
69 | 49, 67, 68 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑅 ∈ IDomn ∧ (𝑓 ∈ 𝐵 ∧ (𝐷‘𝑓) = 0)) → 𝑂:𝐵⟶(Base‘(𝑅 ↑s (Base‘𝑅)))) |
70 | | simprl 790 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑅 ∈ IDomn ∧ (𝑓 ∈ 𝐵 ∧ (𝐷‘𝑓) = 0)) → 𝑓 ∈ 𝐵) |
71 | 69, 70 | ffvelrnd 6268 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑅 ∈ IDomn ∧ (𝑓 ∈ 𝐵 ∧ (𝐷‘𝑓) = 0)) → (𝑂‘𝑓) ∈ (Base‘(𝑅 ↑s (Base‘𝑅)))) |
72 | 62, 52, 63, 64, 66, 71 | pwselbas 15972 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑅 ∈ IDomn ∧ (𝑓 ∈ 𝐵 ∧ (𝐷‘𝑓) = 0)) → (𝑂‘𝑓):(Base‘𝑅)⟶(Base‘𝑅)) |
73 | | ffn 5958 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑂‘𝑓):(Base‘𝑅)⟶(Base‘𝑅) → (𝑂‘𝑓) Fn (Base‘𝑅)) |
74 | | fniniseg 6246 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑂‘𝑓) Fn (Base‘𝑅) → (𝑥 ∈ (◡(𝑂‘𝑓) “ {𝑊}) ↔ (𝑥 ∈ (Base‘𝑅) ∧ ((𝑂‘𝑓)‘𝑥) = 𝑊))) |
75 | 72, 73, 74 | 3syl 18 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑅 ∈ IDomn ∧ (𝑓 ∈ 𝐵 ∧ (𝐷‘𝑓) = 0)) → (𝑥 ∈ (◡(𝑂‘𝑓) “ {𝑊}) ↔ (𝑥 ∈ (Base‘𝑅) ∧ ((𝑂‘𝑓)‘𝑥) = 𝑊))) |
76 | 75 | simplbda 652 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑅 ∈ IDomn ∧ (𝑓 ∈ 𝐵 ∧ (𝐷‘𝑓) = 0)) ∧ 𝑥 ∈ (◡(𝑂‘𝑓) “ {𝑊})) → ((𝑂‘𝑓)‘𝑥) = 𝑊) |
77 | 75 | simprbda 651 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑅 ∈ IDomn ∧ (𝑓 ∈ 𝐵 ∧ (𝐷‘𝑓) = 0)) ∧ 𝑥 ∈ (◡(𝑂‘𝑓) “ {𝑊})) → 𝑥 ∈ (Base‘𝑅)) |
78 | | fvex 6113 |
. . . . . . . . . . . . . . . . . . 19
⊢
((coe1‘𝑓)‘0) ∈ V |
79 | 78 | fvconst2 6374 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ (Base‘𝑅) → (((Base‘𝑅) ×
{((coe1‘𝑓)‘0)})‘𝑥) = ((coe1‘𝑓)‘0)) |
80 | 77, 79 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑅 ∈ IDomn ∧ (𝑓 ∈ 𝐵 ∧ (𝐷‘𝑓) = 0)) ∧ 𝑥 ∈ (◡(𝑂‘𝑓) “ {𝑊})) → (((Base‘𝑅) × {((coe1‘𝑓)‘0)})‘𝑥) =
((coe1‘𝑓)‘0)) |
81 | 61, 76, 80 | 3eqtr3rd 2653 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑅 ∈ IDomn ∧ (𝑓 ∈ 𝐵 ∧ (𝐷‘𝑓) = 0)) ∧ 𝑥 ∈ (◡(𝑂‘𝑓) “ {𝑊})) → ((coe1‘𝑓)‘0) = 𝑊) |
82 | 81 | fveq2d 6107 |
. . . . . . . . . . . . . . 15
⊢ (((𝑅 ∈ IDomn ∧ (𝑓 ∈ 𝐵 ∧ (𝐷‘𝑓) = 0)) ∧ 𝑥 ∈ (◡(𝑂‘𝑓) “ {𝑊})) → ((algSc‘𝑃)‘((coe1‘𝑓)‘0)) =
((algSc‘𝑃)‘𝑊)) |
83 | | fta1g.w |
. . . . . . . . . . . . . . . . 17
⊢ 𝑊 = (0g‘𝑅) |
84 | 10, 44, 83, 11 | ply1scl0 19481 |
. . . . . . . . . . . . . . . 16
⊢ (𝑅 ∈ Ring →
((algSc‘𝑃)‘𝑊) = 0 ) |
85 | 42, 84 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (((𝑅 ∈ IDomn ∧ (𝑓 ∈ 𝐵 ∧ (𝐷‘𝑓) = 0)) ∧ 𝑥 ∈ (◡(𝑂‘𝑓) “ {𝑊})) → ((algSc‘𝑃)‘𝑊) = 0 ) |
86 | 47, 82, 85 | 3eqtrd 2648 |
. . . . . . . . . . . . . 14
⊢ (((𝑅 ∈ IDomn ∧ (𝑓 ∈ 𝐵 ∧ (𝐷‘𝑓) = 0)) ∧ 𝑥 ∈ (◡(𝑂‘𝑓) “ {𝑊})) → 𝑓 = 0 ) |
87 | 86 | ex 449 |
. . . . . . . . . . . . 13
⊢ ((𝑅 ∈ IDomn ∧ (𝑓 ∈ 𝐵 ∧ (𝐷‘𝑓) = 0)) → (𝑥 ∈ (◡(𝑂‘𝑓) “ {𝑊}) → 𝑓 = 0 )) |
88 | 87 | necon3ad 2795 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ IDomn ∧ (𝑓 ∈ 𝐵 ∧ (𝐷‘𝑓) = 0)) → (𝑓 ≠ 0 → ¬ 𝑥 ∈ (◡(𝑂‘𝑓) “ {𝑊}))) |
89 | 38, 88 | mpd 15 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ IDomn ∧ (𝑓 ∈ 𝐵 ∧ (𝐷‘𝑓) = 0)) → ¬ 𝑥 ∈ (◡(𝑂‘𝑓) “ {𝑊})) |
90 | 89 | eq0rdv 3931 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ IDomn ∧ (𝑓 ∈ 𝐵 ∧ (𝐷‘𝑓) = 0)) → (◡(𝑂‘𝑓) “ {𝑊}) = ∅) |
91 | 90 | fveq2d 6107 |
. . . . . . . . 9
⊢ ((𝑅 ∈ IDomn ∧ (𝑓 ∈ 𝐵 ∧ (𝐷‘𝑓) = 0)) → (#‘(◡(𝑂‘𝑓) “ {𝑊})) = (#‘∅)) |
92 | | hash0 13019 |
. . . . . . . . 9
⊢
(#‘∅) = 0 |
93 | 91, 92 | syl6eq 2660 |
. . . . . . . 8
⊢ ((𝑅 ∈ IDomn ∧ (𝑓 ∈ 𝐵 ∧ (𝐷‘𝑓) = 0)) → (#‘(◡(𝑂‘𝑓) “ {𝑊})) = 0) |
94 | 40, 31 | syl5breqr 4621 |
. . . . . . . 8
⊢ ((𝑅 ∈ IDomn ∧ (𝑓 ∈ 𝐵 ∧ (𝐷‘𝑓) = 0)) → 0 ≤ (𝐷‘𝑓)) |
95 | 93, 94 | eqbrtrd 4605 |
. . . . . . 7
⊢ ((𝑅 ∈ IDomn ∧ (𝑓 ∈ 𝐵 ∧ (𝐷‘𝑓) = 0)) → (#‘(◡(𝑂‘𝑓) “ {𝑊})) ≤ (𝐷‘𝑓)) |
96 | 95 | expr 641 |
. . . . . 6
⊢ ((𝑅 ∈ IDomn ∧ 𝑓 ∈ 𝐵) → ((𝐷‘𝑓) = 0 → (#‘(◡(𝑂‘𝑓) “ {𝑊})) ≤ (𝐷‘𝑓))) |
97 | 96 | ralrimiva 2949 |
. . . . 5
⊢ (𝑅 ∈ IDomn →
∀𝑓 ∈ 𝐵 ((𝐷‘𝑓) = 0 → (#‘(◡(𝑂‘𝑓) “ {𝑊})) ≤ (𝐷‘𝑓))) |
98 | | fveq2 6103 |
. . . . . . . . . . 11
⊢ (𝑓 = 𝑔 → (𝐷‘𝑓) = (𝐷‘𝑔)) |
99 | 98 | eqeq1d 2612 |
. . . . . . . . . 10
⊢ (𝑓 = 𝑔 → ((𝐷‘𝑓) = 𝑑 ↔ (𝐷‘𝑔) = 𝑑)) |
100 | | fveq2 6103 |
. . . . . . . . . . . . . 14
⊢ (𝑓 = 𝑔 → (𝑂‘𝑓) = (𝑂‘𝑔)) |
101 | 100 | cnveqd 5220 |
. . . . . . . . . . . . 13
⊢ (𝑓 = 𝑔 → ◡(𝑂‘𝑓) = ◡(𝑂‘𝑔)) |
102 | 101 | imaeq1d 5384 |
. . . . . . . . . . . 12
⊢ (𝑓 = 𝑔 → (◡(𝑂‘𝑓) “ {𝑊}) = (◡(𝑂‘𝑔) “ {𝑊})) |
103 | 102 | fveq2d 6107 |
. . . . . . . . . . 11
⊢ (𝑓 = 𝑔 → (#‘(◡(𝑂‘𝑓) “ {𝑊})) = (#‘(◡(𝑂‘𝑔) “ {𝑊}))) |
104 | 103, 98 | breq12d 4596 |
. . . . . . . . . 10
⊢ (𝑓 = 𝑔 → ((#‘(◡(𝑂‘𝑓) “ {𝑊})) ≤ (𝐷‘𝑓) ↔ (#‘(◡(𝑂‘𝑔) “ {𝑊})) ≤ (𝐷‘𝑔))) |
105 | 99, 104 | imbi12d 333 |
. . . . . . . . 9
⊢ (𝑓 = 𝑔 → (((𝐷‘𝑓) = 𝑑 → (#‘(◡(𝑂‘𝑓) “ {𝑊})) ≤ (𝐷‘𝑓)) ↔ ((𝐷‘𝑔) = 𝑑 → (#‘(◡(𝑂‘𝑔) “ {𝑊})) ≤ (𝐷‘𝑔)))) |
106 | 105 | cbvralv 3147 |
. . . . . . . 8
⊢
(∀𝑓 ∈
𝐵 ((𝐷‘𝑓) = 𝑑 → (#‘(◡(𝑂‘𝑓) “ {𝑊})) ≤ (𝐷‘𝑓)) ↔ ∀𝑔 ∈ 𝐵 ((𝐷‘𝑔) = 𝑑 → (#‘(◡(𝑂‘𝑔) “ {𝑊})) ≤ (𝐷‘𝑔))) |
107 | | simprr 792 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑅 ∈ IDomn ∧ 𝑑 ∈ ℕ0)
∧ (𝑓 ∈ 𝐵 ∧ (𝐷‘𝑓) = (𝑑 + 1))) → (𝐷‘𝑓) = (𝑑 + 1)) |
108 | | peano2nn0 11210 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑑 ∈ ℕ0
→ (𝑑 + 1) ∈
ℕ0) |
109 | 108 | ad2antlr 759 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑅 ∈ IDomn ∧ 𝑑 ∈ ℕ0)
∧ (𝑓 ∈ 𝐵 ∧ (𝐷‘𝑓) = (𝑑 + 1))) → (𝑑 + 1) ∈
ℕ0) |
110 | 107, 109 | eqeltrd 2688 |
. . . . . . . . . . . . . . 15
⊢ (((𝑅 ∈ IDomn ∧ 𝑑 ∈ ℕ0)
∧ (𝑓 ∈ 𝐵 ∧ (𝐷‘𝑓) = (𝑑 + 1))) → (𝐷‘𝑓) ∈
ℕ0) |
111 | 110 | nn0ge0d 11231 |
. . . . . . . . . . . . . 14
⊢ (((𝑅 ∈ IDomn ∧ 𝑑 ∈ ℕ0)
∧ (𝑓 ∈ 𝐵 ∧ (𝐷‘𝑓) = (𝑑 + 1))) → 0 ≤ (𝐷‘𝑓)) |
112 | | fveq2 6103 |
. . . . . . . . . . . . . . . 16
⊢ ((◡(𝑂‘𝑓) “ {𝑊}) = ∅ → (#‘(◡(𝑂‘𝑓) “ {𝑊})) = (#‘∅)) |
113 | 112, 92 | syl6eq 2660 |
. . . . . . . . . . . . . . 15
⊢ ((◡(𝑂‘𝑓) “ {𝑊}) = ∅ → (#‘(◡(𝑂‘𝑓) “ {𝑊})) = 0) |
114 | 113 | breq1d 4593 |
. . . . . . . . . . . . . 14
⊢ ((◡(𝑂‘𝑓) “ {𝑊}) = ∅ → ((#‘(◡(𝑂‘𝑓) “ {𝑊})) ≤ (𝐷‘𝑓) ↔ 0 ≤ (𝐷‘𝑓))) |
115 | 111, 114 | syl5ibrcom 236 |
. . . . . . . . . . . . 13
⊢ (((𝑅 ∈ IDomn ∧ 𝑑 ∈ ℕ0)
∧ (𝑓 ∈ 𝐵 ∧ (𝐷‘𝑓) = (𝑑 + 1))) → ((◡(𝑂‘𝑓) “ {𝑊}) = ∅ → (#‘(◡(𝑂‘𝑓) “ {𝑊})) ≤ (𝐷‘𝑓))) |
116 | 115 | a1dd 48 |
. . . . . . . . . . . 12
⊢ (((𝑅 ∈ IDomn ∧ 𝑑 ∈ ℕ0)
∧ (𝑓 ∈ 𝐵 ∧ (𝐷‘𝑓) = (𝑑 + 1))) → ((◡(𝑂‘𝑓) “ {𝑊}) = ∅ → (∀𝑔 ∈ 𝐵 ((𝐷‘𝑔) = 𝑑 → (#‘(◡(𝑂‘𝑔) “ {𝑊})) ≤ (𝐷‘𝑔)) → (#‘(◡(𝑂‘𝑓) “ {𝑊})) ≤ (𝐷‘𝑓)))) |
117 | | n0 3890 |
. . . . . . . . . . . . 13
⊢ ((◡(𝑂‘𝑓) “ {𝑊}) ≠ ∅ ↔ ∃𝑥 𝑥 ∈ (◡(𝑂‘𝑓) “ {𝑊})) |
118 | | simplll 794 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑅 ∈ IDomn ∧ 𝑑 ∈ ℕ0)
∧ (𝑓 ∈ 𝐵 ∧ (𝐷‘𝑓) = (𝑑 + 1))) ∧ (𝑥 ∈ (◡(𝑂‘𝑓) “ {𝑊}) ∧ ∀𝑔 ∈ 𝐵 ((𝐷‘𝑔) = 𝑑 → (#‘(◡(𝑂‘𝑔) “ {𝑊})) ≤ (𝐷‘𝑔)))) → 𝑅 ∈ IDomn) |
119 | | simplrl 796 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑅 ∈ IDomn ∧ 𝑑 ∈ ℕ0)
∧ (𝑓 ∈ 𝐵 ∧ (𝐷‘𝑓) = (𝑑 + 1))) ∧ (𝑥 ∈ (◡(𝑂‘𝑓) “ {𝑊}) ∧ ∀𝑔 ∈ 𝐵 ((𝐷‘𝑔) = 𝑑 → (#‘(◡(𝑂‘𝑔) “ {𝑊})) ≤ (𝐷‘𝑔)))) → 𝑓 ∈ 𝐵) |
120 | | eqid 2610 |
. . . . . . . . . . . . . . . 16
⊢
(var1‘𝑅) = (var1‘𝑅) |
121 | | eqid 2610 |
. . . . . . . . . . . . . . . 16
⊢
(-g‘𝑃) = (-g‘𝑃) |
122 | | eqid 2610 |
. . . . . . . . . . . . . . . 16
⊢
((var1‘𝑅)(-g‘𝑃)((algSc‘𝑃)‘𝑥)) = ((var1‘𝑅)(-g‘𝑃)((algSc‘𝑃)‘𝑥)) |
123 | | simpllr 795 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑅 ∈ IDomn ∧ 𝑑 ∈ ℕ0)
∧ (𝑓 ∈ 𝐵 ∧ (𝐷‘𝑓) = (𝑑 + 1))) ∧ (𝑥 ∈ (◡(𝑂‘𝑓) “ {𝑊}) ∧ ∀𝑔 ∈ 𝐵 ((𝐷‘𝑔) = 𝑑 → (#‘(◡(𝑂‘𝑔) “ {𝑊})) ≤ (𝐷‘𝑔)))) → 𝑑 ∈ ℕ0) |
124 | | simplrr 797 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑅 ∈ IDomn ∧ 𝑑 ∈ ℕ0)
∧ (𝑓 ∈ 𝐵 ∧ (𝐷‘𝑓) = (𝑑 + 1))) ∧ (𝑥 ∈ (◡(𝑂‘𝑓) “ {𝑊}) ∧ ∀𝑔 ∈ 𝐵 ((𝐷‘𝑔) = 𝑑 → (#‘(◡(𝑂‘𝑔) “ {𝑊})) ≤ (𝐷‘𝑔)))) → (𝐷‘𝑓) = (𝑑 + 1)) |
125 | | simprl 790 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑅 ∈ IDomn ∧ 𝑑 ∈ ℕ0)
∧ (𝑓 ∈ 𝐵 ∧ (𝐷‘𝑓) = (𝑑 + 1))) ∧ (𝑥 ∈ (◡(𝑂‘𝑓) “ {𝑊}) ∧ ∀𝑔 ∈ 𝐵 ((𝐷‘𝑔) = 𝑑 → (#‘(◡(𝑂‘𝑔) “ {𝑊})) ≤ (𝐷‘𝑔)))) → 𝑥 ∈ (◡(𝑂‘𝑓) “ {𝑊})) |
126 | | simprr 792 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑅 ∈ IDomn ∧ 𝑑 ∈ ℕ0)
∧ (𝑓 ∈ 𝐵 ∧ (𝐷‘𝑓) = (𝑑 + 1))) ∧ (𝑥 ∈ (◡(𝑂‘𝑓) “ {𝑊}) ∧ ∀𝑔 ∈ 𝐵 ((𝐷‘𝑔) = 𝑑 → (#‘(◡(𝑂‘𝑔) “ {𝑊})) ≤ (𝐷‘𝑔)))) → ∀𝑔 ∈ 𝐵 ((𝐷‘𝑔) = 𝑑 → (#‘(◡(𝑂‘𝑔) “ {𝑊})) ≤ (𝐷‘𝑔))) |
127 | 10, 12, 9, 57, 83, 11, 118, 119, 52, 120, 121, 44, 122, 123, 124, 125, 126 | fta1glem2 23730 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑅 ∈ IDomn ∧ 𝑑 ∈ ℕ0)
∧ (𝑓 ∈ 𝐵 ∧ (𝐷‘𝑓) = (𝑑 + 1))) ∧ (𝑥 ∈ (◡(𝑂‘𝑓) “ {𝑊}) ∧ ∀𝑔 ∈ 𝐵 ((𝐷‘𝑔) = 𝑑 → (#‘(◡(𝑂‘𝑔) “ {𝑊})) ≤ (𝐷‘𝑔)))) → (#‘(◡(𝑂‘𝑓) “ {𝑊})) ≤ (𝐷‘𝑓)) |
128 | 127 | exp32 629 |
. . . . . . . . . . . . . 14
⊢ (((𝑅 ∈ IDomn ∧ 𝑑 ∈ ℕ0)
∧ (𝑓 ∈ 𝐵 ∧ (𝐷‘𝑓) = (𝑑 + 1))) → (𝑥 ∈ (◡(𝑂‘𝑓) “ {𝑊}) → (∀𝑔 ∈ 𝐵 ((𝐷‘𝑔) = 𝑑 → (#‘(◡(𝑂‘𝑔) “ {𝑊})) ≤ (𝐷‘𝑔)) → (#‘(◡(𝑂‘𝑓) “ {𝑊})) ≤ (𝐷‘𝑓)))) |
129 | 128 | exlimdv 1848 |
. . . . . . . . . . . . 13
⊢ (((𝑅 ∈ IDomn ∧ 𝑑 ∈ ℕ0)
∧ (𝑓 ∈ 𝐵 ∧ (𝐷‘𝑓) = (𝑑 + 1))) → (∃𝑥 𝑥 ∈ (◡(𝑂‘𝑓) “ {𝑊}) → (∀𝑔 ∈ 𝐵 ((𝐷‘𝑔) = 𝑑 → (#‘(◡(𝑂‘𝑔) “ {𝑊})) ≤ (𝐷‘𝑔)) → (#‘(◡(𝑂‘𝑓) “ {𝑊})) ≤ (𝐷‘𝑓)))) |
130 | 117, 129 | syl5bi 231 |
. . . . . . . . . . . 12
⊢ (((𝑅 ∈ IDomn ∧ 𝑑 ∈ ℕ0)
∧ (𝑓 ∈ 𝐵 ∧ (𝐷‘𝑓) = (𝑑 + 1))) → ((◡(𝑂‘𝑓) “ {𝑊}) ≠ ∅ → (∀𝑔 ∈ 𝐵 ((𝐷‘𝑔) = 𝑑 → (#‘(◡(𝑂‘𝑔) “ {𝑊})) ≤ (𝐷‘𝑔)) → (#‘(◡(𝑂‘𝑓) “ {𝑊})) ≤ (𝐷‘𝑓)))) |
131 | 116, 130 | pm2.61dne 2868 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ IDomn ∧ 𝑑 ∈ ℕ0)
∧ (𝑓 ∈ 𝐵 ∧ (𝐷‘𝑓) = (𝑑 + 1))) → (∀𝑔 ∈ 𝐵 ((𝐷‘𝑔) = 𝑑 → (#‘(◡(𝑂‘𝑔) “ {𝑊})) ≤ (𝐷‘𝑔)) → (#‘(◡(𝑂‘𝑓) “ {𝑊})) ≤ (𝐷‘𝑓))) |
132 | 131 | expr 641 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ IDomn ∧ 𝑑 ∈ ℕ0)
∧ 𝑓 ∈ 𝐵) → ((𝐷‘𝑓) = (𝑑 + 1) → (∀𝑔 ∈ 𝐵 ((𝐷‘𝑔) = 𝑑 → (#‘(◡(𝑂‘𝑔) “ {𝑊})) ≤ (𝐷‘𝑔)) → (#‘(◡(𝑂‘𝑓) “ {𝑊})) ≤ (𝐷‘𝑓)))) |
133 | 132 | com23 84 |
. . . . . . . . 9
⊢ (((𝑅 ∈ IDomn ∧ 𝑑 ∈ ℕ0)
∧ 𝑓 ∈ 𝐵) → (∀𝑔 ∈ 𝐵 ((𝐷‘𝑔) = 𝑑 → (#‘(◡(𝑂‘𝑔) “ {𝑊})) ≤ (𝐷‘𝑔)) → ((𝐷‘𝑓) = (𝑑 + 1) → (#‘(◡(𝑂‘𝑓) “ {𝑊})) ≤ (𝐷‘𝑓)))) |
134 | 133 | ralrimdva 2952 |
. . . . . . . 8
⊢ ((𝑅 ∈ IDomn ∧ 𝑑 ∈ ℕ0)
→ (∀𝑔 ∈
𝐵 ((𝐷‘𝑔) = 𝑑 → (#‘(◡(𝑂‘𝑔) “ {𝑊})) ≤ (𝐷‘𝑔)) → ∀𝑓 ∈ 𝐵 ((𝐷‘𝑓) = (𝑑 + 1) → (#‘(◡(𝑂‘𝑓) “ {𝑊})) ≤ (𝐷‘𝑓)))) |
135 | 106, 134 | syl5bi 231 |
. . . . . . 7
⊢ ((𝑅 ∈ IDomn ∧ 𝑑 ∈ ℕ0)
→ (∀𝑓 ∈
𝐵 ((𝐷‘𝑓) = 𝑑 → (#‘(◡(𝑂‘𝑓) “ {𝑊})) ≤ (𝐷‘𝑓)) → ∀𝑓 ∈ 𝐵 ((𝐷‘𝑓) = (𝑑 + 1) → (#‘(◡(𝑂‘𝑓) “ {𝑊})) ≤ (𝐷‘𝑓)))) |
136 | 135 | expcom 450 |
. . . . . 6
⊢ (𝑑 ∈ ℕ0
→ (𝑅 ∈ IDomn
→ (∀𝑓 ∈
𝐵 ((𝐷‘𝑓) = 𝑑 → (#‘(◡(𝑂‘𝑓) “ {𝑊})) ≤ (𝐷‘𝑓)) → ∀𝑓 ∈ 𝐵 ((𝐷‘𝑓) = (𝑑 + 1) → (#‘(◡(𝑂‘𝑓) “ {𝑊})) ≤ (𝐷‘𝑓))))) |
137 | 136 | a2d 29 |
. . . . 5
⊢ (𝑑 ∈ ℕ0
→ ((𝑅 ∈ IDomn
→ ∀𝑓 ∈
𝐵 ((𝐷‘𝑓) = 𝑑 → (#‘(◡(𝑂‘𝑓) “ {𝑊})) ≤ (𝐷‘𝑓))) → (𝑅 ∈ IDomn → ∀𝑓 ∈ 𝐵 ((𝐷‘𝑓) = (𝑑 + 1) → (#‘(◡(𝑂‘𝑓) “ {𝑊})) ≤ (𝐷‘𝑓))))) |
138 | 18, 22, 26, 30, 97, 137 | nn0ind 11348 |
. . . 4
⊢ ((𝐷‘𝐹) ∈ ℕ0 → (𝑅 ∈ IDomn →
∀𝑓 ∈ 𝐵 ((𝐷‘𝑓) = (𝐷‘𝐹) → (#‘(◡(𝑂‘𝑓) “ {𝑊})) ≤ (𝐷‘𝑓)))) |
139 | 14, 3, 138 | sylc 63 |
. . 3
⊢ (𝜑 → ∀𝑓 ∈ 𝐵 ((𝐷‘𝑓) = (𝐷‘𝐹) → (#‘(◡(𝑂‘𝑓) “ {𝑊})) ≤ (𝐷‘𝑓))) |
140 | | fveq2 6103 |
. . . . . 6
⊢ (𝑓 = 𝐹 → (𝐷‘𝑓) = (𝐷‘𝐹)) |
141 | 140 | eqeq1d 2612 |
. . . . 5
⊢ (𝑓 = 𝐹 → ((𝐷‘𝑓) = (𝐷‘𝐹) ↔ (𝐷‘𝐹) = (𝐷‘𝐹))) |
142 | | fveq2 6103 |
. . . . . . . . 9
⊢ (𝑓 = 𝐹 → (𝑂‘𝑓) = (𝑂‘𝐹)) |
143 | 142 | cnveqd 5220 |
. . . . . . . 8
⊢ (𝑓 = 𝐹 → ◡(𝑂‘𝑓) = ◡(𝑂‘𝐹)) |
144 | 143 | imaeq1d 5384 |
. . . . . . 7
⊢ (𝑓 = 𝐹 → (◡(𝑂‘𝑓) “ {𝑊}) = (◡(𝑂‘𝐹) “ {𝑊})) |
145 | 144 | fveq2d 6107 |
. . . . . 6
⊢ (𝑓 = 𝐹 → (#‘(◡(𝑂‘𝑓) “ {𝑊})) = (#‘(◡(𝑂‘𝐹) “ {𝑊}))) |
146 | 145, 140 | breq12d 4596 |
. . . . 5
⊢ (𝑓 = 𝐹 → ((#‘(◡(𝑂‘𝑓) “ {𝑊})) ≤ (𝐷‘𝑓) ↔ (#‘(◡(𝑂‘𝐹) “ {𝑊})) ≤ (𝐷‘𝐹))) |
147 | 141, 146 | imbi12d 333 |
. . . 4
⊢ (𝑓 = 𝐹 → (((𝐷‘𝑓) = (𝐷‘𝐹) → (#‘(◡(𝑂‘𝑓) “ {𝑊})) ≤ (𝐷‘𝑓)) ↔ ((𝐷‘𝐹) = (𝐷‘𝐹) → (#‘(◡(𝑂‘𝐹) “ {𝑊})) ≤ (𝐷‘𝐹)))) |
148 | 147 | rspcv 3278 |
. . 3
⊢ (𝐹 ∈ 𝐵 → (∀𝑓 ∈ 𝐵 ((𝐷‘𝑓) = (𝐷‘𝐹) → (#‘(◡(𝑂‘𝑓) “ {𝑊})) ≤ (𝐷‘𝑓)) → ((𝐷‘𝐹) = (𝐷‘𝐹) → (#‘(◡(𝑂‘𝐹) “ {𝑊})) ≤ (𝐷‘𝐹)))) |
149 | 2, 139, 148 | sylc 63 |
. 2
⊢ (𝜑 → ((𝐷‘𝐹) = (𝐷‘𝐹) → (#‘(◡(𝑂‘𝐹) “ {𝑊})) ≤ (𝐷‘𝐹))) |
150 | 1, 149 | mpi 20 |
1
⊢ (𝜑 → (#‘(◡(𝑂‘𝐹) “ {𝑊})) ≤ (𝐷‘𝐹)) |