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 𝑃 = ( Poly1𝑅 )
fta1g.b 𝐵 = ( Base ‘ 𝑃 )
fta1g.d 𝐷 = ( deg1𝑅 )
fta1g.o 𝑂 = ( eval1𝑅 )
fta1g.w 𝑊 = ( 0g𝑅 )
fta1g.z 0 = ( 0g𝑃 )
fta1g.1 ( 𝜑𝑅 ∈ IDomn )
fta1g.2 ( 𝜑𝐹𝐵 )
fta1g.3 ( 𝜑𝐹0 )
Assertion fta1g ( 𝜑 → ( ♯ ‘ ( ( 𝑂𝐹 ) “ { 𝑊 } ) ) ≤ ( 𝐷𝐹 ) )

Proof

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