This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem vietadeg1

Description: The degree of a product of H of linear polynomials of the form X - Z is H . (Contributed by Thierry Arnoux, 15-Feb-2026)

Ref Expression
Hypotheses vieta.w ⊢ 𝑊 = ( Poly1 ‘ 𝑅 )
vieta.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
vieta.3 ⊢ − = ( -g ‘ 𝑊 )
vieta.m ⊢ 𝑀 = ( mulGrp ‘ 𝑊 )
vieta.q ⊢ 𝑄 = ( 𝐼 eval 𝑅 )
vieta.e ⊢ 𝐸 = ( 𝐼 eSymPoly 𝑅 )
vieta.n ⊢ 𝑁 = ( invg ‘ 𝑅 )
vieta.1 ⊢ 1 = ( 1r ‘ 𝑅 )
vieta.t ⊢ · = ( .r ‘ 𝑅 )
vieta.x ⊢ 𝑋 = ( var1 ‘ 𝑅 )
vieta.a ⊢ 𝐴 = ( algSc ‘ 𝑊 )
vieta.p ⊢ ↑ = ( .g ‘ ( mulGrp ‘ 𝑅 ) )
vieta.h ⊢ 𝐻 = ( ♯ ‘ 𝐼 )
vieta.i ⊢ ( 𝜑 → 𝐼 ∈ Fin )
vieta.r ⊢ ( 𝜑 → 𝑅 ∈ IDomn )
vieta.z ⊢ ( 𝜑 → 𝑍 : 𝐼 ⟶ 𝐵 )
vieta.f ⊢ 𝐹 = ( 𝑀 Σg ( 𝑛 ∈ 𝐼 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑍 ‘ 𝑛 ) ) ) ) )
vietadeg1.1 ⊢ 𝐷 = ( deg1 ‘ 𝑅 )
Assertion vietadeg1 ( 𝜑 → ( 𝐷 ‘ 𝐹 ) = 𝐻 )

Proof

Step Hyp Ref Expression
1 vieta.w ⊢ 𝑊 = ( Poly1 ‘ 𝑅 )
2 vieta.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
3 vieta.3 ⊢ − = ( -g ‘ 𝑊 )
4 vieta.m ⊢ 𝑀 = ( mulGrp ‘ 𝑊 )
5 vieta.q ⊢ 𝑄 = ( 𝐼 eval 𝑅 )
6 vieta.e ⊢ 𝐸 = ( 𝐼 eSymPoly 𝑅 )
7 vieta.n ⊢ 𝑁 = ( invg ‘ 𝑅 )
8 vieta.1 ⊢ 1 = ( 1r ‘ 𝑅 )
9 vieta.t ⊢ · = ( .r ‘ 𝑅 )
10 vieta.x ⊢ 𝑋 = ( var1 ‘ 𝑅 )
11 vieta.a ⊢ 𝐴 = ( algSc ‘ 𝑊 )
12 vieta.p ⊢ ↑ = ( .g ‘ ( mulGrp ‘ 𝑅 ) )
13 vieta.h ⊢ 𝐻 = ( ♯ ‘ 𝐼 )
14 vieta.i ⊢ ( 𝜑 → 𝐼 ∈ Fin )
15 vieta.r ⊢ ( 𝜑 → 𝑅 ∈ IDomn )
16 vieta.z ⊢ ( 𝜑 → 𝑍 : 𝐼 ⟶ 𝐵 )
17 vieta.f ⊢ 𝐹 = ( 𝑀 Σg ( 𝑛 ∈ 𝐼 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑍 ‘ 𝑛 ) ) ) ) )
18 vietadeg1.1 ⊢ 𝐷 = ( deg1 ‘ 𝑅 )
19 17 fveq2i ⊢ ( 𝐷 ‘ 𝐹 ) = ( 𝐷 ‘ ( 𝑀 Σg ( 𝑛 ∈ 𝐼 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑍 ‘ 𝑛 ) ) ) ) ) )
20 eqid ⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
21 eqid ⊢ ( 0g ‘ 𝑊 ) = ( 0g ‘ 𝑊 )
22 15 idomringd ⊢ ( 𝜑 → 𝑅 ∈ Ring )
23 1 ply1ring ⊢ ( 𝑅 ∈ Ring → 𝑊 ∈ Ring )
24 ringgrp ⊢ ( 𝑊 ∈ Ring → 𝑊 ∈ Grp )
25 22 23 24 3syl ⊢ ( 𝜑 → 𝑊 ∈ Grp )
26 25 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐼 ) → 𝑊 ∈ Grp )
27 10 1 20 vr1cl ⊢ ( 𝑅 ∈ Ring → 𝑋 ∈ ( Base ‘ 𝑊 ) )
28 22 27 syl ⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ 𝑊 ) )
29 28 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐼 ) → 𝑋 ∈ ( Base ‘ 𝑊 ) )
30 eqid ⊢ ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑊 )
31 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝑊 ) ) = ( Base ‘ ( Scalar ‘ 𝑊 ) )
32 15 idomcringd ⊢ ( 𝜑 → 𝑅 ∈ CRing )
33 1 ply1assa ⊢ ( 𝑅 ∈ CRing → 𝑊 ∈ AssAlg )
34 32 33 syl ⊢ ( 𝜑 → 𝑊 ∈ AssAlg )
35 34 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐼 ) → 𝑊 ∈ AssAlg )
36 16 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐼 ) → ( 𝑍 ‘ 𝑛 ) ∈ 𝐵 )
37 1 ply1sca ⊢ ( 𝑅 ∈ IDomn → 𝑅 = ( Scalar ‘ 𝑊 ) )
38 15 37 syl ⊢ ( 𝜑 → 𝑅 = ( Scalar ‘ 𝑊 ) )
39 38 fveq2d ⊢ ( 𝜑 → ( Base ‘ 𝑅 ) = ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
40 2 39 eqtrid ⊢ ( 𝜑 → 𝐵 = ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
41 40 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐼 ) → 𝐵 = ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
42 36 41 eleqtrd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐼 ) → ( 𝑍 ‘ 𝑛 ) ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
43 11 30 31 35 42 asclelbas ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐼 ) → ( 𝐴 ‘ ( 𝑍 ‘ 𝑛 ) ) ∈ ( Base ‘ 𝑊 ) )
44 20 3 26 29 43 grpsubcld ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐼 ) → ( 𝑋 − ( 𝐴 ‘ ( 𝑍 ‘ 𝑛 ) ) ) ∈ ( Base ‘ 𝑊 ) )
45 15 idomdomd ⊢ ( 𝜑 → 𝑅 ∈ Domn )
46 domnnzr ⊢ ( 𝑅 ∈ Domn → 𝑅 ∈ NzRing )
47 45 46 syl ⊢ ( 𝜑 → 𝑅 ∈ NzRing )
48 18 1 10 47 deg1vr ⊢ ( 𝜑 → ( 𝐷 ‘ 𝑋 ) = 1 )
49 48 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝐼 ) ∧ ( 𝑋 − ( 𝐴 ‘ ( 𝑍 ‘ 𝑛 ) ) ) = ( 0g ‘ 𝑊 ) ) → ( 𝐷 ‘ 𝑋 ) = 1 )
50 18 1 20 deg1cl ⊢ ( 𝑋 ∈ ( Base ‘ 𝑊 ) → ( 𝐷 ‘ 𝑋 ) ∈ ( ℕ0 ∪ { -∞ } ) )
51 28 50 syl ⊢ ( 𝜑 → ( 𝐷 ‘ 𝑋 ) ∈ ( ℕ0 ∪ { -∞ } ) )
52 51 nn0mnfxrd ⊢ ( 𝜑 → ( 𝐷 ‘ 𝑋 ) ∈ ℝ* )
53 52 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝐼 ) ∧ ( 𝑋 − ( 𝐴 ‘ ( 𝑍 ‘ 𝑛 ) ) ) = ( 0g ‘ 𝑊 ) ) → ( 𝐷 ‘ 𝑋 ) ∈ ℝ* )
54 49 53 eqeltrrd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝐼 ) ∧ ( 𝑋 − ( 𝐴 ‘ ( 𝑍 ‘ 𝑛 ) ) ) = ( 0g ‘ 𝑊 ) ) → 1 ∈ ℝ* )
55 51 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝐼 ) ∧ ( 𝑋 − ( 𝐴 ‘ ( 𝑍 ‘ 𝑛 ) ) ) = ( 0g ‘ 𝑊 ) ) → ( 𝐷 ‘ 𝑋 ) ∈ ( ℕ0 ∪ { -∞ } ) )
56 0zd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝐼 ) ∧ ( 𝑋 − ( 𝐴 ‘ ( 𝑍 ‘ 𝑛 ) ) ) = ( 0g ‘ 𝑊 ) ) → 0 ∈ ℤ )
57 26 adantr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝐼 ) ∧ ( 𝑋 − ( 𝐴 ‘ ( 𝑍 ‘ 𝑛 ) ) ) = ( 0g ‘ 𝑊 ) ) → 𝑊 ∈ Grp )
58 29 adantr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝐼 ) ∧ ( 𝑋 − ( 𝐴 ‘ ( 𝑍 ‘ 𝑛 ) ) ) = ( 0g ‘ 𝑊 ) ) → 𝑋 ∈ ( Base ‘ 𝑊 ) )
59 43 adantr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝐼 ) ∧ ( 𝑋 − ( 𝐴 ‘ ( 𝑍 ‘ 𝑛 ) ) ) = ( 0g ‘ 𝑊 ) ) → ( 𝐴 ‘ ( 𝑍 ‘ 𝑛 ) ) ∈ ( Base ‘ 𝑊 ) )
60 simpr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝐼 ) ∧ ( 𝑋 − ( 𝐴 ‘ ( 𝑍 ‘ 𝑛 ) ) ) = ( 0g ‘ 𝑊 ) ) → ( 𝑋 − ( 𝐴 ‘ ( 𝑍 ‘ 𝑛 ) ) ) = ( 0g ‘ 𝑊 ) )
61 20 21 3 grpsubeq0 ⊢ ( ( 𝑊 ∈ Grp ∧ 𝑋 ∈ ( Base ‘ 𝑊 ) ∧ ( 𝐴 ‘ ( 𝑍 ‘ 𝑛 ) ) ∈ ( Base ‘ 𝑊 ) ) → ( ( 𝑋 − ( 𝐴 ‘ ( 𝑍 ‘ 𝑛 ) ) ) = ( 0g ‘ 𝑊 ) ↔ 𝑋 = ( 𝐴 ‘ ( 𝑍 ‘ 𝑛 ) ) ) )
62 61 biimpa ⊢ ( ( ( 𝑊 ∈ Grp ∧ 𝑋 ∈ ( Base ‘ 𝑊 ) ∧ ( 𝐴 ‘ ( 𝑍 ‘ 𝑛 ) ) ∈ ( Base ‘ 𝑊 ) ) ∧ ( 𝑋 − ( 𝐴 ‘ ( 𝑍 ‘ 𝑛 ) ) ) = ( 0g ‘ 𝑊 ) ) → 𝑋 = ( 𝐴 ‘ ( 𝑍 ‘ 𝑛 ) ) )
63 57 58 59 60 62 syl31anc ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝐼 ) ∧ ( 𝑋 − ( 𝐴 ‘ ( 𝑍 ‘ 𝑛 ) ) ) = ( 0g ‘ 𝑊 ) ) → 𝑋 = ( 𝐴 ‘ ( 𝑍 ‘ 𝑛 ) ) )
64 63 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝐼 ) ∧ ( 𝑋 − ( 𝐴 ‘ ( 𝑍 ‘ 𝑛 ) ) ) = ( 0g ‘ 𝑊 ) ) → ( 𝐷 ‘ 𝑋 ) = ( 𝐷 ‘ ( 𝐴 ‘ ( 𝑍 ‘ 𝑛 ) ) ) )
65 22 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐼 ) → 𝑅 ∈ Ring )
66 18 1 2 11 deg1sclle ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑍 ‘ 𝑛 ) ∈ 𝐵 ) → ( 𝐷 ‘ ( 𝐴 ‘ ( 𝑍 ‘ 𝑛 ) ) ) ≤ 0 )
67 65 36 66 syl2anc ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐼 ) → ( 𝐷 ‘ ( 𝐴 ‘ ( 𝑍 ‘ 𝑛 ) ) ) ≤ 0 )
68 67 adantr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝐼 ) ∧ ( 𝑋 − ( 𝐴 ‘ ( 𝑍 ‘ 𝑛 ) ) ) = ( 0g ‘ 𝑊 ) ) → ( 𝐷 ‘ ( 𝐴 ‘ ( 𝑍 ‘ 𝑛 ) ) ) ≤ 0 )
69 64 68 eqbrtrd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝐼 ) ∧ ( 𝑋 − ( 𝐴 ‘ ( 𝑍 ‘ 𝑛 ) ) ) = ( 0g ‘ 𝑊 ) ) → ( 𝐷 ‘ 𝑋 ) ≤ 0 )
70 degltp1le ⊢ ( ( ( 𝐷 ‘ 𝑋 ) ∈ ( ℕ0 ∪ { -∞ } ) ∧ 0 ∈ ℤ ) → ( ( 𝐷 ‘ 𝑋 ) < ( 0 + 1 ) ↔ ( 𝐷 ‘ 𝑋 ) ≤ 0 ) )
71 70 biimpar ⊢ ( ( ( ( 𝐷 ‘ 𝑋 ) ∈ ( ℕ0 ∪ { -∞ } ) ∧ 0 ∈ ℤ ) ∧ ( 𝐷 ‘ 𝑋 ) ≤ 0 ) → ( 𝐷 ‘ 𝑋 ) < ( 0 + 1 ) )
72 55 56 69 71 syl21anc ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝐼 ) ∧ ( 𝑋 − ( 𝐴 ‘ ( 𝑍 ‘ 𝑛 ) ) ) = ( 0g ‘ 𝑊 ) ) → ( 𝐷 ‘ 𝑋 ) < ( 0 + 1 ) )
73 0p1e1 ⊢ ( 0 + 1 ) = 1
74 72 73 breqtrdi ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝐼 ) ∧ ( 𝑋 − ( 𝐴 ‘ ( 𝑍 ‘ 𝑛 ) ) ) = ( 0g ‘ 𝑊 ) ) → ( 𝐷 ‘ 𝑋 ) < 1 )
75 53 54 74 xrgtned ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝐼 ) ∧ ( 𝑋 − ( 𝐴 ‘ ( 𝑍 ‘ 𝑛 ) ) ) = ( 0g ‘ 𝑊 ) ) → 1 ≠ ( 𝐷 ‘ 𝑋 ) )
76 75 necomd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝐼 ) ∧ ( 𝑋 − ( 𝐴 ‘ ( 𝑍 ‘ 𝑛 ) ) ) = ( 0g ‘ 𝑊 ) ) → ( 𝐷 ‘ 𝑋 ) ≠ 1 )
77 76 neneqd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝐼 ) ∧ ( 𝑋 − ( 𝐴 ‘ ( 𝑍 ‘ 𝑛 ) ) ) = ( 0g ‘ 𝑊 ) ) → ¬ ( 𝐷 ‘ 𝑋 ) = 1 )
78 49 77 pm2.65da ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐼 ) → ¬ ( 𝑋 − ( 𝐴 ‘ ( 𝑍 ‘ 𝑛 ) ) ) = ( 0g ‘ 𝑊 ) )
79 78 neqned ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐼 ) → ( 𝑋 − ( 𝐴 ‘ ( 𝑍 ‘ 𝑛 ) ) ) ≠ ( 0g ‘ 𝑊 ) )
80 44 79 eldifsnd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐼 ) → ( 𝑋 − ( 𝐴 ‘ ( 𝑍 ‘ 𝑛 ) ) ) ∈ ( ( Base ‘ 𝑊 ) ∖ { ( 0g ‘ 𝑊 ) } ) )
81 80 fmpttd ⊢ ( 𝜑 → ( 𝑛 ∈ 𝐼 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑍 ‘ 𝑛 ) ) ) ) : 𝐼 ⟶ ( ( Base ‘ 𝑊 ) ∖ { ( 0g ‘ 𝑊 ) } ) )
82 18 1 20 4 21 14 15 81 deg1prod ⊢ ( 𝜑 → ( 𝐷 ‘ ( 𝑀 Σg ( 𝑛 ∈ 𝐼 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑍 ‘ 𝑛 ) ) ) ) ) ) = Σ 𝑘 ∈ 𝐼 ( 𝐷 ‘ ( ( 𝑛 ∈ 𝐼 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑍 ‘ 𝑛 ) ) ) ) ‘ 𝑘 ) ) )
83 eqid ⊢ ( 𝑛 ∈ 𝐼 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑍 ‘ 𝑛 ) ) ) ) = ( 𝑛 ∈ 𝐼 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑍 ‘ 𝑛 ) ) ) )
84 2fveq3 ⊢ ( 𝑛 = 𝑘 → ( 𝐴 ‘ ( 𝑍 ‘ 𝑛 ) ) = ( 𝐴 ‘ ( 𝑍 ‘ 𝑘 ) ) )
85 84 oveq2d ⊢ ( 𝑛 = 𝑘 → ( 𝑋 − ( 𝐴 ‘ ( 𝑍 ‘ 𝑛 ) ) ) = ( 𝑋 − ( 𝐴 ‘ ( 𝑍 ‘ 𝑘 ) ) ) )
86 simpr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) → 𝑘 ∈ 𝐼 )
87 ovexd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) → ( 𝑋 − ( 𝐴 ‘ ( 𝑍 ‘ 𝑘 ) ) ) ∈ V )
88 83 85 86 87 fvmptd3 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) → ( ( 𝑛 ∈ 𝐼 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑍 ‘ 𝑛 ) ) ) ) ‘ 𝑘 ) = ( 𝑋 − ( 𝐴 ‘ ( 𝑍 ‘ 𝑘 ) ) ) )
89 88 fveq2d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) → ( 𝐷 ‘ ( ( 𝑛 ∈ 𝐼 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑍 ‘ 𝑛 ) ) ) ) ‘ 𝑘 ) ) = ( 𝐷 ‘ ( 𝑋 − ( 𝐴 ‘ ( 𝑍 ‘ 𝑘 ) ) ) ) )
90 18 1 20 deg1xrcl ⊢ ( ( 𝐴 ‘ ( 𝑍 ‘ 𝑛 ) ) ∈ ( Base ‘ 𝑊 ) → ( 𝐷 ‘ ( 𝐴 ‘ ( 𝑍 ‘ 𝑛 ) ) ) ∈ ℝ* )
91 43 90 syl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐼 ) → ( 𝐷 ‘ ( 𝐴 ‘ ( 𝑍 ‘ 𝑛 ) ) ) ∈ ℝ* )
92 0xr ⊢ 0 ∈ ℝ*
93 92 a1i ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐼 ) → 0 ∈ ℝ* )
94 1xr ⊢ 1 ∈ ℝ*
95 94 a1i ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐼 ) → 1 ∈ ℝ* )
96 0lt1 ⊢ 0 < 1
97 96 a1i ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐼 ) → 0 < 1 )
98 91 93 95 67 97 xrlelttrd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐼 ) → ( 𝐷 ‘ ( 𝐴 ‘ ( 𝑍 ‘ 𝑛 ) ) ) < 1 )
99 48 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐼 ) → ( 𝐷 ‘ 𝑋 ) = 1 )
100 98 99 breqtrrd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐼 ) → ( 𝐷 ‘ ( 𝐴 ‘ ( 𝑍 ‘ 𝑛 ) ) ) < ( 𝐷 ‘ 𝑋 ) )
101 1 18 65 20 3 29 43 100 deg1sub ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐼 ) → ( 𝐷 ‘ ( 𝑋 − ( 𝐴 ‘ ( 𝑍 ‘ 𝑛 ) ) ) ) = ( 𝐷 ‘ 𝑋 ) )
102 101 99 eqtrd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐼 ) → ( 𝐷 ‘ ( 𝑋 − ( 𝐴 ‘ ( 𝑍 ‘ 𝑛 ) ) ) ) = 1 )
103 102 ralrimiva ⊢ ( 𝜑 → ∀ 𝑛 ∈ 𝐼 ( 𝐷 ‘ ( 𝑋 − ( 𝐴 ‘ ( 𝑍 ‘ 𝑛 ) ) ) ) = 1 )
104 85 fveqeq2d ⊢ ( 𝑛 = 𝑘 → ( ( 𝐷 ‘ ( 𝑋 − ( 𝐴 ‘ ( 𝑍 ‘ 𝑛 ) ) ) ) = 1 ↔ ( 𝐷 ‘ ( 𝑋 − ( 𝐴 ‘ ( 𝑍 ‘ 𝑘 ) ) ) ) = 1 ) )
105 104 cbvralvw ⊢ ( ∀ 𝑛 ∈ 𝐼 ( 𝐷 ‘ ( 𝑋 − ( 𝐴 ‘ ( 𝑍 ‘ 𝑛 ) ) ) ) = 1 ↔ ∀ 𝑘 ∈ 𝐼 ( 𝐷 ‘ ( 𝑋 − ( 𝐴 ‘ ( 𝑍 ‘ 𝑘 ) ) ) ) = 1 )
106 103 105 sylib ⊢ ( 𝜑 → ∀ 𝑘 ∈ 𝐼 ( 𝐷 ‘ ( 𝑋 − ( 𝐴 ‘ ( 𝑍 ‘ 𝑘 ) ) ) ) = 1 )
107 106 r19.21bi ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) → ( 𝐷 ‘ ( 𝑋 − ( 𝐴 ‘ ( 𝑍 ‘ 𝑘 ) ) ) ) = 1 )
108 89 107 eqtrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) → ( 𝐷 ‘ ( ( 𝑛 ∈ 𝐼 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑍 ‘ 𝑛 ) ) ) ) ‘ 𝑘 ) ) = 1 )
109 108 sumeq2dv ⊢ ( 𝜑 → Σ 𝑘 ∈ 𝐼 ( 𝐷 ‘ ( ( 𝑛 ∈ 𝐼 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑍 ‘ 𝑛 ) ) ) ) ‘ 𝑘 ) ) = Σ 𝑘 ∈ 𝐼 1 )
110 1cnd ⊢ ( 𝜑 → 1 ∈ ℂ )
111 fsumconst ⊢ ( ( 𝐼 ∈ Fin ∧ 1 ∈ ℂ ) → Σ 𝑘 ∈ 𝐼 1 = ( ( ♯ ‘ 𝐼 ) · 1 ) )
112 14 110 111 syl2anc ⊢ ( 𝜑 → Σ 𝑘 ∈ 𝐼 1 = ( ( ♯ ‘ 𝐼 ) · 1 ) )
113 hashcl ⊢ ( 𝐼 ∈ Fin → ( ♯ ‘ 𝐼 ) ∈ ℕ0 )
114 14 113 syl ⊢ ( 𝜑 → ( ♯ ‘ 𝐼 ) ∈ ℕ0 )
115 114 nn0cnd ⊢ ( 𝜑 → ( ♯ ‘ 𝐼 ) ∈ ℂ )
116 115 mulridd ⊢ ( 𝜑 → ( ( ♯ ‘ 𝐼 ) · 1 ) = ( ♯ ‘ 𝐼 ) )
117 116 13 eqtr4di ⊢ ( 𝜑 → ( ( ♯ ‘ 𝐼 ) · 1 ) = 𝐻 )
118 109 112 117 3eqtrd ⊢ ( 𝜑 → Σ 𝑘 ∈ 𝐼 ( 𝐷 ‘ ( ( 𝑛 ∈ 𝐼 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑍 ‘ 𝑛 ) ) ) ) ‘ 𝑘 ) ) = 𝐻 )
119 82 118 eqtrd ⊢ ( 𝜑 → ( 𝐷 ‘ ( 𝑀 Σg ( 𝑛 ∈ 𝐼 ↦ ( 𝑋 − ( 𝐴 ‘ ( 𝑍 ‘ 𝑛 ) ) ) ) ) ) = 𝐻 )
120 19 119 eqtrid ⊢ ( 𝜑 → ( 𝐷 ‘ 𝐹 ) = 𝐻 )