Metamath Proof Explorer

Theorem fta1g

Description: The one-sided fundamental theorem of algebra. A polynomial of degree n has at most n roots. Unlike the real fundamental theorem fta , which is only true in CC and other algebraically closed fields, this is true in any integral domain. (Contributed by Mario Carneiro, 12-Jun-2015)

Ref Expression
Hypotheses fta1g.p ⊢ P = Poly 1 ⁡ R
fta1g.b ⊢ B = Base P
fta1g.d ⊢ D = deg 1 ⁡ R
fta1g.o ⊢ O = eval 1 ⁡ R
fta1g.w ⊢ W = 0 R
fta1g.z ⊢ 0 ˙ = 0 P
fta1g.1 ⊢ φ → R ∈ IDomn
fta1g.2 ⊢ φ → F ∈ B
fta1g.3 ⊢ φ → F ≠ 0 ˙
Assertion fta1g ⊢ φ → O ⁡ F -1 W ≤ D ⁡ F

Proof

Step Hyp Ref Expression
1 fta1g.p ⊢ P = Poly 1 ⁡ R
2 fta1g.b ⊢ B = Base P
3 fta1g.d ⊢ D = deg 1 ⁡ R
4 fta1g.o ⊢ O = eval 1 ⁡ R
5 fta1g.w ⊢ W = 0 R
6 fta1g.z ⊢ 0 ˙ = 0 P
7 fta1g.1 ⊢ φ → R ∈ IDomn
8 fta1g.2 ⊢ φ → F ∈ B
9 fta1g.3 ⊢ φ → F ≠ 0 ˙
10 eqid ⊢ D ⁡ F = D ⁡ F
11 fveqeq2 ⊢ f = F → D ⁡ f = D ⁡ F ↔ D ⁡ F = D ⁡ F
12 fveq2 ⊢ f = F → O ⁡ f = O ⁡ F
13 12 cnveqd ⊢ f = F → O ⁡ f -1 = O ⁡ F -1
14 13 imaeq1d ⊢ f = F → O ⁡ f -1 W = O ⁡ F -1 W
15 14 fveq2d ⊢ f = F → O ⁡ f -1 W = O ⁡ F -1 W
16 fveq2 ⊢ f = F → D ⁡ f = D ⁡ F
17 15 16 breq12d ⊢ f = F → O ⁡ f -1 W ≤ D ⁡ f ↔ O ⁡ F -1 W ≤ D ⁡ F
18 11 17 imbi12d ⊢ f = F → D ⁡ f = D ⁡ F → O ⁡ f -1 W ≤ D ⁡ f ↔ D ⁡ F = D ⁡ F → O ⁡ F -1 W ≤ D ⁡ F
19 isidom ⊢ R ∈ IDomn ↔ R ∈ CRing ∧ R ∈ Domn
20 19 simplbi ⊢ R ∈ IDomn → R ∈ CRing
21 crngring ⊢ R ∈ CRing → R ∈ Ring
22 7 20 21 3syl ⊢ φ → R ∈ Ring
23 3 1 6 2 deg1nn0cl ⊢ R ∈ Ring ∧ F ∈ B ∧ F ≠ 0 ˙ → D ⁡ F ∈ ℕ 0
24 22 8 9 23 syl3anc ⊢ φ → D ⁡ F ∈ ℕ 0
25 eqeq2 ⊢ x = 0 → D ⁡ f = x ↔ D ⁡ f = 0
26 25 imbi1d ⊢ x = 0 → D ⁡ f = x → O ⁡ f -1 W ≤ D ⁡ f ↔ D ⁡ f = 0 → O ⁡ f -1 W ≤ D ⁡ f
27 26 ralbidv ⊢ x = 0 → ∀ f ∈ B D ⁡ f = x → O ⁡ f -1 W ≤ D ⁡ f ↔ ∀ f ∈ B D ⁡ f = 0 → O ⁡ f -1 W ≤ D ⁡ f
28 27 imbi2d ⊢ x = 0 → R ∈ IDomn → ∀ f ∈ B D ⁡ f = x → O ⁡ f -1 W ≤ D ⁡ f ↔ R ∈ IDomn → ∀ f ∈ B D ⁡ f = 0 → O ⁡ f -1 W ≤ D ⁡ f
29 eqeq2 ⊢ x = d → D ⁡ f = x ↔ D ⁡ f = d
30 29 imbi1d ⊢ x = d → D ⁡ f = x → O ⁡ f -1 W ≤ D ⁡ f ↔ D ⁡ f = d → O ⁡ f -1 W ≤ D ⁡ f
31 30 ralbidv ⊢ x = d → ∀ f ∈ B D ⁡ f = x → O ⁡ f -1 W ≤ D ⁡ f ↔ ∀ f ∈ B D ⁡ f = d → O ⁡ f -1 W ≤ D ⁡ f
32 31 imbi2d ⊢ x = d → R ∈ IDomn → ∀ f ∈ B D ⁡ f = x → O ⁡ f -1 W ≤ D ⁡ f ↔ R ∈ IDomn → ∀ f ∈ B D ⁡ f = d → O ⁡ f -1 W ≤ D ⁡ f
33 eqeq2 ⊢ x = d + 1 → D ⁡ f = x ↔ D ⁡ f = d + 1
34 33 imbi1d ⊢ x = d + 1 → D ⁡ f = x → O ⁡ f -1 W ≤ D ⁡ f ↔ D ⁡ f = d + 1 → O ⁡ f -1 W ≤ D ⁡ f
35 34 ralbidv ⊢ x = d + 1 → ∀ f ∈ B D ⁡ f = x → O ⁡ f -1 W ≤ D ⁡ f ↔ ∀ f ∈ B D ⁡ f = d + 1 → O ⁡ f -1 W ≤ D ⁡ f
36 35 imbi2d ⊢ x = d + 1 → R ∈ IDomn → ∀ f ∈ B D ⁡ f = x → O ⁡ f -1 W ≤ D ⁡ f ↔ R ∈ IDomn → ∀ f ∈ B D ⁡ f = d + 1 → O ⁡ f -1 W ≤ D ⁡ f
37 eqeq2 ⊢ x = D ⁡ F → D ⁡ f = x ↔ D ⁡ f = D ⁡ F
38 37 imbi1d ⊢ x = D ⁡ F → D ⁡ f = x → O ⁡ f -1 W ≤ D ⁡ f ↔ D ⁡ f = D ⁡ F → O ⁡ f -1 W ≤ D ⁡ f
39 38 ralbidv ⊢ x = D ⁡ F → ∀ f ∈ B D ⁡ f = x → O ⁡ f -1 W ≤ D ⁡ f ↔ ∀ f ∈ B D ⁡ f = D ⁡ F → O ⁡ f -1 W ≤ D ⁡ f
40 39 imbi2d ⊢ x = D ⁡ F → R ∈ IDomn → ∀ f ∈ B D ⁡ f = x → O ⁡ f -1 W ≤ D ⁡ f ↔ R ∈ IDomn → ∀ f ∈ B D ⁡ f = D ⁡ F → O ⁡ f -1 W ≤ D ⁡ f
41 simprr ⊢ R ∈ IDomn ∧ f ∈ B ∧ D ⁡ f = 0 → D ⁡ f = 0
42 0nn0 ⊢ 0 ∈ ℕ 0
43 41 42 eqeltrdi ⊢ R ∈ IDomn ∧ f ∈ B ∧ D ⁡ f = 0 → D ⁡ f ∈ ℕ 0
44 20 21 syl ⊢ R ∈ IDomn → R ∈ Ring
45 simpl ⊢ f ∈ B ∧ D ⁡ f = 0 → f ∈ B
46 3 1 6 2 deg1nn0clb ⊢ R ∈ Ring ∧ f ∈ B → f ≠ 0 ˙ ↔ D ⁡ f ∈ ℕ 0
47 44 45 46 syl2an ⊢ R ∈ IDomn ∧ f ∈ B ∧ D ⁡ f = 0 → f ≠ 0 ˙ ↔ D ⁡ f ∈ ℕ 0
48 43 47 mpbird ⊢ R ∈ IDomn ∧ f ∈ B ∧ D ⁡ f = 0 → f ≠ 0 ˙
49 simplrr ⊢ R ∈ IDomn ∧ f ∈ B ∧ D ⁡ f = 0 ∧ x ∈ O ⁡ f -1 W → D ⁡ f = 0
50 0le0 ⊢ 0 ≤ 0
51 49 50 eqbrtrdi ⊢ R ∈ IDomn ∧ f ∈ B ∧ D ⁡ f = 0 ∧ x ∈ O ⁡ f -1 W → D ⁡ f ≤ 0
52 44 ad2antrr ⊢ R ∈ IDomn ∧ f ∈ B ∧ D ⁡ f = 0 ∧ x ∈ O ⁡ f -1 W → R ∈ Ring
53 simplrl ⊢ R ∈ IDomn ∧ f ∈ B ∧ D ⁡ f = 0 ∧ x ∈ O ⁡ f -1 W → f ∈ B
54 eqid ⊢ algSc ⁡ P = algSc ⁡ P
55 3 1 2 54 deg1le0 ⊢ R ∈ Ring ∧ f ∈ B → D ⁡ f ≤ 0 ↔ f = algSc ⁡ P ⁡ coe 1 ⁡ f ⁡ 0
56 52 53 55 syl2anc ⊢ R ∈ IDomn ∧ f ∈ B ∧ D ⁡ f = 0 ∧ x ∈ O ⁡ f -1 W → D ⁡ f ≤ 0 ↔ f = algSc ⁡ P ⁡ coe 1 ⁡ f ⁡ 0
57 51 56 mpbid ⊢ R ∈ IDomn ∧ f ∈ B ∧ D ⁡ f = 0 ∧ x ∈ O ⁡ f -1 W → f = algSc ⁡ P ⁡ coe 1 ⁡ f ⁡ 0
58 57 fveq2d ⊢ R ∈ IDomn ∧ f ∈ B ∧ D ⁡ f = 0 ∧ x ∈ O ⁡ f -1 W → O ⁡ f = O ⁡ algSc ⁡ P ⁡ coe 1 ⁡ f ⁡ 0
59 20 adantr ⊢ R ∈ IDomn ∧ f ∈ B ∧ D ⁡ f = 0 → R ∈ CRing
60 59 adantr ⊢ R ∈ IDomn ∧ f ∈ B ∧ D ⁡ f = 0 ∧ x ∈ O ⁡ f -1 W → R ∈ CRing
61 eqid ⊢ coe 1 ⁡ f = coe 1 ⁡ f
62 eqid ⊢ Base R = Base R
63 61 2 1 62 coe1f ⊢ f ∈ B → coe 1 ⁡ f : ℕ 0 ⟶ Base R
64 53 63 syl ⊢ R ∈ IDomn ∧ f ∈ B ∧ D ⁡ f = 0 ∧ x ∈ O ⁡ f -1 W → coe 1 ⁡ f : ℕ 0 ⟶ Base R
65 ffvelrn ⊢ coe 1 ⁡ f : ℕ 0 ⟶ Base R ∧ 0 ∈ ℕ 0 → coe 1 ⁡ f ⁡ 0 ∈ Base R
66 64 42 65 sylancl ⊢ R ∈ IDomn ∧ f ∈ B ∧ D ⁡ f = 0 ∧ x ∈ O ⁡ f -1 W → coe 1 ⁡ f ⁡ 0 ∈ Base R
67 4 1 62 54 evl1sca ⊢ R ∈ CRing ∧ coe 1 ⁡ f ⁡ 0 ∈ Base R → O ⁡ algSc ⁡ P ⁡ coe 1 ⁡ f ⁡ 0 = Base R × coe 1 ⁡ f ⁡ 0
68 60 66 67 syl2anc ⊢ R ∈ IDomn ∧ f ∈ B ∧ D ⁡ f = 0 ∧ x ∈ O ⁡ f -1 W → O ⁡ algSc ⁡ P ⁡ coe 1 ⁡ f ⁡ 0 = Base R × coe 1 ⁡ f ⁡ 0
69 58 68 eqtrd ⊢ R ∈ IDomn ∧ f ∈ B ∧ D ⁡ f = 0 ∧ x ∈ O ⁡ f -1 W → O ⁡ f = Base R × coe 1 ⁡ f ⁡ 0
70 69 fveq1d ⊢ R ∈ IDomn ∧ f ∈ B ∧ D ⁡ f = 0 ∧ x ∈ O ⁡ f -1 W → O ⁡ f ⁡ x = Base R × coe 1 ⁡ f ⁡ 0 ⁡ x
71 eqid ⊢ R ↑ 𝑠 Base R = R ↑ 𝑠 Base R
72 eqid ⊢ Base R ↑ 𝑠 Base R = Base R ↑ 𝑠 Base R
73 simpl ⊢ R ∈ IDomn ∧ f ∈ B ∧ D ⁡ f = 0 → R ∈ IDomn
74 fvexd ⊢ R ∈ IDomn ∧ f ∈ B ∧ D ⁡ f = 0 → Base R ∈ V
75 4 1 71 62 evl1rhm ⊢ R ∈ CRing → O ∈ P RingHom R ↑ 𝑠 Base R
76 2 72 rhmf ⊢ O ∈ P RingHom R ↑ 𝑠 Base R → O : B ⟶ Base R ↑ 𝑠 Base R
77 59 75 76 3syl ⊢ R ∈ IDomn ∧ f ∈ B ∧ D ⁡ f = 0 → O : B ⟶ Base R ↑ 𝑠 Base R
78 simprl ⊢ R ∈ IDomn ∧ f ∈ B ∧ D ⁡ f = 0 → f ∈ B
79 77 78 ffvelrnd ⊢ R ∈ IDomn ∧ f ∈ B ∧ D ⁡ f = 0 → O ⁡ f ∈ Base R ↑ 𝑠 Base R
80 71 62 72 73 74 79 pwselbas ⊢ R ∈ IDomn ∧ f ∈ B ∧ D ⁡ f = 0 → O ⁡ f : Base R ⟶ Base R
81 ffn ⊢ O ⁡ f : Base R ⟶ Base R → O ⁡ f Fn Base R
82 fniniseg ⊢ O ⁡ f Fn Base R → x ∈ O ⁡ f -1 W ↔ x ∈ Base R ∧ O ⁡ f ⁡ x = W
83 80 81 82 3syl ⊢ R ∈ IDomn ∧ f ∈ B ∧ D ⁡ f = 0 → x ∈ O ⁡ f -1 W ↔ x ∈ Base R ∧ O ⁡ f ⁡ x = W
84 83 simplbda ⊢ R ∈ IDomn ∧ f ∈ B ∧ D ⁡ f = 0 ∧ x ∈ O ⁡ f -1 W → O ⁡ f ⁡ x = W
85 83 simprbda ⊢ R ∈ IDomn ∧ f ∈ B ∧ D ⁡ f = 0 ∧ x ∈ O ⁡ f -1 W → x ∈ Base R
86 fvex ⊢ coe 1 ⁡ f ⁡ 0 ∈ V
87 86 fvconst2 ⊢ x ∈ Base R → Base R × coe 1 ⁡ f ⁡ 0 ⁡ x = coe 1 ⁡ f ⁡ 0
88 85 87 syl ⊢ R ∈ IDomn ∧ f ∈ B ∧ D ⁡ f = 0 ∧ x ∈ O ⁡ f -1 W → Base R × coe 1 ⁡ f ⁡ 0 ⁡ x = coe 1 ⁡ f ⁡ 0
89 70 84 88 3eqtr3rd ⊢ R ∈ IDomn ∧ f ∈ B ∧ D ⁡ f = 0 ∧ x ∈ O ⁡ f -1 W → coe 1 ⁡ f ⁡ 0 = W
90 89 fveq2d ⊢ R ∈ IDomn ∧ f ∈ B ∧ D ⁡ f = 0 ∧ x ∈ O ⁡ f -1 W → algSc ⁡ P ⁡ coe 1 ⁡ f ⁡ 0 = algSc ⁡ P ⁡ W
91 1 54 5 6 ply1scl0 ⊢ R ∈ Ring → algSc ⁡ P ⁡ W = 0 ˙
92 52 91 syl ⊢ R ∈ IDomn ∧ f ∈ B ∧ D ⁡ f = 0 ∧ x ∈ O ⁡ f -1 W → algSc ⁡ P ⁡ W = 0 ˙
93 57 90 92 3eqtrd ⊢ R ∈ IDomn ∧ f ∈ B ∧ D ⁡ f = 0 ∧ x ∈ O ⁡ f -1 W → f = 0 ˙
94 93 ex ⊢ R ∈ IDomn ∧ f ∈ B ∧ D ⁡ f = 0 → x ∈ O ⁡ f -1 W → f = 0 ˙
95 94 necon3ad ⊢ R ∈ IDomn ∧ f ∈ B ∧ D ⁡ f = 0 → f ≠ 0 ˙ → ¬ x ∈ O ⁡ f -1 W
96 48 95 mpd ⊢ R ∈ IDomn ∧ f ∈ B ∧ D ⁡ f = 0 → ¬ x ∈ O ⁡ f -1 W
97 96 eq0rdv ⊢ R ∈ IDomn ∧ f ∈ B ∧ D ⁡ f = 0 → O ⁡ f -1 W = ∅
98 97 fveq2d ⊢ R ∈ IDomn ∧ f ∈ B ∧ D ⁡ f = 0 → O ⁡ f -1 W = ∅
99 hash0 ⊢ ∅ = 0
100 98 99 eqtrdi ⊢ R ∈ IDomn ∧ f ∈ B ∧ D ⁡ f = 0 → O ⁡ f -1 W = 0
101 50 41 breqtrrid ⊢ R ∈ IDomn ∧ f ∈ B ∧ D ⁡ f = 0 → 0 ≤ D ⁡ f
102 100 101 eqbrtrd ⊢ R ∈ IDomn ∧ f ∈ B ∧ D ⁡ f = 0 → O ⁡ f -1 W ≤ D ⁡ f
103 102 expr ⊢ R ∈ IDomn ∧ f ∈ B → D ⁡ f = 0 → O ⁡ f -1 W ≤ D ⁡ f
104 103 ralrimiva ⊢ R ∈ IDomn → ∀ f ∈ B D ⁡ f = 0 → O ⁡ f -1 W ≤ D ⁡ f
105 fveqeq2 ⊢ f = g → D ⁡ f = d ↔ D ⁡ g = d
106 fveq2 ⊢ f = g → O ⁡ f = O ⁡ g
107 106 cnveqd ⊢ f = g → O ⁡ f -1 = O ⁡ g -1
108 107 imaeq1d ⊢ f = g → O ⁡ f -1 W = O ⁡ g -1 W
109 108 fveq2d ⊢ f = g → O ⁡ f -1 W = O ⁡ g -1 W
110 fveq2 ⊢ f = g → D ⁡ f = D ⁡ g
111 109 110 breq12d ⊢ f = g → O ⁡ f -1 W ≤ D ⁡ f ↔ O ⁡ g -1 W ≤ D ⁡ g
112 105 111 imbi12d ⊢ f = g → D ⁡ f = d → O ⁡ f -1 W ≤ D ⁡ f ↔ D ⁡ g = d → O ⁡ g -1 W ≤ D ⁡ g
113 112 cbvralvw ⊢ ∀ f ∈ B D ⁡ f = d → O ⁡ f -1 W ≤ D ⁡ f ↔ ∀ g ∈ B D ⁡ g = d → O ⁡ g -1 W ≤ D ⁡ g
114 simprr ⊢ R ∈ IDomn ∧ d ∈ ℕ 0 ∧ f ∈ B ∧ D ⁡ f = d + 1 → D ⁡ f = d + 1
115 peano2nn0 ⊢ d ∈ ℕ 0 → d + 1 ∈ ℕ 0
116 115 ad2antlr ⊢ R ∈ IDomn ∧ d ∈ ℕ 0 ∧ f ∈ B ∧ D ⁡ f = d + 1 → d + 1 ∈ ℕ 0
117 114 116 eqeltrd ⊢ R ∈ IDomn ∧ d ∈ ℕ 0 ∧ f ∈ B ∧ D ⁡ f = d + 1 → D ⁡ f ∈ ℕ 0
118 117 nn0ge0d ⊢ R ∈ IDomn ∧ d ∈ ℕ 0 ∧ f ∈ B ∧ D ⁡ f = d + 1 → 0 ≤ D ⁡ f
119 fveq2 ⊢ O ⁡ f -1 W = ∅ → O ⁡ f -1 W = ∅
120 119 99 eqtrdi ⊢ O ⁡ f -1 W = ∅ → O ⁡ f -1 W = 0
121 120 breq1d ⊢ O ⁡ f -1 W = ∅ → O ⁡ f -1 W ≤ D ⁡ f ↔ 0 ≤ D ⁡ f
122 118 121 syl5ibrcom ⊢ R ∈ IDomn ∧ d ∈ ℕ 0 ∧ f ∈ B ∧ D ⁡ f = d + 1 → O ⁡ f -1 W = ∅ → O ⁡ f -1 W ≤ D ⁡ f
123 122 a1dd ⊢ R ∈ IDomn ∧ d ∈ ℕ 0 ∧ f ∈ B ∧ D ⁡ f = d + 1 → O ⁡ f -1 W = ∅ → ∀ g ∈ B D ⁡ g = d → O ⁡ g -1 W ≤ D ⁡ g → O ⁡ f -1 W ≤ D ⁡ f
124 n0 ⊢ O ⁡ f -1 W ≠ ∅ ↔ ∃ x x ∈ O ⁡ f -1 W
125 simplll ⊢ R ∈ IDomn ∧ d ∈ ℕ 0 ∧ f ∈ B ∧ D ⁡ f = d + 1 ∧ x ∈ O ⁡ f -1 W ∧ ∀ g ∈ B D ⁡ g = d → O ⁡ g -1 W ≤ D ⁡ g → R ∈ IDomn
126 simplrl ⊢ R ∈ IDomn ∧ d ∈ ℕ 0 ∧ f ∈ B ∧ D ⁡ f = d + 1 ∧ x ∈ O ⁡ f -1 W ∧ ∀ g ∈ B D ⁡ g = d → O ⁡ g -1 W ≤ D ⁡ g → f ∈ B
127 eqid ⊢ var 1 ⁡ R = var 1 ⁡ R
128 eqid ⊢ - P = - P
129 eqid ⊢ var 1 ⁡ R - P algSc ⁡ P ⁡ x = var 1 ⁡ R - P algSc ⁡ P ⁡ x
130 simpllr ⊢ R ∈ IDomn ∧ d ∈ ℕ 0 ∧ f ∈ B ∧ D ⁡ f = d + 1 ∧ x ∈ O ⁡ f -1 W ∧ ∀ g ∈ B D ⁡ g = d → O ⁡ g -1 W ≤ D ⁡ g → d ∈ ℕ 0
131 simplrr ⊢ R ∈ IDomn ∧ d ∈ ℕ 0 ∧ f ∈ B ∧ D ⁡ f = d + 1 ∧ x ∈ O ⁡ f -1 W ∧ ∀ g ∈ B D ⁡ g = d → O ⁡ g -1 W ≤ D ⁡ g → D ⁡ f = d + 1
132 simprl ⊢ R ∈ IDomn ∧ d ∈ ℕ 0 ∧ f ∈ B ∧ D ⁡ f = d + 1 ∧ x ∈ O ⁡ f -1 W ∧ ∀ g ∈ B D ⁡ g = d → O ⁡ g -1 W ≤ D ⁡ g → x ∈ O ⁡ f -1 W
133 simprr ⊢ R ∈ IDomn ∧ d ∈ ℕ 0 ∧ f ∈ B ∧ D ⁡ f = d + 1 ∧ x ∈ O ⁡ f -1 W ∧ ∀ g ∈ B D ⁡ g = d → O ⁡ g -1 W ≤ D ⁡ g → ∀ g ∈ B D ⁡ g = d → O ⁡ g -1 W ≤ D ⁡ g
134 1 2 3 4 5 6 125 126 62 127 128 54 129 130 131 132 133 fta1glem2 ⊢ R ∈ IDomn ∧ d ∈ ℕ 0 ∧ f ∈ B ∧ D ⁡ f = d + 1 ∧ x ∈ O ⁡ f -1 W ∧ ∀ g ∈ B D ⁡ g = d → O ⁡ g -1 W ≤ D ⁡ g → O ⁡ f -1 W ≤ D ⁡ f
135 134 exp32 ⊢ R ∈ IDomn ∧ d ∈ ℕ 0 ∧ f ∈ B ∧ D ⁡ f = d + 1 → x ∈ O ⁡ f -1 W → ∀ g ∈ B D ⁡ g = d → O ⁡ g -1 W ≤ D ⁡ g → O ⁡ f -1 W ≤ D ⁡ f
136 135 exlimdv ⊢ R ∈ IDomn ∧ d ∈ ℕ 0 ∧ f ∈ B ∧ D ⁡ f = d + 1 → ∃ x x ∈ O ⁡ f -1 W → ∀ g ∈ B D ⁡ g = d → O ⁡ g -1 W ≤ D ⁡ g → O ⁡ f -1 W ≤ D ⁡ f
137 124 136 syl5bi ⊢ R ∈ IDomn ∧ d ∈ ℕ 0 ∧ f ∈ B ∧ D ⁡ f = d + 1 → O ⁡ f -1 W ≠ ∅ → ∀ g ∈ B D ⁡ g = d → O ⁡ g -1 W ≤ D ⁡ g → O ⁡ f -1 W ≤ D ⁡ f
138 123 137 pm2.61dne ⊢ R ∈ IDomn ∧ d ∈ ℕ 0 ∧ f ∈ B ∧ D ⁡ f = d + 1 → ∀ g ∈ B D ⁡ g = d → O ⁡ g -1 W ≤ D ⁡ g → O ⁡ f -1 W ≤ D ⁡ f
139 138 expr ⊢ R ∈ IDomn ∧ d ∈ ℕ 0 ∧ f ∈ B → D ⁡ f = d + 1 → ∀ g ∈ B D ⁡ g = d → O ⁡ g -1 W ≤ D ⁡ g → O ⁡ f -1 W ≤ D ⁡ f
140 139 com23 ⊢ R ∈ IDomn ∧ d ∈ ℕ 0 ∧ f ∈ B → ∀ g ∈ B D ⁡ g = d → O ⁡ g -1 W ≤ D ⁡ g → D ⁡ f = d + 1 → O ⁡ f -1 W ≤ D ⁡ f
141 140 ralrimdva ⊢ R ∈ IDomn ∧ d ∈ ℕ 0 → ∀ g ∈ B D ⁡ g = d → O ⁡ g -1 W ≤ D ⁡ g → ∀ f ∈ B D ⁡ f = d + 1 → O ⁡ f -1 W ≤ D ⁡ f
142 113 141 syl5bi ⊢ R ∈ IDomn ∧ d ∈ ℕ 0 → ∀ f ∈ B D ⁡ f = d → O ⁡ f -1 W ≤ D ⁡ f → ∀ f ∈ B D ⁡ f = d + 1 → O ⁡ f -1 W ≤ D ⁡ f
143 142 expcom ⊢ d ∈ ℕ 0 → R ∈ IDomn → ∀ f ∈ B D ⁡ f = d → O ⁡ f -1 W ≤ D ⁡ f → ∀ f ∈ B D ⁡ f = d + 1 → O ⁡ f -1 W ≤ D ⁡ f
144 143 a2d ⊢ d ∈ ℕ 0 → R ∈ IDomn → ∀ f ∈ B D ⁡ f = d → O ⁡ f -1 W ≤ D ⁡ f → R ∈ IDomn → ∀ f ∈ B D ⁡ f = d + 1 → O ⁡ f -1 W ≤ D ⁡ f
145 28 32 36 40 104 144 nn0ind ⊢ D ⁡ F ∈ ℕ 0 → R ∈ IDomn → ∀ f ∈ B D ⁡ f = D ⁡ F → O ⁡ f -1 W ≤ D ⁡ f
146 24 7 145 sylc ⊢ φ → ∀ f ∈ B D ⁡ f = D ⁡ F → O ⁡ f -1 W ≤ D ⁡ f
147 18 146 8 rspcdva ⊢ φ → D ⁡ F = D ⁡ F → O ⁡ F -1 W ≤ D ⁡ F
148 10 147 mpi ⊢ φ → O ⁡ F -1 W ≤ D ⁡ F