Metamath Proof Explorer

Theorem fsumiun

Description: Sum over a disjoint indexed union. (Contributed by Mario Carneiro, 1-Jul-2015) (Revised by Mario Carneiro, 10-Dec-2016)

Ref Expression
Hypotheses fsumiun.1 ⊢ ( 𝜑 → 𝐴 ∈ Fin )
fsumiun.2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ Fin )
fsumiun.3 ⊢ ( 𝜑 → Disj 𝑥 ∈ 𝐴 𝐵 )
fsumiun.4 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ) ) → 𝐶 ∈ ℂ )
Assertion fsumiun ( 𝜑 → Σ 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 𝐶 = Σ 𝑥 ∈ 𝐴 Σ 𝑘 ∈ 𝐵 𝐶 )

Proof

Step Hyp Ref Expression
1 fsumiun.1 ⊢ ( 𝜑 → 𝐴 ∈ Fin )
2 fsumiun.2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ Fin )
3 fsumiun.3 ⊢ ( 𝜑 → Disj 𝑥 ∈ 𝐴 𝐵 )
4 fsumiun.4 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ) ) → 𝐶 ∈ ℂ )
5 ssid ⊢ 𝐴 ⊆ 𝐴
6 sseq1 ⊢ ( 𝑢 = ∅ → ( 𝑢 ⊆ 𝐴 ↔ ∅ ⊆ 𝐴 ) )
7 iuneq1 ⊢ ( 𝑢 = ∅ → ∪ 𝑥 ∈ 𝑢 𝐵 = ∪ 𝑥 ∈ ∅ 𝐵 )
8 0iun ⊢ ∪ 𝑥 ∈ ∅ 𝐵 = ∅
9 7 8 syl6eq ⊢ ( 𝑢 = ∅ → ∪ 𝑥 ∈ 𝑢 𝐵 = ∅ )
10 9 sumeq1d ⊢ ( 𝑢 = ∅ → Σ 𝑘 ∈ ∪ 𝑥 ∈ 𝑢 𝐵 𝐶 = Σ 𝑘 ∈ ∅ 𝐶 )
11 sumeq1 ⊢ ( 𝑢 = ∅ → Σ 𝑥 ∈ 𝑢 Σ 𝑘 ∈ 𝐵 𝐶 = Σ 𝑥 ∈ ∅ Σ 𝑘 ∈ 𝐵 𝐶 )
12 10 11 eqeq12d ⊢ ( 𝑢 = ∅ → ( Σ 𝑘 ∈ ∪ 𝑥 ∈ 𝑢 𝐵 𝐶 = Σ 𝑥 ∈ 𝑢 Σ 𝑘 ∈ 𝐵 𝐶 ↔ Σ 𝑘 ∈ ∅ 𝐶 = Σ 𝑥 ∈ ∅ Σ 𝑘 ∈ 𝐵 𝐶 ) )
13 6 12 imbi12d ⊢ ( 𝑢 = ∅ → ( ( 𝑢 ⊆ 𝐴 → Σ 𝑘 ∈ ∪ 𝑥 ∈ 𝑢 𝐵 𝐶 = Σ 𝑥 ∈ 𝑢 Σ 𝑘 ∈ 𝐵 𝐶 ) ↔ ( ∅ ⊆ 𝐴 → Σ 𝑘 ∈ ∅ 𝐶 = Σ 𝑥 ∈ ∅ Σ 𝑘 ∈ 𝐵 𝐶 ) ) )
14 13 imbi2d ⊢ ( 𝑢 = ∅ → ( ( 𝜑 → ( 𝑢 ⊆ 𝐴 → Σ 𝑘 ∈ ∪ 𝑥 ∈ 𝑢 𝐵 𝐶 = Σ 𝑥 ∈ 𝑢 Σ 𝑘 ∈ 𝐵 𝐶 ) ) ↔ ( 𝜑 → ( ∅ ⊆ 𝐴 → Σ 𝑘 ∈ ∅ 𝐶 = Σ 𝑥 ∈ ∅ Σ 𝑘 ∈ 𝐵 𝐶 ) ) ) )
15 sseq1 ⊢ ( 𝑢 = 𝑧 → ( 𝑢 ⊆ 𝐴 ↔ 𝑧 ⊆ 𝐴 ) )
16 iuneq1 ⊢ ( 𝑢 = 𝑧 → ∪ 𝑥 ∈ 𝑢 𝐵 = ∪ 𝑥 ∈ 𝑧 𝐵 )
17 16 sumeq1d ⊢ ( 𝑢 = 𝑧 → Σ 𝑘 ∈ ∪ 𝑥 ∈ 𝑢 𝐵 𝐶 = Σ 𝑘 ∈ ∪ 𝑥 ∈ 𝑧 𝐵 𝐶 )
18 sumeq1 ⊢ ( 𝑢 = 𝑧 → Σ 𝑥 ∈ 𝑢 Σ 𝑘 ∈ 𝐵 𝐶 = Σ 𝑥 ∈ 𝑧 Σ 𝑘 ∈ 𝐵 𝐶 )
19 17 18 eqeq12d ⊢ ( 𝑢 = 𝑧 → ( Σ 𝑘 ∈ ∪ 𝑥 ∈ 𝑢 𝐵 𝐶 = Σ 𝑥 ∈ 𝑢 Σ 𝑘 ∈ 𝐵 𝐶 ↔ Σ 𝑘 ∈ ∪ 𝑥 ∈ 𝑧 𝐵 𝐶 = Σ 𝑥 ∈ 𝑧 Σ 𝑘 ∈ 𝐵 𝐶 ) )
20 15 19 imbi12d ⊢ ( 𝑢 = 𝑧 → ( ( 𝑢 ⊆ 𝐴 → Σ 𝑘 ∈ ∪ 𝑥 ∈ 𝑢 𝐵 𝐶 = Σ 𝑥 ∈ 𝑢 Σ 𝑘 ∈ 𝐵 𝐶 ) ↔ ( 𝑧 ⊆ 𝐴 → Σ 𝑘 ∈ ∪ 𝑥 ∈ 𝑧 𝐵 𝐶 = Σ 𝑥 ∈ 𝑧 Σ 𝑘 ∈ 𝐵 𝐶 ) ) )
21 20 imbi2d ⊢ ( 𝑢 = 𝑧 → ( ( 𝜑 → ( 𝑢 ⊆ 𝐴 → Σ 𝑘 ∈ ∪ 𝑥 ∈ 𝑢 𝐵 𝐶 = Σ 𝑥 ∈ 𝑢 Σ 𝑘 ∈ 𝐵 𝐶 ) ) ↔ ( 𝜑 → ( 𝑧 ⊆ 𝐴 → Σ 𝑘 ∈ ∪ 𝑥 ∈ 𝑧 𝐵 𝐶 = Σ 𝑥 ∈ 𝑧 Σ 𝑘 ∈ 𝐵 𝐶 ) ) ) )
22 sseq1 ⊢ ( 𝑢 = ( 𝑧 ∪ { 𝑤 } ) → ( 𝑢 ⊆ 𝐴 ↔ ( 𝑧 ∪ { 𝑤 } ) ⊆ 𝐴 ) )
23 iuneq1 ⊢ ( 𝑢 = ( 𝑧 ∪ { 𝑤 } ) → ∪ 𝑥 ∈ 𝑢 𝐵 = ∪ 𝑥 ∈ ( 𝑧 ∪ { 𝑤 } ) 𝐵 )
24 23 sumeq1d ⊢ ( 𝑢 = ( 𝑧 ∪ { 𝑤 } ) → Σ 𝑘 ∈ ∪ 𝑥 ∈ 𝑢 𝐵 𝐶 = Σ 𝑘 ∈ ∪ 𝑥 ∈ ( 𝑧 ∪ { 𝑤 } ) 𝐵 𝐶 )
25 sumeq1 ⊢ ( 𝑢 = ( 𝑧 ∪ { 𝑤 } ) → Σ 𝑥 ∈ 𝑢 Σ 𝑘 ∈ 𝐵 𝐶 = Σ 𝑥 ∈ ( 𝑧 ∪ { 𝑤 } ) Σ 𝑘 ∈ 𝐵 𝐶 )
26 24 25 eqeq12d ⊢ ( 𝑢 = ( 𝑧 ∪ { 𝑤 } ) → ( Σ 𝑘 ∈ ∪ 𝑥 ∈ 𝑢 𝐵 𝐶 = Σ 𝑥 ∈ 𝑢 Σ 𝑘 ∈ 𝐵 𝐶 ↔ Σ 𝑘 ∈ ∪ 𝑥 ∈ ( 𝑧 ∪ { 𝑤 } ) 𝐵 𝐶 = Σ 𝑥 ∈ ( 𝑧 ∪ { 𝑤 } ) Σ 𝑘 ∈ 𝐵 𝐶 ) )
27 22 26 imbi12d ⊢ ( 𝑢 = ( 𝑧 ∪ { 𝑤 } ) → ( ( 𝑢 ⊆ 𝐴 → Σ 𝑘 ∈ ∪ 𝑥 ∈ 𝑢 𝐵 𝐶 = Σ 𝑥 ∈ 𝑢 Σ 𝑘 ∈ 𝐵 𝐶 ) ↔ ( ( 𝑧 ∪ { 𝑤 } ) ⊆ 𝐴 → Σ 𝑘 ∈ ∪ 𝑥 ∈ ( 𝑧 ∪ { 𝑤 } ) 𝐵 𝐶 = Σ 𝑥 ∈ ( 𝑧 ∪ { 𝑤 } ) Σ 𝑘 ∈ 𝐵 𝐶 ) ) )
28 27 imbi2d ⊢ ( 𝑢 = ( 𝑧 ∪ { 𝑤 } ) → ( ( 𝜑 → ( 𝑢 ⊆ 𝐴 → Σ 𝑘 ∈ ∪ 𝑥 ∈ 𝑢 𝐵 𝐶 = Σ 𝑥 ∈ 𝑢 Σ 𝑘 ∈ 𝐵 𝐶 ) ) ↔ ( 𝜑 → ( ( 𝑧 ∪ { 𝑤 } ) ⊆ 𝐴 → Σ 𝑘 ∈ ∪ 𝑥 ∈ ( 𝑧 ∪ { 𝑤 } ) 𝐵 𝐶 = Σ 𝑥 ∈ ( 𝑧 ∪ { 𝑤 } ) Σ 𝑘 ∈ 𝐵 𝐶 ) ) ) )
29 sseq1 ⊢ ( 𝑢 = 𝐴 → ( 𝑢 ⊆ 𝐴 ↔ 𝐴 ⊆ 𝐴 ) )
30 iuneq1 ⊢ ( 𝑢 = 𝐴 → ∪ 𝑥 ∈ 𝑢 𝐵 = ∪ 𝑥 ∈ 𝐴 𝐵 )
31 30 sumeq1d ⊢ ( 𝑢 = 𝐴 → Σ 𝑘 ∈ ∪ 𝑥 ∈ 𝑢 𝐵 𝐶 = Σ 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 𝐶 )
32 sumeq1 ⊢ ( 𝑢 = 𝐴 → Σ 𝑥 ∈ 𝑢 Σ 𝑘 ∈ 𝐵 𝐶 = Σ 𝑥 ∈ 𝐴 Σ 𝑘 ∈ 𝐵 𝐶 )
33 31 32 eqeq12d ⊢ ( 𝑢 = 𝐴 → ( Σ 𝑘 ∈ ∪ 𝑥 ∈ 𝑢 𝐵 𝐶 = Σ 𝑥 ∈ 𝑢 Σ 𝑘 ∈ 𝐵 𝐶 ↔ Σ 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 𝐶 = Σ 𝑥 ∈ 𝐴 Σ 𝑘 ∈ 𝐵 𝐶 ) )
34 29 33 imbi12d ⊢ ( 𝑢 = 𝐴 → ( ( 𝑢 ⊆ 𝐴 → Σ 𝑘 ∈ ∪ 𝑥 ∈ 𝑢 𝐵 𝐶 = Σ 𝑥 ∈ 𝑢 Σ 𝑘 ∈ 𝐵 𝐶 ) ↔ ( 𝐴 ⊆ 𝐴 → Σ 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 𝐶 = Σ 𝑥 ∈ 𝐴 Σ 𝑘 ∈ 𝐵 𝐶 ) ) )
35 34 imbi2d ⊢ ( 𝑢 = 𝐴 → ( ( 𝜑 → ( 𝑢 ⊆ 𝐴 → Σ 𝑘 ∈ ∪ 𝑥 ∈ 𝑢 𝐵 𝐶 = Σ 𝑥 ∈ 𝑢 Σ 𝑘 ∈ 𝐵 𝐶 ) ) ↔ ( 𝜑 → ( 𝐴 ⊆ 𝐴 → Σ 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 𝐶 = Σ 𝑥 ∈ 𝐴 Σ 𝑘 ∈ 𝐵 𝐶 ) ) ) )
36 sum0 ⊢ Σ 𝑘 ∈ ∅ 𝐶 = 0
37 sum0 ⊢ Σ 𝑥 ∈ ∅ Σ 𝑘 ∈ 𝐵 𝐶 = 0
38 36 37 eqtr4i ⊢ Σ 𝑘 ∈ ∅ 𝐶 = Σ 𝑥 ∈ ∅ Σ 𝑘 ∈ 𝐵 𝐶
39 38 2a1i ⊢ ( 𝜑 → ( ∅ ⊆ 𝐴 → Σ 𝑘 ∈ ∅ 𝐶 = Σ 𝑥 ∈ ∅ Σ 𝑘 ∈ 𝐵 𝐶 ) )
40 id ⊢ ( ( 𝑧 ∪ { 𝑤 } ) ⊆ 𝐴 → ( 𝑧 ∪ { 𝑤 } ) ⊆ 𝐴 )
41 40 unssad ⊢ ( ( 𝑧 ∪ { 𝑤 } ) ⊆ 𝐴 → 𝑧 ⊆ 𝐴 )
42 41 imim1i ⊢ ( ( 𝑧 ⊆ 𝐴 → Σ 𝑘 ∈ ∪ 𝑥 ∈ 𝑧 𝐵 𝐶 = Σ 𝑥 ∈ 𝑧 Σ 𝑘 ∈ 𝐵 𝐶 ) → ( ( 𝑧 ∪ { 𝑤 } ) ⊆ 𝐴 → Σ 𝑘 ∈ ∪ 𝑥 ∈ 𝑧 𝐵 𝐶 = Σ 𝑥 ∈ 𝑧 Σ 𝑘 ∈ 𝐵 𝐶 ) )
43 oveq1 ⊢ ( Σ 𝑘 ∈ ∪ 𝑥 ∈ 𝑧 𝐵 𝐶 = Σ 𝑥 ∈ 𝑧 Σ 𝑘 ∈ 𝐵 𝐶 → ( Σ 𝑘 ∈ ∪ 𝑥 ∈ 𝑧 𝐵 𝐶 + Σ 𝑘 ∈ ⦋ 𝑤 / 𝑥 ⦌ 𝐵 𝐶 ) = ( Σ 𝑥 ∈ 𝑧 Σ 𝑘 ∈ 𝐵 𝐶 + Σ 𝑘 ∈ ⦋ 𝑤 / 𝑥 ⦌ 𝐵 𝐶 ) )
44 nfcv ⊢ Ⅎ 𝑧 𝐵
45 nfcsb1v ⊢ Ⅎ 𝑥 ⦋ 𝑧 / 𝑥 ⦌ 𝐵
46 csbeq1a ⊢ ( 𝑥 = 𝑧 → 𝐵 = ⦋ 𝑧 / 𝑥 ⦌ 𝐵 )
47 44 45 46 cbviun ⊢ ∪ 𝑥 ∈ { 𝑤 } 𝐵 = ∪ 𝑧 ∈ { 𝑤 } ⦋ 𝑧 / 𝑥 ⦌ 𝐵
48 vex ⊢ 𝑤 ∈ V
49 csbeq1 ⊢ ( 𝑧 = 𝑤 → ⦋ 𝑧 / 𝑥 ⦌ 𝐵 = ⦋ 𝑤 / 𝑥 ⦌ 𝐵 )
50 48 49 iunxsn ⊢ ∪ 𝑧 ∈ { 𝑤 } ⦋ 𝑧 / 𝑥 ⦌ 𝐵 = ⦋ 𝑤 / 𝑥 ⦌ 𝐵
51 47 50 eqtri ⊢ ∪ 𝑥 ∈ { 𝑤 } 𝐵 = ⦋ 𝑤 / 𝑥 ⦌ 𝐵
52 51 ineq2i ⊢ ( ∪ 𝑥 ∈ 𝑧 𝐵 ∩ ∪ 𝑥 ∈ { 𝑤 } 𝐵 ) = ( ∪ 𝑥 ∈ 𝑧 𝐵 ∩ ⦋ 𝑤 / 𝑥 ⦌ 𝐵 )
53 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑤 ∈ 𝑧 ) ∧ ( 𝑧 ∪ { 𝑤 } ) ⊆ 𝐴 ) → Disj 𝑥 ∈ 𝐴 𝐵 )
54 41 adantl ⊢ ( ( ( 𝜑 ∧ ¬ 𝑤 ∈ 𝑧 ) ∧ ( 𝑧 ∪ { 𝑤 } ) ⊆ 𝐴 ) → 𝑧 ⊆ 𝐴 )
55 simpr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑤 ∈ 𝑧 ) ∧ ( 𝑧 ∪ { 𝑤 } ) ⊆ 𝐴 ) → ( 𝑧 ∪ { 𝑤 } ) ⊆ 𝐴 )
56 55 unssbd ⊢ ( ( ( 𝜑 ∧ ¬ 𝑤 ∈ 𝑧 ) ∧ ( 𝑧 ∪ { 𝑤 } ) ⊆ 𝐴 ) → { 𝑤 } ⊆ 𝐴 )
57 simplr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑤 ∈ 𝑧 ) ∧ ( 𝑧 ∪ { 𝑤 } ) ⊆ 𝐴 ) → ¬ 𝑤 ∈ 𝑧 )
58 disjsn ⊢ ( ( 𝑧 ∩ { 𝑤 } ) = ∅ ↔ ¬ 𝑤 ∈ 𝑧 )
59 57 58 sylibr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑤 ∈ 𝑧 ) ∧ ( 𝑧 ∪ { 𝑤 } ) ⊆ 𝐴 ) → ( 𝑧 ∩ { 𝑤 } ) = ∅ )
60 disjiun ⊢ ( ( Disj 𝑥 ∈ 𝐴 𝐵 ∧ ( 𝑧 ⊆ 𝐴 ∧ { 𝑤 } ⊆ 𝐴 ∧ ( 𝑧 ∩ { 𝑤 } ) = ∅ ) ) → ( ∪ 𝑥 ∈ 𝑧 𝐵 ∩ ∪ 𝑥 ∈ { 𝑤 } 𝐵 ) = ∅ )
61 53 54 56 59 60 syl13anc ⊢ ( ( ( 𝜑 ∧ ¬ 𝑤 ∈ 𝑧 ) ∧ ( 𝑧 ∪ { 𝑤 } ) ⊆ 𝐴 ) → ( ∪ 𝑥 ∈ 𝑧 𝐵 ∩ ∪ 𝑥 ∈ { 𝑤 } 𝐵 ) = ∅ )
62 52 61 syl5eqr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑤 ∈ 𝑧 ) ∧ ( 𝑧 ∪ { 𝑤 } ) ⊆ 𝐴 ) → ( ∪ 𝑥 ∈ 𝑧 𝐵 ∩ ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ) = ∅ )
63 iunxun ⊢ ∪ 𝑥 ∈ ( 𝑧 ∪ { 𝑤 } ) 𝐵 = ( ∪ 𝑥 ∈ 𝑧 𝐵 ∪ ∪ 𝑥 ∈ { 𝑤 } 𝐵 )
64 51 uneq2i ⊢ ( ∪ 𝑥 ∈ 𝑧 𝐵 ∪ ∪ 𝑥 ∈ { 𝑤 } 𝐵 ) = ( ∪ 𝑥 ∈ 𝑧 𝐵 ∪ ⦋ 𝑤 / 𝑥 ⦌ 𝐵 )
65 63 64 eqtri ⊢ ∪ 𝑥 ∈ ( 𝑧 ∪ { 𝑤 } ) 𝐵 = ( ∪ 𝑥 ∈ 𝑧 𝐵 ∪ ⦋ 𝑤 / 𝑥 ⦌ 𝐵 )
66 65 a1i ⊢ ( ( ( 𝜑 ∧ ¬ 𝑤 ∈ 𝑧 ) ∧ ( 𝑧 ∪ { 𝑤 } ) ⊆ 𝐴 ) → ∪ 𝑥 ∈ ( 𝑧 ∪ { 𝑤 } ) 𝐵 = ( ∪ 𝑥 ∈ 𝑧 𝐵 ∪ ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ) )
67 1 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑤 ∈ 𝑧 ) ∧ ( 𝑧 ∪ { 𝑤 } ) ⊆ 𝐴 ) → 𝐴 ∈ Fin )
68 67 55 ssfid ⊢ ( ( ( 𝜑 ∧ ¬ 𝑤 ∈ 𝑧 ) ∧ ( 𝑧 ∪ { 𝑤 } ) ⊆ 𝐴 ) → ( 𝑧 ∪ { 𝑤 } ) ∈ Fin )
69 2 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 𝐵 ∈ Fin )
70 69 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑤 ∈ 𝑧 ) ∧ ( 𝑧 ∪ { 𝑤 } ) ⊆ 𝐴 ) → ∀ 𝑥 ∈ 𝐴 𝐵 ∈ Fin )
71 ssralv ⊢ ( ( 𝑧 ∪ { 𝑤 } ) ⊆ 𝐴 → ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ Fin → ∀ 𝑥 ∈ ( 𝑧 ∪ { 𝑤 } ) 𝐵 ∈ Fin ) )
72 55 70 71 sylc ⊢ ( ( ( 𝜑 ∧ ¬ 𝑤 ∈ 𝑧 ) ∧ ( 𝑧 ∪ { 𝑤 } ) ⊆ 𝐴 ) → ∀ 𝑥 ∈ ( 𝑧 ∪ { 𝑤 } ) 𝐵 ∈ Fin )
73 iunfi ⊢ ( ( ( 𝑧 ∪ { 𝑤 } ) ∈ Fin ∧ ∀ 𝑥 ∈ ( 𝑧 ∪ { 𝑤 } ) 𝐵 ∈ Fin ) → ∪ 𝑥 ∈ ( 𝑧 ∪ { 𝑤 } ) 𝐵 ∈ Fin )
74 68 72 73 syl2anc ⊢ ( ( ( 𝜑 ∧ ¬ 𝑤 ∈ 𝑧 ) ∧ ( 𝑧 ∪ { 𝑤 } ) ⊆ 𝐴 ) → ∪ 𝑥 ∈ ( 𝑧 ∪ { 𝑤 } ) 𝐵 ∈ Fin )
75 iunss1 ⊢ ( ( 𝑧 ∪ { 𝑤 } ) ⊆ 𝐴 → ∪ 𝑥 ∈ ( 𝑧 ∪ { 𝑤 } ) 𝐵 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 )
76 75 adantl ⊢ ( ( ( 𝜑 ∧ ¬ 𝑤 ∈ 𝑧 ) ∧ ( 𝑧 ∪ { 𝑤 } ) ⊆ 𝐴 ) → ∪ 𝑥 ∈ ( 𝑧 ∪ { 𝑤 } ) 𝐵 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 )
77 76 sselda ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑤 ∈ 𝑧 ) ∧ ( 𝑧 ∪ { 𝑤 } ) ⊆ 𝐴 ) ∧ 𝑘 ∈ ∪ 𝑥 ∈ ( 𝑧 ∪ { 𝑤 } ) 𝐵 ) → 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 )
78 eliun ⊢ ( 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∃ 𝑥 ∈ 𝐴 𝑘 ∈ 𝐵 )
79 4 rexlimdvaa ⊢ ( 𝜑 → ( ∃ 𝑥 ∈ 𝐴 𝑘 ∈ 𝐵 → 𝐶 ∈ ℂ ) )
80 79 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑤 ∈ 𝑧 ) ∧ ( 𝑧 ∪ { 𝑤 } ) ⊆ 𝐴 ) → ( ∃ 𝑥 ∈ 𝐴 𝑘 ∈ 𝐵 → 𝐶 ∈ ℂ ) )
81 78 80 syl5bi ⊢ ( ( ( 𝜑 ∧ ¬ 𝑤 ∈ 𝑧 ) ∧ ( 𝑧 ∪ { 𝑤 } ) ⊆ 𝐴 ) → ( 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 → 𝐶 ∈ ℂ ) )
82 81 imp ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑤 ∈ 𝑧 ) ∧ ( 𝑧 ∪ { 𝑤 } ) ⊆ 𝐴 ) ∧ 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) → 𝐶 ∈ ℂ )
83 77 82 syldan ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑤 ∈ 𝑧 ) ∧ ( 𝑧 ∪ { 𝑤 } ) ⊆ 𝐴 ) ∧ 𝑘 ∈ ∪ 𝑥 ∈ ( 𝑧 ∪ { 𝑤 } ) 𝐵 ) → 𝐶 ∈ ℂ )
84 62 66 74 83 fsumsplit ⊢ ( ( ( 𝜑 ∧ ¬ 𝑤 ∈ 𝑧 ) ∧ ( 𝑧 ∪ { 𝑤 } ) ⊆ 𝐴 ) → Σ 𝑘 ∈ ∪ 𝑥 ∈ ( 𝑧 ∪ { 𝑤 } ) 𝐵 𝐶 = ( Σ 𝑘 ∈ ∪ 𝑥 ∈ 𝑧 𝐵 𝐶 + Σ 𝑘 ∈ ⦋ 𝑤 / 𝑥 ⦌ 𝐵 𝐶 ) )
85 eqidd ⊢ ( ( ( 𝜑 ∧ ¬ 𝑤 ∈ 𝑧 ) ∧ ( 𝑧 ∪ { 𝑤 } ) ⊆ 𝐴 ) → ( 𝑧 ∪ { 𝑤 } ) = ( 𝑧 ∪ { 𝑤 } ) )
86 55 sselda ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑤 ∈ 𝑧 ) ∧ ( 𝑧 ∪ { 𝑤 } ) ⊆ 𝐴 ) ∧ 𝑥 ∈ ( 𝑧 ∪ { 𝑤 } ) ) → 𝑥 ∈ 𝐴 )
87 4 anassrs ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑘 ∈ 𝐵 ) → 𝐶 ∈ ℂ )
88 2 87 fsumcl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → Σ 𝑘 ∈ 𝐵 𝐶 ∈ ℂ )
89 88 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 Σ 𝑘 ∈ 𝐵 𝐶 ∈ ℂ )
90 89 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑤 ∈ 𝑧 ) ∧ ( 𝑧 ∪ { 𝑤 } ) ⊆ 𝐴 ) → ∀ 𝑥 ∈ 𝐴 Σ 𝑘 ∈ 𝐵 𝐶 ∈ ℂ )
91 90 r19.21bi ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑤 ∈ 𝑧 ) ∧ ( 𝑧 ∪ { 𝑤 } ) ⊆ 𝐴 ) ∧ 𝑥 ∈ 𝐴 ) → Σ 𝑘 ∈ 𝐵 𝐶 ∈ ℂ )
92 86 91 syldan ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑤 ∈ 𝑧 ) ∧ ( 𝑧 ∪ { 𝑤 } ) ⊆ 𝐴 ) ∧ 𝑥 ∈ ( 𝑧 ∪ { 𝑤 } ) ) → Σ 𝑘 ∈ 𝐵 𝐶 ∈ ℂ )
93 59 85 68 92 fsumsplit ⊢ ( ( ( 𝜑 ∧ ¬ 𝑤 ∈ 𝑧 ) ∧ ( 𝑧 ∪ { 𝑤 } ) ⊆ 𝐴 ) → Σ 𝑥 ∈ ( 𝑧 ∪ { 𝑤 } ) Σ 𝑘 ∈ 𝐵 𝐶 = ( Σ 𝑥 ∈ 𝑧 Σ 𝑘 ∈ 𝐵 𝐶 + Σ 𝑥 ∈ { 𝑤 } Σ 𝑘 ∈ 𝐵 𝐶 ) )
94 nfcv ⊢ Ⅎ 𝑧 Σ 𝑘 ∈ 𝐵 𝐶
95 nfcv ⊢ Ⅎ 𝑥 𝐶
96 45 95 nfsumw ⊢ Ⅎ 𝑥 Σ 𝑘 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 𝐶
97 46 sumeq1d ⊢ ( 𝑥 = 𝑧 → Σ 𝑘 ∈ 𝐵 𝐶 = Σ 𝑘 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 𝐶 )
98 94 96 97 cbvsumi ⊢ Σ 𝑥 ∈ { 𝑤 } Σ 𝑘 ∈ 𝐵 𝐶 = Σ 𝑧 ∈ { 𝑤 } Σ 𝑘 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 𝐶
99 48 snss ⊢ ( 𝑤 ∈ 𝐴 ↔ { 𝑤 } ⊆ 𝐴 )
100 56 99 sylibr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑤 ∈ 𝑧 ) ∧ ( 𝑧 ∪ { 𝑤 } ) ⊆ 𝐴 ) → 𝑤 ∈ 𝐴 )
101 nfcsb1v ⊢ Ⅎ 𝑥 ⦋ 𝑤 / 𝑥 ⦌ 𝐵
102 101 95 nfsumw ⊢ Ⅎ 𝑥 Σ 𝑘 ∈ ⦋ 𝑤 / 𝑥 ⦌ 𝐵 𝐶
103 102 nfel1 ⊢ Ⅎ 𝑥 Σ 𝑘 ∈ ⦋ 𝑤 / 𝑥 ⦌ 𝐵 𝐶 ∈ ℂ
104 csbeq1a ⊢ ( 𝑥 = 𝑤 → 𝐵 = ⦋ 𝑤 / 𝑥 ⦌ 𝐵 )
105 104 sumeq1d ⊢ ( 𝑥 = 𝑤 → Σ 𝑘 ∈ 𝐵 𝐶 = Σ 𝑘 ∈ ⦋ 𝑤 / 𝑥 ⦌ 𝐵 𝐶 )
106 105 eleq1d ⊢ ( 𝑥 = 𝑤 → ( Σ 𝑘 ∈ 𝐵 𝐶 ∈ ℂ ↔ Σ 𝑘 ∈ ⦋ 𝑤 / 𝑥 ⦌ 𝐵 𝐶 ∈ ℂ ) )
107 103 106 rspc ⊢ ( 𝑤 ∈ 𝐴 → ( ∀ 𝑥 ∈ 𝐴 Σ 𝑘 ∈ 𝐵 𝐶 ∈ ℂ → Σ 𝑘 ∈ ⦋ 𝑤 / 𝑥 ⦌ 𝐵 𝐶 ∈ ℂ ) )
108 100 90 107 sylc ⊢ ( ( ( 𝜑 ∧ ¬ 𝑤 ∈ 𝑧 ) ∧ ( 𝑧 ∪ { 𝑤 } ) ⊆ 𝐴 ) → Σ 𝑘 ∈ ⦋ 𝑤 / 𝑥 ⦌ 𝐵 𝐶 ∈ ℂ )
109 49 sumeq1d ⊢ ( 𝑧 = 𝑤 → Σ 𝑘 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 𝐶 = Σ 𝑘 ∈ ⦋ 𝑤 / 𝑥 ⦌ 𝐵 𝐶 )
110 109 sumsn ⊢ ( ( 𝑤 ∈ V ∧ Σ 𝑘 ∈ ⦋ 𝑤 / 𝑥 ⦌ 𝐵 𝐶 ∈ ℂ ) → Σ 𝑧 ∈ { 𝑤 } Σ 𝑘 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 𝐶 = Σ 𝑘 ∈ ⦋ 𝑤 / 𝑥 ⦌ 𝐵 𝐶 )
111 48 108 110 sylancr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑤 ∈ 𝑧 ) ∧ ( 𝑧 ∪ { 𝑤 } ) ⊆ 𝐴 ) → Σ 𝑧 ∈ { 𝑤 } Σ 𝑘 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 𝐶 = Σ 𝑘 ∈ ⦋ 𝑤 / 𝑥 ⦌ 𝐵 𝐶 )
112 98 111 syl5eq ⊢ ( ( ( 𝜑 ∧ ¬ 𝑤 ∈ 𝑧 ) ∧ ( 𝑧 ∪ { 𝑤 } ) ⊆ 𝐴 ) → Σ 𝑥 ∈ { 𝑤 } Σ 𝑘 ∈ 𝐵 𝐶 = Σ 𝑘 ∈ ⦋ 𝑤 / 𝑥 ⦌ 𝐵 𝐶 )
113 112 oveq2d ⊢ ( ( ( 𝜑 ∧ ¬ 𝑤 ∈ 𝑧 ) ∧ ( 𝑧 ∪ { 𝑤 } ) ⊆ 𝐴 ) → ( Σ 𝑥 ∈ 𝑧 Σ 𝑘 ∈ 𝐵 𝐶 + Σ 𝑥 ∈ { 𝑤 } Σ 𝑘 ∈ 𝐵 𝐶 ) = ( Σ 𝑥 ∈ 𝑧 Σ 𝑘 ∈ 𝐵 𝐶 + Σ 𝑘 ∈ ⦋ 𝑤 / 𝑥 ⦌ 𝐵 𝐶 ) )
114 93 113 eqtrd ⊢ ( ( ( 𝜑 ∧ ¬ 𝑤 ∈ 𝑧 ) ∧ ( 𝑧 ∪ { 𝑤 } ) ⊆ 𝐴 ) → Σ 𝑥 ∈ ( 𝑧 ∪ { 𝑤 } ) Σ 𝑘 ∈ 𝐵 𝐶 = ( Σ 𝑥 ∈ 𝑧 Σ 𝑘 ∈ 𝐵 𝐶 + Σ 𝑘 ∈ ⦋ 𝑤 / 𝑥 ⦌ 𝐵 𝐶 ) )
115 84 114 eqeq12d ⊢ ( ( ( 𝜑 ∧ ¬ 𝑤 ∈ 𝑧 ) ∧ ( 𝑧 ∪ { 𝑤 } ) ⊆ 𝐴 ) → ( Σ 𝑘 ∈ ∪ 𝑥 ∈ ( 𝑧 ∪ { 𝑤 } ) 𝐵 𝐶 = Σ 𝑥 ∈ ( 𝑧 ∪ { 𝑤 } ) Σ 𝑘 ∈ 𝐵 𝐶 ↔ ( Σ 𝑘 ∈ ∪ 𝑥 ∈ 𝑧 𝐵 𝐶 + Σ 𝑘 ∈ ⦋ 𝑤 / 𝑥 ⦌ 𝐵 𝐶 ) = ( Σ 𝑥 ∈ 𝑧 Σ 𝑘 ∈ 𝐵 𝐶 + Σ 𝑘 ∈ ⦋ 𝑤 / 𝑥 ⦌ 𝐵 𝐶 ) ) )
116 43 115 syl5ibr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑤 ∈ 𝑧 ) ∧ ( 𝑧 ∪ { 𝑤 } ) ⊆ 𝐴 ) → ( Σ 𝑘 ∈ ∪ 𝑥 ∈ 𝑧 𝐵 𝐶 = Σ 𝑥 ∈ 𝑧 Σ 𝑘 ∈ 𝐵 𝐶 → Σ 𝑘 ∈ ∪ 𝑥 ∈ ( 𝑧 ∪ { 𝑤 } ) 𝐵 𝐶 = Σ 𝑥 ∈ ( 𝑧 ∪ { 𝑤 } ) Σ 𝑘 ∈ 𝐵 𝐶 ) )
117 116 ex ⊢ ( ( 𝜑 ∧ ¬ 𝑤 ∈ 𝑧 ) → ( ( 𝑧 ∪ { 𝑤 } ) ⊆ 𝐴 → ( Σ 𝑘 ∈ ∪ 𝑥 ∈ 𝑧 𝐵 𝐶 = Σ 𝑥 ∈ 𝑧 Σ 𝑘 ∈ 𝐵 𝐶 → Σ 𝑘 ∈ ∪ 𝑥 ∈ ( 𝑧 ∪ { 𝑤 } ) 𝐵 𝐶 = Σ 𝑥 ∈ ( 𝑧 ∪ { 𝑤 } ) Σ 𝑘 ∈ 𝐵 𝐶 ) ) )
118 117 a2d ⊢ ( ( 𝜑 ∧ ¬ 𝑤 ∈ 𝑧 ) → ( ( ( 𝑧 ∪ { 𝑤 } ) ⊆ 𝐴 → Σ 𝑘 ∈ ∪ 𝑥 ∈ 𝑧 𝐵 𝐶 = Σ 𝑥 ∈ 𝑧 Σ 𝑘 ∈ 𝐵 𝐶 ) → ( ( 𝑧 ∪ { 𝑤 } ) ⊆ 𝐴 → Σ 𝑘 ∈ ∪ 𝑥 ∈ ( 𝑧 ∪ { 𝑤 } ) 𝐵 𝐶 = Σ 𝑥 ∈ ( 𝑧 ∪ { 𝑤 } ) Σ 𝑘 ∈ 𝐵 𝐶 ) ) )
119 42 118 syl5 ⊢ ( ( 𝜑 ∧ ¬ 𝑤 ∈ 𝑧 ) → ( ( 𝑧 ⊆ 𝐴 → Σ 𝑘 ∈ ∪ 𝑥 ∈ 𝑧 𝐵 𝐶 = Σ 𝑥 ∈ 𝑧 Σ 𝑘 ∈ 𝐵 𝐶 ) → ( ( 𝑧 ∪ { 𝑤 } ) ⊆ 𝐴 → Σ 𝑘 ∈ ∪ 𝑥 ∈ ( 𝑧 ∪ { 𝑤 } ) 𝐵 𝐶 = Σ 𝑥 ∈ ( 𝑧 ∪ { 𝑤 } ) Σ 𝑘 ∈ 𝐵 𝐶 ) ) )
120 119 expcom ⊢ ( ¬ 𝑤 ∈ 𝑧 → ( 𝜑 → ( ( 𝑧 ⊆ 𝐴 → Σ 𝑘 ∈ ∪ 𝑥 ∈ 𝑧 𝐵 𝐶 = Σ 𝑥 ∈ 𝑧 Σ 𝑘 ∈ 𝐵 𝐶 ) → ( ( 𝑧 ∪ { 𝑤 } ) ⊆ 𝐴 → Σ 𝑘 ∈ ∪ 𝑥 ∈ ( 𝑧 ∪ { 𝑤 } ) 𝐵 𝐶 = Σ 𝑥 ∈ ( 𝑧 ∪ { 𝑤 } ) Σ 𝑘 ∈ 𝐵 𝐶 ) ) ) )
121 120 a2d ⊢ ( ¬ 𝑤 ∈ 𝑧 → ( ( 𝜑 → ( 𝑧 ⊆ 𝐴 → Σ 𝑘 ∈ ∪ 𝑥 ∈ 𝑧 𝐵 𝐶 = Σ 𝑥 ∈ 𝑧 Σ 𝑘 ∈ 𝐵 𝐶 ) ) → ( 𝜑 → ( ( 𝑧 ∪ { 𝑤 } ) ⊆ 𝐴 → Σ 𝑘 ∈ ∪ 𝑥 ∈ ( 𝑧 ∪ { 𝑤 } ) 𝐵 𝐶 = Σ 𝑥 ∈ ( 𝑧 ∪ { 𝑤 } ) Σ 𝑘 ∈ 𝐵 𝐶 ) ) ) )
122 121 adantl ⊢ ( ( 𝑧 ∈ Fin ∧ ¬ 𝑤 ∈ 𝑧 ) → ( ( 𝜑 → ( 𝑧 ⊆ 𝐴 → Σ 𝑘 ∈ ∪ 𝑥 ∈ 𝑧 𝐵 𝐶 = Σ 𝑥 ∈ 𝑧 Σ 𝑘 ∈ 𝐵 𝐶 ) ) → ( 𝜑 → ( ( 𝑧 ∪ { 𝑤 } ) ⊆ 𝐴 → Σ 𝑘 ∈ ∪ 𝑥 ∈ ( 𝑧 ∪ { 𝑤 } ) 𝐵 𝐶 = Σ 𝑥 ∈ ( 𝑧 ∪ { 𝑤 } ) Σ 𝑘 ∈ 𝐵 𝐶 ) ) ) )
123 14 21 28 35 39 122 findcard2s ⊢ ( 𝐴 ∈ Fin → ( 𝜑 → ( 𝐴 ⊆ 𝐴 → Σ 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 𝐶 = Σ 𝑥 ∈ 𝐴 Σ 𝑘 ∈ 𝐵 𝐶 ) ) )
124 1 123 mpcom ⊢ ( 𝜑 → ( 𝐴 ⊆ 𝐴 → Σ 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 𝐶 = Σ 𝑥 ∈ 𝐴 Σ 𝑘 ∈ 𝐵 𝐶 ) )
125 5 124 mpi ⊢ ( 𝜑 → Σ 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 𝐶 = Σ 𝑥 ∈ 𝐴 Σ 𝑘 ∈ 𝐵 𝐶 )