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