Metamath Proof Explorer

Theorem esumrnmpt2

Description: Rewrite an extended sum into a sum on the range of a mapping function. (Contributed by Thierry Arnoux, 30-May-2020)

Ref Expression
Hypotheses esumrnmpt2.1 ⊢ ( 𝑦 = 𝐵 → 𝐶 = 𝐷 )
esumrnmpt2.2 ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
esumrnmpt2.3 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐷 ∈ ( 0 [,] +∞ ) )
esumrnmpt2.4 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ 𝑊 )
esumrnmpt2.5 ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) ∧ 𝐵 = ∅ ) → 𝐷 = 0 )
esumrnmpt2.6 ⊢ ( 𝜑 → Disj 𝑘 ∈ 𝐴 𝐵 )
Assertion esumrnmpt2 ( 𝜑 → Σ* 𝑦 ∈ ran ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) 𝐶 = Σ* 𝑘 ∈ 𝐴 𝐷 )

Proof

Step Hyp Ref Expression
1 esumrnmpt2.1 ⊢ ( 𝑦 = 𝐵 → 𝐶 = 𝐷 )
2 esumrnmpt2.2 ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
3 esumrnmpt2.3 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐷 ∈ ( 0 [,] +∞ ) )
4 esumrnmpt2.4 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ 𝑊 )
5 esumrnmpt2.5 ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) ∧ 𝐵 = ∅ ) → 𝐷 = 0 )
6 esumrnmpt2.6 ⊢ ( 𝜑 → Disj 𝑘 ∈ 𝐴 𝐵 )
7 nfrab1 ⊢ Ⅎ 𝑘 { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ }
8 ssrab2 ⊢ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ⊆ 𝐴
9 8 a1i ⊢ ( 𝜑 → { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ⊆ 𝐴 )
10 2 9 ssexd ⊢ ( 𝜑 → { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ∈ V )
11 9 sselda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ) → 𝑘 ∈ 𝐴 )
12 11 3 syldan ⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ) → 𝐷 ∈ ( 0 [,] +∞ ) )
13 11 4 syldan ⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ) → 𝐵 ∈ 𝑊 )
14 rabid ⊢ ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ↔ ( 𝑘 ∈ 𝐴 ∧ ¬ 𝐵 = ∅ ) )
15 14 simprbi ⊢ ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } → ¬ 𝐵 = ∅ )
16 15 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ) → ¬ 𝐵 = ∅ )
17 elsng ⊢ ( 𝐵 ∈ 𝑊 → ( 𝐵 ∈ { ∅ } ↔ 𝐵 = ∅ ) )
18 13 17 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ) → ( 𝐵 ∈ { ∅ } ↔ 𝐵 = ∅ ) )
19 16 18 mtbird ⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ) → ¬ 𝐵 ∈ { ∅ } )
20 13 19 eldifd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ) → 𝐵 ∈ ( 𝑊 ∖ { ∅ } ) )
21 nfcv ⊢ Ⅎ 𝑘 𝐴
22 7 21 disjss1f ⊢ ( { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ⊆ 𝐴 → ( Disj 𝑘 ∈ 𝐴 𝐵 → Disj 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } 𝐵 ) )
23 9 6 22 sylc ⊢ ( 𝜑 → Disj 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } 𝐵 )
24 7 1 10 12 20 23 esumrnmpt ⊢ ( 𝜑 → Σ* 𝑦 ∈ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ↦ 𝐵 ) 𝐶 = Σ* 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } 𝐷 )
25 nfv ⊢ Ⅎ 𝑦 ( 𝜑 ∧ ∃ 𝑘 ∈ 𝐴 𝐵 = ∅ )
26 snex ⊢ { ∅ } ∈ V
27 26 a1i ⊢ ( ( 𝜑 ∧ ∃ 𝑘 ∈ 𝐴 𝐵 = ∅ ) → { ∅ } ∈ V )
28 velsn ⊢ ( 𝑦 ∈ { ∅ } ↔ 𝑦 = ∅ )
29 28 bilani ⊢ ( ( ( 𝜑 ∧ ∃ 𝑘 ∈ 𝐴 𝐵 = ∅ ) ∧ 𝑦 ∈ { ∅ } ) → 𝑦 = ∅ )
30 nfv ⊢ Ⅎ 𝑘 𝜑
31 nfre1 ⊢ Ⅎ 𝑘 ∃ 𝑘 ∈ 𝐴 𝐵 = ∅
32 30 31 nfan ⊢ Ⅎ 𝑘 ( 𝜑 ∧ ∃ 𝑘 ∈ 𝐴 𝐵 = ∅ )
33 nfv ⊢ Ⅎ 𝑘 𝑦 = ∅
34 32 33 nfan ⊢ Ⅎ 𝑘 ( ( 𝜑 ∧ ∃ 𝑘 ∈ 𝐴 𝐵 = ∅ ) ∧ 𝑦 = ∅ )
35 nfv ⊢ Ⅎ 𝑘 𝐶 = 0
36 simpllr ⊢ ( ( ( ( ( 𝜑 ∧ ∃ 𝑘 ∈ 𝐴 𝐵 = ∅ ) ∧ 𝑦 = ∅ ) ∧ 𝑘 ∈ 𝐴 ) ∧ 𝐵 = ∅ ) → 𝑦 = ∅ )
37 simpr ⊢ ( ( ( ( ( 𝜑 ∧ ∃ 𝑘 ∈ 𝐴 𝐵 = ∅ ) ∧ 𝑦 = ∅ ) ∧ 𝑘 ∈ 𝐴 ) ∧ 𝐵 = ∅ ) → 𝐵 = ∅ )
38 36 37 eqtr4d ⊢ ( ( ( ( ( 𝜑 ∧ ∃ 𝑘 ∈ 𝐴 𝐵 = ∅ ) ∧ 𝑦 = ∅ ) ∧ 𝑘 ∈ 𝐴 ) ∧ 𝐵 = ∅ ) → 𝑦 = 𝐵 )
39 38 1 syl ⊢ ( ( ( ( ( 𝜑 ∧ ∃ 𝑘 ∈ 𝐴 𝐵 = ∅ ) ∧ 𝑦 = ∅ ) ∧ 𝑘 ∈ 𝐴 ) ∧ 𝐵 = ∅ ) → 𝐶 = 𝐷 )
40 simp-4l ⊢ ( ( ( ( ( 𝜑 ∧ ∃ 𝑘 ∈ 𝐴 𝐵 = ∅ ) ∧ 𝑦 = ∅ ) ∧ 𝑘 ∈ 𝐴 ) ∧ 𝐵 = ∅ ) → 𝜑 )
41 simplr ⊢ ( ( ( ( ( 𝜑 ∧ ∃ 𝑘 ∈ 𝐴 𝐵 = ∅ ) ∧ 𝑦 = ∅ ) ∧ 𝑘 ∈ 𝐴 ) ∧ 𝐵 = ∅ ) → 𝑘 ∈ 𝐴 )
42 40 41 37 5 syl21anc ⊢ ( ( ( ( ( 𝜑 ∧ ∃ 𝑘 ∈ 𝐴 𝐵 = ∅ ) ∧ 𝑦 = ∅ ) ∧ 𝑘 ∈ 𝐴 ) ∧ 𝐵 = ∅ ) → 𝐷 = 0 )
43 39 42 eqtrd ⊢ ( ( ( ( ( 𝜑 ∧ ∃ 𝑘 ∈ 𝐴 𝐵 = ∅ ) ∧ 𝑦 = ∅ ) ∧ 𝑘 ∈ 𝐴 ) ∧ 𝐵 = ∅ ) → 𝐶 = 0 )
44 simplr ⊢ ( ( ( 𝜑 ∧ ∃ 𝑘 ∈ 𝐴 𝐵 = ∅ ) ∧ 𝑦 = ∅ ) → ∃ 𝑘 ∈ 𝐴 𝐵 = ∅ )
45 34 35 43 44 r19.29af2 ⊢ ( ( ( 𝜑 ∧ ∃ 𝑘 ∈ 𝐴 𝐵 = ∅ ) ∧ 𝑦 = ∅ ) → 𝐶 = 0 )
46 29 45 syldan ⊢ ( ( ( 𝜑 ∧ ∃ 𝑘 ∈ 𝐴 𝐵 = ∅ ) ∧ 𝑦 ∈ { ∅ } ) → 𝐶 = 0 )
47 0e0iccpnf ⊢ 0 ∈ ( 0 [,] +∞ )
48 46 47 eqeltrdi ⊢ ( ( ( 𝜑 ∧ ∃ 𝑘 ∈ 𝐴 𝐵 = ∅ ) ∧ 𝑦 ∈ { ∅ } ) → 𝐶 ∈ ( 0 [,] +∞ ) )
49 nfcv ⊢ Ⅎ 𝑘 𝑦
50 nfmpt1 ⊢ Ⅎ 𝑘 ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ↦ 𝐵 )
51 50 nfrn ⊢ Ⅎ 𝑘 ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ↦ 𝐵 )
52 49 51 nfel ⊢ Ⅎ 𝑘 𝑦 ∈ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ↦ 𝐵 )
53 30 52 nfan ⊢ Ⅎ 𝑘 ( 𝜑 ∧ 𝑦 ∈ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ↦ 𝐵 ) )
54 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ↦ 𝐵 ) ) ∧ 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ) ∧ 𝑦 = 𝐵 ) → 𝑦 = 𝐵 )
55 rabid ⊢ ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ↔ ( 𝑘 ∈ 𝐴 ∧ 𝐵 = ∅ ) )
56 55 simprbi ⊢ ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } → 𝐵 = ∅ )
57 56 ad2antlr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ↦ 𝐵 ) ) ∧ 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ) ∧ 𝑦 = 𝐵 ) → 𝐵 = ∅ )
58 54 57 eqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ↦ 𝐵 ) ) ∧ 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ) ∧ 𝑦 = 𝐵 ) → 𝑦 = ∅ )
59 58 28 sylibr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ↦ 𝐵 ) ) ∧ 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ) ∧ 𝑦 = 𝐵 ) → 𝑦 ∈ { ∅ } )
60 vex ⊢ 𝑦 ∈ V
61 eqid ⊢ ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ↦ 𝐵 ) = ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ↦ 𝐵 )
62 61 elrnmpt ⊢ ( 𝑦 ∈ V → ( 𝑦 ∈ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ↦ 𝐵 ) ↔ ∃ 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } 𝑦 = 𝐵 ) )
63 60 62 ax-mp ⊢ ( 𝑦 ∈ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ↦ 𝐵 ) ↔ ∃ 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } 𝑦 = 𝐵 )
64 63 bilani ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ↦ 𝐵 ) ) → ∃ 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } 𝑦 = 𝐵 )
65 53 59 64 r19.29af ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ↦ 𝐵 ) ) → 𝑦 ∈ { ∅ } )
66 65 ex ⊢ ( 𝜑 → ( 𝑦 ∈ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ↦ 𝐵 ) → 𝑦 ∈ { ∅ } ) )
67 66 ssrdv ⊢ ( 𝜑 → ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ↦ 𝐵 ) ⊆ { ∅ } )
68 67 adantr ⊢ ( ( 𝜑 ∧ ∃ 𝑘 ∈ 𝐴 𝐵 = ∅ ) → ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ↦ 𝐵 ) ⊆ { ∅ } )
69 25 27 48 68 esummono ⊢ ( ( 𝜑 ∧ ∃ 𝑘 ∈ 𝐴 𝐵 = ∅ ) → Σ* 𝑦 ∈ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ↦ 𝐵 ) 𝐶 ≤ Σ* 𝑦 ∈ { ∅ } 𝐶 )
70 0ex ⊢ ∅ ∈ V
71 70 a1i ⊢ ( ( 𝜑 ∧ ∃ 𝑘 ∈ 𝐴 𝐵 = ∅ ) → ∅ ∈ V )
72 47 a1i ⊢ ( ( 𝜑 ∧ ∃ 𝑘 ∈ 𝐴 𝐵 = ∅ ) → 0 ∈ ( 0 [,] +∞ ) )
73 45 71 72 esumsn ⊢ ( ( 𝜑 ∧ ∃ 𝑘 ∈ 𝐴 𝐵 = ∅ ) → Σ* 𝑦 ∈ { ∅ } 𝐶 = 0 )
74 69 73 breqtrd ⊢ ( ( 𝜑 ∧ ∃ 𝑘 ∈ 𝐴 𝐵 = ∅ ) → Σ* 𝑦 ∈ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ↦ 𝐵 ) 𝐶 ≤ 0 )
75 simpr ⊢ ( ( 𝜑 ∧ ¬ ∃ 𝑘 ∈ 𝐴 𝐵 = ∅ ) → ¬ ∃ 𝑘 ∈ 𝐴 𝐵 = ∅ )
76 nfv ⊢ Ⅎ 𝑦 ¬ ∃ 𝑘 ∈ 𝐴 𝐵 = ∅
77 31 nfn ⊢ Ⅎ 𝑘 ¬ ∃ 𝑘 ∈ 𝐴 𝐵 = ∅
78 rabn0 ⊢ ( { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ≠ ∅ ↔ ∃ 𝑘 ∈ 𝐴 𝐵 = ∅ )
79 78 biimpi ⊢ ( { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ≠ ∅ → ∃ 𝑘 ∈ 𝐴 𝐵 = ∅ )
80 79 necon1bi ⊢ ( ¬ ∃ 𝑘 ∈ 𝐴 𝐵 = ∅ → { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } = ∅ )
81 eqid ⊢ 𝐵 = 𝐵
82 81 a1i ⊢ ( ¬ ∃ 𝑘 ∈ 𝐴 𝐵 = ∅ → 𝐵 = 𝐵 )
83 77 80 82 mpteq12df ⊢ ( ¬ ∃ 𝑘 ∈ 𝐴 𝐵 = ∅ → ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ↦ 𝐵 ) = ( 𝑘 ∈ ∅ ↦ 𝐵 ) )
84 mpt0 ⊢ ( 𝑘 ∈ ∅ ↦ 𝐵 ) = ∅
85 83 84 eqtrdi ⊢ ( ¬ ∃ 𝑘 ∈ 𝐴 𝐵 = ∅ → ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ↦ 𝐵 ) = ∅ )
86 85 rneqd ⊢ ( ¬ ∃ 𝑘 ∈ 𝐴 𝐵 = ∅ → ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ↦ 𝐵 ) = ran ∅ )
87 rn0 ⊢ ran ∅ = ∅
88 86 87 eqtrdi ⊢ ( ¬ ∃ 𝑘 ∈ 𝐴 𝐵 = ∅ → ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ↦ 𝐵 ) = ∅ )
89 76 88 esumeq1d ⊢ ( ¬ ∃ 𝑘 ∈ 𝐴 𝐵 = ∅ → Σ* 𝑦 ∈ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ↦ 𝐵 ) 𝐶 = Σ* 𝑦 ∈ ∅ 𝐶 )
90 esumnul ⊢ Σ* 𝑦 ∈ ∅ 𝐶 = 0
91 89 90 eqtrdi ⊢ ( ¬ ∃ 𝑘 ∈ 𝐴 𝐵 = ∅ → Σ* 𝑦 ∈ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ↦ 𝐵 ) 𝐶 = 0 )
92 0le0 ⊢ 0 ≤ 0
93 91 92 eqbrtrdi ⊢ ( ¬ ∃ 𝑘 ∈ 𝐴 𝐵 = ∅ → Σ* 𝑦 ∈ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ↦ 𝐵 ) 𝐶 ≤ 0 )
94 75 93 syl ⊢ ( ( 𝜑 ∧ ¬ ∃ 𝑘 ∈ 𝐴 𝐵 = ∅ ) → Σ* 𝑦 ∈ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ↦ 𝐵 ) 𝐶 ≤ 0 )
95 74 94 pm2.61dan ⊢ ( 𝜑 → Σ* 𝑦 ∈ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ↦ 𝐵 ) 𝐶 ≤ 0 )
96 ssrab2 ⊢ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ⊆ 𝐴
97 96 a1i ⊢ ( 𝜑 → { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ⊆ 𝐴 )
98 2 97 ssexd ⊢ ( 𝜑 → { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ∈ V )
99 nfrab1 ⊢ Ⅎ 𝑘 { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ }
100 99 mptexgf ⊢ ( { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ∈ V → ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ↦ 𝐵 ) ∈ V )
101 rnexg ⊢ ( ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ↦ 𝐵 ) ∈ V → ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ↦ 𝐵 ) ∈ V )
102 98 100 101 3syl ⊢ ( 𝜑 → ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ↦ 𝐵 ) ∈ V )
103 1 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ↦ 𝐵 ) ) ∧ 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ) ∧ 𝑦 = 𝐵 ) → 𝐶 = 𝐷 )
104 simplll ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ↦ 𝐵 ) ) ∧ 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ) ∧ 𝑦 = 𝐵 ) → 𝜑 )
105 97 sselda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ) → 𝑘 ∈ 𝐴 )
106 105 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ↦ 𝐵 ) ) ∧ 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ) → 𝑘 ∈ 𝐴 )
107 106 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ↦ 𝐵 ) ) ∧ 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ) ∧ 𝑦 = 𝐵 ) → 𝑘 ∈ 𝐴 )
108 104 107 3 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ↦ 𝐵 ) ) ∧ 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ) ∧ 𝑦 = 𝐵 ) → 𝐷 ∈ ( 0 [,] +∞ ) )
109 103 108 eqeltrd ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ↦ 𝐵 ) ) ∧ 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ) ∧ 𝑦 = 𝐵 ) → 𝐶 ∈ ( 0 [,] +∞ ) )
110 53 109 64 r19.29af ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ↦ 𝐵 ) ) → 𝐶 ∈ ( 0 [,] +∞ ) )
111 110 ralrimiva ⊢ ( 𝜑 → ∀ 𝑦 ∈ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ↦ 𝐵 ) 𝐶 ∈ ( 0 [,] +∞ ) )
112 nfcv ⊢ Ⅎ 𝑦 ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ↦ 𝐵 )
113 112 esumcl ⊢ ( ( ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ↦ 𝐵 ) ∈ V ∧ ∀ 𝑦 ∈ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ↦ 𝐵 ) 𝐶 ∈ ( 0 [,] +∞ ) ) → Σ* 𝑦 ∈ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ↦ 𝐵 ) 𝐶 ∈ ( 0 [,] +∞ ) )
114 102 111 113 syl2anc ⊢ ( 𝜑 → Σ* 𝑦 ∈ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ↦ 𝐵 ) 𝐶 ∈ ( 0 [,] +∞ ) )
115 elxrge0 ⊢ ( Σ* 𝑦 ∈ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ↦ 𝐵 ) 𝐶 ∈ ( 0 [,] +∞ ) ↔ ( Σ* 𝑦 ∈ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ↦ 𝐵 ) 𝐶 ∈ ℝ* ∧ 0 ≤ Σ* 𝑦 ∈ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ↦ 𝐵 ) 𝐶 ) )
116 115 simprbi ⊢ ( Σ* 𝑦 ∈ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ↦ 𝐵 ) 𝐶 ∈ ( 0 [,] +∞ ) → 0 ≤ Σ* 𝑦 ∈ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ↦ 𝐵 ) 𝐶 )
117 114 116 syl ⊢ ( 𝜑 → 0 ≤ Σ* 𝑦 ∈ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ↦ 𝐵 ) 𝐶 )
118 95 117 jca ⊢ ( 𝜑 → ( Σ* 𝑦 ∈ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ↦ 𝐵 ) 𝐶 ≤ 0 ∧ 0 ≤ Σ* 𝑦 ∈ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ↦ 𝐵 ) 𝐶 ) )
119 iccssxr ⊢ ( 0 [,] +∞ ) ⊆ ℝ*
120 119 114 sselid ⊢ ( 𝜑 → Σ* 𝑦 ∈ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ↦ 𝐵 ) 𝐶 ∈ ℝ* )
121 119 47 sselii ⊢ 0 ∈ ℝ*
122 121 a1i ⊢ ( 𝜑 → 0 ∈ ℝ* )
123 xrletri3 ⊢ ( ( Σ* 𝑦 ∈ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ↦ 𝐵 ) 𝐶 ∈ ℝ* ∧ 0 ∈ ℝ* ) → ( Σ* 𝑦 ∈ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ↦ 𝐵 ) 𝐶 = 0 ↔ ( Σ* 𝑦 ∈ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ↦ 𝐵 ) 𝐶 ≤ 0 ∧ 0 ≤ Σ* 𝑦 ∈ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ↦ 𝐵 ) 𝐶 ) ) )
124 120 122 123 syl2anc ⊢ ( 𝜑 → ( Σ* 𝑦 ∈ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ↦ 𝐵 ) 𝐶 = 0 ↔ ( Σ* 𝑦 ∈ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ↦ 𝐵 ) 𝐶 ≤ 0 ∧ 0 ≤ Σ* 𝑦 ∈ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ↦ 𝐵 ) 𝐶 ) ) )
125 118 124 mpbird ⊢ ( 𝜑 → Σ* 𝑦 ∈ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ↦ 𝐵 ) 𝐶 = 0 )
126 125 oveq1d ⊢ ( 𝜑 → ( Σ* 𝑦 ∈ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ↦ 𝐵 ) 𝐶 +𝑒 Σ* 𝑦 ∈ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ↦ 𝐵 ) 𝐶 ) = ( 0 +𝑒 Σ* 𝑦 ∈ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ↦ 𝐵 ) 𝐶 ) )
127 12 ralrimiva ⊢ ( 𝜑 → ∀ 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } 𝐷 ∈ ( 0 [,] +∞ ) )
128 7 esumcl ⊢ ( ( { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ∈ V ∧ ∀ 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } 𝐷 ∈ ( 0 [,] +∞ ) ) → Σ* 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } 𝐷 ∈ ( 0 [,] +∞ ) )
129 10 127 128 syl2anc ⊢ ( 𝜑 → Σ* 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } 𝐷 ∈ ( 0 [,] +∞ ) )
130 119 129 sselid ⊢ ( 𝜑 → Σ* 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } 𝐷 ∈ ℝ* )
131 24 130 eqeltrd ⊢ ( 𝜑 → Σ* 𝑦 ∈ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ↦ 𝐵 ) 𝐶 ∈ ℝ* )
132 xaddlid ⊢ ( Σ* 𝑦 ∈ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ↦ 𝐵 ) 𝐶 ∈ ℝ* → ( 0 +𝑒 Σ* 𝑦 ∈ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ↦ 𝐵 ) 𝐶 ) = Σ* 𝑦 ∈ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ↦ 𝐵 ) 𝐶 )
133 131 132 syl ⊢ ( 𝜑 → ( 0 +𝑒 Σ* 𝑦 ∈ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ↦ 𝐵 ) 𝐶 ) = Σ* 𝑦 ∈ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ↦ 𝐵 ) 𝐶 )
134 126 133 eqtrd ⊢ ( 𝜑 → ( Σ* 𝑦 ∈ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ↦ 𝐵 ) 𝐶 +𝑒 Σ* 𝑦 ∈ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ↦ 𝐵 ) 𝐶 ) = Σ* 𝑦 ∈ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ↦ 𝐵 ) 𝐶 )
135 simpl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ) → 𝜑 )
136 56 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ) → 𝐵 = ∅ )
137 135 105 136 5 syl21anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ) → 𝐷 = 0 )
138 137 ralrimiva ⊢ ( 𝜑 → ∀ 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } 𝐷 = 0 )
139 30 138 esumeq2d ⊢ ( 𝜑 → Σ* 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } 𝐷 = Σ* 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } 0 )
140 99 esum0 ⊢ ( { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ∈ V → Σ* 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } 0 = 0 )
141 98 140 syl ⊢ ( 𝜑 → Σ* 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } 0 = 0 )
142 139 141 eqtrd ⊢ ( 𝜑 → Σ* 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } 𝐷 = 0 )
143 142 oveq1d ⊢ ( 𝜑 → ( Σ* 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } 𝐷 +𝑒 Σ* 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } 𝐷 ) = ( 0 +𝑒 Σ* 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } 𝐷 ) )
144 xaddlid ⊢ ( Σ* 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } 𝐷 ∈ ℝ* → ( 0 +𝑒 Σ* 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } 𝐷 ) = Σ* 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } 𝐷 )
145 130 144 syl ⊢ ( 𝜑 → ( 0 +𝑒 Σ* 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } 𝐷 ) = Σ* 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } 𝐷 )
146 143 145 eqtrd ⊢ ( 𝜑 → ( Σ* 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } 𝐷 +𝑒 Σ* 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } 𝐷 ) = Σ* 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } 𝐷 )
147 24 134 146 3eqtr4d ⊢ ( 𝜑 → ( Σ* 𝑦 ∈ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ↦ 𝐵 ) 𝐶 +𝑒 Σ* 𝑦 ∈ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ↦ 𝐵 ) 𝐶 ) = ( Σ* 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } 𝐷 +𝑒 Σ* 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } 𝐷 ) )
148 nfv ⊢ Ⅎ 𝑦 𝜑
149 nfcv ⊢ Ⅎ 𝑦 ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ↦ 𝐵 )
150 7 mptexgf ⊢ ( { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ∈ V → ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ↦ 𝐵 ) ∈ V )
151 rnexg ⊢ ( ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ↦ 𝐵 ) ∈ V → ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ↦ 𝐵 ) ∈ V )
152 10 150 151 3syl ⊢ ( 𝜑 → ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ↦ 𝐵 ) ∈ V )
153 67 ssrind ⊢ ( 𝜑 → ( ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ↦ 𝐵 ) ∩ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ↦ 𝐵 ) ) ⊆ ( { ∅ } ∩ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ↦ 𝐵 ) ) )
154 incom ⊢ ( ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ↦ 𝐵 ) ∩ { ∅ } ) = ( { ∅ } ∩ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ↦ 𝐵 ) )
155 15 neqned ⊢ ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } → 𝐵 ≠ ∅ )
156 155 necomd ⊢ ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } → ∅ ≠ 𝐵 )
157 156 neneqd ⊢ ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } → ¬ ∅ = 𝐵 )
158 157 nrex ⊢ ¬ ∃ 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ∅ = 𝐵
159 eqid ⊢ ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ↦ 𝐵 ) = ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ↦ 𝐵 )
160 159 elrnmpt ⊢ ( ∅ ∈ V → ( ∅ ∈ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ↦ 𝐵 ) ↔ ∃ 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ∅ = 𝐵 ) )
161 70 160 ax-mp ⊢ ( ∅ ∈ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ↦ 𝐵 ) ↔ ∃ 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ∅ = 𝐵 )
162 158 161 mtbir ⊢ ¬ ∅ ∈ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ↦ 𝐵 )
163 disjsn ⊢ ( ( ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ↦ 𝐵 ) ∩ { ∅ } ) = ∅ ↔ ¬ ∅ ∈ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ↦ 𝐵 ) )
164 162 163 mpbir ⊢ ( ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ↦ 𝐵 ) ∩ { ∅ } ) = ∅
165 154 164 eqtr3i ⊢ ( { ∅ } ∩ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ↦ 𝐵 ) ) = ∅
166 153 165 sseqtrdi ⊢ ( 𝜑 → ( ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ↦ 𝐵 ) ∩ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ↦ 𝐵 ) ) ⊆ ∅ )
167 ss0 ⊢ ( ( ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ↦ 𝐵 ) ∩ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ↦ 𝐵 ) ) ⊆ ∅ → ( ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ↦ 𝐵 ) ∩ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ↦ 𝐵 ) ) = ∅ )
168 166 167 syl ⊢ ( 𝜑 → ( ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ↦ 𝐵 ) ∩ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ↦ 𝐵 ) ) = ∅ )
169 nfmpt1 ⊢ Ⅎ 𝑘 ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ↦ 𝐵 )
170 169 nfrn ⊢ Ⅎ 𝑘 ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ↦ 𝐵 )
171 49 170 nfel ⊢ Ⅎ 𝑘 𝑦 ∈ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ↦ 𝐵 )
172 30 171 nfan ⊢ Ⅎ 𝑘 ( 𝜑 ∧ 𝑦 ∈ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ↦ 𝐵 ) )
173 1 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ↦ 𝐵 ) ) ∧ 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ) ∧ 𝑦 = 𝐵 ) → 𝐶 = 𝐷 )
174 simplll ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ↦ 𝐵 ) ) ∧ 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ) ∧ 𝑦 = 𝐵 ) → 𝜑 )
175 11 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ↦ 𝐵 ) ) ∧ 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ) → 𝑘 ∈ 𝐴 )
176 175 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ↦ 𝐵 ) ) ∧ 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ) ∧ 𝑦 = 𝐵 ) → 𝑘 ∈ 𝐴 )
177 174 176 3 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ↦ 𝐵 ) ) ∧ 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ) ∧ 𝑦 = 𝐵 ) → 𝐷 ∈ ( 0 [,] +∞ ) )
178 173 177 eqeltrd ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ↦ 𝐵 ) ) ∧ 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ) ∧ 𝑦 = 𝐵 ) → 𝐶 ∈ ( 0 [,] +∞ ) )
179 159 elrnmpt ⊢ ( 𝑦 ∈ V → ( 𝑦 ∈ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ↦ 𝐵 ) ↔ ∃ 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } 𝑦 = 𝐵 ) )
180 60 179 ax-mp ⊢ ( 𝑦 ∈ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ↦ 𝐵 ) ↔ ∃ 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } 𝑦 = 𝐵 )
181 180 bilani ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ↦ 𝐵 ) ) → ∃ 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } 𝑦 = 𝐵 )
182 172 178 181 r19.29af ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ↦ 𝐵 ) ) → 𝐶 ∈ ( 0 [,] +∞ ) )
183 148 112 149 102 152 168 110 182 esumsplit ⊢ ( 𝜑 → Σ* 𝑦 ∈ ( ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ↦ 𝐵 ) ∪ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ↦ 𝐵 ) ) 𝐶 = ( Σ* 𝑦 ∈ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ↦ 𝐵 ) 𝐶 +𝑒 Σ* 𝑦 ∈ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ↦ 𝐵 ) 𝐶 ) )
184 rabnc ⊢ ( { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ∩ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ) = ∅
185 184 a1i ⊢ ( 𝜑 → ( { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ∩ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ) = ∅ )
186 105 3 syldan ⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ) → 𝐷 ∈ ( 0 [,] +∞ ) )
187 30 99 7 98 10 185 186 12 esumsplit ⊢ ( 𝜑 → Σ* 𝑘 ∈ ( { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ∪ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ) 𝐷 = ( Σ* 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } 𝐷 +𝑒 Σ* 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } 𝐷 ) )
188 147 183 187 3eqtr4d ⊢ ( 𝜑 → Σ* 𝑦 ∈ ( ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ↦ 𝐵 ) ∪ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ↦ 𝐵 ) ) 𝐶 = Σ* 𝑘 ∈ ( { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ∪ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ) 𝐷 )
189 rabxm ⊢ 𝐴 = ( { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ∪ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } )
190 189 81 mpteq12i ⊢ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑘 ∈ ( { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ∪ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ) ↦ 𝐵 )
191 mptun ⊢ ( 𝑘 ∈ ( { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ∪ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ) ↦ 𝐵 ) = ( ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ↦ 𝐵 ) ∪ ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ↦ 𝐵 ) )
192 190 191 eqtri ⊢ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) = ( ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ↦ 𝐵 ) ∪ ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ↦ 𝐵 ) )
193 192 rneqi ⊢ ran ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) = ran ( ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ↦ 𝐵 ) ∪ ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ↦ 𝐵 ) )
194 rnun ⊢ ran ( ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ↦ 𝐵 ) ∪ ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ↦ 𝐵 ) ) = ( ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ↦ 𝐵 ) ∪ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ↦ 𝐵 ) )
195 193 194 eqtri ⊢ ran ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) = ( ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ↦ 𝐵 ) ∪ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ↦ 𝐵 ) )
196 195 a1i ⊢ ( 𝜑 → ran ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) = ( ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ↦ 𝐵 ) ∪ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ↦ 𝐵 ) ) )
197 148 196 esumeq1d ⊢ ( 𝜑 → Σ* 𝑦 ∈ ran ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) 𝐶 = Σ* 𝑦 ∈ ( ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ↦ 𝐵 ) ∪ ran ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ↦ 𝐵 ) ) 𝐶 )
198 189 a1i ⊢ ( 𝜑 → 𝐴 = ( { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ∪ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ) )
199 30 198 esumeq1d ⊢ ( 𝜑 → Σ* 𝑘 ∈ 𝐴 𝐷 = Σ* 𝑘 ∈ ( { 𝑘 ∈ 𝐴 ∣ 𝐵 = ∅ } ∪ { 𝑘 ∈ 𝐴 ∣ ¬ 𝐵 = ∅ } ) 𝐷 )
200 188 197 199 3eqtr4d ⊢ ( 𝜑 → Σ* 𝑦 ∈ ran ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) 𝐶 = Σ* 𝑘 ∈ 𝐴 𝐷 )