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 ffvelcdm ⊢ ( ( ( 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 ffvelcdmd ⊢ ( ( 𝑅 ∈ 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 biimtrid ⊢ ( ( ( 𝑅 ∈ 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 biimtrid ⊢ ( ( 𝑅 ∈ 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 ⊢ ( 𝜑 → ( ♯ ‘ ( ◡ ( 𝑂 ‘ 𝐹 ) “ { 𝑊 } ) ) ≤ ( 𝐷 ‘ 𝐹 ) )