Step |
Hyp |
Ref |
Expression |
1 |
|
sge0resplit.a |
⊢ ( 𝜑 → 𝐴 ∈ 𝑉 ) |
2 |
|
sge0resplit.b |
⊢ ( 𝜑 → 𝐵 ∈ 𝑊 ) |
3 |
|
sge0resplit.u |
⊢ 𝑈 = ( 𝐴 ∪ 𝐵 ) |
4 |
|
sge0resplit.in0 |
⊢ ( 𝜑 → ( 𝐴 ∩ 𝐵 ) = ∅ ) |
5 |
|
sge0resplit.f |
⊢ ( 𝜑 → 𝐹 : 𝑈 ⟶ ( 0 [,] +∞ ) ) |
6 |
|
sge0resplit.re |
⊢ ( 𝜑 → ( Σ^ ‘ 𝐹 ) ∈ ℝ ) |
7 |
|
ssun1 |
⊢ 𝐴 ⊆ ( 𝐴 ∪ 𝐵 ) |
8 |
3
|
eqcomi |
⊢ ( 𝐴 ∪ 𝐵 ) = 𝑈 |
9 |
7 8
|
sseqtri |
⊢ 𝐴 ⊆ 𝑈 |
10 |
9
|
a1i |
⊢ ( 𝜑 → 𝐴 ⊆ 𝑈 ) |
11 |
5 10
|
fssresd |
⊢ ( 𝜑 → ( 𝐹 ↾ 𝐴 ) : 𝐴 ⟶ ( 0 [,] +∞ ) ) |
12 |
3
|
a1i |
⊢ ( 𝜑 → 𝑈 = ( 𝐴 ∪ 𝐵 ) ) |
13 |
|
unexg |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐴 ∪ 𝐵 ) ∈ V ) |
14 |
1 2 13
|
syl2anc |
⊢ ( 𝜑 → ( 𝐴 ∪ 𝐵 ) ∈ V ) |
15 |
12 14
|
eqeltrd |
⊢ ( 𝜑 → 𝑈 ∈ V ) |
16 |
15 5 6
|
sge0ssre |
⊢ ( 𝜑 → ( Σ^ ‘ ( 𝐹 ↾ 𝐴 ) ) ∈ ℝ ) |
17 |
1 11 16
|
sge0supre |
⊢ ( 𝜑 → ( Σ^ ‘ ( 𝐹 ↾ 𝐴 ) ) = sup ( ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ) , ℝ , < ) ) |
18 |
17 16
|
eqeltrrd |
⊢ ( 𝜑 → sup ( ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ) , ℝ , < ) ∈ ℝ ) |
19 |
|
ssun2 |
⊢ 𝐵 ⊆ ( 𝐴 ∪ 𝐵 ) |
20 |
19 8
|
sseqtri |
⊢ 𝐵 ⊆ 𝑈 |
21 |
20
|
a1i |
⊢ ( 𝜑 → 𝐵 ⊆ 𝑈 ) |
22 |
5 21
|
fssresd |
⊢ ( 𝜑 → ( 𝐹 ↾ 𝐵 ) : 𝐵 ⟶ ( 0 [,] +∞ ) ) |
23 |
15 5 6
|
sge0ssre |
⊢ ( 𝜑 → ( Σ^ ‘ ( 𝐹 ↾ 𝐵 ) ) ∈ ℝ ) |
24 |
2 22 23
|
sge0supre |
⊢ ( 𝜑 → ( Σ^ ‘ ( 𝐹 ↾ 𝐵 ) ) = sup ( ran ( 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) , ℝ , < ) ) |
25 |
24 23
|
eqeltrrd |
⊢ ( 𝜑 → sup ( ran ( 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) , ℝ , < ) ∈ ℝ ) |
26 |
|
rexadd |
⊢ ( ( sup ( ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ) , ℝ , < ) ∈ ℝ ∧ sup ( ran ( 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) , ℝ , < ) ∈ ℝ ) → ( sup ( ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ) , ℝ , < ) +𝑒 sup ( ran ( 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) , ℝ , < ) ) = ( sup ( ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ) , ℝ , < ) + sup ( ran ( 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) , ℝ , < ) ) ) |
27 |
18 25 26
|
syl2anc |
⊢ ( 𝜑 → ( sup ( ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ) , ℝ , < ) +𝑒 sup ( ran ( 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) , ℝ , < ) ) = ( sup ( ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ) , ℝ , < ) + sup ( ran ( 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) , ℝ , < ) ) ) |
28 |
15 5 6
|
sge0rern |
⊢ ( 𝜑 → ¬ +∞ ∈ ran 𝐹 ) |
29 |
|
nelrnres |
⊢ ( ¬ +∞ ∈ ran 𝐹 → ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) |
30 |
28 29
|
syl |
⊢ ( 𝜑 → ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐴 ) ) |
31 |
11 30
|
fge0iccico |
⊢ ( 𝜑 → ( 𝐹 ↾ 𝐴 ) : 𝐴 ⟶ ( 0 [,) +∞ ) ) |
32 |
31
|
sge0rnre |
⊢ ( 𝜑 → ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ) ⊆ ℝ ) |
33 |
|
sge0rnn0 |
⊢ ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ) ≠ ∅ |
34 |
33
|
a1i |
⊢ ( 𝜑 → ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ) ≠ ∅ ) |
35 |
1 31
|
sge0reval |
⊢ ( 𝜑 → ( Σ^ ‘ ( 𝐹 ↾ 𝐴 ) ) = sup ( ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ) , ℝ* , < ) ) |
36 |
35
|
eqcomd |
⊢ ( 𝜑 → sup ( ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ) , ℝ* , < ) = ( Σ^ ‘ ( 𝐹 ↾ 𝐴 ) ) ) |
37 |
36 16
|
eqeltrd |
⊢ ( 𝜑 → sup ( ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ) , ℝ* , < ) ∈ ℝ ) |
38 |
|
supxrre3 |
⊢ ( ( ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ) ⊆ ℝ ∧ ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ) ≠ ∅ ) → ( sup ( ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ) , ℝ* , < ) ∈ ℝ ↔ ∃ 𝑤 ∈ ℝ ∀ 𝑡 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ) 𝑡 ≤ 𝑤 ) ) |
39 |
32 34 38
|
syl2anc |
⊢ ( 𝜑 → ( sup ( ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ) , ℝ* , < ) ∈ ℝ ↔ ∃ 𝑤 ∈ ℝ ∀ 𝑡 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ) 𝑡 ≤ 𝑤 ) ) |
40 |
37 39
|
mpbid |
⊢ ( 𝜑 → ∃ 𝑤 ∈ ℝ ∀ 𝑡 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ) 𝑡 ≤ 𝑤 ) |
41 |
|
nelrnres |
⊢ ( ¬ +∞ ∈ ran 𝐹 → ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) |
42 |
28 41
|
syl |
⊢ ( 𝜑 → ¬ +∞ ∈ ran ( 𝐹 ↾ 𝐵 ) ) |
43 |
22 42
|
fge0iccico |
⊢ ( 𝜑 → ( 𝐹 ↾ 𝐵 ) : 𝐵 ⟶ ( 0 [,) +∞ ) ) |
44 |
43
|
sge0rnre |
⊢ ( 𝜑 → ran ( 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) ⊆ ℝ ) |
45 |
|
sge0rnn0 |
⊢ ran ( 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) ≠ ∅ |
46 |
45
|
a1i |
⊢ ( 𝜑 → ran ( 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) ≠ ∅ ) |
47 |
2 43
|
sge0reval |
⊢ ( 𝜑 → ( Σ^ ‘ ( 𝐹 ↾ 𝐵 ) ) = sup ( ran ( 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) , ℝ* , < ) ) |
48 |
47
|
eqcomd |
⊢ ( 𝜑 → sup ( ran ( 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) , ℝ* , < ) = ( Σ^ ‘ ( 𝐹 ↾ 𝐵 ) ) ) |
49 |
48 23
|
eqeltrd |
⊢ ( 𝜑 → sup ( ran ( 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) , ℝ* , < ) ∈ ℝ ) |
50 |
|
supxrre3 |
⊢ ( ( ran ( 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) ⊆ ℝ ∧ ran ( 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) ≠ ∅ ) → ( sup ( ran ( 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) , ℝ* , < ) ∈ ℝ ↔ ∃ 𝑤 ∈ ℝ ∀ 𝑡 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) 𝑡 ≤ 𝑤 ) ) |
51 |
44 46 50
|
syl2anc |
⊢ ( 𝜑 → ( sup ( ran ( 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) , ℝ* , < ) ∈ ℝ ↔ ∃ 𝑤 ∈ ℝ ∀ 𝑡 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) 𝑡 ≤ 𝑤 ) ) |
52 |
49 51
|
mpbid |
⊢ ( 𝜑 → ∃ 𝑤 ∈ ℝ ∀ 𝑡 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) 𝑡 ≤ 𝑤 ) |
53 |
|
eqid |
⊢ { 𝑧 ∣ ∃ 𝑣 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ) ∃ 𝑢 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) 𝑧 = ( 𝑣 + 𝑢 ) } = { 𝑧 ∣ ∃ 𝑣 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ) ∃ 𝑢 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) 𝑧 = ( 𝑣 + 𝑢 ) } |
54 |
32 34 40 44 46 52 53
|
supadd |
⊢ ( 𝜑 → ( sup ( ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ) , ℝ , < ) + sup ( ran ( 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) , ℝ , < ) ) = sup ( { 𝑧 ∣ ∃ 𝑣 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ) ∃ 𝑢 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) 𝑧 = ( 𝑣 + 𝑢 ) } , ℝ , < ) ) |
55 |
|
simpl |
⊢ ( ( 𝜑 ∧ 𝑟 ∈ { 𝑧 ∣ ∃ 𝑣 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ) ∃ 𝑢 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) 𝑧 = ( 𝑣 + 𝑢 ) } ) → 𝜑 ) |
56 |
|
vex |
⊢ 𝑟 ∈ V |
57 |
|
eqeq1 |
⊢ ( 𝑧 = 𝑟 → ( 𝑧 = ( 𝑣 + 𝑢 ) ↔ 𝑟 = ( 𝑣 + 𝑢 ) ) ) |
58 |
57
|
rexbidv |
⊢ ( 𝑧 = 𝑟 → ( ∃ 𝑢 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) 𝑧 = ( 𝑣 + 𝑢 ) ↔ ∃ 𝑢 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) 𝑟 = ( 𝑣 + 𝑢 ) ) ) |
59 |
58
|
rexbidv |
⊢ ( 𝑧 = 𝑟 → ( ∃ 𝑣 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ) ∃ 𝑢 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) 𝑧 = ( 𝑣 + 𝑢 ) ↔ ∃ 𝑣 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ) ∃ 𝑢 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) 𝑟 = ( 𝑣 + 𝑢 ) ) ) |
60 |
56 59
|
elab |
⊢ ( 𝑟 ∈ { 𝑧 ∣ ∃ 𝑣 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ) ∃ 𝑢 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) 𝑧 = ( 𝑣 + 𝑢 ) } ↔ ∃ 𝑣 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ) ∃ 𝑢 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) 𝑟 = ( 𝑣 + 𝑢 ) ) |
61 |
60
|
biimpi |
⊢ ( 𝑟 ∈ { 𝑧 ∣ ∃ 𝑣 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ) ∃ 𝑢 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) 𝑧 = ( 𝑣 + 𝑢 ) } → ∃ 𝑣 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ) ∃ 𝑢 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) 𝑟 = ( 𝑣 + 𝑢 ) ) |
62 |
61
|
adantl |
⊢ ( ( 𝜑 ∧ 𝑟 ∈ { 𝑧 ∣ ∃ 𝑣 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ) ∃ 𝑢 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) 𝑧 = ( 𝑣 + 𝑢 ) } ) → ∃ 𝑣 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ) ∃ 𝑢 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) 𝑟 = ( 𝑣 + 𝑢 ) ) |
63 |
|
simpl |
⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ) ∧ 𝑢 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) ) ) → 𝜑 ) |
64 |
|
vex |
⊢ 𝑣 ∈ V |
65 |
|
sumeq1 |
⊢ ( 𝑥 = 𝑎 → Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) = Σ 𝑦 ∈ 𝑎 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ) |
66 |
65
|
cbvmptv |
⊢ ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ) = ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑎 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ) |
67 |
66
|
elrnmpt |
⊢ ( 𝑣 ∈ V → ( 𝑣 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ) ↔ ∃ 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) 𝑣 = Σ 𝑦 ∈ 𝑎 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ) ) |
68 |
64 67
|
ax-mp |
⊢ ( 𝑣 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ) ↔ ∃ 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) 𝑣 = Σ 𝑦 ∈ 𝑎 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ) |
69 |
68
|
biimpi |
⊢ ( 𝑣 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ) → ∃ 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) 𝑣 = Σ 𝑦 ∈ 𝑎 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ) |
70 |
69
|
adantr |
⊢ ( ( 𝑣 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ) ∧ 𝑢 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) ) → ∃ 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) 𝑣 = Σ 𝑦 ∈ 𝑎 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ) |
71 |
|
vex |
⊢ 𝑢 ∈ V |
72 |
|
sumeq1 |
⊢ ( 𝑥 = 𝑏 → Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) = Σ 𝑦 ∈ 𝑏 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) |
73 |
72
|
cbvmptv |
⊢ ( 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) = ( 𝑏 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑏 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) |
74 |
73
|
elrnmpt |
⊢ ( 𝑢 ∈ V → ( 𝑢 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) ↔ ∃ 𝑏 ∈ ( 𝒫 𝐵 ∩ Fin ) 𝑢 = Σ 𝑦 ∈ 𝑏 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) ) |
75 |
71 74
|
ax-mp |
⊢ ( 𝑢 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) ↔ ∃ 𝑏 ∈ ( 𝒫 𝐵 ∩ Fin ) 𝑢 = Σ 𝑦 ∈ 𝑏 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) |
76 |
75
|
biimpi |
⊢ ( 𝑢 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) → ∃ 𝑏 ∈ ( 𝒫 𝐵 ∩ Fin ) 𝑢 = Σ 𝑦 ∈ 𝑏 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) |
77 |
76
|
adantl |
⊢ ( ( 𝑣 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ) ∧ 𝑢 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) ) → ∃ 𝑏 ∈ ( 𝒫 𝐵 ∩ Fin ) 𝑢 = Σ 𝑦 ∈ 𝑏 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) |
78 |
70 77
|
jca |
⊢ ( ( 𝑣 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ) ∧ 𝑢 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) ) → ( ∃ 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) 𝑣 = Σ 𝑦 ∈ 𝑎 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ∧ ∃ 𝑏 ∈ ( 𝒫 𝐵 ∩ Fin ) 𝑢 = Σ 𝑦 ∈ 𝑏 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) ) |
79 |
|
reeanv |
⊢ ( ∃ 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ∃ 𝑏 ∈ ( 𝒫 𝐵 ∩ Fin ) ( 𝑣 = Σ 𝑦 ∈ 𝑎 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ∧ 𝑢 = Σ 𝑦 ∈ 𝑏 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) ↔ ( ∃ 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) 𝑣 = Σ 𝑦 ∈ 𝑎 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ∧ ∃ 𝑏 ∈ ( 𝒫 𝐵 ∩ Fin ) 𝑢 = Σ 𝑦 ∈ 𝑏 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) ) |
80 |
78 79
|
sylibr |
⊢ ( ( 𝑣 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ) ∧ 𝑢 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) ) → ∃ 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ∃ 𝑏 ∈ ( 𝒫 𝐵 ∩ Fin ) ( 𝑣 = Σ 𝑦 ∈ 𝑎 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ∧ 𝑢 = Σ 𝑦 ∈ 𝑏 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) ) |
81 |
80
|
adantl |
⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ) ∧ 𝑢 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) ) ) → ∃ 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ∃ 𝑏 ∈ ( 𝒫 𝐵 ∩ Fin ) ( 𝑣 = Σ 𝑦 ∈ 𝑎 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ∧ 𝑢 = Σ 𝑦 ∈ 𝑏 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) ) |
82 |
|
eqid |
⊢ ( 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) = ( 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) |
83 |
|
elinel1 |
⊢ ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) → 𝑎 ∈ 𝒫 𝐴 ) |
84 |
|
elpwi |
⊢ ( 𝑎 ∈ 𝒫 𝐴 → 𝑎 ⊆ 𝐴 ) |
85 |
|
id |
⊢ ( 𝑎 ⊆ 𝐴 → 𝑎 ⊆ 𝐴 ) |
86 |
85 9
|
sstrdi |
⊢ ( 𝑎 ⊆ 𝐴 → 𝑎 ⊆ 𝑈 ) |
87 |
84 86
|
syl |
⊢ ( 𝑎 ∈ 𝒫 𝐴 → 𝑎 ⊆ 𝑈 ) |
88 |
83 87
|
syl |
⊢ ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) → 𝑎 ⊆ 𝑈 ) |
89 |
88
|
adantr |
⊢ ( ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑏 ∈ ( 𝒫 𝐵 ∩ Fin ) ) → 𝑎 ⊆ 𝑈 ) |
90 |
|
elinel1 |
⊢ ( 𝑏 ∈ ( 𝒫 𝐵 ∩ Fin ) → 𝑏 ∈ 𝒫 𝐵 ) |
91 |
|
elpwi |
⊢ ( 𝑏 ∈ 𝒫 𝐵 → 𝑏 ⊆ 𝐵 ) |
92 |
|
id |
⊢ ( 𝑏 ⊆ 𝐵 → 𝑏 ⊆ 𝐵 ) |
93 |
92 20
|
sstrdi |
⊢ ( 𝑏 ⊆ 𝐵 → 𝑏 ⊆ 𝑈 ) |
94 |
91 93
|
syl |
⊢ ( 𝑏 ∈ 𝒫 𝐵 → 𝑏 ⊆ 𝑈 ) |
95 |
90 94
|
syl |
⊢ ( 𝑏 ∈ ( 𝒫 𝐵 ∩ Fin ) → 𝑏 ⊆ 𝑈 ) |
96 |
95
|
adantl |
⊢ ( ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑏 ∈ ( 𝒫 𝐵 ∩ Fin ) ) → 𝑏 ⊆ 𝑈 ) |
97 |
89 96
|
unssd |
⊢ ( ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑏 ∈ ( 𝒫 𝐵 ∩ Fin ) ) → ( 𝑎 ∪ 𝑏 ) ⊆ 𝑈 ) |
98 |
|
vex |
⊢ 𝑎 ∈ V |
99 |
|
vex |
⊢ 𝑏 ∈ V |
100 |
98 99
|
unex |
⊢ ( 𝑎 ∪ 𝑏 ) ∈ V |
101 |
100
|
elpw |
⊢ ( ( 𝑎 ∪ 𝑏 ) ∈ 𝒫 𝑈 ↔ ( 𝑎 ∪ 𝑏 ) ⊆ 𝑈 ) |
102 |
97 101
|
sylibr |
⊢ ( ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑏 ∈ ( 𝒫 𝐵 ∩ Fin ) ) → ( 𝑎 ∪ 𝑏 ) ∈ 𝒫 𝑈 ) |
103 |
|
elinel2 |
⊢ ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) → 𝑎 ∈ Fin ) |
104 |
103
|
adantr |
⊢ ( ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑏 ∈ ( 𝒫 𝐵 ∩ Fin ) ) → 𝑎 ∈ Fin ) |
105 |
|
elinel2 |
⊢ ( 𝑏 ∈ ( 𝒫 𝐵 ∩ Fin ) → 𝑏 ∈ Fin ) |
106 |
105
|
adantl |
⊢ ( ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑏 ∈ ( 𝒫 𝐵 ∩ Fin ) ) → 𝑏 ∈ Fin ) |
107 |
|
unfi |
⊢ ( ( 𝑎 ∈ Fin ∧ 𝑏 ∈ Fin ) → ( 𝑎 ∪ 𝑏 ) ∈ Fin ) |
108 |
104 106 107
|
syl2anc |
⊢ ( ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑏 ∈ ( 𝒫 𝐵 ∩ Fin ) ) → ( 𝑎 ∪ 𝑏 ) ∈ Fin ) |
109 |
102 108
|
elind |
⊢ ( ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑏 ∈ ( 𝒫 𝐵 ∩ Fin ) ) → ( 𝑎 ∪ 𝑏 ) ∈ ( 𝒫 𝑈 ∩ Fin ) ) |
110 |
109
|
adantl |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑏 ∈ ( 𝒫 𝐵 ∩ Fin ) ) ) → ( 𝑎 ∪ 𝑏 ) ∈ ( 𝒫 𝑈 ∩ Fin ) ) |
111 |
110
|
ad2antrr |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑏 ∈ ( 𝒫 𝐵 ∩ Fin ) ) ) ∧ ( 𝑣 = Σ 𝑦 ∈ 𝑎 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ∧ 𝑢 = Σ 𝑦 ∈ 𝑏 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) ) ∧ 𝑟 = ( 𝑣 + 𝑢 ) ) → ( 𝑎 ∪ 𝑏 ) ∈ ( 𝒫 𝑈 ∩ Fin ) ) |
112 |
|
simpl |
⊢ ( ( 𝑣 = Σ 𝑦 ∈ 𝑎 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ∧ 𝑢 = Σ 𝑦 ∈ 𝑏 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) → 𝑣 = Σ 𝑦 ∈ 𝑎 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ) |
113 |
|
simpr |
⊢ ( ( 𝑣 = Σ 𝑦 ∈ 𝑎 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ∧ 𝑢 = Σ 𝑦 ∈ 𝑏 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) → 𝑢 = Σ 𝑦 ∈ 𝑏 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) |
114 |
112 113
|
oveq12d |
⊢ ( ( 𝑣 = Σ 𝑦 ∈ 𝑎 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ∧ 𝑢 = Σ 𝑦 ∈ 𝑏 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) → ( 𝑣 + 𝑢 ) = ( Σ 𝑦 ∈ 𝑎 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) + Σ 𝑦 ∈ 𝑏 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) ) |
115 |
114
|
adantl |
⊢ ( ( ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑏 ∈ ( 𝒫 𝐵 ∩ Fin ) ) ∧ ( 𝑣 = Σ 𝑦 ∈ 𝑎 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ∧ 𝑢 = Σ 𝑦 ∈ 𝑏 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) ) → ( 𝑣 + 𝑢 ) = ( Σ 𝑦 ∈ 𝑎 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) + Σ 𝑦 ∈ 𝑏 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) ) |
116 |
83 84
|
syl |
⊢ ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) → 𝑎 ⊆ 𝐴 ) |
117 |
116
|
sselda |
⊢ ( ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑦 ∈ 𝑎 ) → 𝑦 ∈ 𝐴 ) |
118 |
|
fvres |
⊢ ( 𝑦 ∈ 𝐴 → ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) = ( 𝐹 ‘ 𝑦 ) ) |
119 |
117 118
|
syl |
⊢ ( ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑦 ∈ 𝑎 ) → ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) = ( 𝐹 ‘ 𝑦 ) ) |
120 |
119
|
sumeq2dv |
⊢ ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) → Σ 𝑦 ∈ 𝑎 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) = Σ 𝑦 ∈ 𝑎 ( 𝐹 ‘ 𝑦 ) ) |
121 |
120
|
adantr |
⊢ ( ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑏 ∈ ( 𝒫 𝐵 ∩ Fin ) ) → Σ 𝑦 ∈ 𝑎 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) = Σ 𝑦 ∈ 𝑎 ( 𝐹 ‘ 𝑦 ) ) |
122 |
90 91
|
syl |
⊢ ( 𝑏 ∈ ( 𝒫 𝐵 ∩ Fin ) → 𝑏 ⊆ 𝐵 ) |
123 |
122
|
sselda |
⊢ ( ( 𝑏 ∈ ( 𝒫 𝐵 ∩ Fin ) ∧ 𝑦 ∈ 𝑏 ) → 𝑦 ∈ 𝐵 ) |
124 |
|
fvres |
⊢ ( 𝑦 ∈ 𝐵 → ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) = ( 𝐹 ‘ 𝑦 ) ) |
125 |
123 124
|
syl |
⊢ ( ( 𝑏 ∈ ( 𝒫 𝐵 ∩ Fin ) ∧ 𝑦 ∈ 𝑏 ) → ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) = ( 𝐹 ‘ 𝑦 ) ) |
126 |
125
|
sumeq2dv |
⊢ ( 𝑏 ∈ ( 𝒫 𝐵 ∩ Fin ) → Σ 𝑦 ∈ 𝑏 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) = Σ 𝑦 ∈ 𝑏 ( 𝐹 ‘ 𝑦 ) ) |
127 |
126
|
adantl |
⊢ ( ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑏 ∈ ( 𝒫 𝐵 ∩ Fin ) ) → Σ 𝑦 ∈ 𝑏 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) = Σ 𝑦 ∈ 𝑏 ( 𝐹 ‘ 𝑦 ) ) |
128 |
121 127
|
oveq12d |
⊢ ( ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑏 ∈ ( 𝒫 𝐵 ∩ Fin ) ) → ( Σ 𝑦 ∈ 𝑎 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) + Σ 𝑦 ∈ 𝑏 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) = ( Σ 𝑦 ∈ 𝑎 ( 𝐹 ‘ 𝑦 ) + Σ 𝑦 ∈ 𝑏 ( 𝐹 ‘ 𝑦 ) ) ) |
129 |
128
|
adantr |
⊢ ( ( ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑏 ∈ ( 𝒫 𝐵 ∩ Fin ) ) ∧ ( 𝑣 = Σ 𝑦 ∈ 𝑎 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ∧ 𝑢 = Σ 𝑦 ∈ 𝑏 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) ) → ( Σ 𝑦 ∈ 𝑎 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) + Σ 𝑦 ∈ 𝑏 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) = ( Σ 𝑦 ∈ 𝑎 ( 𝐹 ‘ 𝑦 ) + Σ 𝑦 ∈ 𝑏 ( 𝐹 ‘ 𝑦 ) ) ) |
130 |
115 129
|
eqtrd |
⊢ ( ( ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑏 ∈ ( 𝒫 𝐵 ∩ Fin ) ) ∧ ( 𝑣 = Σ 𝑦 ∈ 𝑎 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ∧ 𝑢 = Σ 𝑦 ∈ 𝑏 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) ) → ( 𝑣 + 𝑢 ) = ( Σ 𝑦 ∈ 𝑎 ( 𝐹 ‘ 𝑦 ) + Σ 𝑦 ∈ 𝑏 ( 𝐹 ‘ 𝑦 ) ) ) |
131 |
130
|
ad4ant23 |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑏 ∈ ( 𝒫 𝐵 ∩ Fin ) ) ) ∧ ( 𝑣 = Σ 𝑦 ∈ 𝑎 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ∧ 𝑢 = Σ 𝑦 ∈ 𝑏 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) ) ∧ 𝑟 = ( 𝑣 + 𝑢 ) ) → ( 𝑣 + 𝑢 ) = ( Σ 𝑦 ∈ 𝑎 ( 𝐹 ‘ 𝑦 ) + Σ 𝑦 ∈ 𝑏 ( 𝐹 ‘ 𝑦 ) ) ) |
132 |
|
simpr |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑏 ∈ ( 𝒫 𝐵 ∩ Fin ) ) ) ∧ ( 𝑣 = Σ 𝑦 ∈ 𝑎 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ∧ 𝑢 = Σ 𝑦 ∈ 𝑏 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) ) ∧ 𝑟 = ( 𝑣 + 𝑢 ) ) → 𝑟 = ( 𝑣 + 𝑢 ) ) |
133 |
4
|
adantr |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑏 ∈ ( 𝒫 𝐵 ∩ Fin ) ) ) → ( 𝐴 ∩ 𝐵 ) = ∅ ) |
134 |
116
|
ad2antrl |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑏 ∈ ( 𝒫 𝐵 ∩ Fin ) ) ) → 𝑎 ⊆ 𝐴 ) |
135 |
122
|
adantl |
⊢ ( ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑏 ∈ ( 𝒫 𝐵 ∩ Fin ) ) → 𝑏 ⊆ 𝐵 ) |
136 |
135
|
adantl |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑏 ∈ ( 𝒫 𝐵 ∩ Fin ) ) ) → 𝑏 ⊆ 𝐵 ) |
137 |
|
ssin0 |
⊢ ( ( ( 𝐴 ∩ 𝐵 ) = ∅ ∧ 𝑎 ⊆ 𝐴 ∧ 𝑏 ⊆ 𝐵 ) → ( 𝑎 ∩ 𝑏 ) = ∅ ) |
138 |
133 134 136 137
|
syl3anc |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑏 ∈ ( 𝒫 𝐵 ∩ Fin ) ) ) → ( 𝑎 ∩ 𝑏 ) = ∅ ) |
139 |
|
eqidd |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑏 ∈ ( 𝒫 𝐵 ∩ Fin ) ) ) → ( 𝑎 ∪ 𝑏 ) = ( 𝑎 ∪ 𝑏 ) ) |
140 |
108
|
adantl |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑏 ∈ ( 𝒫 𝐵 ∩ Fin ) ) ) → ( 𝑎 ∪ 𝑏 ) ∈ Fin ) |
141 |
|
rge0ssre |
⊢ ( 0 [,) +∞ ) ⊆ ℝ |
142 |
|
ax-resscn |
⊢ ℝ ⊆ ℂ |
143 |
141 142
|
sstri |
⊢ ( 0 [,) +∞ ) ⊆ ℂ |
144 |
5 28
|
fge0iccico |
⊢ ( 𝜑 → 𝐹 : 𝑈 ⟶ ( 0 [,) +∞ ) ) |
145 |
144
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑏 ∈ ( 𝒫 𝐵 ∩ Fin ) ) ) ∧ 𝑦 ∈ ( 𝑎 ∪ 𝑏 ) ) → 𝐹 : 𝑈 ⟶ ( 0 [,) +∞ ) ) |
146 |
97
|
sselda |
⊢ ( ( ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑏 ∈ ( 𝒫 𝐵 ∩ Fin ) ) ∧ 𝑦 ∈ ( 𝑎 ∪ 𝑏 ) ) → 𝑦 ∈ 𝑈 ) |
147 |
146
|
adantll |
⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑏 ∈ ( 𝒫 𝐵 ∩ Fin ) ) ) ∧ 𝑦 ∈ ( 𝑎 ∪ 𝑏 ) ) → 𝑦 ∈ 𝑈 ) |
148 |
145 147
|
ffvelrnd |
⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑏 ∈ ( 𝒫 𝐵 ∩ Fin ) ) ) ∧ 𝑦 ∈ ( 𝑎 ∪ 𝑏 ) ) → ( 𝐹 ‘ 𝑦 ) ∈ ( 0 [,) +∞ ) ) |
149 |
143 148
|
sseldi |
⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑏 ∈ ( 𝒫 𝐵 ∩ Fin ) ) ) ∧ 𝑦 ∈ ( 𝑎 ∪ 𝑏 ) ) → ( 𝐹 ‘ 𝑦 ) ∈ ℂ ) |
150 |
138 139 140 149
|
fsumsplit |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑏 ∈ ( 𝒫 𝐵 ∩ Fin ) ) ) → Σ 𝑦 ∈ ( 𝑎 ∪ 𝑏 ) ( 𝐹 ‘ 𝑦 ) = ( Σ 𝑦 ∈ 𝑎 ( 𝐹 ‘ 𝑦 ) + Σ 𝑦 ∈ 𝑏 ( 𝐹 ‘ 𝑦 ) ) ) |
151 |
150
|
ad2antrr |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑏 ∈ ( 𝒫 𝐵 ∩ Fin ) ) ) ∧ ( 𝑣 = Σ 𝑦 ∈ 𝑎 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ∧ 𝑢 = Σ 𝑦 ∈ 𝑏 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) ) ∧ 𝑟 = ( 𝑣 + 𝑢 ) ) → Σ 𝑦 ∈ ( 𝑎 ∪ 𝑏 ) ( 𝐹 ‘ 𝑦 ) = ( Σ 𝑦 ∈ 𝑎 ( 𝐹 ‘ 𝑦 ) + Σ 𝑦 ∈ 𝑏 ( 𝐹 ‘ 𝑦 ) ) ) |
152 |
131 132 151
|
3eqtr4d |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑏 ∈ ( 𝒫 𝐵 ∩ Fin ) ) ) ∧ ( 𝑣 = Σ 𝑦 ∈ 𝑎 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ∧ 𝑢 = Σ 𝑦 ∈ 𝑏 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) ) ∧ 𝑟 = ( 𝑣 + 𝑢 ) ) → 𝑟 = Σ 𝑦 ∈ ( 𝑎 ∪ 𝑏 ) ( 𝐹 ‘ 𝑦 ) ) |
153 |
|
sumeq1 |
⊢ ( 𝑥 = ( 𝑎 ∪ 𝑏 ) → Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) = Σ 𝑦 ∈ ( 𝑎 ∪ 𝑏 ) ( 𝐹 ‘ 𝑦 ) ) |
154 |
153
|
rspceeqv |
⊢ ( ( ( 𝑎 ∪ 𝑏 ) ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ 𝑟 = Σ 𝑦 ∈ ( 𝑎 ∪ 𝑏 ) ( 𝐹 ‘ 𝑦 ) ) → ∃ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) 𝑟 = Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) |
155 |
111 152 154
|
syl2anc |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑏 ∈ ( 𝒫 𝐵 ∩ Fin ) ) ) ∧ ( 𝑣 = Σ 𝑦 ∈ 𝑎 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ∧ 𝑢 = Σ 𝑦 ∈ 𝑏 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) ) ∧ 𝑟 = ( 𝑣 + 𝑢 ) ) → ∃ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) 𝑟 = Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) |
156 |
56
|
a1i |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑏 ∈ ( 𝒫 𝐵 ∩ Fin ) ) ) ∧ ( 𝑣 = Σ 𝑦 ∈ 𝑎 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ∧ 𝑢 = Σ 𝑦 ∈ 𝑏 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) ) ∧ 𝑟 = ( 𝑣 + 𝑢 ) ) → 𝑟 ∈ V ) |
157 |
82 155 156
|
elrnmptd |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑏 ∈ ( 𝒫 𝐵 ∩ Fin ) ) ) ∧ ( 𝑣 = Σ 𝑦 ∈ 𝑎 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ∧ 𝑢 = Σ 𝑦 ∈ 𝑏 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) ) ∧ 𝑟 = ( 𝑣 + 𝑢 ) ) → 𝑟 ∈ ran ( 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) ) |
158 |
157
|
ex |
⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑏 ∈ ( 𝒫 𝐵 ∩ Fin ) ) ) ∧ ( 𝑣 = Σ 𝑦 ∈ 𝑎 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ∧ 𝑢 = Σ 𝑦 ∈ 𝑏 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) ) → ( 𝑟 = ( 𝑣 + 𝑢 ) → 𝑟 ∈ ran ( 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) ) ) |
159 |
158
|
ex |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑏 ∈ ( 𝒫 𝐵 ∩ Fin ) ) ) → ( ( 𝑣 = Σ 𝑦 ∈ 𝑎 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ∧ 𝑢 = Σ 𝑦 ∈ 𝑏 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) → ( 𝑟 = ( 𝑣 + 𝑢 ) → 𝑟 ∈ ran ( 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) ) ) ) |
160 |
159
|
ex |
⊢ ( 𝜑 → ( ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 𝑏 ∈ ( 𝒫 𝐵 ∩ Fin ) ) → ( ( 𝑣 = Σ 𝑦 ∈ 𝑎 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ∧ 𝑢 = Σ 𝑦 ∈ 𝑏 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) → ( 𝑟 = ( 𝑣 + 𝑢 ) → 𝑟 ∈ ran ( 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) ) ) ) ) |
161 |
160
|
rexlimdvv |
⊢ ( 𝜑 → ( ∃ 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ∃ 𝑏 ∈ ( 𝒫 𝐵 ∩ Fin ) ( 𝑣 = Σ 𝑦 ∈ 𝑎 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ∧ 𝑢 = Σ 𝑦 ∈ 𝑏 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) → ( 𝑟 = ( 𝑣 + 𝑢 ) → 𝑟 ∈ ran ( 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) ) ) ) |
162 |
161
|
imp |
⊢ ( ( 𝜑 ∧ ∃ 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ∃ 𝑏 ∈ ( 𝒫 𝐵 ∩ Fin ) ( 𝑣 = Σ 𝑦 ∈ 𝑎 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ∧ 𝑢 = Σ 𝑦 ∈ 𝑏 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) ) → ( 𝑟 = ( 𝑣 + 𝑢 ) → 𝑟 ∈ ran ( 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) ) ) |
163 |
63 81 162
|
syl2anc |
⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ) ∧ 𝑢 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) ) ) → ( 𝑟 = ( 𝑣 + 𝑢 ) → 𝑟 ∈ ran ( 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) ) ) |
164 |
163
|
ex |
⊢ ( 𝜑 → ( ( 𝑣 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ) ∧ 𝑢 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) ) → ( 𝑟 = ( 𝑣 + 𝑢 ) → 𝑟 ∈ ran ( 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) ) ) ) |
165 |
164
|
rexlimdvv |
⊢ ( 𝜑 → ( ∃ 𝑣 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ) ∃ 𝑢 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) 𝑟 = ( 𝑣 + 𝑢 ) → 𝑟 ∈ ran ( 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) ) ) |
166 |
165
|
imp |
⊢ ( ( 𝜑 ∧ ∃ 𝑣 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ) ∃ 𝑢 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) 𝑟 = ( 𝑣 + 𝑢 ) ) → 𝑟 ∈ ran ( 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) ) |
167 |
55 62 166
|
syl2anc |
⊢ ( ( 𝜑 ∧ 𝑟 ∈ { 𝑧 ∣ ∃ 𝑣 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ) ∃ 𝑢 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) 𝑧 = ( 𝑣 + 𝑢 ) } ) → 𝑟 ∈ ran ( 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) ) |
168 |
167
|
ex |
⊢ ( 𝜑 → ( 𝑟 ∈ { 𝑧 ∣ ∃ 𝑣 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ) ∃ 𝑢 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) 𝑧 = ( 𝑣 + 𝑢 ) } → 𝑟 ∈ ran ( 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) ) ) |
169 |
82
|
elrnmpt |
⊢ ( 𝑟 ∈ ran ( 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) → ( 𝑟 ∈ ran ( 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) ↔ ∃ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) 𝑟 = Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) ) |
170 |
169
|
ibi |
⊢ ( 𝑟 ∈ ran ( 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) → ∃ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) 𝑟 = Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) |
171 |
170
|
adantl |
⊢ ( ( 𝜑 ∧ 𝑟 ∈ ran ( 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) ) → ∃ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) 𝑟 = Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) |
172 |
|
nfv |
⊢ Ⅎ 𝑥 𝜑 |
173 |
|
nfcv |
⊢ Ⅎ 𝑥 𝑟 |
174 |
|
nfmpt1 |
⊢ Ⅎ 𝑥 ( 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) |
175 |
174
|
nfrn |
⊢ Ⅎ 𝑥 ran ( 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) |
176 |
173 175
|
nfel |
⊢ Ⅎ 𝑥 𝑟 ∈ ran ( 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) |
177 |
172 176
|
nfan |
⊢ Ⅎ 𝑥 ( 𝜑 ∧ 𝑟 ∈ ran ( 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) ) |
178 |
|
nfmpt1 |
⊢ Ⅎ 𝑥 ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ) |
179 |
178
|
nfrn |
⊢ Ⅎ 𝑥 ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ) |
180 |
|
nfmpt1 |
⊢ Ⅎ 𝑥 ( 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) |
181 |
180
|
nfrn |
⊢ Ⅎ 𝑥 ran ( 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) |
182 |
|
nfv |
⊢ Ⅎ 𝑥 𝑟 = ( 𝑣 + 𝑢 ) |
183 |
181 182
|
nfrex |
⊢ Ⅎ 𝑥 ∃ 𝑢 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) 𝑟 = ( 𝑣 + 𝑢 ) |
184 |
179 183
|
nfrex |
⊢ Ⅎ 𝑥 ∃ 𝑣 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ) ∃ 𝑢 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) 𝑟 = ( 𝑣 + 𝑢 ) |
185 |
|
inss2 |
⊢ ( 𝑥 ∩ 𝐴 ) ⊆ 𝐴 |
186 |
185
|
sseli |
⊢ ( 𝑦 ∈ ( 𝑥 ∩ 𝐴 ) → 𝑦 ∈ 𝐴 ) |
187 |
186
|
adantl |
⊢ ( ( 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ 𝑦 ∈ ( 𝑥 ∩ 𝐴 ) ) → 𝑦 ∈ 𝐴 ) |
188 |
118
|
eqcomd |
⊢ ( 𝑦 ∈ 𝐴 → ( 𝐹 ‘ 𝑦 ) = ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ) |
189 |
187 188
|
syl |
⊢ ( ( 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ 𝑦 ∈ ( 𝑥 ∩ 𝐴 ) ) → ( 𝐹 ‘ 𝑦 ) = ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ) |
190 |
189
|
sumeq2dv |
⊢ ( 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) → Σ 𝑦 ∈ ( 𝑥 ∩ 𝐴 ) ( 𝐹 ‘ 𝑦 ) = Σ 𝑦 ∈ ( 𝑥 ∩ 𝐴 ) ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ) |
191 |
|
sumeq1 |
⊢ ( 𝑥 = 𝑧 → Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) = Σ 𝑦 ∈ 𝑧 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ) |
192 |
191
|
cbvmptv |
⊢ ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ) = ( 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑧 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ) |
193 |
|
vex |
⊢ 𝑥 ∈ V |
194 |
193
|
inex1 |
⊢ ( 𝑥 ∩ 𝐴 ) ∈ V |
195 |
194
|
elpw |
⊢ ( ( 𝑥 ∩ 𝐴 ) ∈ 𝒫 𝐴 ↔ ( 𝑥 ∩ 𝐴 ) ⊆ 𝐴 ) |
196 |
185 195
|
mpbir |
⊢ ( 𝑥 ∩ 𝐴 ) ∈ 𝒫 𝐴 |
197 |
196
|
a1i |
⊢ ( 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) → ( 𝑥 ∩ 𝐴 ) ∈ 𝒫 𝐴 ) |
198 |
|
elinel2 |
⊢ ( 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) → 𝑥 ∈ Fin ) |
199 |
|
inss1 |
⊢ ( 𝑥 ∩ 𝐴 ) ⊆ 𝑥 |
200 |
199
|
a1i |
⊢ ( 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) → ( 𝑥 ∩ 𝐴 ) ⊆ 𝑥 ) |
201 |
|
ssfi |
⊢ ( ( 𝑥 ∈ Fin ∧ ( 𝑥 ∩ 𝐴 ) ⊆ 𝑥 ) → ( 𝑥 ∩ 𝐴 ) ∈ Fin ) |
202 |
198 200 201
|
syl2anc |
⊢ ( 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) → ( 𝑥 ∩ 𝐴 ) ∈ Fin ) |
203 |
197 202
|
elind |
⊢ ( 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) → ( 𝑥 ∩ 𝐴 ) ∈ ( 𝒫 𝐴 ∩ Fin ) ) |
204 |
|
eqidd |
⊢ ( 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) → Σ 𝑦 ∈ ( 𝑥 ∩ 𝐴 ) ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) = Σ 𝑦 ∈ ( 𝑥 ∩ 𝐴 ) ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ) |
205 |
|
sumeq1 |
⊢ ( 𝑧 = ( 𝑥 ∩ 𝐴 ) → Σ 𝑦 ∈ 𝑧 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) = Σ 𝑦 ∈ ( 𝑥 ∩ 𝐴 ) ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ) |
206 |
205
|
rspceeqv |
⊢ ( ( ( 𝑥 ∩ 𝐴 ) ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ Σ 𝑦 ∈ ( 𝑥 ∩ 𝐴 ) ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) = Σ 𝑦 ∈ ( 𝑥 ∩ 𝐴 ) ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ) → ∃ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) Σ 𝑦 ∈ ( 𝑥 ∩ 𝐴 ) ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) = Σ 𝑦 ∈ 𝑧 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ) |
207 |
203 204 206
|
syl2anc |
⊢ ( 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) → ∃ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) Σ 𝑦 ∈ ( 𝑥 ∩ 𝐴 ) ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) = Σ 𝑦 ∈ 𝑧 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ) |
208 |
|
sumex |
⊢ Σ 𝑦 ∈ ( 𝑥 ∩ 𝐴 ) ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ∈ V |
209 |
208
|
a1i |
⊢ ( 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) → Σ 𝑦 ∈ ( 𝑥 ∩ 𝐴 ) ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ∈ V ) |
210 |
192 207 209
|
elrnmptd |
⊢ ( 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) → Σ 𝑦 ∈ ( 𝑥 ∩ 𝐴 ) ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ∈ ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ) ) |
211 |
190 210
|
eqeltrd |
⊢ ( 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) → Σ 𝑦 ∈ ( 𝑥 ∩ 𝐴 ) ( 𝐹 ‘ 𝑦 ) ∈ ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ) ) |
212 |
211
|
3ad2ant2 |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ 𝑟 = Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) → Σ 𝑦 ∈ ( 𝑥 ∩ 𝐴 ) ( 𝐹 ‘ 𝑦 ) ∈ ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ) ) |
213 |
|
sumeq1 |
⊢ ( 𝑥 = 𝑧 → Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) = Σ 𝑦 ∈ 𝑧 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) |
214 |
213
|
cbvmptv |
⊢ ( 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) = ( 𝑧 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑧 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) |
215 |
|
inss2 |
⊢ ( 𝑥 ∩ 𝐵 ) ⊆ 𝐵 |
216 |
193
|
inex1 |
⊢ ( 𝑥 ∩ 𝐵 ) ∈ V |
217 |
216
|
elpw |
⊢ ( ( 𝑥 ∩ 𝐵 ) ∈ 𝒫 𝐵 ↔ ( 𝑥 ∩ 𝐵 ) ⊆ 𝐵 ) |
218 |
215 217
|
mpbir |
⊢ ( 𝑥 ∩ 𝐵 ) ∈ 𝒫 𝐵 |
219 |
218
|
a1i |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ 𝑟 = Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) → ( 𝑥 ∩ 𝐵 ) ∈ 𝒫 𝐵 ) |
220 |
|
inss1 |
⊢ ( 𝑥 ∩ 𝐵 ) ⊆ 𝑥 |
221 |
220
|
a1i |
⊢ ( 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) → ( 𝑥 ∩ 𝐵 ) ⊆ 𝑥 ) |
222 |
|
ssfi |
⊢ ( ( 𝑥 ∈ Fin ∧ ( 𝑥 ∩ 𝐵 ) ⊆ 𝑥 ) → ( 𝑥 ∩ 𝐵 ) ∈ Fin ) |
223 |
198 221 222
|
syl2anc |
⊢ ( 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) → ( 𝑥 ∩ 𝐵 ) ∈ Fin ) |
224 |
223
|
3ad2ant2 |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ 𝑟 = Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) → ( 𝑥 ∩ 𝐵 ) ∈ Fin ) |
225 |
219 224
|
elind |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ 𝑟 = Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) → ( 𝑥 ∩ 𝐵 ) ∈ ( 𝒫 𝐵 ∩ Fin ) ) |
226 |
215
|
sseli |
⊢ ( 𝑦 ∈ ( 𝑥 ∩ 𝐵 ) → 𝑦 ∈ 𝐵 ) |
227 |
124
|
eqcomd |
⊢ ( 𝑦 ∈ 𝐵 → ( 𝐹 ‘ 𝑦 ) = ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) |
228 |
226 227
|
syl |
⊢ ( 𝑦 ∈ ( 𝑥 ∩ 𝐵 ) → ( 𝐹 ‘ 𝑦 ) = ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) |
229 |
228
|
sumeq2i |
⊢ Σ 𝑦 ∈ ( 𝑥 ∩ 𝐵 ) ( 𝐹 ‘ 𝑦 ) = Σ 𝑦 ∈ ( 𝑥 ∩ 𝐵 ) ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) |
230 |
229
|
a1i |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ) → Σ 𝑦 ∈ ( 𝑥 ∩ 𝐵 ) ( 𝐹 ‘ 𝑦 ) = Σ 𝑦 ∈ ( 𝑥 ∩ 𝐵 ) ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) |
231 |
230
|
3adant3 |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ 𝑟 = Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) → Σ 𝑦 ∈ ( 𝑥 ∩ 𝐵 ) ( 𝐹 ‘ 𝑦 ) = Σ 𝑦 ∈ ( 𝑥 ∩ 𝐵 ) ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) |
232 |
|
sumeq1 |
⊢ ( 𝑧 = ( 𝑥 ∩ 𝐵 ) → Σ 𝑦 ∈ 𝑧 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) = Σ 𝑦 ∈ ( 𝑥 ∩ 𝐵 ) ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) |
233 |
232
|
rspceeqv |
⊢ ( ( ( 𝑥 ∩ 𝐵 ) ∈ ( 𝒫 𝐵 ∩ Fin ) ∧ Σ 𝑦 ∈ ( 𝑥 ∩ 𝐵 ) ( 𝐹 ‘ 𝑦 ) = Σ 𝑦 ∈ ( 𝑥 ∩ 𝐵 ) ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) → ∃ 𝑧 ∈ ( 𝒫 𝐵 ∩ Fin ) Σ 𝑦 ∈ ( 𝑥 ∩ 𝐵 ) ( 𝐹 ‘ 𝑦 ) = Σ 𝑦 ∈ 𝑧 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) |
234 |
225 231 233
|
syl2anc |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ 𝑟 = Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) → ∃ 𝑧 ∈ ( 𝒫 𝐵 ∩ Fin ) Σ 𝑦 ∈ ( 𝑥 ∩ 𝐵 ) ( 𝐹 ‘ 𝑦 ) = Σ 𝑦 ∈ 𝑧 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) |
235 |
|
sumex |
⊢ Σ 𝑦 ∈ ( 𝑥 ∩ 𝐵 ) ( 𝐹 ‘ 𝑦 ) ∈ V |
236 |
235
|
a1i |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ 𝑟 = Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) → Σ 𝑦 ∈ ( 𝑥 ∩ 𝐵 ) ( 𝐹 ‘ 𝑦 ) ∈ V ) |
237 |
214 234 236
|
elrnmptd |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ 𝑟 = Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) → Σ 𝑦 ∈ ( 𝑥 ∩ 𝐵 ) ( 𝐹 ‘ 𝑦 ) ∈ ran ( 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) ) |
238 |
|
simp3 |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ 𝑟 = Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) → 𝑟 = Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) |
239 |
185
|
a1i |
⊢ ( 𝜑 → ( 𝑥 ∩ 𝐴 ) ⊆ 𝐴 ) |
240 |
215
|
a1i |
⊢ ( 𝜑 → ( 𝑥 ∩ 𝐵 ) ⊆ 𝐵 ) |
241 |
|
ssin0 |
⊢ ( ( ( 𝐴 ∩ 𝐵 ) = ∅ ∧ ( 𝑥 ∩ 𝐴 ) ⊆ 𝐴 ∧ ( 𝑥 ∩ 𝐵 ) ⊆ 𝐵 ) → ( ( 𝑥 ∩ 𝐴 ) ∩ ( 𝑥 ∩ 𝐵 ) ) = ∅ ) |
242 |
4 239 240 241
|
syl3anc |
⊢ ( 𝜑 → ( ( 𝑥 ∩ 𝐴 ) ∩ ( 𝑥 ∩ 𝐵 ) ) = ∅ ) |
243 |
242
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ) → ( ( 𝑥 ∩ 𝐴 ) ∩ ( 𝑥 ∩ 𝐵 ) ) = ∅ ) |
244 |
|
elinel1 |
⊢ ( 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) → 𝑥 ∈ 𝒫 𝑈 ) |
245 |
|
elpwi |
⊢ ( 𝑥 ∈ 𝒫 𝑈 → 𝑥 ⊆ 𝑈 ) |
246 |
244 245
|
syl |
⊢ ( 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) → 𝑥 ⊆ 𝑈 ) |
247 |
3
|
ineq2i |
⊢ ( 𝑥 ∩ 𝑈 ) = ( 𝑥 ∩ ( 𝐴 ∪ 𝐵 ) ) |
248 |
247
|
a1i |
⊢ ( 𝑥 ⊆ 𝑈 → ( 𝑥 ∩ 𝑈 ) = ( 𝑥 ∩ ( 𝐴 ∪ 𝐵 ) ) ) |
249 |
|
dfss |
⊢ ( 𝑥 ⊆ 𝑈 ↔ 𝑥 = ( 𝑥 ∩ 𝑈 ) ) |
250 |
249
|
biimpi |
⊢ ( 𝑥 ⊆ 𝑈 → 𝑥 = ( 𝑥 ∩ 𝑈 ) ) |
251 |
|
indi |
⊢ ( 𝑥 ∩ ( 𝐴 ∪ 𝐵 ) ) = ( ( 𝑥 ∩ 𝐴 ) ∪ ( 𝑥 ∩ 𝐵 ) ) |
252 |
251
|
eqcomi |
⊢ ( ( 𝑥 ∩ 𝐴 ) ∪ ( 𝑥 ∩ 𝐵 ) ) = ( 𝑥 ∩ ( 𝐴 ∪ 𝐵 ) ) |
253 |
252
|
a1i |
⊢ ( 𝑥 ⊆ 𝑈 → ( ( 𝑥 ∩ 𝐴 ) ∪ ( 𝑥 ∩ 𝐵 ) ) = ( 𝑥 ∩ ( 𝐴 ∪ 𝐵 ) ) ) |
254 |
248 250 253
|
3eqtr4d |
⊢ ( 𝑥 ⊆ 𝑈 → 𝑥 = ( ( 𝑥 ∩ 𝐴 ) ∪ ( 𝑥 ∩ 𝐵 ) ) ) |
255 |
246 254
|
syl |
⊢ ( 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) → 𝑥 = ( ( 𝑥 ∩ 𝐴 ) ∪ ( 𝑥 ∩ 𝐵 ) ) ) |
256 |
255
|
adantl |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ) → 𝑥 = ( ( 𝑥 ∩ 𝐴 ) ∪ ( 𝑥 ∩ 𝐵 ) ) ) |
257 |
198
|
adantl |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ) → 𝑥 ∈ Fin ) |
258 |
144
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ) ∧ 𝑦 ∈ 𝑥 ) → 𝐹 : 𝑈 ⟶ ( 0 [,) +∞ ) ) |
259 |
246
|
sselda |
⊢ ( ( 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ 𝑦 ∈ 𝑥 ) → 𝑦 ∈ 𝑈 ) |
260 |
259
|
adantll |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ) ∧ 𝑦 ∈ 𝑥 ) → 𝑦 ∈ 𝑈 ) |
261 |
258 260
|
ffvelrnd |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ) ∧ 𝑦 ∈ 𝑥 ) → ( 𝐹 ‘ 𝑦 ) ∈ ( 0 [,) +∞ ) ) |
262 |
143 261
|
sseldi |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ) ∧ 𝑦 ∈ 𝑥 ) → ( 𝐹 ‘ 𝑦 ) ∈ ℂ ) |
263 |
243 256 257 262
|
fsumsplit |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ) → Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) = ( Σ 𝑦 ∈ ( 𝑥 ∩ 𝐴 ) ( 𝐹 ‘ 𝑦 ) + Σ 𝑦 ∈ ( 𝑥 ∩ 𝐵 ) ( 𝐹 ‘ 𝑦 ) ) ) |
264 |
263
|
3adant3 |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ 𝑟 = Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) → Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) = ( Σ 𝑦 ∈ ( 𝑥 ∩ 𝐴 ) ( 𝐹 ‘ 𝑦 ) + Σ 𝑦 ∈ ( 𝑥 ∩ 𝐵 ) ( 𝐹 ‘ 𝑦 ) ) ) |
265 |
238 264
|
eqtrd |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ 𝑟 = Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) → 𝑟 = ( Σ 𝑦 ∈ ( 𝑥 ∩ 𝐴 ) ( 𝐹 ‘ 𝑦 ) + Σ 𝑦 ∈ ( 𝑥 ∩ 𝐵 ) ( 𝐹 ‘ 𝑦 ) ) ) |
266 |
|
oveq2 |
⊢ ( 𝑢 = Σ 𝑦 ∈ ( 𝑥 ∩ 𝐵 ) ( 𝐹 ‘ 𝑦 ) → ( Σ 𝑦 ∈ ( 𝑥 ∩ 𝐴 ) ( 𝐹 ‘ 𝑦 ) + 𝑢 ) = ( Σ 𝑦 ∈ ( 𝑥 ∩ 𝐴 ) ( 𝐹 ‘ 𝑦 ) + Σ 𝑦 ∈ ( 𝑥 ∩ 𝐵 ) ( 𝐹 ‘ 𝑦 ) ) ) |
267 |
266
|
rspceeqv |
⊢ ( ( Σ 𝑦 ∈ ( 𝑥 ∩ 𝐵 ) ( 𝐹 ‘ 𝑦 ) ∈ ran ( 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) ∧ 𝑟 = ( Σ 𝑦 ∈ ( 𝑥 ∩ 𝐴 ) ( 𝐹 ‘ 𝑦 ) + Σ 𝑦 ∈ ( 𝑥 ∩ 𝐵 ) ( 𝐹 ‘ 𝑦 ) ) ) → ∃ 𝑢 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) 𝑟 = ( Σ 𝑦 ∈ ( 𝑥 ∩ 𝐴 ) ( 𝐹 ‘ 𝑦 ) + 𝑢 ) ) |
268 |
237 265 267
|
syl2anc |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ 𝑟 = Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) → ∃ 𝑢 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) 𝑟 = ( Σ 𝑦 ∈ ( 𝑥 ∩ 𝐴 ) ( 𝐹 ‘ 𝑦 ) + 𝑢 ) ) |
269 |
|
oveq1 |
⊢ ( 𝑣 = Σ 𝑦 ∈ ( 𝑥 ∩ 𝐴 ) ( 𝐹 ‘ 𝑦 ) → ( 𝑣 + 𝑢 ) = ( Σ 𝑦 ∈ ( 𝑥 ∩ 𝐴 ) ( 𝐹 ‘ 𝑦 ) + 𝑢 ) ) |
270 |
269
|
eqeq2d |
⊢ ( 𝑣 = Σ 𝑦 ∈ ( 𝑥 ∩ 𝐴 ) ( 𝐹 ‘ 𝑦 ) → ( 𝑟 = ( 𝑣 + 𝑢 ) ↔ 𝑟 = ( Σ 𝑦 ∈ ( 𝑥 ∩ 𝐴 ) ( 𝐹 ‘ 𝑦 ) + 𝑢 ) ) ) |
271 |
270
|
rexbidv |
⊢ ( 𝑣 = Σ 𝑦 ∈ ( 𝑥 ∩ 𝐴 ) ( 𝐹 ‘ 𝑦 ) → ( ∃ 𝑢 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) 𝑟 = ( 𝑣 + 𝑢 ) ↔ ∃ 𝑢 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) 𝑟 = ( Σ 𝑦 ∈ ( 𝑥 ∩ 𝐴 ) ( 𝐹 ‘ 𝑦 ) + 𝑢 ) ) ) |
272 |
271
|
rspcev |
⊢ ( ( Σ 𝑦 ∈ ( 𝑥 ∩ 𝐴 ) ( 𝐹 ‘ 𝑦 ) ∈ ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ) ∧ ∃ 𝑢 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) 𝑟 = ( Σ 𝑦 ∈ ( 𝑥 ∩ 𝐴 ) ( 𝐹 ‘ 𝑦 ) + 𝑢 ) ) → ∃ 𝑣 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ) ∃ 𝑢 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) 𝑟 = ( 𝑣 + 𝑢 ) ) |
273 |
212 268 272
|
syl2anc |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ 𝑟 = Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) → ∃ 𝑣 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ) ∃ 𝑢 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) 𝑟 = ( 𝑣 + 𝑢 ) ) |
274 |
273
|
3exp |
⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) → ( 𝑟 = Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) → ∃ 𝑣 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ) ∃ 𝑢 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) 𝑟 = ( 𝑣 + 𝑢 ) ) ) ) |
275 |
274
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑟 ∈ ran ( 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) ) → ( 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) → ( 𝑟 = Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) → ∃ 𝑣 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ) ∃ 𝑢 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) 𝑟 = ( 𝑣 + 𝑢 ) ) ) ) |
276 |
177 184 275
|
rexlimd |
⊢ ( ( 𝜑 ∧ 𝑟 ∈ ran ( 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) ) → ( ∃ 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) 𝑟 = Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) → ∃ 𝑣 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ) ∃ 𝑢 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) 𝑟 = ( 𝑣 + 𝑢 ) ) ) |
277 |
171 276
|
mpd |
⊢ ( ( 𝜑 ∧ 𝑟 ∈ ran ( 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) ) → ∃ 𝑣 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ) ∃ 𝑢 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) 𝑟 = ( 𝑣 + 𝑢 ) ) |
278 |
277 60
|
sylibr |
⊢ ( ( 𝜑 ∧ 𝑟 ∈ ran ( 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) ) → 𝑟 ∈ { 𝑧 ∣ ∃ 𝑣 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ) ∃ 𝑢 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) 𝑧 = ( 𝑣 + 𝑢 ) } ) |
279 |
278
|
ex |
⊢ ( 𝜑 → ( 𝑟 ∈ ran ( 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) → 𝑟 ∈ { 𝑧 ∣ ∃ 𝑣 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ) ∃ 𝑢 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) 𝑧 = ( 𝑣 + 𝑢 ) } ) ) |
280 |
168 279
|
impbid |
⊢ ( 𝜑 → ( 𝑟 ∈ { 𝑧 ∣ ∃ 𝑣 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ) ∃ 𝑢 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) 𝑧 = ( 𝑣 + 𝑢 ) } ↔ 𝑟 ∈ ran ( 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) ) ) |
281 |
280
|
alrimiv |
⊢ ( 𝜑 → ∀ 𝑟 ( 𝑟 ∈ { 𝑧 ∣ ∃ 𝑣 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ) ∃ 𝑢 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) 𝑧 = ( 𝑣 + 𝑢 ) } ↔ 𝑟 ∈ ran ( 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) ) ) |
282 |
|
dfcleq |
⊢ ( { 𝑧 ∣ ∃ 𝑣 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ) ∃ 𝑢 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) 𝑧 = ( 𝑣 + 𝑢 ) } = ran ( 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) ↔ ∀ 𝑟 ( 𝑟 ∈ { 𝑧 ∣ ∃ 𝑣 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ) ∃ 𝑢 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) 𝑧 = ( 𝑣 + 𝑢 ) } ↔ 𝑟 ∈ ran ( 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) ) ) |
283 |
281 282
|
sylibr |
⊢ ( 𝜑 → { 𝑧 ∣ ∃ 𝑣 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ) ∃ 𝑢 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) 𝑧 = ( 𝑣 + 𝑢 ) } = ran ( 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) ) |
284 |
283
|
supeq1d |
⊢ ( 𝜑 → sup ( { 𝑧 ∣ ∃ 𝑣 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ) ∃ 𝑢 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) 𝑧 = ( 𝑣 + 𝑢 ) } , ℝ , < ) = sup ( ran ( 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) , ℝ , < ) ) |
285 |
27 54 284
|
3eqtrrd |
⊢ ( 𝜑 → sup ( ran ( 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) , ℝ , < ) = ( sup ( ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ) , ℝ , < ) +𝑒 sup ( ran ( 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) , ℝ , < ) ) ) |
286 |
15 5 6
|
sge0supre |
⊢ ( 𝜑 → ( Σ^ ‘ 𝐹 ) = sup ( ran ( 𝑥 ∈ ( 𝒫 𝑈 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) , ℝ , < ) ) |
287 |
17 24
|
oveq12d |
⊢ ( 𝜑 → ( ( Σ^ ‘ ( 𝐹 ↾ 𝐴 ) ) +𝑒 ( Σ^ ‘ ( 𝐹 ↾ 𝐵 ) ) ) = ( sup ( ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ) , ℝ , < ) +𝑒 sup ( ran ( 𝑥 ∈ ( 𝒫 𝐵 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑦 ) ) , ℝ , < ) ) ) |
288 |
285 286 287
|
3eqtr4d |
⊢ ( 𝜑 → ( Σ^ ‘ 𝐹 ) = ( ( Σ^ ‘ ( 𝐹 ↾ 𝐴 ) ) +𝑒 ( Σ^ ‘ ( 𝐹 ↾ 𝐵 ) ) ) ) |
289 |
|
rexadd |
⊢ ( ( ( Σ^ ‘ ( 𝐹 ↾ 𝐴 ) ) ∈ ℝ ∧ ( Σ^ ‘ ( 𝐹 ↾ 𝐵 ) ) ∈ ℝ ) → ( ( Σ^ ‘ ( 𝐹 ↾ 𝐴 ) ) +𝑒 ( Σ^ ‘ ( 𝐹 ↾ 𝐵 ) ) ) = ( ( Σ^ ‘ ( 𝐹 ↾ 𝐴 ) ) + ( Σ^ ‘ ( 𝐹 ↾ 𝐵 ) ) ) ) |
290 |
16 23 289
|
syl2anc |
⊢ ( 𝜑 → ( ( Σ^ ‘ ( 𝐹 ↾ 𝐴 ) ) +𝑒 ( Σ^ ‘ ( 𝐹 ↾ 𝐵 ) ) ) = ( ( Σ^ ‘ ( 𝐹 ↾ 𝐴 ) ) + ( Σ^ ‘ ( 𝐹 ↾ 𝐵 ) ) ) ) |
291 |
288 290
|
eqtrd |
⊢ ( 𝜑 → ( Σ^ ‘ 𝐹 ) = ( ( Σ^ ‘ ( 𝐹 ↾ 𝐴 ) ) + ( Σ^ ‘ ( 𝐹 ↾ 𝐵 ) ) ) ) |