Metamath Proof Explorer

Theorem gsumzaddlem

Description: The sum of two group sums. (Contributed by Mario Carneiro, 25-Apr-2016) (Revised by AV, 5-Jun-2019)

Ref Expression
Hypotheses gsumzadd.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
gsumzadd.0 ⊢ 0 = ( 0g ‘ 𝐺 )
gsumzadd.p ⊢ + = ( +g ‘ 𝐺 )
gsumzadd.z ⊢ 𝑍 = ( Cntz ‘ 𝐺 )
gsumzadd.g ⊢ ( 𝜑 → 𝐺 ∈ Mnd )
gsumzadd.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
gsumzadd.fn ⊢ ( 𝜑 → 𝐹 finSupp 0 )
gsumzadd.hn ⊢ ( 𝜑 → 𝐻 finSupp 0 )
gsumzaddlem.w ⊢ 𝑊 = ( ( 𝐹 ∪ 𝐻 ) supp 0 )
gsumzaddlem.f ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
gsumzaddlem.h ⊢ ( 𝜑 → 𝐻 : 𝐴 ⟶ 𝐵 )
gsumzaddlem.1 ⊢ ( 𝜑 → ran 𝐹 ⊆ ( 𝑍 ‘ ran 𝐹 ) )
gsumzaddlem.2 ⊢ ( 𝜑 → ran 𝐻 ⊆ ( 𝑍 ‘ ran 𝐻 ) )
gsumzaddlem.3 ⊢ ( 𝜑 → ran ( 𝐹 ∘f + 𝐻 ) ⊆ ( 𝑍 ‘ ran ( 𝐹 ∘f + 𝐻 ) ) )
gsumzaddlem.4 ⊢ ( ( 𝜑 ∧ ( 𝑥 ⊆ 𝐴 ∧ 𝑘 ∈ ( 𝐴 ∖ 𝑥 ) ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ( 𝑍 ‘ { ( 𝐺 Σg ( 𝐻 ↾ 𝑥 ) ) } ) )
Assertion gsumzaddlem ( 𝜑 → ( 𝐺 Σg ( 𝐹 ∘f + 𝐻 ) ) = ( ( 𝐺 Σg 𝐹 ) + ( 𝐺 Σg 𝐻 ) ) )

Proof

Step Hyp Ref Expression
1 gsumzadd.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 gsumzadd.0 ⊢ 0 = ( 0g ‘ 𝐺 )
3 gsumzadd.p ⊢ + = ( +g ‘ 𝐺 )
4 gsumzadd.z ⊢ 𝑍 = ( Cntz ‘ 𝐺 )
5 gsumzadd.g ⊢ ( 𝜑 → 𝐺 ∈ Mnd )
6 gsumzadd.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
7 gsumzadd.fn ⊢ ( 𝜑 → 𝐹 finSupp 0 )
8 gsumzadd.hn ⊢ ( 𝜑 → 𝐻 finSupp 0 )
9 gsumzaddlem.w ⊢ 𝑊 = ( ( 𝐹 ∪ 𝐻 ) supp 0 )
10 gsumzaddlem.f ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
11 gsumzaddlem.h ⊢ ( 𝜑 → 𝐻 : 𝐴 ⟶ 𝐵 )
12 gsumzaddlem.1 ⊢ ( 𝜑 → ran 𝐹 ⊆ ( 𝑍 ‘ ran 𝐹 ) )
13 gsumzaddlem.2 ⊢ ( 𝜑 → ran 𝐻 ⊆ ( 𝑍 ‘ ran 𝐻 ) )
14 gsumzaddlem.3 ⊢ ( 𝜑 → ran ( 𝐹 ∘f + 𝐻 ) ⊆ ( 𝑍 ‘ ran ( 𝐹 ∘f + 𝐻 ) ) )
15 gsumzaddlem.4 ⊢ ( ( 𝜑 ∧ ( 𝑥 ⊆ 𝐴 ∧ 𝑘 ∈ ( 𝐴 ∖ 𝑥 ) ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ( 𝑍 ‘ { ( 𝐺 Σg ( 𝐻 ↾ 𝑥 ) ) } ) )
16 1 2 mndidcl ⊢ ( 𝐺 ∈ Mnd → 0 ∈ 𝐵 )
17 5 16 syl ⊢ ( 𝜑 → 0 ∈ 𝐵 )
18 1 3 2 mndlid ⊢ ( ( 𝐺 ∈ Mnd ∧ 0 ∈ 𝐵 ) → ( 0 + 0 ) = 0 )
19 5 17 18 syl2anc ⊢ ( 𝜑 → ( 0 + 0 ) = 0 )
20 19 adantr ⊢ ( ( 𝜑 ∧ 𝑊 = ∅ ) → ( 0 + 0 ) = 0 )
21 2 fvexi ⊢ 0 ∈ V
22 21 a1i ⊢ ( 𝜑 → 0 ∈ V )
23 11 6 fexd ⊢ ( 𝜑 → 𝐻 ∈ V )
24 23 suppun ⊢ ( 𝜑 → ( 𝐹 supp 0 ) ⊆ ( ( 𝐹 ∪ 𝐻 ) supp 0 ) )
25 24 9 sseqtrrdi ⊢ ( 𝜑 → ( 𝐹 supp 0 ) ⊆ 𝑊 )
26 10 6 22 25 gsumcllem ⊢ ( ( 𝜑 ∧ 𝑊 = ∅ ) → 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 0 ) )
27 26 oveq2d ⊢ ( ( 𝜑 ∧ 𝑊 = ∅ ) → ( 𝐺 Σg 𝐹 ) = ( 𝐺 Σg ( 𝑥 ∈ 𝐴 ↦ 0 ) ) )
28 2 gsumz ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑉 ) → ( 𝐺 Σg ( 𝑥 ∈ 𝐴 ↦ 0 ) ) = 0 )
29 5 6 28 syl2anc ⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑥 ∈ 𝐴 ↦ 0 ) ) = 0 )
30 29 adantr ⊢ ( ( 𝜑 ∧ 𝑊 = ∅ ) → ( 𝐺 Σg ( 𝑥 ∈ 𝐴 ↦ 0 ) ) = 0 )
31 27 30 eqtrd ⊢ ( ( 𝜑 ∧ 𝑊 = ∅ ) → ( 𝐺 Σg 𝐹 ) = 0 )
32 10 6 fexd ⊢ ( 𝜑 → 𝐹 ∈ V )
33 32 suppun ⊢ ( 𝜑 → ( 𝐻 supp 0 ) ⊆ ( ( 𝐻 ∪ 𝐹 ) supp 0 ) )
34 uncom ⊢ ( 𝐹 ∪ 𝐻 ) = ( 𝐻 ∪ 𝐹 )
35 34 oveq1i ⊢ ( ( 𝐹 ∪ 𝐻 ) supp 0 ) = ( ( 𝐻 ∪ 𝐹 ) supp 0 )
36 33 35 sseqtrrdi ⊢ ( 𝜑 → ( 𝐻 supp 0 ) ⊆ ( ( 𝐹 ∪ 𝐻 ) supp 0 ) )
37 36 9 sseqtrrdi ⊢ ( 𝜑 → ( 𝐻 supp 0 ) ⊆ 𝑊 )
38 11 6 22 37 gsumcllem ⊢ ( ( 𝜑 ∧ 𝑊 = ∅ ) → 𝐻 = ( 𝑥 ∈ 𝐴 ↦ 0 ) )
39 38 oveq2d ⊢ ( ( 𝜑 ∧ 𝑊 = ∅ ) → ( 𝐺 Σg 𝐻 ) = ( 𝐺 Σg ( 𝑥 ∈ 𝐴 ↦ 0 ) ) )
40 39 30 eqtrd ⊢ ( ( 𝜑 ∧ 𝑊 = ∅ ) → ( 𝐺 Σg 𝐻 ) = 0 )
41 31 40 oveq12d ⊢ ( ( 𝜑 ∧ 𝑊 = ∅ ) → ( ( 𝐺 Σg 𝐹 ) + ( 𝐺 Σg 𝐻 ) ) = ( 0 + 0 ) )
42 6 adantr ⊢ ( ( 𝜑 ∧ 𝑊 = ∅ ) → 𝐴 ∈ 𝑉 )
43 17 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑊 = ∅ ) ∧ 𝑥 ∈ 𝐴 ) → 0 ∈ 𝐵 )
44 42 43 43 26 38 offval2 ⊢ ( ( 𝜑 ∧ 𝑊 = ∅ ) → ( 𝐹 ∘f + 𝐻 ) = ( 𝑥 ∈ 𝐴 ↦ ( 0 + 0 ) ) )
45 20 mpteq2dv ⊢ ( ( 𝜑 ∧ 𝑊 = ∅ ) → ( 𝑥 ∈ 𝐴 ↦ ( 0 + 0 ) ) = ( 𝑥 ∈ 𝐴 ↦ 0 ) )
46 44 45 eqtrd ⊢ ( ( 𝜑 ∧ 𝑊 = ∅ ) → ( 𝐹 ∘f + 𝐻 ) = ( 𝑥 ∈ 𝐴 ↦ 0 ) )
47 46 oveq2d ⊢ ( ( 𝜑 ∧ 𝑊 = ∅ ) → ( 𝐺 Σg ( 𝐹 ∘f + 𝐻 ) ) = ( 𝐺 Σg ( 𝑥 ∈ 𝐴 ↦ 0 ) ) )
48 47 30 eqtrd ⊢ ( ( 𝜑 ∧ 𝑊 = ∅ ) → ( 𝐺 Σg ( 𝐹 ∘f + 𝐻 ) ) = 0 )
49 20 41 48 3eqtr4rd ⊢ ( ( 𝜑 ∧ 𝑊 = ∅ ) → ( 𝐺 Σg ( 𝐹 ∘f + 𝐻 ) ) = ( ( 𝐺 Σg 𝐹 ) + ( 𝐺 Σg 𝐻 ) ) )
50 49 ex ⊢ ( 𝜑 → ( 𝑊 = ∅ → ( 𝐺 Σg ( 𝐹 ∘f + 𝐻 ) ) = ( ( 𝐺 Σg 𝐹 ) + ( 𝐺 Σg 𝐻 ) ) ) )
51 5 adantr ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ 𝑊 ) ) → 𝐺 ∈ Mnd )
52 1 3 mndcl ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) → ( 𝑧 + 𝑤 ) ∈ 𝐵 )
53 52 3expb ⊢ ( ( 𝐺 ∈ Mnd ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) → ( 𝑧 + 𝑤 ) ∈ 𝐵 )
54 51 53 sylan ⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ 𝑊 ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) → ( 𝑧 + 𝑤 ) ∈ 𝐵 )
55 54 caovclg ⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ 𝑊 ) ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 + 𝑦 ) ∈ 𝐵 )
56 simprl ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ 𝑊 ) ) → ( ♯ ‘ 𝑊 ) ∈ ℕ )
57 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
58 56 57 eleqtrdi ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ 𝑊 ) ) → ( ♯ ‘ 𝑊 ) ∈ ( ℤ≥ ‘ 1 ) )
59 10 adantr ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ 𝑊 ) ) → 𝐹 : 𝐴 ⟶ 𝐵 )
60 f1of1 ⊢ ( 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ 𝑊 → 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1→ 𝑊 )
61 60 ad2antll ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ 𝑊 ) ) → 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1→ 𝑊 )
62 suppssdm ⊢ ( ( 𝐹 ∪ 𝐻 ) supp 0 ) ⊆ dom ( 𝐹 ∪ 𝐻 )
63 62 a1i ⊢ ( 𝜑 → ( ( 𝐹 ∪ 𝐻 ) supp 0 ) ⊆ dom ( 𝐹 ∪ 𝐻 ) )
64 9 a1i ⊢ ( 𝜑 → 𝑊 = ( ( 𝐹 ∪ 𝐻 ) supp 0 ) )
65 dmun ⊢ dom ( 𝐹 ∪ 𝐻 ) = ( dom 𝐹 ∪ dom 𝐻 )
66 10 fdmd ⊢ ( 𝜑 → dom 𝐹 = 𝐴 )
67 11 fdmd ⊢ ( 𝜑 → dom 𝐻 = 𝐴 )
68 66 67 uneq12d ⊢ ( 𝜑 → ( dom 𝐹 ∪ dom 𝐻 ) = ( 𝐴 ∪ 𝐴 ) )
69 unidm ⊢ ( 𝐴 ∪ 𝐴 ) = 𝐴
70 68 69 eqtrdi ⊢ ( 𝜑 → ( dom 𝐹 ∪ dom 𝐻 ) = 𝐴 )
71 65 70 eqtr2id ⊢ ( 𝜑 → 𝐴 = dom ( 𝐹 ∪ 𝐻 ) )
72 63 64 71 3sstr4d ⊢ ( 𝜑 → 𝑊 ⊆ 𝐴 )
73 72 adantr ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ 𝑊 ) ) → 𝑊 ⊆ 𝐴 )
74 f1ss ⊢ ( ( 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1→ 𝑊 ∧ 𝑊 ⊆ 𝐴 ) → 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1→ 𝐴 )
75 61 73 74 syl2anc ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ 𝑊 ) ) → 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1→ 𝐴 )
76 f1f ⊢ ( 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1→ 𝐴 → 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) ⟶ 𝐴 )
77 75 76 syl ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ 𝑊 ) ) → 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) ⟶ 𝐴 )
78 fco ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) ⟶ 𝐴 ) → ( 𝐹 ∘ 𝑓 ) : ( 1 ... ( ♯ ‘ 𝑊 ) ) ⟶ 𝐵 )
79 59 77 78 syl2anc ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ 𝑊 ) ) → ( 𝐹 ∘ 𝑓 ) : ( 1 ... ( ♯ ‘ 𝑊 ) ) ⟶ 𝐵 )
80 79 ffvelrnda ⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ 𝑊 ) ) ∧ 𝑘 ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝐹 ∘ 𝑓 ) ‘ 𝑘 ) ∈ 𝐵 )
81 11 adantr ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ 𝑊 ) ) → 𝐻 : 𝐴 ⟶ 𝐵 )
82 fco ⊢ ( ( 𝐻 : 𝐴 ⟶ 𝐵 ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) ⟶ 𝐴 ) → ( 𝐻 ∘ 𝑓 ) : ( 1 ... ( ♯ ‘ 𝑊 ) ) ⟶ 𝐵 )
83 81 77 82 syl2anc ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ 𝑊 ) ) → ( 𝐻 ∘ 𝑓 ) : ( 1 ... ( ♯ ‘ 𝑊 ) ) ⟶ 𝐵 )
84 83 ffvelrnda ⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ 𝑊 ) ) ∧ 𝑘 ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝐻 ∘ 𝑓 ) ‘ 𝑘 ) ∈ 𝐵 )
85 59 ffnd ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ 𝑊 ) ) → 𝐹 Fn 𝐴 )
86 81 ffnd ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ 𝑊 ) ) → 𝐻 Fn 𝐴 )
87 6 adantr ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ 𝑊 ) ) → 𝐴 ∈ 𝑉 )
88 ovexd ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ 𝑊 ) ) → ( 1 ... ( ♯ ‘ 𝑊 ) ) ∈ V )
89 inidm ⊢ ( 𝐴 ∩ 𝐴 ) = 𝐴
90 85 86 77 87 87 88 89 ofco ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ 𝑊 ) ) → ( ( 𝐹 ∘f + 𝐻 ) ∘ 𝑓 ) = ( ( 𝐹 ∘ 𝑓 ) ∘f + ( 𝐻 ∘ 𝑓 ) ) )
91 90 fveq1d ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ 𝑊 ) ) → ( ( ( 𝐹 ∘f + 𝐻 ) ∘ 𝑓 ) ‘ 𝑘 ) = ( ( ( 𝐹 ∘ 𝑓 ) ∘f + ( 𝐻 ∘ 𝑓 ) ) ‘ 𝑘 ) )
92 91 adantr ⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ 𝑊 ) ) ∧ 𝑘 ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) ) → ( ( ( 𝐹 ∘f + 𝐻 ) ∘ 𝑓 ) ‘ 𝑘 ) = ( ( ( 𝐹 ∘ 𝑓 ) ∘f + ( 𝐻 ∘ 𝑓 ) ) ‘ 𝑘 ) )
93 fnfco ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) ⟶ 𝐴 ) → ( 𝐹 ∘ 𝑓 ) Fn ( 1 ... ( ♯ ‘ 𝑊 ) ) )
94 85 77 93 syl2anc ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ 𝑊 ) ) → ( 𝐹 ∘ 𝑓 ) Fn ( 1 ... ( ♯ ‘ 𝑊 ) ) )
95 fnfco ⊢ ( ( 𝐻 Fn 𝐴 ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) ⟶ 𝐴 ) → ( 𝐻 ∘ 𝑓 ) Fn ( 1 ... ( ♯ ‘ 𝑊 ) ) )
96 86 77 95 syl2anc ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ 𝑊 ) ) → ( 𝐻 ∘ 𝑓 ) Fn ( 1 ... ( ♯ ‘ 𝑊 ) ) )
97 inidm ⊢ ( ( 1 ... ( ♯ ‘ 𝑊 ) ) ∩ ( 1 ... ( ♯ ‘ 𝑊 ) ) ) = ( 1 ... ( ♯ ‘ 𝑊 ) )
98 eqidd ⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ 𝑊 ) ) ∧ 𝑘 ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝐹 ∘ 𝑓 ) ‘ 𝑘 ) = ( ( 𝐹 ∘ 𝑓 ) ‘ 𝑘 ) )
99 eqidd ⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ 𝑊 ) ) ∧ 𝑘 ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝐻 ∘ 𝑓 ) ‘ 𝑘 ) = ( ( 𝐻 ∘ 𝑓 ) ‘ 𝑘 ) )
100 94 96 88 88 97 98 99 ofval ⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ 𝑊 ) ) ∧ 𝑘 ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) ) → ( ( ( 𝐹 ∘ 𝑓 ) ∘f + ( 𝐻 ∘ 𝑓 ) ) ‘ 𝑘 ) = ( ( ( 𝐹 ∘ 𝑓 ) ‘ 𝑘 ) + ( ( 𝐻 ∘ 𝑓 ) ‘ 𝑘 ) ) )
101 92 100 eqtrd ⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ 𝑊 ) ) ∧ 𝑘 ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) ) → ( ( ( 𝐹 ∘f + 𝐻 ) ∘ 𝑓 ) ‘ 𝑘 ) = ( ( ( 𝐹 ∘ 𝑓 ) ‘ 𝑘 ) + ( ( 𝐻 ∘ 𝑓 ) ‘ 𝑘 ) ) )
102 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ 𝑊 ) ) ∧ 𝑛 ∈ ( 1 ..^ ( ♯ ‘ 𝑊 ) ) ) → 𝐺 ∈ Mnd )
103 elfzouz ⊢ ( 𝑛 ∈ ( 1 ..^ ( ♯ ‘ 𝑊 ) ) → 𝑛 ∈ ( ℤ≥ ‘ 1 ) )
104 103 adantl ⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ 𝑊 ) ) ∧ 𝑛 ∈ ( 1 ..^ ( ♯ ‘ 𝑊 ) ) ) → 𝑛 ∈ ( ℤ≥ ‘ 1 ) )
105 elfzouz2 ⊢ ( 𝑛 ∈ ( 1 ..^ ( ♯ ‘ 𝑊 ) ) → ( ♯ ‘ 𝑊 ) ∈ ( ℤ≥ ‘ 𝑛 ) )
106 105 adantl ⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ 𝑊 ) ) ∧ 𝑛 ∈ ( 1 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ♯ ‘ 𝑊 ) ∈ ( ℤ≥ ‘ 𝑛 ) )
107 fzss2 ⊢ ( ( ♯ ‘ 𝑊 ) ∈ ( ℤ≥ ‘ 𝑛 ) → ( 1 ... 𝑛 ) ⊆ ( 1 ... ( ♯ ‘ 𝑊 ) ) )
108 106 107 syl ⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ 𝑊 ) ) ∧ 𝑛 ∈ ( 1 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( 1 ... 𝑛 ) ⊆ ( 1 ... ( ♯ ‘ 𝑊 ) ) )
109 108 sselda ⊢ ( ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ 𝑊 ) ) ∧ 𝑛 ∈ ( 1 ..^ ( ♯ ‘ 𝑊 ) ) ) ∧ 𝑘 ∈ ( 1 ... 𝑛 ) ) → 𝑘 ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) )
110 80 adantlr ⊢ ( ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ 𝑊 ) ) ∧ 𝑛 ∈ ( 1 ..^ ( ♯ ‘ 𝑊 ) ) ) ∧ 𝑘 ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝐹 ∘ 𝑓 ) ‘ 𝑘 ) ∈ 𝐵 )
111 109 110 syldan ⊢ ( ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ 𝑊 ) ) ∧ 𝑛 ∈ ( 1 ..^ ( ♯ ‘ 𝑊 ) ) ) ∧ 𝑘 ∈ ( 1 ... 𝑛 ) ) → ( ( 𝐹 ∘ 𝑓 ) ‘ 𝑘 ) ∈ 𝐵 )
112 1 3 mndcl ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝑘 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ) → ( 𝑘 + 𝑥 ) ∈ 𝐵 )
113 112 3expb ⊢ ( ( 𝐺 ∈ Mnd ∧ ( 𝑘 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ) ) → ( 𝑘 + 𝑥 ) ∈ 𝐵 )
114 102 113 sylan ⊢ ( ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ 𝑊 ) ) ∧ 𝑛 ∈ ( 1 ..^ ( ♯ ‘ 𝑊 ) ) ) ∧ ( 𝑘 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ) ) → ( 𝑘 + 𝑥 ) ∈ 𝐵 )
115 104 111 114 seqcl ⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ 𝑊 ) ) ∧ 𝑛 ∈ ( 1 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( seq 1 ( + , ( 𝐹 ∘ 𝑓 ) ) ‘ 𝑛 ) ∈ 𝐵 )
116 84 adantlr ⊢ ( ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ 𝑊 ) ) ∧ 𝑛 ∈ ( 1 ..^ ( ♯ ‘ 𝑊 ) ) ) ∧ 𝑘 ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝐻 ∘ 𝑓 ) ‘ 𝑘 ) ∈ 𝐵 )
117 109 116 syldan ⊢ ( ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ 𝑊 ) ) ∧ 𝑛 ∈ ( 1 ..^ ( ♯ ‘ 𝑊 ) ) ) ∧ 𝑘 ∈ ( 1 ... 𝑛 ) ) → ( ( 𝐻 ∘ 𝑓 ) ‘ 𝑘 ) ∈ 𝐵 )
118 104 117 114 seqcl ⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ 𝑊 ) ) ∧ 𝑛 ∈ ( 1 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( seq 1 ( + , ( 𝐻 ∘ 𝑓 ) ) ‘ 𝑛 ) ∈ 𝐵 )
119 fzofzp1 ⊢ ( 𝑛 ∈ ( 1 ..^ ( ♯ ‘ 𝑊 ) ) → ( 𝑛 + 1 ) ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) )
120 ffvelrn ⊢ ( ( ( 𝐹 ∘ 𝑓 ) : ( 1 ... ( ♯ ‘ 𝑊 ) ) ⟶ 𝐵 ∧ ( 𝑛 + 1 ) ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝐹 ∘ 𝑓 ) ‘ ( 𝑛 + 1 ) ) ∈ 𝐵 )
121 79 119 120 syl2an ⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ 𝑊 ) ) ∧ 𝑛 ∈ ( 1 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝐹 ∘ 𝑓 ) ‘ ( 𝑛 + 1 ) ) ∈ 𝐵 )
122 ffvelrn ⊢ ( ( ( 𝐻 ∘ 𝑓 ) : ( 1 ... ( ♯ ‘ 𝑊 ) ) ⟶ 𝐵 ∧ ( 𝑛 + 1 ) ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝐻 ∘ 𝑓 ) ‘ ( 𝑛 + 1 ) ) ∈ 𝐵 )
123 83 119 122 syl2an ⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ 𝑊 ) ) ∧ 𝑛 ∈ ( 1 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝐻 ∘ 𝑓 ) ‘ ( 𝑛 + 1 ) ) ∈ 𝐵 )
124 fvco3 ⊢ ( ( 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) ⟶ 𝐴 ∧ ( 𝑛 + 1 ) ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝐹 ∘ 𝑓 ) ‘ ( 𝑛 + 1 ) ) = ( 𝐹 ‘ ( 𝑓 ‘ ( 𝑛 + 1 ) ) ) )
125 77 119 124 syl2an ⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ 𝑊 ) ) ∧ 𝑛 ∈ ( 1 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝐹 ∘ 𝑓 ) ‘ ( 𝑛 + 1 ) ) = ( 𝐹 ‘ ( 𝑓 ‘ ( 𝑛 + 1 ) ) ) )
126 fveq2 ⊢ ( 𝑘 = ( 𝑓 ‘ ( 𝑛 + 1 ) ) → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ ( 𝑓 ‘ ( 𝑛 + 1 ) ) ) )
127 126 eleq1d ⊢ ( 𝑘 = ( 𝑓 ‘ ( 𝑛 + 1 ) ) → ( ( 𝐹 ‘ 𝑘 ) ∈ ( 𝑍 ‘ { ( 𝐺 Σg ( 𝐻 ↾ ( 𝑓 “ ( 1 ... 𝑛 ) ) ) ) } ) ↔ ( 𝐹 ‘ ( 𝑓 ‘ ( 𝑛 + 1 ) ) ) ∈ ( 𝑍 ‘ { ( 𝐺 Σg ( 𝐻 ↾ ( 𝑓 “ ( 1 ... 𝑛 ) ) ) ) } ) ) )
128 15 expr ⊢ ( ( 𝜑 ∧ 𝑥 ⊆ 𝐴 ) → ( 𝑘 ∈ ( 𝐴 ∖ 𝑥 ) → ( 𝐹 ‘ 𝑘 ) ∈ ( 𝑍 ‘ { ( 𝐺 Σg ( 𝐻 ↾ 𝑥 ) ) } ) ) )
129 128 ralrimiv ⊢ ( ( 𝜑 ∧ 𝑥 ⊆ 𝐴 ) → ∀ 𝑘 ∈ ( 𝐴 ∖ 𝑥 ) ( 𝐹 ‘ 𝑘 ) ∈ ( 𝑍 ‘ { ( 𝐺 Σg ( 𝐻 ↾ 𝑥 ) ) } ) )
130 129 ex ⊢ ( 𝜑 → ( 𝑥 ⊆ 𝐴 → ∀ 𝑘 ∈ ( 𝐴 ∖ 𝑥 ) ( 𝐹 ‘ 𝑘 ) ∈ ( 𝑍 ‘ { ( 𝐺 Σg ( 𝐻 ↾ 𝑥 ) ) } ) ) )
131 130 alrimiv ⊢ ( 𝜑 → ∀ 𝑥 ( 𝑥 ⊆ 𝐴 → ∀ 𝑘 ∈ ( 𝐴 ∖ 𝑥 ) ( 𝐹 ‘ 𝑘 ) ∈ ( 𝑍 ‘ { ( 𝐺 Σg ( 𝐻 ↾ 𝑥 ) ) } ) ) )
132 131 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ 𝑊 ) ) ∧ 𝑛 ∈ ( 1 ..^ ( ♯ ‘ 𝑊 ) ) ) → ∀ 𝑥 ( 𝑥 ⊆ 𝐴 → ∀ 𝑘 ∈ ( 𝐴 ∖ 𝑥 ) ( 𝐹 ‘ 𝑘 ) ∈ ( 𝑍 ‘ { ( 𝐺 Σg ( 𝐻 ↾ 𝑥 ) ) } ) ) )
133 imassrn ⊢ ( 𝑓 “ ( 1 ... 𝑛 ) ) ⊆ ran 𝑓
134 77 adantr ⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ 𝑊 ) ) ∧ 𝑛 ∈ ( 1 ..^ ( ♯ ‘ 𝑊 ) ) ) → 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) ⟶ 𝐴 )
135 134 frnd ⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ 𝑊 ) ) ∧ 𝑛 ∈ ( 1 ..^ ( ♯ ‘ 𝑊 ) ) ) → ran 𝑓 ⊆ 𝐴 )
136 133 135 sstrid ⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ 𝑊 ) ) ∧ 𝑛 ∈ ( 1 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( 𝑓 “ ( 1 ... 𝑛 ) ) ⊆ 𝐴 )
137 vex ⊢ 𝑓 ∈ V
138 137 imaex ⊢ ( 𝑓 “ ( 1 ... 𝑛 ) ) ∈ V
139 sseq1 ⊢ ( 𝑥 = ( 𝑓 “ ( 1 ... 𝑛 ) ) → ( 𝑥 ⊆ 𝐴 ↔ ( 𝑓 “ ( 1 ... 𝑛 ) ) ⊆ 𝐴 ) )
140 difeq2 ⊢ ( 𝑥 = ( 𝑓 “ ( 1 ... 𝑛 ) ) → ( 𝐴 ∖ 𝑥 ) = ( 𝐴 ∖ ( 𝑓 “ ( 1 ... 𝑛 ) ) ) )
141 reseq2 ⊢ ( 𝑥 = ( 𝑓 “ ( 1 ... 𝑛 ) ) → ( 𝐻 ↾ 𝑥 ) = ( 𝐻 ↾ ( 𝑓 “ ( 1 ... 𝑛 ) ) ) )
142 141 oveq2d ⊢ ( 𝑥 = ( 𝑓 “ ( 1 ... 𝑛 ) ) → ( 𝐺 Σg ( 𝐻 ↾ 𝑥 ) ) = ( 𝐺 Σg ( 𝐻 ↾ ( 𝑓 “ ( 1 ... 𝑛 ) ) ) ) )
143 142 sneqd ⊢ ( 𝑥 = ( 𝑓 “ ( 1 ... 𝑛 ) ) → { ( 𝐺 Σg ( 𝐻 ↾ 𝑥 ) ) } = { ( 𝐺 Σg ( 𝐻 ↾ ( 𝑓 “ ( 1 ... 𝑛 ) ) ) ) } )
144 143 fveq2d ⊢ ( 𝑥 = ( 𝑓 “ ( 1 ... 𝑛 ) ) → ( 𝑍 ‘ { ( 𝐺 Σg ( 𝐻 ↾ 𝑥 ) ) } ) = ( 𝑍 ‘ { ( 𝐺 Σg ( 𝐻 ↾ ( 𝑓 “ ( 1 ... 𝑛 ) ) ) ) } ) )
145 144 eleq2d ⊢ ( 𝑥 = ( 𝑓 “ ( 1 ... 𝑛 ) ) → ( ( 𝐹 ‘ 𝑘 ) ∈ ( 𝑍 ‘ { ( 𝐺 Σg ( 𝐻 ↾ 𝑥 ) ) } ) ↔ ( 𝐹 ‘ 𝑘 ) ∈ ( 𝑍 ‘ { ( 𝐺 Σg ( 𝐻 ↾ ( 𝑓 “ ( 1 ... 𝑛 ) ) ) ) } ) ) )
146 140 145 raleqbidv ⊢ ( 𝑥 = ( 𝑓 “ ( 1 ... 𝑛 ) ) → ( ∀ 𝑘 ∈ ( 𝐴 ∖ 𝑥 ) ( 𝐹 ‘ 𝑘 ) ∈ ( 𝑍 ‘ { ( 𝐺 Σg ( 𝐻 ↾ 𝑥 ) ) } ) ↔ ∀ 𝑘 ∈ ( 𝐴 ∖ ( 𝑓 “ ( 1 ... 𝑛 ) ) ) ( 𝐹 ‘ 𝑘 ) ∈ ( 𝑍 ‘ { ( 𝐺 Σg ( 𝐻 ↾ ( 𝑓 “ ( 1 ... 𝑛 ) ) ) ) } ) ) )
147 139 146 imbi12d ⊢ ( 𝑥 = ( 𝑓 “ ( 1 ... 𝑛 ) ) → ( ( 𝑥 ⊆ 𝐴 → ∀ 𝑘 ∈ ( 𝐴 ∖ 𝑥 ) ( 𝐹 ‘ 𝑘 ) ∈ ( 𝑍 ‘ { ( 𝐺 Σg ( 𝐻 ↾ 𝑥 ) ) } ) ) ↔ ( ( 𝑓 “ ( 1 ... 𝑛 ) ) ⊆ 𝐴 → ∀ 𝑘 ∈ ( 𝐴 ∖ ( 𝑓 “ ( 1 ... 𝑛 ) ) ) ( 𝐹 ‘ 𝑘 ) ∈ ( 𝑍 ‘ { ( 𝐺 Σg ( 𝐻 ↾ ( 𝑓 “ ( 1 ... 𝑛 ) ) ) ) } ) ) ) )
148 138 147 spcv ⊢ ( ∀ 𝑥 ( 𝑥 ⊆ 𝐴 → ∀ 𝑘 ∈ ( 𝐴 ∖ 𝑥 ) ( 𝐹 ‘ 𝑘 ) ∈ ( 𝑍 ‘ { ( 𝐺 Σg ( 𝐻 ↾ 𝑥 ) ) } ) ) → ( ( 𝑓 “ ( 1 ... 𝑛 ) ) ⊆ 𝐴 → ∀ 𝑘 ∈ ( 𝐴 ∖ ( 𝑓 “ ( 1 ... 𝑛 ) ) ) ( 𝐹 ‘ 𝑘 ) ∈ ( 𝑍 ‘ { ( 𝐺 Σg ( 𝐻 ↾ ( 𝑓 “ ( 1 ... 𝑛 ) ) ) ) } ) ) )
149 132 136 148 sylc ⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ 𝑊 ) ) ∧ 𝑛 ∈ ( 1 ..^ ( ♯ ‘ 𝑊 ) ) ) → ∀ 𝑘 ∈ ( 𝐴 ∖ ( 𝑓 “ ( 1 ... 𝑛 ) ) ) ( 𝐹 ‘ 𝑘 ) ∈ ( 𝑍 ‘ { ( 𝐺 Σg ( 𝐻 ↾ ( 𝑓 “ ( 1 ... 𝑛 ) ) ) ) } ) )
150 ffvelrn ⊢ ( ( 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) ⟶ 𝐴 ∧ ( 𝑛 + 1 ) ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) ) → ( 𝑓 ‘ ( 𝑛 + 1 ) ) ∈ 𝐴 )
151 77 119 150 syl2an ⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ 𝑊 ) ) ∧ 𝑛 ∈ ( 1 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( 𝑓 ‘ ( 𝑛 + 1 ) ) ∈ 𝐴 )
152 fzp1nel ⊢ ¬ ( 𝑛 + 1 ) ∈ ( 1 ... 𝑛 )
153 75 adantr ⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ 𝑊 ) ) ∧ 𝑛 ∈ ( 1 ..^ ( ♯ ‘ 𝑊 ) ) ) → 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1→ 𝐴 )
154 119 adantl ⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ 𝑊 ) ) ∧ 𝑛 ∈ ( 1 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( 𝑛 + 1 ) ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) )
155 f1elima ⊢ ( ( 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1→ 𝐴 ∧ ( 𝑛 + 1 ) ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) ∧ ( 1 ... 𝑛 ) ⊆ ( 1 ... ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝑓 ‘ ( 𝑛 + 1 ) ) ∈ ( 𝑓 “ ( 1 ... 𝑛 ) ) ↔ ( 𝑛 + 1 ) ∈ ( 1 ... 𝑛 ) ) )
156 153 154 108 155 syl3anc ⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ 𝑊 ) ) ∧ 𝑛 ∈ ( 1 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝑓 ‘ ( 𝑛 + 1 ) ) ∈ ( 𝑓 “ ( 1 ... 𝑛 ) ) ↔ ( 𝑛 + 1 ) ∈ ( 1 ... 𝑛 ) ) )
157 152 156 mtbiri ⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ 𝑊 ) ) ∧ 𝑛 ∈ ( 1 ..^ ( ♯ ‘ 𝑊 ) ) ) → ¬ ( 𝑓 ‘ ( 𝑛 + 1 ) ) ∈ ( 𝑓 “ ( 1 ... 𝑛 ) ) )
158 151 157 eldifd ⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ 𝑊 ) ) ∧ 𝑛 ∈ ( 1 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( 𝑓 ‘ ( 𝑛 + 1 ) ) ∈ ( 𝐴 ∖ ( 𝑓 “ ( 1 ... 𝑛 ) ) ) )
159 127 149 158 rspcdva ⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ 𝑊 ) ) ∧ 𝑛 ∈ ( 1 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( 𝐹 ‘ ( 𝑓 ‘ ( 𝑛 + 1 ) ) ) ∈ ( 𝑍 ‘ { ( 𝐺 Σg ( 𝐻 ↾ ( 𝑓 “ ( 1 ... 𝑛 ) ) ) ) } ) )
160 125 159 eqeltrd ⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ 𝑊 ) ) ∧ 𝑛 ∈ ( 1 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝐹 ∘ 𝑓 ) ‘ ( 𝑛 + 1 ) ) ∈ ( 𝑍 ‘ { ( 𝐺 Σg ( 𝐻 ↾ ( 𝑓 “ ( 1 ... 𝑛 ) ) ) ) } ) )
161 138 a1i ⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ 𝑊 ) ) ∧ 𝑛 ∈ ( 1 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( 𝑓 “ ( 1 ... 𝑛 ) ) ∈ V )
162 11 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ 𝑊 ) ) ∧ 𝑛 ∈ ( 1 ..^ ( ♯ ‘ 𝑊 ) ) ) → 𝐻 : 𝐴 ⟶ 𝐵 )
163 162 136 fssresd ⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ 𝑊 ) ) ∧ 𝑛 ∈ ( 1 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( 𝐻 ↾ ( 𝑓 “ ( 1 ... 𝑛 ) ) ) : ( 𝑓 “ ( 1 ... 𝑛 ) ) ⟶ 𝐵 )
164 13 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ 𝑊 ) ) ∧ 𝑛 ∈ ( 1 ..^ ( ♯ ‘ 𝑊 ) ) ) → ran 𝐻 ⊆ ( 𝑍 ‘ ran 𝐻 ) )
165 resss ⊢ ( 𝐻 ↾ ( 𝑓 “ ( 1 ... 𝑛 ) ) ) ⊆ 𝐻
166 165 rnssi ⊢ ran ( 𝐻 ↾ ( 𝑓 “ ( 1 ... 𝑛 ) ) ) ⊆ ran 𝐻
167 4 cntzidss ⊢ ( ( ran 𝐻 ⊆ ( 𝑍 ‘ ran 𝐻 ) ∧ ran ( 𝐻 ↾ ( 𝑓 “ ( 1 ... 𝑛 ) ) ) ⊆ ran 𝐻 ) → ran ( 𝐻 ↾ ( 𝑓 “ ( 1 ... 𝑛 ) ) ) ⊆ ( 𝑍 ‘ ran ( 𝐻 ↾ ( 𝑓 “ ( 1 ... 𝑛 ) ) ) ) )
168 164 166 167 sylancl ⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ 𝑊 ) ) ∧ 𝑛 ∈ ( 1 ..^ ( ♯ ‘ 𝑊 ) ) ) → ran ( 𝐻 ↾ ( 𝑓 “ ( 1 ... 𝑛 ) ) ) ⊆ ( 𝑍 ‘ ran ( 𝐻 ↾ ( 𝑓 “ ( 1 ... 𝑛 ) ) ) ) )
169 104 57 eleqtrrdi ⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ 𝑊 ) ) ∧ 𝑛 ∈ ( 1 ..^ ( ♯ ‘ 𝑊 ) ) ) → 𝑛 ∈ ℕ )
170 f1ores ⊢ ( ( 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1→ 𝐴 ∧ ( 1 ... 𝑛 ) ⊆ ( 1 ... ( ♯ ‘ 𝑊 ) ) ) → ( 𝑓 ↾ ( 1 ... 𝑛 ) ) : ( 1 ... 𝑛 ) –1-1-onto→ ( 𝑓 “ ( 1 ... 𝑛 ) ) )
171 153 108 170 syl2anc ⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ 𝑊 ) ) ∧ 𝑛 ∈ ( 1 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( 𝑓 ↾ ( 1 ... 𝑛 ) ) : ( 1 ... 𝑛 ) –1-1-onto→ ( 𝑓 “ ( 1 ... 𝑛 ) ) )
172 f1of1 ⊢ ( ( 𝑓 ↾ ( 1 ... 𝑛 ) ) : ( 1 ... 𝑛 ) –1-1-onto→ ( 𝑓 “ ( 1 ... 𝑛 ) ) → ( 𝑓 ↾ ( 1 ... 𝑛 ) ) : ( 1 ... 𝑛 ) –1-1→ ( 𝑓 “ ( 1 ... 𝑛 ) ) )
173 171 172 syl ⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ 𝑊 ) ) ∧ 𝑛 ∈ ( 1 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( 𝑓 ↾ ( 1 ... 𝑛 ) ) : ( 1 ... 𝑛 ) –1-1→ ( 𝑓 “ ( 1 ... 𝑛 ) ) )
174 suppssdm ⊢ ( ( 𝐻 ↾ ( 𝑓 “ ( 1 ... 𝑛 ) ) ) supp 0 ) ⊆ dom ( 𝐻 ↾ ( 𝑓 “ ( 1 ... 𝑛 ) ) )
175 dmres ⊢ dom ( 𝐻 ↾ ( 𝑓 “ ( 1 ... 𝑛 ) ) ) = ( ( 𝑓 “ ( 1 ... 𝑛 ) ) ∩ dom 𝐻 )
176 175 a1i ⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ 𝑊 ) ) ∧ 𝑛 ∈ ( 1 ..^ ( ♯ ‘ 𝑊 ) ) ) → dom ( 𝐻 ↾ ( 𝑓 “ ( 1 ... 𝑛 ) ) ) = ( ( 𝑓 “ ( 1 ... 𝑛 ) ) ∩ dom 𝐻 ) )
177 174 176 sseqtrid ⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ 𝑊 ) ) ∧ 𝑛 ∈ ( 1 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝐻 ↾ ( 𝑓 “ ( 1 ... 𝑛 ) ) ) supp 0 ) ⊆ ( ( 𝑓 “ ( 1 ... 𝑛 ) ) ∩ dom 𝐻 ) )
178 inss1 ⊢ ( ( 𝑓 “ ( 1 ... 𝑛 ) ) ∩ dom 𝐻 ) ⊆ ( 𝑓 “ ( 1 ... 𝑛 ) )
179 df-ima ⊢ ( 𝑓 “ ( 1 ... 𝑛 ) ) = ran ( 𝑓 ↾ ( 1 ... 𝑛 ) )
180 179 a1i ⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ 𝑊 ) ) ∧ 𝑛 ∈ ( 1 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( 𝑓 “ ( 1 ... 𝑛 ) ) = ran ( 𝑓 ↾ ( 1 ... 𝑛 ) ) )
181 178 180 sseqtrid ⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ 𝑊 ) ) ∧ 𝑛 ∈ ( 1 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝑓 “ ( 1 ... 𝑛 ) ) ∩ dom 𝐻 ) ⊆ ran ( 𝑓 ↾ ( 1 ... 𝑛 ) ) )
182 177 181 sstrd ⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ 𝑊 ) ) ∧ 𝑛 ∈ ( 1 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝐻 ↾ ( 𝑓 “ ( 1 ... 𝑛 ) ) ) supp 0 ) ⊆ ran ( 𝑓 ↾ ( 1 ... 𝑛 ) ) )
183 eqid ⊢ ( ( ( 𝐻 ↾ ( 𝑓 “ ( 1 ... 𝑛 ) ) ) ∘ ( 𝑓 ↾ ( 1 ... 𝑛 ) ) ) supp 0 ) = ( ( ( 𝐻 ↾ ( 𝑓 “ ( 1 ... 𝑛 ) ) ) ∘ ( 𝑓 ↾ ( 1 ... 𝑛 ) ) ) supp 0 )
184 1 2 3 4 102 161 163 168 169 173 182 183 gsumval3 ⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ 𝑊 ) ) ∧ 𝑛 ∈ ( 1 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( 𝐺 Σg ( 𝐻 ↾ ( 𝑓 “ ( 1 ... 𝑛 ) ) ) ) = ( seq 1 ( + , ( ( 𝐻 ↾ ( 𝑓 “ ( 1 ... 𝑛 ) ) ) ∘ ( 𝑓 ↾ ( 1 ... 𝑛 ) ) ) ) ‘ 𝑛 ) )
185 179 eqimss2i ⊢ ran ( 𝑓 ↾ ( 1 ... 𝑛 ) ) ⊆ ( 𝑓 “ ( 1 ... 𝑛 ) )
186 cores ⊢ ( ran ( 𝑓 ↾ ( 1 ... 𝑛 ) ) ⊆ ( 𝑓 “ ( 1 ... 𝑛 ) ) → ( ( 𝐻 ↾ ( 𝑓 “ ( 1 ... 𝑛 ) ) ) ∘ ( 𝑓 ↾ ( 1 ... 𝑛 ) ) ) = ( 𝐻 ∘ ( 𝑓 ↾ ( 1 ... 𝑛 ) ) ) )
187 185 186 ax-mp ⊢ ( ( 𝐻 ↾ ( 𝑓 “ ( 1 ... 𝑛 ) ) ) ∘ ( 𝑓 ↾ ( 1 ... 𝑛 ) ) ) = ( 𝐻 ∘ ( 𝑓 ↾ ( 1 ... 𝑛 ) ) )
188 resco ⊢ ( ( 𝐻 ∘ 𝑓 ) ↾ ( 1 ... 𝑛 ) ) = ( 𝐻 ∘ ( 𝑓 ↾ ( 1 ... 𝑛 ) ) )
189 187 188 eqtr4i ⊢ ( ( 𝐻 ↾ ( 𝑓 “ ( 1 ... 𝑛 ) ) ) ∘ ( 𝑓 ↾ ( 1 ... 𝑛 ) ) ) = ( ( 𝐻 ∘ 𝑓 ) ↾ ( 1 ... 𝑛 ) )
190 189 fveq1i ⊢ ( ( ( 𝐻 ↾ ( 𝑓 “ ( 1 ... 𝑛 ) ) ) ∘ ( 𝑓 ↾ ( 1 ... 𝑛 ) ) ) ‘ 𝑘 ) = ( ( ( 𝐻 ∘ 𝑓 ) ↾ ( 1 ... 𝑛 ) ) ‘ 𝑘 )
191 fvres ⊢ ( 𝑘 ∈ ( 1 ... 𝑛 ) → ( ( ( 𝐻 ∘ 𝑓 ) ↾ ( 1 ... 𝑛 ) ) ‘ 𝑘 ) = ( ( 𝐻 ∘ 𝑓 ) ‘ 𝑘 ) )
192 190 191 eqtrid ⊢ ( 𝑘 ∈ ( 1 ... 𝑛 ) → ( ( ( 𝐻 ↾ ( 𝑓 “ ( 1 ... 𝑛 ) ) ) ∘ ( 𝑓 ↾ ( 1 ... 𝑛 ) ) ) ‘ 𝑘 ) = ( ( 𝐻 ∘ 𝑓 ) ‘ 𝑘 ) )
193 192 adantl ⊢ ( ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ 𝑊 ) ) ∧ 𝑛 ∈ ( 1 ..^ ( ♯ ‘ 𝑊 ) ) ) ∧ 𝑘 ∈ ( 1 ... 𝑛 ) ) → ( ( ( 𝐻 ↾ ( 𝑓 “ ( 1 ... 𝑛 ) ) ) ∘ ( 𝑓 ↾ ( 1 ... 𝑛 ) ) ) ‘ 𝑘 ) = ( ( 𝐻 ∘ 𝑓 ) ‘ 𝑘 ) )
194 104 193 seqfveq ⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ 𝑊 ) ) ∧ 𝑛 ∈ ( 1 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( seq 1 ( + , ( ( 𝐻 ↾ ( 𝑓 “ ( 1 ... 𝑛 ) ) ) ∘ ( 𝑓 ↾ ( 1 ... 𝑛 ) ) ) ) ‘ 𝑛 ) = ( seq 1 ( + , ( 𝐻 ∘ 𝑓 ) ) ‘ 𝑛 ) )
195 184 194 eqtr2d ⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ 𝑊 ) ) ∧ 𝑛 ∈ ( 1 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( seq 1 ( + , ( 𝐻 ∘ 𝑓 ) ) ‘ 𝑛 ) = ( 𝐺 Σg ( 𝐻 ↾ ( 𝑓 “ ( 1 ... 𝑛 ) ) ) ) )
196 fvex ⊢ ( seq 1 ( + , ( 𝐻 ∘ 𝑓 ) ) ‘ 𝑛 ) ∈ V
197 196 elsn ⊢ ( ( seq 1 ( + , ( 𝐻 ∘ 𝑓 ) ) ‘ 𝑛 ) ∈ { ( 𝐺 Σg ( 𝐻 ↾ ( 𝑓 “ ( 1 ... 𝑛 ) ) ) ) } ↔ ( seq 1 ( + , ( 𝐻 ∘ 𝑓 ) ) ‘ 𝑛 ) = ( 𝐺 Σg ( 𝐻 ↾ ( 𝑓 “ ( 1 ... 𝑛 ) ) ) ) )
198 195 197 sylibr ⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ 𝑊 ) ) ∧ 𝑛 ∈ ( 1 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( seq 1 ( + , ( 𝐻 ∘ 𝑓 ) ) ‘ 𝑛 ) ∈ { ( 𝐺 Σg ( 𝐻 ↾ ( 𝑓 “ ( 1 ... 𝑛 ) ) ) ) } )
199 3 4 cntzi ⊢ ( ( ( ( 𝐹 ∘ 𝑓 ) ‘ ( 𝑛 + 1 ) ) ∈ ( 𝑍 ‘ { ( 𝐺 Σg ( 𝐻 ↾ ( 𝑓 “ ( 1 ... 𝑛 ) ) ) ) } ) ∧ ( seq 1 ( + , ( 𝐻 ∘ 𝑓 ) ) ‘ 𝑛 ) ∈ { ( 𝐺 Σg ( 𝐻 ↾ ( 𝑓 “ ( 1 ... 𝑛 ) ) ) ) } ) → ( ( ( 𝐹 ∘ 𝑓 ) ‘ ( 𝑛 + 1 ) ) + ( seq 1 ( + , ( 𝐻 ∘ 𝑓 ) ) ‘ 𝑛 ) ) = ( ( seq 1 ( + , ( 𝐻 ∘ 𝑓 ) ) ‘ 𝑛 ) + ( ( 𝐹 ∘ 𝑓 ) ‘ ( 𝑛 + 1 ) ) ) )
200 160 198 199 syl2anc ⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ 𝑊 ) ) ∧ 𝑛 ∈ ( 1 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( ( 𝐹 ∘ 𝑓 ) ‘ ( 𝑛 + 1 ) ) + ( seq 1 ( + , ( 𝐻 ∘ 𝑓 ) ) ‘ 𝑛 ) ) = ( ( seq 1 ( + , ( 𝐻 ∘ 𝑓 ) ) ‘ 𝑛 ) + ( ( 𝐹 ∘ 𝑓 ) ‘ ( 𝑛 + 1 ) ) ) )
201 200 eqcomd ⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ 𝑊 ) ) ∧ 𝑛 ∈ ( 1 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( seq 1 ( + , ( 𝐻 ∘ 𝑓 ) ) ‘ 𝑛 ) + ( ( 𝐹 ∘ 𝑓 ) ‘ ( 𝑛 + 1 ) ) ) = ( ( ( 𝐹 ∘ 𝑓 ) ‘ ( 𝑛 + 1 ) ) + ( seq 1 ( + , ( 𝐻 ∘ 𝑓 ) ) ‘ 𝑛 ) ) )
202 1 3 102 115 118 121 123 201 mnd4g ⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ 𝑊 ) ) ∧ 𝑛 ∈ ( 1 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( ( seq 1 ( + , ( 𝐹 ∘ 𝑓 ) ) ‘ 𝑛 ) + ( seq 1 ( + , ( 𝐻 ∘ 𝑓 ) ) ‘ 𝑛 ) ) + ( ( ( 𝐹 ∘ 𝑓 ) ‘ ( 𝑛 + 1 ) ) + ( ( 𝐻 ∘ 𝑓 ) ‘ ( 𝑛 + 1 ) ) ) ) = ( ( ( seq 1 ( + , ( 𝐹 ∘ 𝑓 ) ) ‘ 𝑛 ) + ( ( 𝐹 ∘ 𝑓 ) ‘ ( 𝑛 + 1 ) ) ) + ( ( seq 1 ( + , ( 𝐻 ∘ 𝑓 ) ) ‘ 𝑛 ) + ( ( 𝐻 ∘ 𝑓 ) ‘ ( 𝑛 + 1 ) ) ) ) )
203 55 55 58 80 84 101 202 seqcaopr3 ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ 𝑊 ) ) → ( seq 1 ( + , ( ( 𝐹 ∘f + 𝐻 ) ∘ 𝑓 ) ) ‘ ( ♯ ‘ 𝑊 ) ) = ( ( seq 1 ( + , ( 𝐹 ∘ 𝑓 ) ) ‘ ( ♯ ‘ 𝑊 ) ) + ( seq 1 ( + , ( 𝐻 ∘ 𝑓 ) ) ‘ ( ♯ ‘ 𝑊 ) ) ) )
204 54 59 81 87 87 89 off ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ 𝑊 ) ) → ( 𝐹 ∘f + 𝐻 ) : 𝐴 ⟶ 𝐵 )
205 14 adantr ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ 𝑊 ) ) → ran ( 𝐹 ∘f + 𝐻 ) ⊆ ( 𝑍 ‘ ran ( 𝐹 ∘f + 𝐻 ) ) )
206 51 113 sylan ⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ 𝑊 ) ) ∧ ( 𝑘 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ) ) → ( 𝑘 + 𝑥 ) ∈ 𝐵 )
207 206 59 81 87 87 89 off ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ 𝑊 ) ) → ( 𝐹 ∘f + 𝐻 ) : 𝐴 ⟶ 𝐵 )
208 eldifi ⊢ ( 𝑥 ∈ ( 𝐴 ∖ ran 𝑓 ) → 𝑥 ∈ 𝐴 )
209 eqidd ⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ 𝑊 ) ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
210 eqidd ⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ 𝑊 ) ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝐻 ‘ 𝑥 ) = ( 𝐻 ‘ 𝑥 ) )
211 85 86 87 87 89 209 210 ofval ⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ 𝑊 ) ) ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐹 ∘f + 𝐻 ) ‘ 𝑥 ) = ( ( 𝐹 ‘ 𝑥 ) + ( 𝐻 ‘ 𝑥 ) ) )
212 208 211 sylan2 ⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ 𝑊 ) ) ∧ 𝑥 ∈ ( 𝐴 ∖ ran 𝑓 ) ) → ( ( 𝐹 ∘f + 𝐻 ) ‘ 𝑥 ) = ( ( 𝐹 ‘ 𝑥 ) + ( 𝐻 ‘ 𝑥 ) ) )
213 24 adantr ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ 𝑊 ) ) → ( 𝐹 supp 0 ) ⊆ ( ( 𝐹 ∪ 𝐻 ) supp 0 ) )
214 f1ofo ⊢ ( 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ 𝑊 → 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –onto→ 𝑊 )
215 forn ⊢ ( 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –onto→ 𝑊 → ran 𝑓 = 𝑊 )
216 214 215 syl ⊢ ( 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ 𝑊 → ran 𝑓 = 𝑊 )
217 216 9 eqtrdi ⊢ ( 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ 𝑊 → ran 𝑓 = ( ( 𝐹 ∪ 𝐻 ) supp 0 ) )
218 217 sseq2d ⊢ ( 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ 𝑊 → ( ( 𝐹 supp 0 ) ⊆ ran 𝑓 ↔ ( 𝐹 supp 0 ) ⊆ ( ( 𝐹 ∪ 𝐻 ) supp 0 ) ) )
219 218 ad2antll ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ 𝑊 ) ) → ( ( 𝐹 supp 0 ) ⊆ ran 𝑓 ↔ ( 𝐹 supp 0 ) ⊆ ( ( 𝐹 ∪ 𝐻 ) supp 0 ) ) )
220 213 219 mpbird ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ 𝑊 ) ) → ( 𝐹 supp 0 ) ⊆ ran 𝑓 )
221 21 a1i ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ 𝑊 ) ) → 0 ∈ V )
222 59 220 87 221 suppssr ⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ 𝑊 ) ) ∧ 𝑥 ∈ ( 𝐴 ∖ ran 𝑓 ) ) → ( 𝐹 ‘ 𝑥 ) = 0 )
223 33 adantr ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ 𝑊 ) ) → ( 𝐻 supp 0 ) ⊆ ( ( 𝐻 ∪ 𝐹 ) supp 0 ) )
224 223 35 sseqtrrdi ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ 𝑊 ) ) → ( 𝐻 supp 0 ) ⊆ ( ( 𝐹 ∪ 𝐻 ) supp 0 ) )
225 217 sseq2d ⊢ ( 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ 𝑊 → ( ( 𝐻 supp 0 ) ⊆ ran 𝑓 ↔ ( 𝐻 supp 0 ) ⊆ ( ( 𝐹 ∪ 𝐻 ) supp 0 ) ) )
226 225 ad2antll ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ 𝑊 ) ) → ( ( 𝐻 supp 0 ) ⊆ ran 𝑓 ↔ ( 𝐻 supp 0 ) ⊆ ( ( 𝐹 ∪ 𝐻 ) supp 0 ) ) )
227 224 226 mpbird ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ 𝑊 ) ) → ( 𝐻 supp 0 ) ⊆ ran 𝑓 )
228 81 227 87 221 suppssr ⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ 𝑊 ) ) ∧ 𝑥 ∈ ( 𝐴 ∖ ran 𝑓 ) ) → ( 𝐻 ‘ 𝑥 ) = 0 )
229 222 228 oveq12d ⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ 𝑊 ) ) ∧ 𝑥 ∈ ( 𝐴 ∖ ran 𝑓 ) ) → ( ( 𝐹 ‘ 𝑥 ) + ( 𝐻 ‘ 𝑥 ) ) = ( 0 + 0 ) )
230 19 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ 𝑊 ) ) ∧ 𝑥 ∈ ( 𝐴 ∖ ran 𝑓 ) ) → ( 0 + 0 ) = 0 )
231 212 229 230 3eqtrd ⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ 𝑊 ) ) ∧ 𝑥 ∈ ( 𝐴 ∖ ran 𝑓 ) ) → ( ( 𝐹 ∘f + 𝐻 ) ‘ 𝑥 ) = 0 )
232 207 231 suppss ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ 𝑊 ) ) → ( ( 𝐹 ∘f + 𝐻 ) supp 0 ) ⊆ ran 𝑓 )
233 ovex ⊢ ( 𝐹 ∘f + 𝐻 ) ∈ V
234 233 137 coex ⊢ ( ( 𝐹 ∘f + 𝐻 ) ∘ 𝑓 ) ∈ V
235 suppimacnv ⊢ ( ( ( ( 𝐹 ∘f + 𝐻 ) ∘ 𝑓 ) ∈ V ∧ 0 ∈ V ) → ( ( ( 𝐹 ∘f + 𝐻 ) ∘ 𝑓 ) supp 0 ) = ( ◡ ( ( 𝐹 ∘f + 𝐻 ) ∘ 𝑓 ) “ ( V ∖ { 0 } ) ) )
236 235 eqcomd ⊢ ( ( ( ( 𝐹 ∘f + 𝐻 ) ∘ 𝑓 ) ∈ V ∧ 0 ∈ V ) → ( ◡ ( ( 𝐹 ∘f + 𝐻 ) ∘ 𝑓 ) “ ( V ∖ { 0 } ) ) = ( ( ( 𝐹 ∘f + 𝐻 ) ∘ 𝑓 ) supp 0 ) )
237 234 21 236 mp2an ⊢ ( ◡ ( ( 𝐹 ∘f + 𝐻 ) ∘ 𝑓 ) “ ( V ∖ { 0 } ) ) = ( ( ( 𝐹 ∘f + 𝐻 ) ∘ 𝑓 ) supp 0 )
238 1 2 3 4 51 87 204 205 56 75 232 237 gsumval3 ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ 𝑊 ) ) → ( 𝐺 Σg ( 𝐹 ∘f + 𝐻 ) ) = ( seq 1 ( + , ( ( 𝐹 ∘f + 𝐻 ) ∘ 𝑓 ) ) ‘ ( ♯ ‘ 𝑊 ) ) )
239 12 adantr ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ 𝑊 ) ) → ran 𝐹 ⊆ ( 𝑍 ‘ ran 𝐹 ) )
240 eqid ⊢ ( ( 𝐹 ∘ 𝑓 ) supp 0 ) = ( ( 𝐹 ∘ 𝑓 ) supp 0 )
241 1 2 3 4 51 87 59 239 56 75 220 240 gsumval3 ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ 𝑊 ) ) → ( 𝐺 Σg 𝐹 ) = ( seq 1 ( + , ( 𝐹 ∘ 𝑓 ) ) ‘ ( ♯ ‘ 𝑊 ) ) )
242 13 adantr ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ 𝑊 ) ) → ran 𝐻 ⊆ ( 𝑍 ‘ ran 𝐻 ) )
243 eqid ⊢ ( ( 𝐻 ∘ 𝑓 ) supp 0 ) = ( ( 𝐻 ∘ 𝑓 ) supp 0 )
244 1 2 3 4 51 87 81 242 56 75 227 243 gsumval3 ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ 𝑊 ) ) → ( 𝐺 Σg 𝐻 ) = ( seq 1 ( + , ( 𝐻 ∘ 𝑓 ) ) ‘ ( ♯ ‘ 𝑊 ) ) )
245 241 244 oveq12d ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ 𝑊 ) ) → ( ( 𝐺 Σg 𝐹 ) + ( 𝐺 Σg 𝐻 ) ) = ( ( seq 1 ( + , ( 𝐹 ∘ 𝑓 ) ) ‘ ( ♯ ‘ 𝑊 ) ) + ( seq 1 ( + , ( 𝐻 ∘ 𝑓 ) ) ‘ ( ♯ ‘ 𝑊 ) ) ) )
246 203 238 245 3eqtr4d ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ 𝑊 ) ) → ( 𝐺 Σg ( 𝐹 ∘f + 𝐻 ) ) = ( ( 𝐺 Σg 𝐹 ) + ( 𝐺 Σg 𝐻 ) ) )
247 246 expr ⊢ ( ( 𝜑 ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ) → ( 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ 𝑊 → ( 𝐺 Σg ( 𝐹 ∘f + 𝐻 ) ) = ( ( 𝐺 Σg 𝐹 ) + ( 𝐺 Σg 𝐻 ) ) ) )
248 247 exlimdv ⊢ ( ( 𝜑 ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ) → ( ∃ 𝑓 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ 𝑊 → ( 𝐺 Σg ( 𝐹 ∘f + 𝐻 ) ) = ( ( 𝐺 Σg 𝐹 ) + ( 𝐺 Σg 𝐻 ) ) ) )
249 248 expimpd ⊢ ( 𝜑 → ( ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ ∃ 𝑓 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ 𝑊 ) → ( 𝐺 Σg ( 𝐹 ∘f + 𝐻 ) ) = ( ( 𝐺 Σg 𝐹 ) + ( 𝐺 Σg 𝐻 ) ) ) )
250 7 8 fsuppun ⊢ ( 𝜑 → ( ( 𝐹 ∪ 𝐻 ) supp 0 ) ∈ Fin )
251 9 250 eqeltrid ⊢ ( 𝜑 → 𝑊 ∈ Fin )
252 fz1f1o ⊢ ( 𝑊 ∈ Fin → ( 𝑊 = ∅ ∨ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ ∃ 𝑓 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ 𝑊 ) ) )
253 251 252 syl ⊢ ( 𝜑 → ( 𝑊 = ∅ ∨ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ ∃ 𝑓 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ 𝑊 ) ) )
254 50 249 253 mpjaod ⊢ ( 𝜑 → ( 𝐺 Σg ( 𝐹 ∘f + 𝐻 ) ) = ( ( 𝐺 Σg 𝐹 ) + ( 𝐺 Σg 𝐻 ) ) )