Metamath Proof Explorer

Theorem jensen

Description: Jensen's inequality, a finite extension of the definition of convexity (the last hypothesis). (Contributed by Mario Carneiro, 21-Jun-2015) (Proof shortened by AV, 27-Jul-2019)

Ref Expression
Hypotheses jensen.1 ⊢ ( 𝜑 → 𝐷 ⊆ ℝ )
jensen.2 ⊢ ( 𝜑 → 𝐹 : 𝐷 ⟶ ℝ )
jensen.3 ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐷 ∧ 𝑏 ∈ 𝐷 ) ) → ( 𝑎 [,] 𝑏 ) ⊆ 𝐷 )
jensen.4 ⊢ ( 𝜑 → 𝐴 ∈ Fin )
jensen.5 ⊢ ( 𝜑 → 𝑇 : 𝐴 ⟶ ( 0 [,) +∞ ) )
jensen.6 ⊢ ( 𝜑 → 𝑋 : 𝐴 ⟶ 𝐷 )
jensen.7 ⊢ ( 𝜑 → 0 < ( ℂfld Σg 𝑇 ) )
jensen.8 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ∧ 𝑡 ∈ ( 0 [,] 1 ) ) ) → ( 𝐹 ‘ ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ) ≤ ( ( 𝑡 · ( 𝐹 ‘ 𝑥 ) ) + ( ( 1 − 𝑡 ) · ( 𝐹 ‘ 𝑦 ) ) ) )
Assertion jensen ( 𝜑 → ( ( ( ℂfld Σg ( 𝑇 ∘f · 𝑋 ) ) / ( ℂfld Σg 𝑇 ) ) ∈ 𝐷 ∧ ( 𝐹 ‘ ( ( ℂfld Σg ( 𝑇 ∘f · 𝑋 ) ) / ( ℂfld Σg 𝑇 ) ) ) ≤ ( ( ℂfld Σg ( 𝑇 ∘f · ( 𝐹 ∘ 𝑋 ) ) ) / ( ℂfld Σg 𝑇 ) ) ) )

Proof

Step Hyp Ref Expression
1 jensen.1 ⊢ ( 𝜑 → 𝐷 ⊆ ℝ )
2 jensen.2 ⊢ ( 𝜑 → 𝐹 : 𝐷 ⟶ ℝ )
3 jensen.3 ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐷 ∧ 𝑏 ∈ 𝐷 ) ) → ( 𝑎 [,] 𝑏 ) ⊆ 𝐷 )
4 jensen.4 ⊢ ( 𝜑 → 𝐴 ∈ Fin )
5 jensen.5 ⊢ ( 𝜑 → 𝑇 : 𝐴 ⟶ ( 0 [,) +∞ ) )
6 jensen.6 ⊢ ( 𝜑 → 𝑋 : 𝐴 ⟶ 𝐷 )
7 jensen.7 ⊢ ( 𝜑 → 0 < ( ℂfld Σg 𝑇 ) )
8 jensen.8 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ∧ 𝑡 ∈ ( 0 [,] 1 ) ) ) → ( 𝐹 ‘ ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ) ≤ ( ( 𝑡 · ( 𝐹 ‘ 𝑥 ) ) + ( ( 1 − 𝑡 ) · ( 𝐹 ‘ 𝑦 ) ) ) )
9 5 ffnd ⊢ ( 𝜑 → 𝑇 Fn 𝐴 )
10 fnresdm ⊢ ( 𝑇 Fn 𝐴 → ( 𝑇 ↾ 𝐴 ) = 𝑇 )
11 9 10 syl ⊢ ( 𝜑 → ( 𝑇 ↾ 𝐴 ) = 𝑇 )
12 11 oveq2d ⊢ ( 𝜑 → ( ℂfld Σg ( 𝑇 ↾ 𝐴 ) ) = ( ℂfld Σg 𝑇 ) )
13 7 12 breqtrrd ⊢ ( 𝜑 → 0 < ( ℂfld Σg ( 𝑇 ↾ 𝐴 ) ) )
14 ssid ⊢ 𝐴 ⊆ 𝐴
15 13 14 jctil ⊢ ( 𝜑 → ( 𝐴 ⊆ 𝐴 ∧ 0 < ( ℂfld Σg ( 𝑇 ↾ 𝐴 ) ) ) )
16 sseq1 ⊢ ( 𝑎 = ∅ → ( 𝑎 ⊆ 𝐴 ↔ ∅ ⊆ 𝐴 ) )
17 reseq2 ⊢ ( 𝑎 = ∅ → ( 𝑇 ↾ 𝑎 ) = ( 𝑇 ↾ ∅ ) )
18 res0 ⊢ ( 𝑇 ↾ ∅ ) = ∅
19 17 18 eqtrdi ⊢ ( 𝑎 = ∅ → ( 𝑇 ↾ 𝑎 ) = ∅ )
20 19 oveq2d ⊢ ( 𝑎 = ∅ → ( ℂfld Σg ( 𝑇 ↾ 𝑎 ) ) = ( ℂfld Σg ∅ ) )
21 cnfld0 ⊢ 0 = ( 0g ‘ ℂfld )
22 21 gsum0 ⊢ ( ℂfld Σg ∅ ) = 0
23 20 22 eqtrdi ⊢ ( 𝑎 = ∅ → ( ℂfld Σg ( 𝑇 ↾ 𝑎 ) ) = 0 )
24 23 breq2d ⊢ ( 𝑎 = ∅ → ( 0 < ( ℂfld Σg ( 𝑇 ↾ 𝑎 ) ) ↔ 0 < 0 ) )
25 16 24 anbi12d ⊢ ( 𝑎 = ∅ → ( ( 𝑎 ⊆ 𝐴 ∧ 0 < ( ℂfld Σg ( 𝑇 ↾ 𝑎 ) ) ) ↔ ( ∅ ⊆ 𝐴 ∧ 0 < 0 ) ) )
26 reseq2 ⊢ ( 𝑎 = ∅ → ( ( 𝑇 ∘f · 𝑋 ) ↾ 𝑎 ) = ( ( 𝑇 ∘f · 𝑋 ) ↾ ∅ ) )
27 26 oveq2d ⊢ ( 𝑎 = ∅ → ( ℂfld Σg ( ( 𝑇 ∘f · 𝑋 ) ↾ 𝑎 ) ) = ( ℂfld Σg ( ( 𝑇 ∘f · 𝑋 ) ↾ ∅ ) ) )
28 27 23 oveq12d ⊢ ( 𝑎 = ∅ → ( ( ℂfld Σg ( ( 𝑇 ∘f · 𝑋 ) ↾ 𝑎 ) ) / ( ℂfld Σg ( 𝑇 ↾ 𝑎 ) ) ) = ( ( ℂfld Σg ( ( 𝑇 ∘f · 𝑋 ) ↾ ∅ ) ) / 0 ) )
29 reseq2 ⊢ ( 𝑎 = ∅ → ( ( 𝑇 ∘f · ( 𝐹 ∘ 𝑋 ) ) ↾ 𝑎 ) = ( ( 𝑇 ∘f · ( 𝐹 ∘ 𝑋 ) ) ↾ ∅ ) )
30 29 oveq2d ⊢ ( 𝑎 = ∅ → ( ℂfld Σg ( ( 𝑇 ∘f · ( 𝐹 ∘ 𝑋 ) ) ↾ 𝑎 ) ) = ( ℂfld Σg ( ( 𝑇 ∘f · ( 𝐹 ∘ 𝑋 ) ) ↾ ∅ ) ) )
31 30 23 oveq12d ⊢ ( 𝑎 = ∅ → ( ( ℂfld Σg ( ( 𝑇 ∘f · ( 𝐹 ∘ 𝑋 ) ) ↾ 𝑎 ) ) / ( ℂfld Σg ( 𝑇 ↾ 𝑎 ) ) ) = ( ( ℂfld Σg ( ( 𝑇 ∘f · ( 𝐹 ∘ 𝑋 ) ) ↾ ∅ ) ) / 0 ) )
32 31 breq2d ⊢ ( 𝑎 = ∅ → ( ( 𝐹 ‘ 𝑤 ) ≤ ( ( ℂfld Σg ( ( 𝑇 ∘f · ( 𝐹 ∘ 𝑋 ) ) ↾ 𝑎 ) ) / ( ℂfld Σg ( 𝑇 ↾ 𝑎 ) ) ) ↔ ( 𝐹 ‘ 𝑤 ) ≤ ( ( ℂfld Σg ( ( 𝑇 ∘f · ( 𝐹 ∘ 𝑋 ) ) ↾ ∅ ) ) / 0 ) ) )
33 32 rabbidv ⊢ ( 𝑎 = ∅ → { 𝑤 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑤 ) ≤ ( ( ℂfld Σg ( ( 𝑇 ∘f · ( 𝐹 ∘ 𝑋 ) ) ↾ 𝑎 ) ) / ( ℂfld Σg ( 𝑇 ↾ 𝑎 ) ) ) } = { 𝑤 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑤 ) ≤ ( ( ℂfld Σg ( ( 𝑇 ∘f · ( 𝐹 ∘ 𝑋 ) ) ↾ ∅ ) ) / 0 ) } )
34 28 33 eleq12d ⊢ ( 𝑎 = ∅ → ( ( ( ℂfld Σg ( ( 𝑇 ∘f · 𝑋 ) ↾ 𝑎 ) ) / ( ℂfld Σg ( 𝑇 ↾ 𝑎 ) ) ) ∈ { 𝑤 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑤 ) ≤ ( ( ℂfld Σg ( ( 𝑇 ∘f · ( 𝐹 ∘ 𝑋 ) ) ↾ 𝑎 ) ) / ( ℂfld Σg ( 𝑇 ↾ 𝑎 ) ) ) } ↔ ( ( ℂfld Σg ( ( 𝑇 ∘f · 𝑋 ) ↾ ∅ ) ) / 0 ) ∈ { 𝑤 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑤 ) ≤ ( ( ℂfld Σg ( ( 𝑇 ∘f · ( 𝐹 ∘ 𝑋 ) ) ↾ ∅ ) ) / 0 ) } ) )
35 25 34 imbi12d ⊢ ( 𝑎 = ∅ → ( ( ( 𝑎 ⊆ 𝐴 ∧ 0 < ( ℂfld Σg ( 𝑇 ↾ 𝑎 ) ) ) → ( ( ℂfld Σg ( ( 𝑇 ∘f · 𝑋 ) ↾ 𝑎 ) ) / ( ℂfld Σg ( 𝑇 ↾ 𝑎 ) ) ) ∈ { 𝑤 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑤 ) ≤ ( ( ℂfld Σg ( ( 𝑇 ∘f · ( 𝐹 ∘ 𝑋 ) ) ↾ 𝑎 ) ) / ( ℂfld Σg ( 𝑇 ↾ 𝑎 ) ) ) } ) ↔ ( ( ∅ ⊆ 𝐴 ∧ 0 < 0 ) → ( ( ℂfld Σg ( ( 𝑇 ∘f · 𝑋 ) ↾ ∅ ) ) / 0 ) ∈ { 𝑤 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑤 ) ≤ ( ( ℂfld Σg ( ( 𝑇 ∘f · ( 𝐹 ∘ 𝑋 ) ) ↾ ∅ ) ) / 0 ) } ) ) )
36 35 imbi2d ⊢ ( 𝑎 = ∅ → ( ( 𝜑 → ( ( 𝑎 ⊆ 𝐴 ∧ 0 < ( ℂfld Σg ( 𝑇 ↾ 𝑎 ) ) ) → ( ( ℂfld Σg ( ( 𝑇 ∘f · 𝑋 ) ↾ 𝑎 ) ) / ( ℂfld Σg ( 𝑇 ↾ 𝑎 ) ) ) ∈ { 𝑤 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑤 ) ≤ ( ( ℂfld Σg ( ( 𝑇 ∘f · ( 𝐹 ∘ 𝑋 ) ) ↾ 𝑎 ) ) / ( ℂfld Σg ( 𝑇 ↾ 𝑎 ) ) ) } ) ) ↔ ( 𝜑 → ( ( ∅ ⊆ 𝐴 ∧ 0 < 0 ) → ( ( ℂfld Σg ( ( 𝑇 ∘f · 𝑋 ) ↾ ∅ ) ) / 0 ) ∈ { 𝑤 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑤 ) ≤ ( ( ℂfld Σg ( ( 𝑇 ∘f · ( 𝐹 ∘ 𝑋 ) ) ↾ ∅ ) ) / 0 ) } ) ) ) )
37 sseq1 ⊢ ( 𝑎 = 𝑘 → ( 𝑎 ⊆ 𝐴 ↔ 𝑘 ⊆ 𝐴 ) )
38 reseq2 ⊢ ( 𝑎 = 𝑘 → ( 𝑇 ↾ 𝑎 ) = ( 𝑇 ↾ 𝑘 ) )
39 38 oveq2d ⊢ ( 𝑎 = 𝑘 → ( ℂfld Σg ( 𝑇 ↾ 𝑎 ) ) = ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) )
40 39 breq2d ⊢ ( 𝑎 = 𝑘 → ( 0 < ( ℂfld Σg ( 𝑇 ↾ 𝑎 ) ) ↔ 0 < ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) )
41 37 40 anbi12d ⊢ ( 𝑎 = 𝑘 → ( ( 𝑎 ⊆ 𝐴 ∧ 0 < ( ℂfld Σg ( 𝑇 ↾ 𝑎 ) ) ) ↔ ( 𝑘 ⊆ 𝐴 ∧ 0 < ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) ) )
42 reseq2 ⊢ ( 𝑎 = 𝑘 → ( ( 𝑇 ∘f · 𝑋 ) ↾ 𝑎 ) = ( ( 𝑇 ∘f · 𝑋 ) ↾ 𝑘 ) )
43 42 oveq2d ⊢ ( 𝑎 = 𝑘 → ( ℂfld Σg ( ( 𝑇 ∘f · 𝑋 ) ↾ 𝑎 ) ) = ( ℂfld Σg ( ( 𝑇 ∘f · 𝑋 ) ↾ 𝑘 ) ) )
44 43 39 oveq12d ⊢ ( 𝑎 = 𝑘 → ( ( ℂfld Σg ( ( 𝑇 ∘f · 𝑋 ) ↾ 𝑎 ) ) / ( ℂfld Σg ( 𝑇 ↾ 𝑎 ) ) ) = ( ( ℂfld Σg ( ( 𝑇 ∘f · 𝑋 ) ↾ 𝑘 ) ) / ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) )
45 reseq2 ⊢ ( 𝑎 = 𝑘 → ( ( 𝑇 ∘f · ( 𝐹 ∘ 𝑋 ) ) ↾ 𝑎 ) = ( ( 𝑇 ∘f · ( 𝐹 ∘ 𝑋 ) ) ↾ 𝑘 ) )
46 45 oveq2d ⊢ ( 𝑎 = 𝑘 → ( ℂfld Σg ( ( 𝑇 ∘f · ( 𝐹 ∘ 𝑋 ) ) ↾ 𝑎 ) ) = ( ℂfld Σg ( ( 𝑇 ∘f · ( 𝐹 ∘ 𝑋 ) ) ↾ 𝑘 ) ) )
47 46 39 oveq12d ⊢ ( 𝑎 = 𝑘 → ( ( ℂfld Σg ( ( 𝑇 ∘f · ( 𝐹 ∘ 𝑋 ) ) ↾ 𝑎 ) ) / ( ℂfld Σg ( 𝑇 ↾ 𝑎 ) ) ) = ( ( ℂfld Σg ( ( 𝑇 ∘f · ( 𝐹 ∘ 𝑋 ) ) ↾ 𝑘 ) ) / ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) )
48 47 breq2d ⊢ ( 𝑎 = 𝑘 → ( ( 𝐹 ‘ 𝑤 ) ≤ ( ( ℂfld Σg ( ( 𝑇 ∘f · ( 𝐹 ∘ 𝑋 ) ) ↾ 𝑎 ) ) / ( ℂfld Σg ( 𝑇 ↾ 𝑎 ) ) ) ↔ ( 𝐹 ‘ 𝑤 ) ≤ ( ( ℂfld Σg ( ( 𝑇 ∘f · ( 𝐹 ∘ 𝑋 ) ) ↾ 𝑘 ) ) / ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) ) )
49 48 rabbidv ⊢ ( 𝑎 = 𝑘 → { 𝑤 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑤 ) ≤ ( ( ℂfld Σg ( ( 𝑇 ∘f · ( 𝐹 ∘ 𝑋 ) ) ↾ 𝑎 ) ) / ( ℂfld Σg ( 𝑇 ↾ 𝑎 ) ) ) } = { 𝑤 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑤 ) ≤ ( ( ℂfld Σg ( ( 𝑇 ∘f · ( 𝐹 ∘ 𝑋 ) ) ↾ 𝑘 ) ) / ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) } )
50 44 49 eleq12d ⊢ ( 𝑎 = 𝑘 → ( ( ( ℂfld Σg ( ( 𝑇 ∘f · 𝑋 ) ↾ 𝑎 ) ) / ( ℂfld Σg ( 𝑇 ↾ 𝑎 ) ) ) ∈ { 𝑤 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑤 ) ≤ ( ( ℂfld Σg ( ( 𝑇 ∘f · ( 𝐹 ∘ 𝑋 ) ) ↾ 𝑎 ) ) / ( ℂfld Σg ( 𝑇 ↾ 𝑎 ) ) ) } ↔ ( ( ℂfld Σg ( ( 𝑇 ∘f · 𝑋 ) ↾ 𝑘 ) ) / ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) ∈ { 𝑤 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑤 ) ≤ ( ( ℂfld Σg ( ( 𝑇 ∘f · ( 𝐹 ∘ 𝑋 ) ) ↾ 𝑘 ) ) / ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) } ) )
51 41 50 imbi12d ⊢ ( 𝑎 = 𝑘 → ( ( ( 𝑎 ⊆ 𝐴 ∧ 0 < ( ℂfld Σg ( 𝑇 ↾ 𝑎 ) ) ) → ( ( ℂfld Σg ( ( 𝑇 ∘f · 𝑋 ) ↾ 𝑎 ) ) / ( ℂfld Σg ( 𝑇 ↾ 𝑎 ) ) ) ∈ { 𝑤 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑤 ) ≤ ( ( ℂfld Σg ( ( 𝑇 ∘f · ( 𝐹 ∘ 𝑋 ) ) ↾ 𝑎 ) ) / ( ℂfld Σg ( 𝑇 ↾ 𝑎 ) ) ) } ) ↔ ( ( 𝑘 ⊆ 𝐴 ∧ 0 < ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) → ( ( ℂfld Σg ( ( 𝑇 ∘f · 𝑋 ) ↾ 𝑘 ) ) / ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) ∈ { 𝑤 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑤 ) ≤ ( ( ℂfld Σg ( ( 𝑇 ∘f · ( 𝐹 ∘ 𝑋 ) ) ↾ 𝑘 ) ) / ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) } ) ) )
52 51 imbi2d ⊢ ( 𝑎 = 𝑘 → ( ( 𝜑 → ( ( 𝑎 ⊆ 𝐴 ∧ 0 < ( ℂfld Σg ( 𝑇 ↾ 𝑎 ) ) ) → ( ( ℂfld Σg ( ( 𝑇 ∘f · 𝑋 ) ↾ 𝑎 ) ) / ( ℂfld Σg ( 𝑇 ↾ 𝑎 ) ) ) ∈ { 𝑤 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑤 ) ≤ ( ( ℂfld Σg ( ( 𝑇 ∘f · ( 𝐹 ∘ 𝑋 ) ) ↾ 𝑎 ) ) / ( ℂfld Σg ( 𝑇 ↾ 𝑎 ) ) ) } ) ) ↔ ( 𝜑 → ( ( 𝑘 ⊆ 𝐴 ∧ 0 < ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) → ( ( ℂfld Σg ( ( 𝑇 ∘f · 𝑋 ) ↾ 𝑘 ) ) / ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) ∈ { 𝑤 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑤 ) ≤ ( ( ℂfld Σg ( ( 𝑇 ∘f · ( 𝐹 ∘ 𝑋 ) ) ↾ 𝑘 ) ) / ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) } ) ) ) )
53 sseq1 ⊢ ( 𝑎 = ( 𝑘 ∪ { 𝑐 } ) → ( 𝑎 ⊆ 𝐴 ↔ ( 𝑘 ∪ { 𝑐 } ) ⊆ 𝐴 ) )
54 reseq2 ⊢ ( 𝑎 = ( 𝑘 ∪ { 𝑐 } ) → ( 𝑇 ↾ 𝑎 ) = ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) )
55 54 oveq2d ⊢ ( 𝑎 = ( 𝑘 ∪ { 𝑐 } ) → ( ℂfld Σg ( 𝑇 ↾ 𝑎 ) ) = ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) )
56 55 breq2d ⊢ ( 𝑎 = ( 𝑘 ∪ { 𝑐 } ) → ( 0 < ( ℂfld Σg ( 𝑇 ↾ 𝑎 ) ) ↔ 0 < ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) )
57 53 56 anbi12d ⊢ ( 𝑎 = ( 𝑘 ∪ { 𝑐 } ) → ( ( 𝑎 ⊆ 𝐴 ∧ 0 < ( ℂfld Σg ( 𝑇 ↾ 𝑎 ) ) ) ↔ ( ( 𝑘 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 0 < ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) ) )
58 reseq2 ⊢ ( 𝑎 = ( 𝑘 ∪ { 𝑐 } ) → ( ( 𝑇 ∘f · 𝑋 ) ↾ 𝑎 ) = ( ( 𝑇 ∘f · 𝑋 ) ↾ ( 𝑘 ∪ { 𝑐 } ) ) )
59 58 oveq2d ⊢ ( 𝑎 = ( 𝑘 ∪ { 𝑐 } ) → ( ℂfld Σg ( ( 𝑇 ∘f · 𝑋 ) ↾ 𝑎 ) ) = ( ℂfld Σg ( ( 𝑇 ∘f · 𝑋 ) ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) )
60 59 55 oveq12d ⊢ ( 𝑎 = ( 𝑘 ∪ { 𝑐 } ) → ( ( ℂfld Σg ( ( 𝑇 ∘f · 𝑋 ) ↾ 𝑎 ) ) / ( ℂfld Σg ( 𝑇 ↾ 𝑎 ) ) ) = ( ( ℂfld Σg ( ( 𝑇 ∘f · 𝑋 ) ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) / ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) )
61 reseq2 ⊢ ( 𝑎 = ( 𝑘 ∪ { 𝑐 } ) → ( ( 𝑇 ∘f · ( 𝐹 ∘ 𝑋 ) ) ↾ 𝑎 ) = ( ( 𝑇 ∘f · ( 𝐹 ∘ 𝑋 ) ) ↾ ( 𝑘 ∪ { 𝑐 } ) ) )
62 61 oveq2d ⊢ ( 𝑎 = ( 𝑘 ∪ { 𝑐 } ) → ( ℂfld Σg ( ( 𝑇 ∘f · ( 𝐹 ∘ 𝑋 ) ) ↾ 𝑎 ) ) = ( ℂfld Σg ( ( 𝑇 ∘f · ( 𝐹 ∘ 𝑋 ) ) ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) )
63 62 55 oveq12d ⊢ ( 𝑎 = ( 𝑘 ∪ { 𝑐 } ) → ( ( ℂfld Σg ( ( 𝑇 ∘f · ( 𝐹 ∘ 𝑋 ) ) ↾ 𝑎 ) ) / ( ℂfld Σg ( 𝑇 ↾ 𝑎 ) ) ) = ( ( ℂfld Σg ( ( 𝑇 ∘f · ( 𝐹 ∘ 𝑋 ) ) ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) / ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) )
64 63 breq2d ⊢ ( 𝑎 = ( 𝑘 ∪ { 𝑐 } ) → ( ( 𝐹 ‘ 𝑤 ) ≤ ( ( ℂfld Σg ( ( 𝑇 ∘f · ( 𝐹 ∘ 𝑋 ) ) ↾ 𝑎 ) ) / ( ℂfld Σg ( 𝑇 ↾ 𝑎 ) ) ) ↔ ( 𝐹 ‘ 𝑤 ) ≤ ( ( ℂfld Σg ( ( 𝑇 ∘f · ( 𝐹 ∘ 𝑋 ) ) ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) / ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) ) )
65 64 rabbidv ⊢ ( 𝑎 = ( 𝑘 ∪ { 𝑐 } ) → { 𝑤 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑤 ) ≤ ( ( ℂfld Σg ( ( 𝑇 ∘f · ( 𝐹 ∘ 𝑋 ) ) ↾ 𝑎 ) ) / ( ℂfld Σg ( 𝑇 ↾ 𝑎 ) ) ) } = { 𝑤 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑤 ) ≤ ( ( ℂfld Σg ( ( 𝑇 ∘f · ( 𝐹 ∘ 𝑋 ) ) ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) / ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) } )
66 60 65 eleq12d ⊢ ( 𝑎 = ( 𝑘 ∪ { 𝑐 } ) → ( ( ( ℂfld Σg ( ( 𝑇 ∘f · 𝑋 ) ↾ 𝑎 ) ) / ( ℂfld Σg ( 𝑇 ↾ 𝑎 ) ) ) ∈ { 𝑤 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑤 ) ≤ ( ( ℂfld Σg ( ( 𝑇 ∘f · ( 𝐹 ∘ 𝑋 ) ) ↾ 𝑎 ) ) / ( ℂfld Σg ( 𝑇 ↾ 𝑎 ) ) ) } ↔ ( ( ℂfld Σg ( ( 𝑇 ∘f · 𝑋 ) ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) / ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) ∈ { 𝑤 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑤 ) ≤ ( ( ℂfld Σg ( ( 𝑇 ∘f · ( 𝐹 ∘ 𝑋 ) ) ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) / ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) } ) )
67 57 66 imbi12d ⊢ ( 𝑎 = ( 𝑘 ∪ { 𝑐 } ) → ( ( ( 𝑎 ⊆ 𝐴 ∧ 0 < ( ℂfld Σg ( 𝑇 ↾ 𝑎 ) ) ) → ( ( ℂfld Σg ( ( 𝑇 ∘f · 𝑋 ) ↾ 𝑎 ) ) / ( ℂfld Σg ( 𝑇 ↾ 𝑎 ) ) ) ∈ { 𝑤 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑤 ) ≤ ( ( ℂfld Σg ( ( 𝑇 ∘f · ( 𝐹 ∘ 𝑋 ) ) ↾ 𝑎 ) ) / ( ℂfld Σg ( 𝑇 ↾ 𝑎 ) ) ) } ) ↔ ( ( ( 𝑘 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 0 < ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) → ( ( ℂfld Σg ( ( 𝑇 ∘f · 𝑋 ) ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) / ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) ∈ { 𝑤 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑤 ) ≤ ( ( ℂfld Σg ( ( 𝑇 ∘f · ( 𝐹 ∘ 𝑋 ) ) ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) / ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) } ) ) )
68 67 imbi2d ⊢ ( 𝑎 = ( 𝑘 ∪ { 𝑐 } ) → ( ( 𝜑 → ( ( 𝑎 ⊆ 𝐴 ∧ 0 < ( ℂfld Σg ( 𝑇 ↾ 𝑎 ) ) ) → ( ( ℂfld Σg ( ( 𝑇 ∘f · 𝑋 ) ↾ 𝑎 ) ) / ( ℂfld Σg ( 𝑇 ↾ 𝑎 ) ) ) ∈ { 𝑤 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑤 ) ≤ ( ( ℂfld Σg ( ( 𝑇 ∘f · ( 𝐹 ∘ 𝑋 ) ) ↾ 𝑎 ) ) / ( ℂfld Σg ( 𝑇 ↾ 𝑎 ) ) ) } ) ) ↔ ( 𝜑 → ( ( ( 𝑘 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 0 < ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) → ( ( ℂfld Σg ( ( 𝑇 ∘f · 𝑋 ) ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) / ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) ∈ { 𝑤 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑤 ) ≤ ( ( ℂfld Σg ( ( 𝑇 ∘f · ( 𝐹 ∘ 𝑋 ) ) ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) / ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) } ) ) ) )
69 sseq1 ⊢ ( 𝑎 = 𝐴 → ( 𝑎 ⊆ 𝐴 ↔ 𝐴 ⊆ 𝐴 ) )
70 reseq2 ⊢ ( 𝑎 = 𝐴 → ( 𝑇 ↾ 𝑎 ) = ( 𝑇 ↾ 𝐴 ) )
71 70 oveq2d ⊢ ( 𝑎 = 𝐴 → ( ℂfld Σg ( 𝑇 ↾ 𝑎 ) ) = ( ℂfld Σg ( 𝑇 ↾ 𝐴 ) ) )
72 71 breq2d ⊢ ( 𝑎 = 𝐴 → ( 0 < ( ℂfld Σg ( 𝑇 ↾ 𝑎 ) ) ↔ 0 < ( ℂfld Σg ( 𝑇 ↾ 𝐴 ) ) ) )
73 69 72 anbi12d ⊢ ( 𝑎 = 𝐴 → ( ( 𝑎 ⊆ 𝐴 ∧ 0 < ( ℂfld Σg ( 𝑇 ↾ 𝑎 ) ) ) ↔ ( 𝐴 ⊆ 𝐴 ∧ 0 < ( ℂfld Σg ( 𝑇 ↾ 𝐴 ) ) ) ) )
74 reseq2 ⊢ ( 𝑎 = 𝐴 → ( ( 𝑇 ∘f · 𝑋 ) ↾ 𝑎 ) = ( ( 𝑇 ∘f · 𝑋 ) ↾ 𝐴 ) )
75 74 oveq2d ⊢ ( 𝑎 = 𝐴 → ( ℂfld Σg ( ( 𝑇 ∘f · 𝑋 ) ↾ 𝑎 ) ) = ( ℂfld Σg ( ( 𝑇 ∘f · 𝑋 ) ↾ 𝐴 ) ) )
76 75 71 oveq12d ⊢ ( 𝑎 = 𝐴 → ( ( ℂfld Σg ( ( 𝑇 ∘f · 𝑋 ) ↾ 𝑎 ) ) / ( ℂfld Σg ( 𝑇 ↾ 𝑎 ) ) ) = ( ( ℂfld Σg ( ( 𝑇 ∘f · 𝑋 ) ↾ 𝐴 ) ) / ( ℂfld Σg ( 𝑇 ↾ 𝐴 ) ) ) )
77 reseq2 ⊢ ( 𝑎 = 𝐴 → ( ( 𝑇 ∘f · ( 𝐹 ∘ 𝑋 ) ) ↾ 𝑎 ) = ( ( 𝑇 ∘f · ( 𝐹 ∘ 𝑋 ) ) ↾ 𝐴 ) )
78 77 oveq2d ⊢ ( 𝑎 = 𝐴 → ( ℂfld Σg ( ( 𝑇 ∘f · ( 𝐹 ∘ 𝑋 ) ) ↾ 𝑎 ) ) = ( ℂfld Σg ( ( 𝑇 ∘f · ( 𝐹 ∘ 𝑋 ) ) ↾ 𝐴 ) ) )
79 78 71 oveq12d ⊢ ( 𝑎 = 𝐴 → ( ( ℂfld Σg ( ( 𝑇 ∘f · ( 𝐹 ∘ 𝑋 ) ) ↾ 𝑎 ) ) / ( ℂfld Σg ( 𝑇 ↾ 𝑎 ) ) ) = ( ( ℂfld Σg ( ( 𝑇 ∘f · ( 𝐹 ∘ 𝑋 ) ) ↾ 𝐴 ) ) / ( ℂfld Σg ( 𝑇 ↾ 𝐴 ) ) ) )
80 79 breq2d ⊢ ( 𝑎 = 𝐴 → ( ( 𝐹 ‘ 𝑤 ) ≤ ( ( ℂfld Σg ( ( 𝑇 ∘f · ( 𝐹 ∘ 𝑋 ) ) ↾ 𝑎 ) ) / ( ℂfld Σg ( 𝑇 ↾ 𝑎 ) ) ) ↔ ( 𝐹 ‘ 𝑤 ) ≤ ( ( ℂfld Σg ( ( 𝑇 ∘f · ( 𝐹 ∘ 𝑋 ) ) ↾ 𝐴 ) ) / ( ℂfld Σg ( 𝑇 ↾ 𝐴 ) ) ) ) )
81 80 rabbidv ⊢ ( 𝑎 = 𝐴 → { 𝑤 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑤 ) ≤ ( ( ℂfld Σg ( ( 𝑇 ∘f · ( 𝐹 ∘ 𝑋 ) ) ↾ 𝑎 ) ) / ( ℂfld Σg ( 𝑇 ↾ 𝑎 ) ) ) } = { 𝑤 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑤 ) ≤ ( ( ℂfld Σg ( ( 𝑇 ∘f · ( 𝐹 ∘ 𝑋 ) ) ↾ 𝐴 ) ) / ( ℂfld Σg ( 𝑇 ↾ 𝐴 ) ) ) } )
82 76 81 eleq12d ⊢ ( 𝑎 = 𝐴 → ( ( ( ℂfld Σg ( ( 𝑇 ∘f · 𝑋 ) ↾ 𝑎 ) ) / ( ℂfld Σg ( 𝑇 ↾ 𝑎 ) ) ) ∈ { 𝑤 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑤 ) ≤ ( ( ℂfld Σg ( ( 𝑇 ∘f · ( 𝐹 ∘ 𝑋 ) ) ↾ 𝑎 ) ) / ( ℂfld Σg ( 𝑇 ↾ 𝑎 ) ) ) } ↔ ( ( ℂfld Σg ( ( 𝑇 ∘f · 𝑋 ) ↾ 𝐴 ) ) / ( ℂfld Σg ( 𝑇 ↾ 𝐴 ) ) ) ∈ { 𝑤 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑤 ) ≤ ( ( ℂfld Σg ( ( 𝑇 ∘f · ( 𝐹 ∘ 𝑋 ) ) ↾ 𝐴 ) ) / ( ℂfld Σg ( 𝑇 ↾ 𝐴 ) ) ) } ) )
83 73 82 imbi12d ⊢ ( 𝑎 = 𝐴 → ( ( ( 𝑎 ⊆ 𝐴 ∧ 0 < ( ℂfld Σg ( 𝑇 ↾ 𝑎 ) ) ) → ( ( ℂfld Σg ( ( 𝑇 ∘f · 𝑋 ) ↾ 𝑎 ) ) / ( ℂfld Σg ( 𝑇 ↾ 𝑎 ) ) ) ∈ { 𝑤 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑤 ) ≤ ( ( ℂfld Σg ( ( 𝑇 ∘f · ( 𝐹 ∘ 𝑋 ) ) ↾ 𝑎 ) ) / ( ℂfld Σg ( 𝑇 ↾ 𝑎 ) ) ) } ) ↔ ( ( 𝐴 ⊆ 𝐴 ∧ 0 < ( ℂfld Σg ( 𝑇 ↾ 𝐴 ) ) ) → ( ( ℂfld Σg ( ( 𝑇 ∘f · 𝑋 ) ↾ 𝐴 ) ) / ( ℂfld Σg ( 𝑇 ↾ 𝐴 ) ) ) ∈ { 𝑤 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑤 ) ≤ ( ( ℂfld Σg ( ( 𝑇 ∘f · ( 𝐹 ∘ 𝑋 ) ) ↾ 𝐴 ) ) / ( ℂfld Σg ( 𝑇 ↾ 𝐴 ) ) ) } ) ) )
84 83 imbi2d ⊢ ( 𝑎 = 𝐴 → ( ( 𝜑 → ( ( 𝑎 ⊆ 𝐴 ∧ 0 < ( ℂfld Σg ( 𝑇 ↾ 𝑎 ) ) ) → ( ( ℂfld Σg ( ( 𝑇 ∘f · 𝑋 ) ↾ 𝑎 ) ) / ( ℂfld Σg ( 𝑇 ↾ 𝑎 ) ) ) ∈ { 𝑤 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑤 ) ≤ ( ( ℂfld Σg ( ( 𝑇 ∘f · ( 𝐹 ∘ 𝑋 ) ) ↾ 𝑎 ) ) / ( ℂfld Σg ( 𝑇 ↾ 𝑎 ) ) ) } ) ) ↔ ( 𝜑 → ( ( 𝐴 ⊆ 𝐴 ∧ 0 < ( ℂfld Σg ( 𝑇 ↾ 𝐴 ) ) ) → ( ( ℂfld Σg ( ( 𝑇 ∘f · 𝑋 ) ↾ 𝐴 ) ) / ( ℂfld Σg ( 𝑇 ↾ 𝐴 ) ) ) ∈ { 𝑤 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑤 ) ≤ ( ( ℂfld Σg ( ( 𝑇 ∘f · ( 𝐹 ∘ 𝑋 ) ) ↾ 𝐴 ) ) / ( ℂfld Σg ( 𝑇 ↾ 𝐴 ) ) ) } ) ) ) )
85 0re ⊢ 0 ∈ ℝ
86 85 ltnri ⊢ ¬ 0 < 0
87 86 pm2.21i ⊢ ( 0 < 0 → ( ( ℂfld Σg ( ( 𝑇 ∘f · 𝑋 ) ↾ ∅ ) ) / 0 ) ∈ { 𝑤 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑤 ) ≤ ( ( ℂfld Σg ( ( 𝑇 ∘f · ( 𝐹 ∘ 𝑋 ) ) ↾ ∅ ) ) / 0 ) } )
88 87 adantl ⊢ ( ( ∅ ⊆ 𝐴 ∧ 0 < 0 ) → ( ( ℂfld Σg ( ( 𝑇 ∘f · 𝑋 ) ↾ ∅ ) ) / 0 ) ∈ { 𝑤 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑤 ) ≤ ( ( ℂfld Σg ( ( 𝑇 ∘f · ( 𝐹 ∘ 𝑋 ) ) ↾ ∅ ) ) / 0 ) } )
89 88 a1i ⊢ ( 𝜑 → ( ( ∅ ⊆ 𝐴 ∧ 0 < 0 ) → ( ( ℂfld Σg ( ( 𝑇 ∘f · 𝑋 ) ↾ ∅ ) ) / 0 ) ∈ { 𝑤 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑤 ) ≤ ( ( ℂfld Σg ( ( 𝑇 ∘f · ( 𝐹 ∘ 𝑋 ) ) ↾ ∅ ) ) / 0 ) } ) )
90 impexp ⊢ ( ( ( 𝑘 ⊆ 𝐴 ∧ 0 < ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) → ( ( ℂfld Σg ( ( 𝑇 ∘f · 𝑋 ) ↾ 𝑘 ) ) / ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) ∈ { 𝑤 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑤 ) ≤ ( ( ℂfld Σg ( ( 𝑇 ∘f · ( 𝐹 ∘ 𝑋 ) ) ↾ 𝑘 ) ) / ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) } ) ↔ ( 𝑘 ⊆ 𝐴 → ( 0 < ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) → ( ( ℂfld Σg ( ( 𝑇 ∘f · 𝑋 ) ↾ 𝑘 ) ) / ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) ∈ { 𝑤 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑤 ) ≤ ( ( ℂfld Σg ( ( 𝑇 ∘f · ( 𝐹 ∘ 𝑋 ) ) ↾ 𝑘 ) ) / ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) } ) ) )
91 simprl ⊢ ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑘 ) ∧ ( ( 𝑘 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 0 < ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) ) → ( 𝑘 ∪ { 𝑐 } ) ⊆ 𝐴 )
92 91 unssad ⊢ ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑘 ) ∧ ( ( 𝑘 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 0 < ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) ) → 𝑘 ⊆ 𝐴 )
93 simpr ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑘 ) ∧ ( ( 𝑘 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 0 < ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) ) ∧ 0 < ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) → 0 < ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) )
94 1 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑘 ) ∧ ( ( 𝑘 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 0 < ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) ) ∧ ( 0 < ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ∧ ( ( ℂfld Σg ( ( 𝑇 ∘f · 𝑋 ) ↾ 𝑘 ) ) / ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) ∈ { 𝑤 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑤 ) ≤ ( ( ℂfld Σg ( ( 𝑇 ∘f · ( 𝐹 ∘ 𝑋 ) ) ↾ 𝑘 ) ) / ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) } ) ) → 𝐷 ⊆ ℝ )
95 2 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑘 ) ∧ ( ( 𝑘 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 0 < ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) ) ∧ ( 0 < ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ∧ ( ( ℂfld Σg ( ( 𝑇 ∘f · 𝑋 ) ↾ 𝑘 ) ) / ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) ∈ { 𝑤 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑤 ) ≤ ( ( ℂfld Σg ( ( 𝑇 ∘f · ( 𝐹 ∘ 𝑋 ) ) ↾ 𝑘 ) ) / ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) } ) ) → 𝐹 : 𝐷 ⟶ ℝ )
96 simplll ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑘 ) ∧ ( ( 𝑘 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 0 < ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) ) ∧ ( 0 < ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ∧ ( ( ℂfld Σg ( ( 𝑇 ∘f · 𝑋 ) ↾ 𝑘 ) ) / ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) ∈ { 𝑤 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑤 ) ≤ ( ( ℂfld Σg ( ( 𝑇 ∘f · ( 𝐹 ∘ 𝑋 ) ) ↾ 𝑘 ) ) / ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) } ) ) → 𝜑 )
97 96 3 sylan ⊢ ( ( ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑘 ) ∧ ( ( 𝑘 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 0 < ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) ) ∧ ( 0 < ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ∧ ( ( ℂfld Σg ( ( 𝑇 ∘f · 𝑋 ) ↾ 𝑘 ) ) / ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) ∈ { 𝑤 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑤 ) ≤ ( ( ℂfld Σg ( ( 𝑇 ∘f · ( 𝐹 ∘ 𝑋 ) ) ↾ 𝑘 ) ) / ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) } ) ) ∧ ( 𝑎 ∈ 𝐷 ∧ 𝑏 ∈ 𝐷 ) ) → ( 𝑎 [,] 𝑏 ) ⊆ 𝐷 )
98 96 4 syl ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑘 ) ∧ ( ( 𝑘 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 0 < ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) ) ∧ ( 0 < ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ∧ ( ( ℂfld Σg ( ( 𝑇 ∘f · 𝑋 ) ↾ 𝑘 ) ) / ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) ∈ { 𝑤 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑤 ) ≤ ( ( ℂfld Σg ( ( 𝑇 ∘f · ( 𝐹 ∘ 𝑋 ) ) ↾ 𝑘 ) ) / ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) } ) ) → 𝐴 ∈ Fin )
99 96 5 syl ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑘 ) ∧ ( ( 𝑘 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 0 < ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) ) ∧ ( 0 < ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ∧ ( ( ℂfld Σg ( ( 𝑇 ∘f · 𝑋 ) ↾ 𝑘 ) ) / ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) ∈ { 𝑤 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑤 ) ≤ ( ( ℂfld Σg ( ( 𝑇 ∘f · ( 𝐹 ∘ 𝑋 ) ) ↾ 𝑘 ) ) / ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) } ) ) → 𝑇 : 𝐴 ⟶ ( 0 [,) +∞ ) )
100 96 6 syl ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑘 ) ∧ ( ( 𝑘 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 0 < ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) ) ∧ ( 0 < ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ∧ ( ( ℂfld Σg ( ( 𝑇 ∘f · 𝑋 ) ↾ 𝑘 ) ) / ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) ∈ { 𝑤 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑤 ) ≤ ( ( ℂfld Σg ( ( 𝑇 ∘f · ( 𝐹 ∘ 𝑋 ) ) ↾ 𝑘 ) ) / ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) } ) ) → 𝑋 : 𝐴 ⟶ 𝐷 )
101 7 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑘 ) ∧ ( ( 𝑘 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 0 < ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) ) ∧ ( 0 < ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ∧ ( ( ℂfld Σg ( ( 𝑇 ∘f · 𝑋 ) ↾ 𝑘 ) ) / ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) ∈ { 𝑤 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑤 ) ≤ ( ( ℂfld Σg ( ( 𝑇 ∘f · ( 𝐹 ∘ 𝑋 ) ) ↾ 𝑘 ) ) / ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) } ) ) → 0 < ( ℂfld Σg 𝑇 ) )
102 96 8 sylan ⊢ ( ( ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑘 ) ∧ ( ( 𝑘 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 0 < ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) ) ∧ ( 0 < ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ∧ ( ( ℂfld Σg ( ( 𝑇 ∘f · 𝑋 ) ↾ 𝑘 ) ) / ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) ∈ { 𝑤 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑤 ) ≤ ( ( ℂfld Σg ( ( 𝑇 ∘f · ( 𝐹 ∘ 𝑋 ) ) ↾ 𝑘 ) ) / ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) } ) ) ∧ ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ∧ 𝑡 ∈ ( 0 [,] 1 ) ) ) → ( 𝐹 ‘ ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ) ≤ ( ( 𝑡 · ( 𝐹 ‘ 𝑥 ) ) + ( ( 1 − 𝑡 ) · ( 𝐹 ‘ 𝑦 ) ) ) )
103 simpllr ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑘 ) ∧ ( ( 𝑘 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 0 < ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) ) ∧ ( 0 < ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ∧ ( ( ℂfld Σg ( ( 𝑇 ∘f · 𝑋 ) ↾ 𝑘 ) ) / ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) ∈ { 𝑤 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑤 ) ≤ ( ( ℂfld Σg ( ( 𝑇 ∘f · ( 𝐹 ∘ 𝑋 ) ) ↾ 𝑘 ) ) / ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) } ) ) → ¬ 𝑐 ∈ 𝑘 )
104 91 adantr ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑘 ) ∧ ( ( 𝑘 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 0 < ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) ) ∧ ( 0 < ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ∧ ( ( ℂfld Σg ( ( 𝑇 ∘f · 𝑋 ) ↾ 𝑘 ) ) / ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) ∈ { 𝑤 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑤 ) ≤ ( ( ℂfld Σg ( ( 𝑇 ∘f · ( 𝐹 ∘ 𝑋 ) ) ↾ 𝑘 ) ) / ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) } ) ) → ( 𝑘 ∪ { 𝑐 } ) ⊆ 𝐴 )
105 eqid ⊢ ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) = ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) )
106 eqid ⊢ ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) = ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) )
107 cnring ⊢ ℂfld ∈ Ring
108 ringcmn ⊢ ( ℂfld ∈ Ring → ℂfld ∈ CMnd )
109 107 108 mp1i ⊢ ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑘 ) ∧ ( ( 𝑘 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 0 < ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) ) → ℂfld ∈ CMnd )
110 4 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑘 ) ∧ ( ( 𝑘 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 0 < ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) ) → 𝐴 ∈ Fin )
111 110 92 ssfid ⊢ ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑘 ) ∧ ( ( 𝑘 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 0 < ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) ) → 𝑘 ∈ Fin )
112 rege0subm ⊢ ( 0 [,) +∞ ) ∈ ( SubMnd ‘ ℂfld )
113 112 a1i ⊢ ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑘 ) ∧ ( ( 𝑘 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 0 < ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) ) → ( 0 [,) +∞ ) ∈ ( SubMnd ‘ ℂfld ) )
114 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑘 ) ∧ ( ( 𝑘 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 0 < ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) ) → 𝑇 : 𝐴 ⟶ ( 0 [,) +∞ ) )
115 114 92 fssresd ⊢ ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑘 ) ∧ ( ( 𝑘 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 0 < ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) ) → ( 𝑇 ↾ 𝑘 ) : 𝑘 ⟶ ( 0 [,) +∞ ) )
116 c0ex ⊢ 0 ∈ V
117 116 a1i ⊢ ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑘 ) ∧ ( ( 𝑘 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 0 < ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) ) → 0 ∈ V )
118 115 111 117 fdmfifsupp ⊢ ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑘 ) ∧ ( ( 𝑘 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 0 < ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) ) → ( 𝑇 ↾ 𝑘 ) finSupp 0 )
119 21 109 111 113 115 118 gsumsubmcl ⊢ ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑘 ) ∧ ( ( 𝑘 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 0 < ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) ) → ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ∈ ( 0 [,) +∞ ) )
120 elrege0 ⊢ ( ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ∈ ( 0 [,) +∞ ) ↔ ( ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ∈ ℝ ∧ 0 ≤ ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) )
121 120 simplbi ⊢ ( ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ∈ ( 0 [,) +∞ ) → ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ∈ ℝ )
122 119 121 syl ⊢ ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑘 ) ∧ ( ( 𝑘 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 0 < ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) ) → ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ∈ ℝ )
123 122 adantr ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑘 ) ∧ ( ( 𝑘 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 0 < ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) ) ∧ ( 0 < ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ∧ ( ( ℂfld Σg ( ( 𝑇 ∘f · 𝑋 ) ↾ 𝑘 ) ) / ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) ∈ { 𝑤 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑤 ) ≤ ( ( ℂfld Σg ( ( 𝑇 ∘f · ( 𝐹 ∘ 𝑋 ) ) ↾ 𝑘 ) ) / ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) } ) ) → ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ∈ ℝ )
124 simprl ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑘 ) ∧ ( ( 𝑘 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 0 < ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) ) ∧ ( 0 < ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ∧ ( ( ℂfld Σg ( ( 𝑇 ∘f · 𝑋 ) ↾ 𝑘 ) ) / ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) ∈ { 𝑤 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑤 ) ≤ ( ( ℂfld Σg ( ( 𝑇 ∘f · ( 𝐹 ∘ 𝑋 ) ) ↾ 𝑘 ) ) / ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) } ) ) → 0 < ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) )
125 123 124 elrpd ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑘 ) ∧ ( ( 𝑘 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 0 < ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) ) ∧ ( 0 < ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ∧ ( ( ℂfld Σg ( ( 𝑇 ∘f · 𝑋 ) ↾ 𝑘 ) ) / ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) ∈ { 𝑤 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑤 ) ≤ ( ( ℂfld Σg ( ( 𝑇 ∘f · ( 𝐹 ∘ 𝑋 ) ) ↾ 𝑘 ) ) / ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) } ) ) → ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ∈ ℝ+ )
126 simprr ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑘 ) ∧ ( ( 𝑘 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 0 < ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) ) ∧ ( 0 < ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ∧ ( ( ℂfld Σg ( ( 𝑇 ∘f · 𝑋 ) ↾ 𝑘 ) ) / ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) ∈ { 𝑤 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑤 ) ≤ ( ( ℂfld Σg ( ( 𝑇 ∘f · ( 𝐹 ∘ 𝑋 ) ) ↾ 𝑘 ) ) / ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) } ) ) → ( ( ℂfld Σg ( ( 𝑇 ∘f · 𝑋 ) ↾ 𝑘 ) ) / ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) ∈ { 𝑤 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑤 ) ≤ ( ( ℂfld Σg ( ( 𝑇 ∘f · ( 𝐹 ∘ 𝑋 ) ) ↾ 𝑘 ) ) / ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) } )
127 fveq2 ⊢ ( 𝑤 = ( ( ℂfld Σg ( ( 𝑇 ∘f · 𝑋 ) ↾ 𝑘 ) ) / ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) → ( 𝐹 ‘ 𝑤 ) = ( 𝐹 ‘ ( ( ℂfld Σg ( ( 𝑇 ∘f · 𝑋 ) ↾ 𝑘 ) ) / ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) ) )
128 127 breq1d ⊢ ( 𝑤 = ( ( ℂfld Σg ( ( 𝑇 ∘f · 𝑋 ) ↾ 𝑘 ) ) / ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) → ( ( 𝐹 ‘ 𝑤 ) ≤ ( ( ℂfld Σg ( ( 𝑇 ∘f · ( 𝐹 ∘ 𝑋 ) ) ↾ 𝑘 ) ) / ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) ↔ ( 𝐹 ‘ ( ( ℂfld Σg ( ( 𝑇 ∘f · 𝑋 ) ↾ 𝑘 ) ) / ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) ) ≤ ( ( ℂfld Σg ( ( 𝑇 ∘f · ( 𝐹 ∘ 𝑋 ) ) ↾ 𝑘 ) ) / ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) ) )
129 128 elrab ⊢ ( ( ( ℂfld Σg ( ( 𝑇 ∘f · 𝑋 ) ↾ 𝑘 ) ) / ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) ∈ { 𝑤 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑤 ) ≤ ( ( ℂfld Σg ( ( 𝑇 ∘f · ( 𝐹 ∘ 𝑋 ) ) ↾ 𝑘 ) ) / ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) } ↔ ( ( ( ℂfld Σg ( ( 𝑇 ∘f · 𝑋 ) ↾ 𝑘 ) ) / ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) ∈ 𝐷 ∧ ( 𝐹 ‘ ( ( ℂfld Σg ( ( 𝑇 ∘f · 𝑋 ) ↾ 𝑘 ) ) / ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) ) ≤ ( ( ℂfld Σg ( ( 𝑇 ∘f · ( 𝐹 ∘ 𝑋 ) ) ↾ 𝑘 ) ) / ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) ) )
130 126 129 sylib ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑘 ) ∧ ( ( 𝑘 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 0 < ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) ) ∧ ( 0 < ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ∧ ( ( ℂfld Σg ( ( 𝑇 ∘f · 𝑋 ) ↾ 𝑘 ) ) / ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) ∈ { 𝑤 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑤 ) ≤ ( ( ℂfld Σg ( ( 𝑇 ∘f · ( 𝐹 ∘ 𝑋 ) ) ↾ 𝑘 ) ) / ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) } ) ) → ( ( ( ℂfld Σg ( ( 𝑇 ∘f · 𝑋 ) ↾ 𝑘 ) ) / ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) ∈ 𝐷 ∧ ( 𝐹 ‘ ( ( ℂfld Σg ( ( 𝑇 ∘f · 𝑋 ) ↾ 𝑘 ) ) / ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) ) ≤ ( ( ℂfld Σg ( ( 𝑇 ∘f · ( 𝐹 ∘ 𝑋 ) ) ↾ 𝑘 ) ) / ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) ) )
131 130 simpld ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑘 ) ∧ ( ( 𝑘 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 0 < ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) ) ∧ ( 0 < ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ∧ ( ( ℂfld Σg ( ( 𝑇 ∘f · 𝑋 ) ↾ 𝑘 ) ) / ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) ∈ { 𝑤 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑤 ) ≤ ( ( ℂfld Σg ( ( 𝑇 ∘f · ( 𝐹 ∘ 𝑋 ) ) ↾ 𝑘 ) ) / ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) } ) ) → ( ( ℂfld Σg ( ( 𝑇 ∘f · 𝑋 ) ↾ 𝑘 ) ) / ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) ∈ 𝐷 )
132 130 simprd ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑘 ) ∧ ( ( 𝑘 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 0 < ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) ) ∧ ( 0 < ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ∧ ( ( ℂfld Σg ( ( 𝑇 ∘f · 𝑋 ) ↾ 𝑘 ) ) / ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) ∈ { 𝑤 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑤 ) ≤ ( ( ℂfld Σg ( ( 𝑇 ∘f · ( 𝐹 ∘ 𝑋 ) ) ↾ 𝑘 ) ) / ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) } ) ) → ( 𝐹 ‘ ( ( ℂfld Σg ( ( 𝑇 ∘f · 𝑋 ) ↾ 𝑘 ) ) / ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) ) ≤ ( ( ℂfld Σg ( ( 𝑇 ∘f · ( 𝐹 ∘ 𝑋 ) ) ↾ 𝑘 ) ) / ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) )
133 94 95 97 98 99 100 101 102 103 104 105 106 125 131 132 jensenlem2 ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑘 ) ∧ ( ( 𝑘 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 0 < ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) ) ∧ ( 0 < ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ∧ ( ( ℂfld Σg ( ( 𝑇 ∘f · 𝑋 ) ↾ 𝑘 ) ) / ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) ∈ { 𝑤 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑤 ) ≤ ( ( ℂfld Σg ( ( 𝑇 ∘f · ( 𝐹 ∘ 𝑋 ) ) ↾ 𝑘 ) ) / ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) } ) ) → ( ( ( ℂfld Σg ( ( 𝑇 ∘f · 𝑋 ) ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) / ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) ∈ 𝐷 ∧ ( 𝐹 ‘ ( ( ℂfld Σg ( ( 𝑇 ∘f · 𝑋 ) ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) / ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) ) ≤ ( ( ℂfld Σg ( ( 𝑇 ∘f · ( 𝐹 ∘ 𝑋 ) ) ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) / ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) ) )
134 fveq2 ⊢ ( 𝑤 = ( ( ℂfld Σg ( ( 𝑇 ∘f · 𝑋 ) ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) / ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) → ( 𝐹 ‘ 𝑤 ) = ( 𝐹 ‘ ( ( ℂfld Σg ( ( 𝑇 ∘f · 𝑋 ) ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) / ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) ) )
135 134 breq1d ⊢ ( 𝑤 = ( ( ℂfld Σg ( ( 𝑇 ∘f · 𝑋 ) ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) / ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) → ( ( 𝐹 ‘ 𝑤 ) ≤ ( ( ℂfld Σg ( ( 𝑇 ∘f · ( 𝐹 ∘ 𝑋 ) ) ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) / ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) ↔ ( 𝐹 ‘ ( ( ℂfld Σg ( ( 𝑇 ∘f · 𝑋 ) ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) / ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) ) ≤ ( ( ℂfld Σg ( ( 𝑇 ∘f · ( 𝐹 ∘ 𝑋 ) ) ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) / ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) ) )
136 135 elrab ⊢ ( ( ( ℂfld Σg ( ( 𝑇 ∘f · 𝑋 ) ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) / ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) ∈ { 𝑤 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑤 ) ≤ ( ( ℂfld Σg ( ( 𝑇 ∘f · ( 𝐹 ∘ 𝑋 ) ) ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) / ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) } ↔ ( ( ( ℂfld Σg ( ( 𝑇 ∘f · 𝑋 ) ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) / ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) ∈ 𝐷 ∧ ( 𝐹 ‘ ( ( ℂfld Σg ( ( 𝑇 ∘f · 𝑋 ) ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) / ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) ) ≤ ( ( ℂfld Σg ( ( 𝑇 ∘f · ( 𝐹 ∘ 𝑋 ) ) ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) / ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) ) )
137 133 136 sylibr ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑘 ) ∧ ( ( 𝑘 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 0 < ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) ) ∧ ( 0 < ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ∧ ( ( ℂfld Σg ( ( 𝑇 ∘f · 𝑋 ) ↾ 𝑘 ) ) / ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) ∈ { 𝑤 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑤 ) ≤ ( ( ℂfld Σg ( ( 𝑇 ∘f · ( 𝐹 ∘ 𝑋 ) ) ↾ 𝑘 ) ) / ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) } ) ) → ( ( ℂfld Σg ( ( 𝑇 ∘f · 𝑋 ) ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) / ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) ∈ { 𝑤 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑤 ) ≤ ( ( ℂfld Σg ( ( 𝑇 ∘f · ( 𝐹 ∘ 𝑋 ) ) ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) / ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) } )
138 137 expr ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑘 ) ∧ ( ( 𝑘 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 0 < ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) ) ∧ 0 < ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) → ( ( ( ℂfld Σg ( ( 𝑇 ∘f · 𝑋 ) ↾ 𝑘 ) ) / ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) ∈ { 𝑤 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑤 ) ≤ ( ( ℂfld Σg ( ( 𝑇 ∘f · ( 𝐹 ∘ 𝑋 ) ) ↾ 𝑘 ) ) / ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) } → ( ( ℂfld Σg ( ( 𝑇 ∘f · 𝑋 ) ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) / ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) ∈ { 𝑤 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑤 ) ≤ ( ( ℂfld Σg ( ( 𝑇 ∘f · ( 𝐹 ∘ 𝑋 ) ) ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) / ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) } ) )
139 93 138 embantd ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑘 ) ∧ ( ( 𝑘 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 0 < ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) ) ∧ 0 < ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) → ( ( 0 < ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) → ( ( ℂfld Σg ( ( 𝑇 ∘f · 𝑋 ) ↾ 𝑘 ) ) / ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) ∈ { 𝑤 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑤 ) ≤ ( ( ℂfld Σg ( ( 𝑇 ∘f · ( 𝐹 ∘ 𝑋 ) ) ↾ 𝑘 ) ) / ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) } ) → ( ( ℂfld Σg ( ( 𝑇 ∘f · 𝑋 ) ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) / ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) ∈ { 𝑤 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑤 ) ≤ ( ( ℂfld Σg ( ( 𝑇 ∘f · ( 𝐹 ∘ 𝑋 ) ) ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) / ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) } ) )
140 cnfldbas ⊢ ℂ = ( Base ‘ ℂfld )
141 ringmnd ⊢ ( ℂfld ∈ Ring → ℂfld ∈ Mnd )
142 107 141 mp1i ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑘 ) ∧ ( ( 𝑘 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 0 < ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) ) ∧ 0 = ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) → ℂfld ∈ Mnd )
143 110 91 ssfid ⊢ ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑘 ) ∧ ( ( 𝑘 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 0 < ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) ) → ( 𝑘 ∪ { 𝑐 } ) ∈ Fin )
144 143 adantr ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑘 ) ∧ ( ( 𝑘 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 0 < ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) ) ∧ 0 = ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) → ( 𝑘 ∪ { 𝑐 } ) ∈ Fin )
145 ssun2 ⊢ { 𝑐 } ⊆ ( 𝑘 ∪ { 𝑐 } )
146 vsnid ⊢ 𝑐 ∈ { 𝑐 }
147 145 146 sselii ⊢ 𝑐 ∈ ( 𝑘 ∪ { 𝑐 } )
148 147 a1i ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑘 ) ∧ ( ( 𝑘 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 0 < ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) ) ∧ 0 = ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) → 𝑐 ∈ ( 𝑘 ∪ { 𝑐 } ) )
149 remulcl ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( 𝑥 · 𝑦 ) ∈ ℝ )
150 149 adantl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ) → ( 𝑥 · 𝑦 ) ∈ ℝ )
151 rge0ssre ⊢ ( 0 [,) +∞ ) ⊆ ℝ
152 fss ⊢ ( ( 𝑇 : 𝐴 ⟶ ( 0 [,) +∞ ) ∧ ( 0 [,) +∞ ) ⊆ ℝ ) → 𝑇 : 𝐴 ⟶ ℝ )
153 5 151 152 sylancl ⊢ ( 𝜑 → 𝑇 : 𝐴 ⟶ ℝ )
154 6 1 fssd ⊢ ( 𝜑 → 𝑋 : 𝐴 ⟶ ℝ )
155 inidm ⊢ ( 𝐴 ∩ 𝐴 ) = 𝐴
156 150 153 154 4 4 155 off ⊢ ( 𝜑 → ( 𝑇 ∘f · 𝑋 ) : 𝐴 ⟶ ℝ )
157 ax-resscn ⊢ ℝ ⊆ ℂ
158 fss ⊢ ( ( ( 𝑇 ∘f · 𝑋 ) : 𝐴 ⟶ ℝ ∧ ℝ ⊆ ℂ ) → ( 𝑇 ∘f · 𝑋 ) : 𝐴 ⟶ ℂ )
159 156 157 158 sylancl ⊢ ( 𝜑 → ( 𝑇 ∘f · 𝑋 ) : 𝐴 ⟶ ℂ )
160 159 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑘 ) ∧ ( ( 𝑘 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 0 < ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) ) ∧ 0 = ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) → ( 𝑇 ∘f · 𝑋 ) : 𝐴 ⟶ ℂ )
161 91 adantr ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑘 ) ∧ ( ( 𝑘 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 0 < ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) ) ∧ 0 = ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) → ( 𝑘 ∪ { 𝑐 } ) ⊆ 𝐴 )
162 160 161 fssresd ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑘 ) ∧ ( ( 𝑘 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 0 < ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) ) ∧ 0 = ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) → ( ( 𝑇 ∘f · 𝑋 ) ↾ ( 𝑘 ∪ { 𝑐 } ) ) : ( 𝑘 ∪ { 𝑐 } ) ⟶ ℂ )
163 5 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑘 ) ∧ ( ( 𝑘 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 0 < ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) ) ∧ 0 = ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) → 𝑇 : 𝐴 ⟶ ( 0 [,) +∞ ) )
164 110 adantr ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑘 ) ∧ ( ( 𝑘 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 0 < ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) ) ∧ 0 = ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) → 𝐴 ∈ Fin )
165 163 164 fexd ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑘 ) ∧ ( ( 𝑘 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 0 < ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) ) ∧ 0 = ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) → 𝑇 ∈ V )
166 6 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑘 ) ∧ ( ( 𝑘 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 0 < ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) ) ∧ 0 = ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) → 𝑋 : 𝐴 ⟶ 𝐷 )
167 166 164 fexd ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑘 ) ∧ ( ( 𝑘 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 0 < ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) ) ∧ 0 = ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) → 𝑋 ∈ V )
168 offres ⊢ ( ( 𝑇 ∈ V ∧ 𝑋 ∈ V ) → ( ( 𝑇 ∘f · 𝑋 ) ↾ ( 𝑘 ∪ { 𝑐 } ) ) = ( ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ∘f · ( 𝑋 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) )
169 165 167 168 syl2anc ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑘 ) ∧ ( ( 𝑘 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 0 < ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) ) ∧ 0 = ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) → ( ( 𝑇 ∘f · 𝑋 ) ↾ ( 𝑘 ∪ { 𝑐 } ) ) = ( ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ∘f · ( 𝑋 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) )
170 169 oveq1d ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑘 ) ∧ ( ( 𝑘 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 0 < ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) ) ∧ 0 = ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) → ( ( ( 𝑇 ∘f · 𝑋 ) ↾ ( 𝑘 ∪ { 𝑐 } ) ) supp 0 ) = ( ( ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ∘f · ( 𝑋 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) supp 0 ) )
171 151 157 sstri ⊢ ( 0 [,) +∞ ) ⊆ ℂ
172 fss ⊢ ( ( 𝑇 : 𝐴 ⟶ ( 0 [,) +∞ ) ∧ ( 0 [,) +∞ ) ⊆ ℂ ) → 𝑇 : 𝐴 ⟶ ℂ )
173 163 171 172 sylancl ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑘 ) ∧ ( ( 𝑘 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 0 < ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) ) ∧ 0 = ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) → 𝑇 : 𝐴 ⟶ ℂ )
174 173 161 fssresd ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑘 ) ∧ ( ( 𝑘 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 0 < ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) ) ∧ 0 = ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) → ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) : ( 𝑘 ∪ { 𝑐 } ) ⟶ ℂ )
175 eldifi ⊢ ( 𝑥 ∈ ( ( 𝑘 ∪ { 𝑐 } ) ∖ { 𝑐 } ) → 𝑥 ∈ ( 𝑘 ∪ { 𝑐 } ) )
176 175 adantl ⊢ ( ( ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑘 ) ∧ ( ( 𝑘 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 0 < ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) ) ∧ 0 = ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) ∧ 𝑥 ∈ ( ( 𝑘 ∪ { 𝑐 } ) ∖ { 𝑐 } ) ) → 𝑥 ∈ ( 𝑘 ∪ { 𝑐 } ) )
177 176 fvresd ⊢ ( ( ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑘 ) ∧ ( ( 𝑘 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 0 < ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) ) ∧ 0 = ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) ∧ 𝑥 ∈ ( ( 𝑘 ∪ { 𝑐 } ) ∖ { 𝑐 } ) ) → ( ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ‘ 𝑥 ) = ( 𝑇 ‘ 𝑥 ) )
178 difun2 ⊢ ( ( 𝑘 ∪ { 𝑐 } ) ∖ { 𝑐 } ) = ( 𝑘 ∖ { 𝑐 } )
179 difss ⊢ ( 𝑘 ∖ { 𝑐 } ) ⊆ 𝑘
180 178 179 eqsstri ⊢ ( ( 𝑘 ∪ { 𝑐 } ) ∖ { 𝑐 } ) ⊆ 𝑘
181 180 sseli ⊢ ( 𝑥 ∈ ( ( 𝑘 ∪ { 𝑐 } ) ∖ { 𝑐 } ) → 𝑥 ∈ 𝑘 )
182 simpr ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑘 ) ∧ ( ( 𝑘 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 0 < ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) ) ∧ 0 = ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) → 0 = ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) )
183 92 adantr ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑘 ) ∧ ( ( 𝑘 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 0 < ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) ) ∧ 0 = ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) → 𝑘 ⊆ 𝐴 )
184 163 183 feqresmpt ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑘 ) ∧ ( ( 𝑘 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 0 < ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) ) ∧ 0 = ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) → ( 𝑇 ↾ 𝑘 ) = ( 𝑥 ∈ 𝑘 ↦ ( 𝑇 ‘ 𝑥 ) ) )
185 184 oveq2d ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑘 ) ∧ ( ( 𝑘 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 0 < ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) ) ∧ 0 = ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) → ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) = ( ℂfld Σg ( 𝑥 ∈ 𝑘 ↦ ( 𝑇 ‘ 𝑥 ) ) ) )
186 111 adantr ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑘 ) ∧ ( ( 𝑘 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 0 < ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) ) ∧ 0 = ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) → 𝑘 ∈ Fin )
187 183 sselda ⊢ ( ( ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑘 ) ∧ ( ( 𝑘 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 0 < ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) ) ∧ 0 = ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) ∧ 𝑥 ∈ 𝑘 ) → 𝑥 ∈ 𝐴 )
188 163 ffvelrnda ⊢ ( ( ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑘 ) ∧ ( ( 𝑘 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 0 < ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) ) ∧ 0 = ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝑇 ‘ 𝑥 ) ∈ ( 0 [,) +∞ ) )
189 187 188 syldan ⊢ ( ( ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑘 ) ∧ ( ( 𝑘 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 0 < ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) ) ∧ 0 = ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) ∧ 𝑥 ∈ 𝑘 ) → ( 𝑇 ‘ 𝑥 ) ∈ ( 0 [,) +∞ ) )
190 171 189 sselid ⊢ ( ( ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑘 ) ∧ ( ( 𝑘 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 0 < ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) ) ∧ 0 = ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) ∧ 𝑥 ∈ 𝑘 ) → ( 𝑇 ‘ 𝑥 ) ∈ ℂ )
191 186 190 gsumfsum ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑘 ) ∧ ( ( 𝑘 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 0 < ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) ) ∧ 0 = ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) → ( ℂfld Σg ( 𝑥 ∈ 𝑘 ↦ ( 𝑇 ‘ 𝑥 ) ) ) = Σ 𝑥 ∈ 𝑘 ( 𝑇 ‘ 𝑥 ) )
192 182 185 191 3eqtrrd ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑘 ) ∧ ( ( 𝑘 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 0 < ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) ) ∧ 0 = ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) → Σ 𝑥 ∈ 𝑘 ( 𝑇 ‘ 𝑥 ) = 0 )
193 elrege0 ⊢ ( ( 𝑇 ‘ 𝑥 ) ∈ ( 0 [,) +∞ ) ↔ ( ( 𝑇 ‘ 𝑥 ) ∈ ℝ ∧ 0 ≤ ( 𝑇 ‘ 𝑥 ) ) )
194 189 193 sylib ⊢ ( ( ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑘 ) ∧ ( ( 𝑘 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 0 < ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) ) ∧ 0 = ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) ∧ 𝑥 ∈ 𝑘 ) → ( ( 𝑇 ‘ 𝑥 ) ∈ ℝ ∧ 0 ≤ ( 𝑇 ‘ 𝑥 ) ) )
195 194 simpld ⊢ ( ( ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑘 ) ∧ ( ( 𝑘 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 0 < ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) ) ∧ 0 = ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) ∧ 𝑥 ∈ 𝑘 ) → ( 𝑇 ‘ 𝑥 ) ∈ ℝ )
196 194 simprd ⊢ ( ( ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑘 ) ∧ ( ( 𝑘 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 0 < ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) ) ∧ 0 = ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) ∧ 𝑥 ∈ 𝑘 ) → 0 ≤ ( 𝑇 ‘ 𝑥 ) )
197 186 195 196 fsum00 ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑘 ) ∧ ( ( 𝑘 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 0 < ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) ) ∧ 0 = ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) → ( Σ 𝑥 ∈ 𝑘 ( 𝑇 ‘ 𝑥 ) = 0 ↔ ∀ 𝑥 ∈ 𝑘 ( 𝑇 ‘ 𝑥 ) = 0 ) )
198 192 197 mpbid ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑘 ) ∧ ( ( 𝑘 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 0 < ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) ) ∧ 0 = ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) → ∀ 𝑥 ∈ 𝑘 ( 𝑇 ‘ 𝑥 ) = 0 )
199 198 r19.21bi ⊢ ( ( ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑘 ) ∧ ( ( 𝑘 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 0 < ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) ) ∧ 0 = ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) ∧ 𝑥 ∈ 𝑘 ) → ( 𝑇 ‘ 𝑥 ) = 0 )
200 181 199 sylan2 ⊢ ( ( ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑘 ) ∧ ( ( 𝑘 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 0 < ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) ) ∧ 0 = ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) ∧ 𝑥 ∈ ( ( 𝑘 ∪ { 𝑐 } ) ∖ { 𝑐 } ) ) → ( 𝑇 ‘ 𝑥 ) = 0 )
201 177 200 eqtrd ⊢ ( ( ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑘 ) ∧ ( ( 𝑘 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 0 < ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) ) ∧ 0 = ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) ∧ 𝑥 ∈ ( ( 𝑘 ∪ { 𝑐 } ) ∖ { 𝑐 } ) ) → ( ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ‘ 𝑥 ) = 0 )
202 174 201 suppss ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑘 ) ∧ ( ( 𝑘 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 0 < ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) ) ∧ 0 = ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) → ( ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) supp 0 ) ⊆ { 𝑐 } )
203 mul02 ⊢ ( 𝑥 ∈ ℂ → ( 0 · 𝑥 ) = 0 )
204 203 adantl ⊢ ( ( ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑘 ) ∧ ( ( 𝑘 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 0 < ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) ) ∧ 0 = ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) ∧ 𝑥 ∈ ℂ ) → ( 0 · 𝑥 ) = 0 )
205 1 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑘 ) ∧ ( ( 𝑘 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 0 < ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) ) ∧ 0 = ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) → 𝐷 ⊆ ℝ )
206 205 157 sstrdi ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑘 ) ∧ ( ( 𝑘 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 0 < ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) ) ∧ 0 = ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) → 𝐷 ⊆ ℂ )
207 166 206 fssd ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑘 ) ∧ ( ( 𝑘 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 0 < ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) ) ∧ 0 = ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) → 𝑋 : 𝐴 ⟶ ℂ )
208 207 161 fssresd ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑘 ) ∧ ( ( 𝑘 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 0 < ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) ) ∧ 0 = ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) → ( 𝑋 ↾ ( 𝑘 ∪ { 𝑐 } ) ) : ( 𝑘 ∪ { 𝑐 } ) ⟶ ℂ )
209 116 a1i ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑘 ) ∧ ( ( 𝑘 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 0 < ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) ) ∧ 0 = ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) → 0 ∈ V )
210 202 204 174 208 144 209 suppssof1 ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑘 ) ∧ ( ( 𝑘 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 0 < ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) ) ∧ 0 = ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) → ( ( ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ∘f · ( 𝑋 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) supp 0 ) ⊆ { 𝑐 } )
211 170 210 eqsstrd ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑘 ) ∧ ( ( 𝑘 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 0 < ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) ) ∧ 0 = ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) → ( ( ( 𝑇 ∘f · 𝑋 ) ↾ ( 𝑘 ∪ { 𝑐 } ) ) supp 0 ) ⊆ { 𝑐 } )
212 140 21 142 144 148 162 211 gsumpt ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑘 ) ∧ ( ( 𝑘 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 0 < ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) ) ∧ 0 = ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) → ( ℂfld Σg ( ( 𝑇 ∘f · 𝑋 ) ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) = ( ( ( 𝑇 ∘f · 𝑋 ) ↾ ( 𝑘 ∪ { 𝑐 } ) ) ‘ 𝑐 ) )
213 148 fvresd ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑘 ) ∧ ( ( 𝑘 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 0 < ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) ) ∧ 0 = ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) → ( ( ( 𝑇 ∘f · 𝑋 ) ↾ ( 𝑘 ∪ { 𝑐 } ) ) ‘ 𝑐 ) = ( ( 𝑇 ∘f · 𝑋 ) ‘ 𝑐 ) )
214 163 ffnd ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑘 ) ∧ ( ( 𝑘 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 0 < ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) ) ∧ 0 = ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) → 𝑇 Fn 𝐴 )
215 166 ffnd ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑘 ) ∧ ( ( 𝑘 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 0 < ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) ) ∧ 0 = ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) → 𝑋 Fn 𝐴 )
216 161 148 sseldd ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑘 ) ∧ ( ( 𝑘 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 0 < ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) ) ∧ 0 = ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) → 𝑐 ∈ 𝐴 )
217 fnfvof ⊢ ( ( ( 𝑇 Fn 𝐴 ∧ 𝑋 Fn 𝐴 ) ∧ ( 𝐴 ∈ Fin ∧ 𝑐 ∈ 𝐴 ) ) → ( ( 𝑇 ∘f · 𝑋 ) ‘ 𝑐 ) = ( ( 𝑇 ‘ 𝑐 ) · ( 𝑋 ‘ 𝑐 ) ) )
218 214 215 164 216 217 syl22anc ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑘 ) ∧ ( ( 𝑘 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 0 < ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) ) ∧ 0 = ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) → ( ( 𝑇 ∘f · 𝑋 ) ‘ 𝑐 ) = ( ( 𝑇 ‘ 𝑐 ) · ( 𝑋 ‘ 𝑐 ) ) )
219 212 213 218 3eqtrd ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑘 ) ∧ ( ( 𝑘 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 0 < ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) ) ∧ 0 = ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) → ( ℂfld Σg ( ( 𝑇 ∘f · 𝑋 ) ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) = ( ( 𝑇 ‘ 𝑐 ) · ( 𝑋 ‘ 𝑐 ) ) )
220 140 21 142 144 148 174 202 gsumpt ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑘 ) ∧ ( ( 𝑘 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 0 < ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) ) ∧ 0 = ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) → ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) = ( ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ‘ 𝑐 ) )
221 148 fvresd ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑘 ) ∧ ( ( 𝑘 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 0 < ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) ) ∧ 0 = ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) → ( ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ‘ 𝑐 ) = ( 𝑇 ‘ 𝑐 ) )
222 220 221 eqtrd ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑘 ) ∧ ( ( 𝑘 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 0 < ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) ) ∧ 0 = ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) → ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) = ( 𝑇 ‘ 𝑐 ) )
223 219 222 oveq12d ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑘 ) ∧ ( ( 𝑘 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 0 < ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) ) ∧ 0 = ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) → ( ( ℂfld Σg ( ( 𝑇 ∘f · 𝑋 ) ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) / ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) = ( ( ( 𝑇 ‘ 𝑐 ) · ( 𝑋 ‘ 𝑐 ) ) / ( 𝑇 ‘ 𝑐 ) ) )
224 207 216 ffvelrnd ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑘 ) ∧ ( ( 𝑘 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 0 < ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) ) ∧ 0 = ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) → ( 𝑋 ‘ 𝑐 ) ∈ ℂ )
225 173 216 ffvelrnd ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑘 ) ∧ ( ( 𝑘 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 0 < ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) ) ∧ 0 = ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) → ( 𝑇 ‘ 𝑐 ) ∈ ℂ )
226 simplrr ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑘 ) ∧ ( ( 𝑘 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 0 < ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) ) ∧ 0 = ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) → 0 < ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) )
227 226 222 breqtrd ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑘 ) ∧ ( ( 𝑘 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 0 < ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) ) ∧ 0 = ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) → 0 < ( 𝑇 ‘ 𝑐 ) )
228 227 gt0ne0d ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑘 ) ∧ ( ( 𝑘 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 0 < ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) ) ∧ 0 = ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) → ( 𝑇 ‘ 𝑐 ) ≠ 0 )
229 224 225 228 divcan3d ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑘 ) ∧ ( ( 𝑘 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 0 < ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) ) ∧ 0 = ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) → ( ( ( 𝑇 ‘ 𝑐 ) · ( 𝑋 ‘ 𝑐 ) ) / ( 𝑇 ‘ 𝑐 ) ) = ( 𝑋 ‘ 𝑐 ) )
230 223 229 eqtrd ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑘 ) ∧ ( ( 𝑘 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 0 < ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) ) ∧ 0 = ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) → ( ( ℂfld Σg ( ( 𝑇 ∘f · 𝑋 ) ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) / ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) = ( 𝑋 ‘ 𝑐 ) )
231 166 216 ffvelrnd ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑘 ) ∧ ( ( 𝑘 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 0 < ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) ) ∧ 0 = ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) → ( 𝑋 ‘ 𝑐 ) ∈ 𝐷 )
232 230 231 eqeltrd ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑘 ) ∧ ( ( 𝑘 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 0 < ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) ) ∧ 0 = ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) → ( ( ℂfld Σg ( ( 𝑇 ∘f · 𝑋 ) ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) / ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) ∈ 𝐷 )
233 2 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑘 ) ∧ ( ( 𝑘 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 0 < ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) ) ∧ 0 = ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) → 𝐹 : 𝐷 ⟶ ℝ )
234 233 231 ffvelrnd ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑘 ) ∧ ( ( 𝑘 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 0 < ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) ) ∧ 0 = ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) → ( 𝐹 ‘ ( 𝑋 ‘ 𝑐 ) ) ∈ ℝ )
235 234 leidd ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑘 ) ∧ ( ( 𝑘 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 0 < ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) ) ∧ 0 = ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) → ( 𝐹 ‘ ( 𝑋 ‘ 𝑐 ) ) ≤ ( 𝐹 ‘ ( 𝑋 ‘ 𝑐 ) ) )
236 230 fveq2d ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑘 ) ∧ ( ( 𝑘 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 0 < ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) ) ∧ 0 = ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) → ( 𝐹 ‘ ( ( ℂfld Σg ( ( 𝑇 ∘f · 𝑋 ) ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) / ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) ) = ( 𝐹 ‘ ( 𝑋 ‘ 𝑐 ) ) )
237 fco ⊢ ( ( 𝐹 : 𝐷 ⟶ ℝ ∧ 𝑋 : 𝐴 ⟶ 𝐷 ) → ( 𝐹 ∘ 𝑋 ) : 𝐴 ⟶ ℝ )
238 2 6 237 syl2anc ⊢ ( 𝜑 → ( 𝐹 ∘ 𝑋 ) : 𝐴 ⟶ ℝ )
239 150 153 238 4 4 155 off ⊢ ( 𝜑 → ( 𝑇 ∘f · ( 𝐹 ∘ 𝑋 ) ) : 𝐴 ⟶ ℝ )
240 fss ⊢ ( ( ( 𝑇 ∘f · ( 𝐹 ∘ 𝑋 ) ) : 𝐴 ⟶ ℝ ∧ ℝ ⊆ ℂ ) → ( 𝑇 ∘f · ( 𝐹 ∘ 𝑋 ) ) : 𝐴 ⟶ ℂ )
241 239 157 240 sylancl ⊢ ( 𝜑 → ( 𝑇 ∘f · ( 𝐹 ∘ 𝑋 ) ) : 𝐴 ⟶ ℂ )
242 241 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑘 ) ∧ ( ( 𝑘 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 0 < ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) ) ∧ 0 = ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) → ( 𝑇 ∘f · ( 𝐹 ∘ 𝑋 ) ) : 𝐴 ⟶ ℂ )
243 242 161 fssresd ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑘 ) ∧ ( ( 𝑘 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 0 < ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) ) ∧ 0 = ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) → ( ( 𝑇 ∘f · ( 𝐹 ∘ 𝑋 ) ) ↾ ( 𝑘 ∪ { 𝑐 } ) ) : ( 𝑘 ∪ { 𝑐 } ) ⟶ ℂ )
244 238 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑘 ) ∧ ( ( 𝑘 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 0 < ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) ) ∧ 0 = ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) → ( 𝐹 ∘ 𝑋 ) : 𝐴 ⟶ ℝ )
245 244 164 fexd ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑘 ) ∧ ( ( 𝑘 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 0 < ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) ) ∧ 0 = ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) → ( 𝐹 ∘ 𝑋 ) ∈ V )
246 offres ⊢ ( ( 𝑇 ∈ V ∧ ( 𝐹 ∘ 𝑋 ) ∈ V ) → ( ( 𝑇 ∘f · ( 𝐹 ∘ 𝑋 ) ) ↾ ( 𝑘 ∪ { 𝑐 } ) ) = ( ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ∘f · ( ( 𝐹 ∘ 𝑋 ) ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) )
247 165 245 246 syl2anc ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑘 ) ∧ ( ( 𝑘 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 0 < ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) ) ∧ 0 = ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) → ( ( 𝑇 ∘f · ( 𝐹 ∘ 𝑋 ) ) ↾ ( 𝑘 ∪ { 𝑐 } ) ) = ( ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ∘f · ( ( 𝐹 ∘ 𝑋 ) ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) )
248 247 oveq1d ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑘 ) ∧ ( ( 𝑘 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 0 < ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) ) ∧ 0 = ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) → ( ( ( 𝑇 ∘f · ( 𝐹 ∘ 𝑋 ) ) ↾ ( 𝑘 ∪ { 𝑐 } ) ) supp 0 ) = ( ( ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ∘f · ( ( 𝐹 ∘ 𝑋 ) ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) supp 0 ) )
249 fss ⊢ ( ( ( 𝐹 ∘ 𝑋 ) : 𝐴 ⟶ ℝ ∧ ℝ ⊆ ℂ ) → ( 𝐹 ∘ 𝑋 ) : 𝐴 ⟶ ℂ )
250 244 157 249 sylancl ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑘 ) ∧ ( ( 𝑘 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 0 < ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) ) ∧ 0 = ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) → ( 𝐹 ∘ 𝑋 ) : 𝐴 ⟶ ℂ )
251 250 161 fssresd ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑘 ) ∧ ( ( 𝑘 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 0 < ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) ) ∧ 0 = ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) → ( ( 𝐹 ∘ 𝑋 ) ↾ ( 𝑘 ∪ { 𝑐 } ) ) : ( 𝑘 ∪ { 𝑐 } ) ⟶ ℂ )
252 202 204 174 251 144 209 suppssof1 ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑘 ) ∧ ( ( 𝑘 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 0 < ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) ) ∧ 0 = ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) → ( ( ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ∘f · ( ( 𝐹 ∘ 𝑋 ) ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) supp 0 ) ⊆ { 𝑐 } )
253 248 252 eqsstrd ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑘 ) ∧ ( ( 𝑘 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 0 < ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) ) ∧ 0 = ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) → ( ( ( 𝑇 ∘f · ( 𝐹 ∘ 𝑋 ) ) ↾ ( 𝑘 ∪ { 𝑐 } ) ) supp 0 ) ⊆ { 𝑐 } )
254 140 21 142 144 148 243 253 gsumpt ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑘 ) ∧ ( ( 𝑘 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 0 < ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) ) ∧ 0 = ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) → ( ℂfld Σg ( ( 𝑇 ∘f · ( 𝐹 ∘ 𝑋 ) ) ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) = ( ( ( 𝑇 ∘f · ( 𝐹 ∘ 𝑋 ) ) ↾ ( 𝑘 ∪ { 𝑐 } ) ) ‘ 𝑐 ) )
255 148 fvresd ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑘 ) ∧ ( ( 𝑘 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 0 < ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) ) ∧ 0 = ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) → ( ( ( 𝑇 ∘f · ( 𝐹 ∘ 𝑋 ) ) ↾ ( 𝑘 ∪ { 𝑐 } ) ) ‘ 𝑐 ) = ( ( 𝑇 ∘f · ( 𝐹 ∘ 𝑋 ) ) ‘ 𝑐 ) )
256 2 ffnd ⊢ ( 𝜑 → 𝐹 Fn 𝐷 )
257 fnfco ⊢ ( ( 𝐹 Fn 𝐷 ∧ 𝑋 : 𝐴 ⟶ 𝐷 ) → ( 𝐹 ∘ 𝑋 ) Fn 𝐴 )
258 256 6 257 syl2anc ⊢ ( 𝜑 → ( 𝐹 ∘ 𝑋 ) Fn 𝐴 )
259 258 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑘 ) ∧ ( ( 𝑘 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 0 < ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) ) ∧ 0 = ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) → ( 𝐹 ∘ 𝑋 ) Fn 𝐴 )
260 fnfvof ⊢ ( ( ( 𝑇 Fn 𝐴 ∧ ( 𝐹 ∘ 𝑋 ) Fn 𝐴 ) ∧ ( 𝐴 ∈ Fin ∧ 𝑐 ∈ 𝐴 ) ) → ( ( 𝑇 ∘f · ( 𝐹 ∘ 𝑋 ) ) ‘ 𝑐 ) = ( ( 𝑇 ‘ 𝑐 ) · ( ( 𝐹 ∘ 𝑋 ) ‘ 𝑐 ) ) )
261 214 259 164 216 260 syl22anc ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑘 ) ∧ ( ( 𝑘 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 0 < ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) ) ∧ 0 = ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) → ( ( 𝑇 ∘f · ( 𝐹 ∘ 𝑋 ) ) ‘ 𝑐 ) = ( ( 𝑇 ‘ 𝑐 ) · ( ( 𝐹 ∘ 𝑋 ) ‘ 𝑐 ) ) )
262 fvco3 ⊢ ( ( 𝑋 : 𝐴 ⟶ 𝐷 ∧ 𝑐 ∈ 𝐴 ) → ( ( 𝐹 ∘ 𝑋 ) ‘ 𝑐 ) = ( 𝐹 ‘ ( 𝑋 ‘ 𝑐 ) ) )
263 166 216 262 syl2anc ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑘 ) ∧ ( ( 𝑘 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 0 < ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) ) ∧ 0 = ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) → ( ( 𝐹 ∘ 𝑋 ) ‘ 𝑐 ) = ( 𝐹 ‘ ( 𝑋 ‘ 𝑐 ) ) )
264 263 oveq2d ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑘 ) ∧ ( ( 𝑘 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 0 < ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) ) ∧ 0 = ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) → ( ( 𝑇 ‘ 𝑐 ) · ( ( 𝐹 ∘ 𝑋 ) ‘ 𝑐 ) ) = ( ( 𝑇 ‘ 𝑐 ) · ( 𝐹 ‘ ( 𝑋 ‘ 𝑐 ) ) ) )
265 261 264 eqtrd ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑘 ) ∧ ( ( 𝑘 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 0 < ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) ) ∧ 0 = ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) → ( ( 𝑇 ∘f · ( 𝐹 ∘ 𝑋 ) ) ‘ 𝑐 ) = ( ( 𝑇 ‘ 𝑐 ) · ( 𝐹 ‘ ( 𝑋 ‘ 𝑐 ) ) ) )
266 254 255 265 3eqtrd ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑘 ) ∧ ( ( 𝑘 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 0 < ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) ) ∧ 0 = ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) → ( ℂfld Σg ( ( 𝑇 ∘f · ( 𝐹 ∘ 𝑋 ) ) ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) = ( ( 𝑇 ‘ 𝑐 ) · ( 𝐹 ‘ ( 𝑋 ‘ 𝑐 ) ) ) )
267 266 222 oveq12d ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑘 ) ∧ ( ( 𝑘 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 0 < ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) ) ∧ 0 = ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) → ( ( ℂfld Σg ( ( 𝑇 ∘f · ( 𝐹 ∘ 𝑋 ) ) ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) / ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) = ( ( ( 𝑇 ‘ 𝑐 ) · ( 𝐹 ‘ ( 𝑋 ‘ 𝑐 ) ) ) / ( 𝑇 ‘ 𝑐 ) ) )
268 234 recnd ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑘 ) ∧ ( ( 𝑘 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 0 < ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) ) ∧ 0 = ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) → ( 𝐹 ‘ ( 𝑋 ‘ 𝑐 ) ) ∈ ℂ )
269 268 225 228 divcan3d ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑘 ) ∧ ( ( 𝑘 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 0 < ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) ) ∧ 0 = ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) → ( ( ( 𝑇 ‘ 𝑐 ) · ( 𝐹 ‘ ( 𝑋 ‘ 𝑐 ) ) ) / ( 𝑇 ‘ 𝑐 ) ) = ( 𝐹 ‘ ( 𝑋 ‘ 𝑐 ) ) )
270 267 269 eqtrd ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑘 ) ∧ ( ( 𝑘 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 0 < ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) ) ∧ 0 = ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) → ( ( ℂfld Σg ( ( 𝑇 ∘f · ( 𝐹 ∘ 𝑋 ) ) ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) / ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) = ( 𝐹 ‘ ( 𝑋 ‘ 𝑐 ) ) )
271 235 236 270 3brtr4d ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑘 ) ∧ ( ( 𝑘 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 0 < ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) ) ∧ 0 = ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) → ( 𝐹 ‘ ( ( ℂfld Σg ( ( 𝑇 ∘f · 𝑋 ) ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) / ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) ) ≤ ( ( ℂfld Σg ( ( 𝑇 ∘f · ( 𝐹 ∘ 𝑋 ) ) ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) / ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) )
272 135 232 271 elrabd ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑘 ) ∧ ( ( 𝑘 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 0 < ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) ) ∧ 0 = ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) → ( ( ℂfld Σg ( ( 𝑇 ∘f · 𝑋 ) ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) / ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) ∈ { 𝑤 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑤 ) ≤ ( ( ℂfld Σg ( ( 𝑇 ∘f · ( 𝐹 ∘ 𝑋 ) ) ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) / ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) } )
273 272 a1d ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑘 ) ∧ ( ( 𝑘 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 0 < ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) ) ∧ 0 = ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) → ( ( 0 < ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) → ( ( ℂfld Σg ( ( 𝑇 ∘f · 𝑋 ) ↾ 𝑘 ) ) / ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) ∈ { 𝑤 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑤 ) ≤ ( ( ℂfld Σg ( ( 𝑇 ∘f · ( 𝐹 ∘ 𝑋 ) ) ↾ 𝑘 ) ) / ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) } ) → ( ( ℂfld Σg ( ( 𝑇 ∘f · 𝑋 ) ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) / ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) ∈ { 𝑤 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑤 ) ≤ ( ( ℂfld Σg ( ( 𝑇 ∘f · ( 𝐹 ∘ 𝑋 ) ) ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) / ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) } ) )
274 120 simprbi ⊢ ( ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ∈ ( 0 [,) +∞ ) → 0 ≤ ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) )
275 119 274 syl ⊢ ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑘 ) ∧ ( ( 𝑘 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 0 < ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) ) → 0 ≤ ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) )
276 leloe ⊢ ( ( 0 ∈ ℝ ∧ ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ∈ ℝ ) → ( 0 ≤ ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ↔ ( 0 < ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ∨ 0 = ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) ) )
277 85 122 276 sylancr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑘 ) ∧ ( ( 𝑘 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 0 < ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) ) → ( 0 ≤ ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ↔ ( 0 < ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ∨ 0 = ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) ) )
278 275 277 mpbid ⊢ ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑘 ) ∧ ( ( 𝑘 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 0 < ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) ) → ( 0 < ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ∨ 0 = ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) )
279 139 273 278 mpjaodan ⊢ ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑘 ) ∧ ( ( 𝑘 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 0 < ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) ) → ( ( 0 < ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) → ( ( ℂfld Σg ( ( 𝑇 ∘f · 𝑋 ) ↾ 𝑘 ) ) / ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) ∈ { 𝑤 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑤 ) ≤ ( ( ℂfld Σg ( ( 𝑇 ∘f · ( 𝐹 ∘ 𝑋 ) ) ↾ 𝑘 ) ) / ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) } ) → ( ( ℂfld Σg ( ( 𝑇 ∘f · 𝑋 ) ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) / ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) ∈ { 𝑤 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑤 ) ≤ ( ( ℂfld Σg ( ( 𝑇 ∘f · ( 𝐹 ∘ 𝑋 ) ) ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) / ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) } ) )
280 92 279 embantd ⊢ ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑘 ) ∧ ( ( 𝑘 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 0 < ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) ) → ( ( 𝑘 ⊆ 𝐴 → ( 0 < ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) → ( ( ℂfld Σg ( ( 𝑇 ∘f · 𝑋 ) ↾ 𝑘 ) ) / ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) ∈ { 𝑤 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑤 ) ≤ ( ( ℂfld Σg ( ( 𝑇 ∘f · ( 𝐹 ∘ 𝑋 ) ) ↾ 𝑘 ) ) / ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) } ) ) → ( ( ℂfld Σg ( ( 𝑇 ∘f · 𝑋 ) ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) / ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) ∈ { 𝑤 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑤 ) ≤ ( ( ℂfld Σg ( ( 𝑇 ∘f · ( 𝐹 ∘ 𝑋 ) ) ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) / ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) } ) )
281 90 280 syl5bi ⊢ ( ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑘 ) ∧ ( ( 𝑘 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 0 < ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) ) → ( ( ( 𝑘 ⊆ 𝐴 ∧ 0 < ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) → ( ( ℂfld Σg ( ( 𝑇 ∘f · 𝑋 ) ↾ 𝑘 ) ) / ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) ∈ { 𝑤 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑤 ) ≤ ( ( ℂfld Σg ( ( 𝑇 ∘f · ( 𝐹 ∘ 𝑋 ) ) ↾ 𝑘 ) ) / ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) } ) → ( ( ℂfld Σg ( ( 𝑇 ∘f · 𝑋 ) ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) / ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) ∈ { 𝑤 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑤 ) ≤ ( ( ℂfld Σg ( ( 𝑇 ∘f · ( 𝐹 ∘ 𝑋 ) ) ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) / ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) } ) )
282 281 ex ⊢ ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑘 ) → ( ( ( 𝑘 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 0 < ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) → ( ( ( 𝑘 ⊆ 𝐴 ∧ 0 < ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) → ( ( ℂfld Σg ( ( 𝑇 ∘f · 𝑋 ) ↾ 𝑘 ) ) / ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) ∈ { 𝑤 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑤 ) ≤ ( ( ℂfld Σg ( ( 𝑇 ∘f · ( 𝐹 ∘ 𝑋 ) ) ↾ 𝑘 ) ) / ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) } ) → ( ( ℂfld Σg ( ( 𝑇 ∘f · 𝑋 ) ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) / ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) ∈ { 𝑤 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑤 ) ≤ ( ( ℂfld Σg ( ( 𝑇 ∘f · ( 𝐹 ∘ 𝑋 ) ) ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) / ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) } ) ) )
283 282 com23 ⊢ ( ( 𝜑 ∧ ¬ 𝑐 ∈ 𝑘 ) → ( ( ( 𝑘 ⊆ 𝐴 ∧ 0 < ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) → ( ( ℂfld Σg ( ( 𝑇 ∘f · 𝑋 ) ↾ 𝑘 ) ) / ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) ∈ { 𝑤 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑤 ) ≤ ( ( ℂfld Σg ( ( 𝑇 ∘f · ( 𝐹 ∘ 𝑋 ) ) ↾ 𝑘 ) ) / ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) } ) → ( ( ( 𝑘 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 0 < ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) → ( ( ℂfld Σg ( ( 𝑇 ∘f · 𝑋 ) ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) / ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) ∈ { 𝑤 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑤 ) ≤ ( ( ℂfld Σg ( ( 𝑇 ∘f · ( 𝐹 ∘ 𝑋 ) ) ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) / ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) } ) ) )
284 283 expcom ⊢ ( ¬ 𝑐 ∈ 𝑘 → ( 𝜑 → ( ( ( 𝑘 ⊆ 𝐴 ∧ 0 < ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) → ( ( ℂfld Σg ( ( 𝑇 ∘f · 𝑋 ) ↾ 𝑘 ) ) / ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) ∈ { 𝑤 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑤 ) ≤ ( ( ℂfld Σg ( ( 𝑇 ∘f · ( 𝐹 ∘ 𝑋 ) ) ↾ 𝑘 ) ) / ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) } ) → ( ( ( 𝑘 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 0 < ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) → ( ( ℂfld Σg ( ( 𝑇 ∘f · 𝑋 ) ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) / ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) ∈ { 𝑤 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑤 ) ≤ ( ( ℂfld Σg ( ( 𝑇 ∘f · ( 𝐹 ∘ 𝑋 ) ) ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) / ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) } ) ) ) )
285 284 adantl ⊢ ( ( 𝑘 ∈ Fin ∧ ¬ 𝑐 ∈ 𝑘 ) → ( 𝜑 → ( ( ( 𝑘 ⊆ 𝐴 ∧ 0 < ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) → ( ( ℂfld Σg ( ( 𝑇 ∘f · 𝑋 ) ↾ 𝑘 ) ) / ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) ∈ { 𝑤 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑤 ) ≤ ( ( ℂfld Σg ( ( 𝑇 ∘f · ( 𝐹 ∘ 𝑋 ) ) ↾ 𝑘 ) ) / ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) } ) → ( ( ( 𝑘 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 0 < ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) → ( ( ℂfld Σg ( ( 𝑇 ∘f · 𝑋 ) ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) / ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) ∈ { 𝑤 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑤 ) ≤ ( ( ℂfld Σg ( ( 𝑇 ∘f · ( 𝐹 ∘ 𝑋 ) ) ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) / ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) } ) ) ) )
286 285 a2d ⊢ ( ( 𝑘 ∈ Fin ∧ ¬ 𝑐 ∈ 𝑘 ) → ( ( 𝜑 → ( ( 𝑘 ⊆ 𝐴 ∧ 0 < ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) → ( ( ℂfld Σg ( ( 𝑇 ∘f · 𝑋 ) ↾ 𝑘 ) ) / ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) ∈ { 𝑤 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑤 ) ≤ ( ( ℂfld Σg ( ( 𝑇 ∘f · ( 𝐹 ∘ 𝑋 ) ) ↾ 𝑘 ) ) / ( ℂfld Σg ( 𝑇 ↾ 𝑘 ) ) ) } ) ) → ( 𝜑 → ( ( ( 𝑘 ∪ { 𝑐 } ) ⊆ 𝐴 ∧ 0 < ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) → ( ( ℂfld Σg ( ( 𝑇 ∘f · 𝑋 ) ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) / ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) ∈ { 𝑤 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑤 ) ≤ ( ( ℂfld Σg ( ( 𝑇 ∘f · ( 𝐹 ∘ 𝑋 ) ) ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) / ( ℂfld Σg ( 𝑇 ↾ ( 𝑘 ∪ { 𝑐 } ) ) ) ) } ) ) ) )
287 36 52 68 84 89 286 findcard2s ⊢ ( 𝐴 ∈ Fin → ( 𝜑 → ( ( 𝐴 ⊆ 𝐴 ∧ 0 < ( ℂfld Σg ( 𝑇 ↾ 𝐴 ) ) ) → ( ( ℂfld Σg ( ( 𝑇 ∘f · 𝑋 ) ↾ 𝐴 ) ) / ( ℂfld Σg ( 𝑇 ↾ 𝐴 ) ) ) ∈ { 𝑤 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑤 ) ≤ ( ( ℂfld Σg ( ( 𝑇 ∘f · ( 𝐹 ∘ 𝑋 ) ) ↾ 𝐴 ) ) / ( ℂfld Σg ( 𝑇 ↾ 𝐴 ) ) ) } ) ) )
288 4 287 mpcom ⊢ ( 𝜑 → ( ( 𝐴 ⊆ 𝐴 ∧ 0 < ( ℂfld Σg ( 𝑇 ↾ 𝐴 ) ) ) → ( ( ℂfld Σg ( ( 𝑇 ∘f · 𝑋 ) ↾ 𝐴 ) ) / ( ℂfld Σg ( 𝑇 ↾ 𝐴 ) ) ) ∈ { 𝑤 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑤 ) ≤ ( ( ℂfld Σg ( ( 𝑇 ∘f · ( 𝐹 ∘ 𝑋 ) ) ↾ 𝐴 ) ) / ( ℂfld Σg ( 𝑇 ↾ 𝐴 ) ) ) } ) )
289 15 288 mpd ⊢ ( 𝜑 → ( ( ℂfld Σg ( ( 𝑇 ∘f · 𝑋 ) ↾ 𝐴 ) ) / ( ℂfld Σg ( 𝑇 ↾ 𝐴 ) ) ) ∈ { 𝑤 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑤 ) ≤ ( ( ℂfld Σg ( ( 𝑇 ∘f · ( 𝐹 ∘ 𝑋 ) ) ↾ 𝐴 ) ) / ( ℂfld Σg ( 𝑇 ↾ 𝐴 ) ) ) } )
290 156 ffnd ⊢ ( 𝜑 → ( 𝑇 ∘f · 𝑋 ) Fn 𝐴 )
291 fnresdm ⊢ ( ( 𝑇 ∘f · 𝑋 ) Fn 𝐴 → ( ( 𝑇 ∘f · 𝑋 ) ↾ 𝐴 ) = ( 𝑇 ∘f · 𝑋 ) )
292 290 291 syl ⊢ ( 𝜑 → ( ( 𝑇 ∘f · 𝑋 ) ↾ 𝐴 ) = ( 𝑇 ∘f · 𝑋 ) )
293 292 oveq2d ⊢ ( 𝜑 → ( ℂfld Σg ( ( 𝑇 ∘f · 𝑋 ) ↾ 𝐴 ) ) = ( ℂfld Σg ( 𝑇 ∘f · 𝑋 ) ) )
294 293 12 oveq12d ⊢ ( 𝜑 → ( ( ℂfld Σg ( ( 𝑇 ∘f · 𝑋 ) ↾ 𝐴 ) ) / ( ℂfld Σg ( 𝑇 ↾ 𝐴 ) ) ) = ( ( ℂfld Σg ( 𝑇 ∘f · 𝑋 ) ) / ( ℂfld Σg 𝑇 ) ) )
295 9 258 4 4 155 offn ⊢ ( 𝜑 → ( 𝑇 ∘f · ( 𝐹 ∘ 𝑋 ) ) Fn 𝐴 )
296 fnresdm ⊢ ( ( 𝑇 ∘f · ( 𝐹 ∘ 𝑋 ) ) Fn 𝐴 → ( ( 𝑇 ∘f · ( 𝐹 ∘ 𝑋 ) ) ↾ 𝐴 ) = ( 𝑇 ∘f · ( 𝐹 ∘ 𝑋 ) ) )
297 295 296 syl ⊢ ( 𝜑 → ( ( 𝑇 ∘f · ( 𝐹 ∘ 𝑋 ) ) ↾ 𝐴 ) = ( 𝑇 ∘f · ( 𝐹 ∘ 𝑋 ) ) )
298 297 oveq2d ⊢ ( 𝜑 → ( ℂfld Σg ( ( 𝑇 ∘f · ( 𝐹 ∘ 𝑋 ) ) ↾ 𝐴 ) ) = ( ℂfld Σg ( 𝑇 ∘f · ( 𝐹 ∘ 𝑋 ) ) ) )
299 298 12 oveq12d ⊢ ( 𝜑 → ( ( ℂfld Σg ( ( 𝑇 ∘f · ( 𝐹 ∘ 𝑋 ) ) ↾ 𝐴 ) ) / ( ℂfld Σg ( 𝑇 ↾ 𝐴 ) ) ) = ( ( ℂfld Σg ( 𝑇 ∘f · ( 𝐹 ∘ 𝑋 ) ) ) / ( ℂfld Σg 𝑇 ) ) )
300 299 breq2d ⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝑤 ) ≤ ( ( ℂfld Σg ( ( 𝑇 ∘f · ( 𝐹 ∘ 𝑋 ) ) ↾ 𝐴 ) ) / ( ℂfld Σg ( 𝑇 ↾ 𝐴 ) ) ) ↔ ( 𝐹 ‘ 𝑤 ) ≤ ( ( ℂfld Σg ( 𝑇 ∘f · ( 𝐹 ∘ 𝑋 ) ) ) / ( ℂfld Σg 𝑇 ) ) ) )
301 300 rabbidv ⊢ ( 𝜑 → { 𝑤 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑤 ) ≤ ( ( ℂfld Σg ( ( 𝑇 ∘f · ( 𝐹 ∘ 𝑋 ) ) ↾ 𝐴 ) ) / ( ℂfld Σg ( 𝑇 ↾ 𝐴 ) ) ) } = { 𝑤 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑤 ) ≤ ( ( ℂfld Σg ( 𝑇 ∘f · ( 𝐹 ∘ 𝑋 ) ) ) / ( ℂfld Σg 𝑇 ) ) } )
302 289 294 301 3eltr3d ⊢ ( 𝜑 → ( ( ℂfld Σg ( 𝑇 ∘f · 𝑋 ) ) / ( ℂfld Σg 𝑇 ) ) ∈ { 𝑤 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑤 ) ≤ ( ( ℂfld Σg ( 𝑇 ∘f · ( 𝐹 ∘ 𝑋 ) ) ) / ( ℂfld Σg 𝑇 ) ) } )
303 fveq2 ⊢ ( 𝑤 = ( ( ℂfld Σg ( 𝑇 ∘f · 𝑋 ) ) / ( ℂfld Σg 𝑇 ) ) → ( 𝐹 ‘ 𝑤 ) = ( 𝐹 ‘ ( ( ℂfld Σg ( 𝑇 ∘f · 𝑋 ) ) / ( ℂfld Σg 𝑇 ) ) ) )
304 303 breq1d ⊢ ( 𝑤 = ( ( ℂfld Σg ( 𝑇 ∘f · 𝑋 ) ) / ( ℂfld Σg 𝑇 ) ) → ( ( 𝐹 ‘ 𝑤 ) ≤ ( ( ℂfld Σg ( 𝑇 ∘f · ( 𝐹 ∘ 𝑋 ) ) ) / ( ℂfld Σg 𝑇 ) ) ↔ ( 𝐹 ‘ ( ( ℂfld Σg ( 𝑇 ∘f · 𝑋 ) ) / ( ℂfld Σg 𝑇 ) ) ) ≤ ( ( ℂfld Σg ( 𝑇 ∘f · ( 𝐹 ∘ 𝑋 ) ) ) / ( ℂfld Σg 𝑇 ) ) ) )
305 304 elrab ⊢ ( ( ( ℂfld Σg ( 𝑇 ∘f · 𝑋 ) ) / ( ℂfld Σg 𝑇 ) ) ∈ { 𝑤 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑤 ) ≤ ( ( ℂfld Σg ( 𝑇 ∘f · ( 𝐹 ∘ 𝑋 ) ) ) / ( ℂfld Σg 𝑇 ) ) } ↔ ( ( ( ℂfld Σg ( 𝑇 ∘f · 𝑋 ) ) / ( ℂfld Σg 𝑇 ) ) ∈ 𝐷 ∧ ( 𝐹 ‘ ( ( ℂfld Σg ( 𝑇 ∘f · 𝑋 ) ) / ( ℂfld Σg 𝑇 ) ) ) ≤ ( ( ℂfld Σg ( 𝑇 ∘f · ( 𝐹 ∘ 𝑋 ) ) ) / ( ℂfld Σg 𝑇 ) ) ) )
306 302 305 sylib ⊢ ( 𝜑 → ( ( ( ℂfld Σg ( 𝑇 ∘f · 𝑋 ) ) / ( ℂfld Σg 𝑇 ) ) ∈ 𝐷 ∧ ( 𝐹 ‘ ( ( ℂfld Σg ( 𝑇 ∘f · 𝑋 ) ) / ( ℂfld Σg 𝑇 ) ) ) ≤ ( ( ℂfld Σg ( 𝑇 ∘f · ( 𝐹 ∘ 𝑋 ) ) ) / ( ℂfld Σg 𝑇 ) ) ) )