Metamath Proof Explorer

Theorem gsumval3lem2

Description: Lemma 2 for gsumval3 . (Contributed by AV, 31-May-2019)

Ref Expression
Hypotheses gsumval3.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
gsumval3.0 ⊢ 0 = ( 0g ‘ 𝐺 )
gsumval3.p ⊢ + = ( +g ‘ 𝐺 )
gsumval3.z ⊢ 𝑍 = ( Cntz ‘ 𝐺 )
gsumval3.g ⊢ ( 𝜑 → 𝐺 ∈ Mnd )
gsumval3.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
gsumval3.f ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
gsumval3.c ⊢ ( 𝜑 → ran 𝐹 ⊆ ( 𝑍 ‘ ran 𝐹 ) )
gsumval3.m ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
gsumval3.h ⊢ ( 𝜑 → 𝐻 : ( 1 ... 𝑀 ) –1-1→ 𝐴 )
gsumval3.n ⊢ ( 𝜑 → ( 𝐹 supp 0 ) ⊆ ran 𝐻 )
gsumval3.w ⊢ 𝑊 = ( ( 𝐹 ∘ 𝐻 ) supp 0 )
Assertion gsumval3lem2 ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( ¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑊 ) ) , 𝑊 ) ) ) → ( 𝐺 Σg 𝐹 ) = ( seq 1 ( + , ( 𝐹 ∘ ( 𝐻 ∘ 𝑓 ) ) ) ‘ ( ♯ ‘ 𝑊 ) ) )

Proof

Step Hyp Ref Expression
1 gsumval3.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 gsumval3.0 ⊢ 0 = ( 0g ‘ 𝐺 )
3 gsumval3.p ⊢ + = ( +g ‘ 𝐺 )
4 gsumval3.z ⊢ 𝑍 = ( Cntz ‘ 𝐺 )
5 gsumval3.g ⊢ ( 𝜑 → 𝐺 ∈ Mnd )
6 gsumval3.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
7 gsumval3.f ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
8 gsumval3.c ⊢ ( 𝜑 → ran 𝐹 ⊆ ( 𝑍 ‘ ran 𝐹 ) )
9 gsumval3.m ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
10 gsumval3.h ⊢ ( 𝜑 → 𝐻 : ( 1 ... 𝑀 ) –1-1→ 𝐴 )
11 gsumval3.n ⊢ ( 𝜑 → ( 𝐹 supp 0 ) ⊆ ran 𝐻 )
12 gsumval3.w ⊢ 𝑊 = ( ( 𝐹 ∘ 𝐻 ) supp 0 )
13 f1f ⊢ ( 𝐻 : ( 1 ... 𝑀 ) –1-1→ 𝐴 → 𝐻 : ( 1 ... 𝑀 ) ⟶ 𝐴 )
14 10 13 syl ⊢ ( 𝜑 → 𝐻 : ( 1 ... 𝑀 ) ⟶ 𝐴 )
15 fzfid ⊢ ( 𝜑 → ( 1 ... 𝑀 ) ∈ Fin )
16 14 15 fexd ⊢ ( 𝜑 → 𝐻 ∈ V )
17 vex ⊢ 𝑓 ∈ V
18 coexg ⊢ ( ( 𝐻 ∈ V ∧ 𝑓 ∈ V ) → ( 𝐻 ∘ 𝑓 ) ∈ V )
19 16 17 18 sylancl ⊢ ( 𝜑 → ( 𝐻 ∘ 𝑓 ) ∈ V )
20 19 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( ¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑊 ) ) , 𝑊 ) ) ) → ( 𝐻 ∘ 𝑓 ) ∈ V )
21 1 2 3 4 5 6 7 8 9 10 11 12 gsumval3lem1 ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( ¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑊 ) ) , 𝑊 ) ) ) → ( 𝐻 ∘ 𝑓 ) : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) )
22 fzfi ⊢ ( 1 ... 𝑀 ) ∈ Fin
23 suppssdm ⊢ ( ( 𝐹 ∘ 𝐻 ) supp 0 ) ⊆ dom ( 𝐹 ∘ 𝐻 )
24 12 23 eqsstri ⊢ 𝑊 ⊆ dom ( 𝐹 ∘ 𝐻 )
25 7 14 fcod ⊢ ( 𝜑 → ( 𝐹 ∘ 𝐻 ) : ( 1 ... 𝑀 ) ⟶ 𝐵 )
26 24 25 fssdm ⊢ ( 𝜑 → 𝑊 ⊆ ( 1 ... 𝑀 ) )
27 ssfi ⊢ ( ( ( 1 ... 𝑀 ) ∈ Fin ∧ 𝑊 ⊆ ( 1 ... 𝑀 ) ) → 𝑊 ∈ Fin )
28 22 26 27 sylancr ⊢ ( 𝜑 → 𝑊 ∈ Fin )
29 28 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( ¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑊 ) ) , 𝑊 ) ) ) → 𝑊 ∈ Fin )
30 10 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( ¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑊 ) ) , 𝑊 ) ) ) → 𝐻 : ( 1 ... 𝑀 ) –1-1→ 𝐴 )
31 26 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( ¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑊 ) ) , 𝑊 ) ) ) → 𝑊 ⊆ ( 1 ... 𝑀 ) )
32 f1ores ⊢ ( ( 𝐻 : ( 1 ... 𝑀 ) –1-1→ 𝐴 ∧ 𝑊 ⊆ ( 1 ... 𝑀 ) ) → ( 𝐻 ↾ 𝑊 ) : 𝑊 –1-1-onto→ ( 𝐻 “ 𝑊 ) )
33 30 31 32 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( ¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑊 ) ) , 𝑊 ) ) ) → ( 𝐻 ↾ 𝑊 ) : 𝑊 –1-1-onto→ ( 𝐻 “ 𝑊 ) )
34 12 imaeq2i ⊢ ( 𝐻 “ 𝑊 ) = ( 𝐻 “ ( ( 𝐹 ∘ 𝐻 ) supp 0 ) )
35 7 6 fexd ⊢ ( 𝜑 → 𝐹 ∈ V )
36 ovex ⊢ ( 1 ... 𝑀 ) ∈ V
37 fex ⊢ ( ( 𝐻 : ( 1 ... 𝑀 ) ⟶ 𝐴 ∧ ( 1 ... 𝑀 ) ∈ V ) → 𝐻 ∈ V )
38 14 36 37 sylancl ⊢ ( 𝜑 → 𝐻 ∈ V )
39 35 38 jca ⊢ ( 𝜑 → ( 𝐹 ∈ V ∧ 𝐻 ∈ V ) )
40 f1fun ⊢ ( 𝐻 : ( 1 ... 𝑀 ) –1-1→ 𝐴 → Fun 𝐻 )
41 10 40 syl ⊢ ( 𝜑 → Fun 𝐻 )
42 41 11 jca ⊢ ( 𝜑 → ( Fun 𝐻 ∧ ( 𝐹 supp 0 ) ⊆ ran 𝐻 ) )
43 imacosupp ⊢ ( ( 𝐹 ∈ V ∧ 𝐻 ∈ V ) → ( ( Fun 𝐻 ∧ ( 𝐹 supp 0 ) ⊆ ran 𝐻 ) → ( 𝐻 “ ( ( 𝐹 ∘ 𝐻 ) supp 0 ) ) = ( 𝐹 supp 0 ) ) )
44 39 42 43 sylc ⊢ ( 𝜑 → ( 𝐻 “ ( ( 𝐹 ∘ 𝐻 ) supp 0 ) ) = ( 𝐹 supp 0 ) )
45 44 adantr ⊢ ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) → ( 𝐻 “ ( ( 𝐹 ∘ 𝐻 ) supp 0 ) ) = ( 𝐹 supp 0 ) )
46 34 45 syl5eq ⊢ ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) → ( 𝐻 “ 𝑊 ) = ( 𝐹 supp 0 ) )
47 46 adantr ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( ¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑊 ) ) , 𝑊 ) ) ) → ( 𝐻 “ 𝑊 ) = ( 𝐹 supp 0 ) )
48 47 f1oeq3d ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( ¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑊 ) ) , 𝑊 ) ) ) → ( ( 𝐻 ↾ 𝑊 ) : 𝑊 –1-1-onto→ ( 𝐻 “ 𝑊 ) ↔ ( 𝐻 ↾ 𝑊 ) : 𝑊 –1-1-onto→ ( 𝐹 supp 0 ) ) )
49 33 48 mpbid ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( ¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑊 ) ) , 𝑊 ) ) ) → ( 𝐻 ↾ 𝑊 ) : 𝑊 –1-1-onto→ ( 𝐹 supp 0 ) )
50 29 49 hasheqf1od ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( ¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑊 ) ) , 𝑊 ) ) ) → ( ♯ ‘ 𝑊 ) = ( ♯ ‘ ( 𝐹 supp 0 ) ) )
51 50 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( ¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑊 ) ) , 𝑊 ) ) ) → ( seq 1 ( + , ( 𝐹 ∘ ( 𝐻 ∘ 𝑓 ) ) ) ‘ ( ♯ ‘ 𝑊 ) ) = ( seq 1 ( + , ( 𝐹 ∘ ( 𝐻 ∘ 𝑓 ) ) ) ‘ ( ♯ ‘ ( 𝐹 supp 0 ) ) ) )
52 21 51 jca ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( ¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑊 ) ) , 𝑊 ) ) ) → ( ( 𝐻 ∘ 𝑓 ) : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) ∧ ( seq 1 ( + , ( 𝐹 ∘ ( 𝐻 ∘ 𝑓 ) ) ) ‘ ( ♯ ‘ 𝑊 ) ) = ( seq 1 ( + , ( 𝐹 ∘ ( 𝐻 ∘ 𝑓 ) ) ) ‘ ( ♯ ‘ ( 𝐹 supp 0 ) ) ) ) )
53 f1oeq1 ⊢ ( 𝑔 = ( 𝐻 ∘ 𝑓 ) → ( 𝑔 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) ↔ ( 𝐻 ∘ 𝑓 ) : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) ) )
54 coeq2 ⊢ ( 𝑔 = ( 𝐻 ∘ 𝑓 ) → ( 𝐹 ∘ 𝑔 ) = ( 𝐹 ∘ ( 𝐻 ∘ 𝑓 ) ) )
55 54 seqeq3d ⊢ ( 𝑔 = ( 𝐻 ∘ 𝑓 ) → seq 1 ( + , ( 𝐹 ∘ 𝑔 ) ) = seq 1 ( + , ( 𝐹 ∘ ( 𝐻 ∘ 𝑓 ) ) ) )
56 55 fveq1d ⊢ ( 𝑔 = ( 𝐻 ∘ 𝑓 ) → ( seq 1 ( + , ( 𝐹 ∘ 𝑔 ) ) ‘ ( ♯ ‘ ( 𝐹 supp 0 ) ) ) = ( seq 1 ( + , ( 𝐹 ∘ ( 𝐻 ∘ 𝑓 ) ) ) ‘ ( ♯ ‘ ( 𝐹 supp 0 ) ) ) )
57 56 eqeq2d ⊢ ( 𝑔 = ( 𝐻 ∘ 𝑓 ) → ( ( seq 1 ( + , ( 𝐹 ∘ ( 𝐻 ∘ 𝑓 ) ) ) ‘ ( ♯ ‘ 𝑊 ) ) = ( seq 1 ( + , ( 𝐹 ∘ 𝑔 ) ) ‘ ( ♯ ‘ ( 𝐹 supp 0 ) ) ) ↔ ( seq 1 ( + , ( 𝐹 ∘ ( 𝐻 ∘ 𝑓 ) ) ) ‘ ( ♯ ‘ 𝑊 ) ) = ( seq 1 ( + , ( 𝐹 ∘ ( 𝐻 ∘ 𝑓 ) ) ) ‘ ( ♯ ‘ ( 𝐹 supp 0 ) ) ) ) )
58 53 57 anbi12d ⊢ ( 𝑔 = ( 𝐻 ∘ 𝑓 ) → ( ( 𝑔 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) ∧ ( seq 1 ( + , ( 𝐹 ∘ ( 𝐻 ∘ 𝑓 ) ) ) ‘ ( ♯ ‘ 𝑊 ) ) = ( seq 1 ( + , ( 𝐹 ∘ 𝑔 ) ) ‘ ( ♯ ‘ ( 𝐹 supp 0 ) ) ) ) ↔ ( ( 𝐻 ∘ 𝑓 ) : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) ∧ ( seq 1 ( + , ( 𝐹 ∘ ( 𝐻 ∘ 𝑓 ) ) ) ‘ ( ♯ ‘ 𝑊 ) ) = ( seq 1 ( + , ( 𝐹 ∘ ( 𝐻 ∘ 𝑓 ) ) ) ‘ ( ♯ ‘ ( 𝐹 supp 0 ) ) ) ) ) )
59 20 52 58 spcedv ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( ¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑊 ) ) , 𝑊 ) ) ) → ∃ 𝑔 ( 𝑔 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) ∧ ( seq 1 ( + , ( 𝐹 ∘ ( 𝐻 ∘ 𝑓 ) ) ) ‘ ( ♯ ‘ 𝑊 ) ) = ( seq 1 ( + , ( 𝐹 ∘ 𝑔 ) ) ‘ ( ♯ ‘ ( 𝐹 supp 0 ) ) ) ) )
60 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( ¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑊 ) ) , 𝑊 ) ) ) → 𝐺 ∈ Mnd )
61 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( ¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑊 ) ) , 𝑊 ) ) ) → 𝐴 ∈ 𝑉 )
62 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( ¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑊 ) ) , 𝑊 ) ) ) → 𝐹 : 𝐴 ⟶ 𝐵 )
63 8 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( ¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑊 ) ) , 𝑊 ) ) ) → ran 𝐹 ⊆ ( 𝑍 ‘ ran 𝐹 ) )
64 f1f1orn ⊢ ( 𝐻 : ( 1 ... 𝑀 ) –1-1→ 𝐴 → 𝐻 : ( 1 ... 𝑀 ) –1-1-onto→ ran 𝐻 )
65 10 64 syl ⊢ ( 𝜑 → 𝐻 : ( 1 ... 𝑀 ) –1-1-onto→ ran 𝐻 )
66 f1oen3g ⊢ ( ( 𝐻 ∈ V ∧ 𝐻 : ( 1 ... 𝑀 ) –1-1-onto→ ran 𝐻 ) → ( 1 ... 𝑀 ) ≈ ran 𝐻 )
67 16 65 66 syl2anc ⊢ ( 𝜑 → ( 1 ... 𝑀 ) ≈ ran 𝐻 )
68 enfi ⊢ ( ( 1 ... 𝑀 ) ≈ ran 𝐻 → ( ( 1 ... 𝑀 ) ∈ Fin ↔ ran 𝐻 ∈ Fin ) )
69 67 68 syl ⊢ ( 𝜑 → ( ( 1 ... 𝑀 ) ∈ Fin ↔ ran 𝐻 ∈ Fin ) )
70 22 69 mpbii ⊢ ( 𝜑 → ran 𝐻 ∈ Fin )
71 70 11 ssfid ⊢ ( 𝜑 → ( 𝐹 supp 0 ) ∈ Fin )
72 71 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( ¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑊 ) ) , 𝑊 ) ) ) → ( 𝐹 supp 0 ) ∈ Fin )
73 12 neeq1i ⊢ ( 𝑊 ≠ ∅ ↔ ( ( 𝐹 ∘ 𝐻 ) supp 0 ) ≠ ∅ )
74 supp0cosupp0 ⊢ ( ( 𝐹 ∈ V ∧ 𝐻 ∈ V ) → ( ( 𝐹 supp 0 ) = ∅ → ( ( 𝐹 ∘ 𝐻 ) supp 0 ) = ∅ ) )
75 74 necon3d ⊢ ( ( 𝐹 ∈ V ∧ 𝐻 ∈ V ) → ( ( ( 𝐹 ∘ 𝐻 ) supp 0 ) ≠ ∅ → ( 𝐹 supp 0 ) ≠ ∅ ) )
76 35 38 75 syl2anc ⊢ ( 𝜑 → ( ( ( 𝐹 ∘ 𝐻 ) supp 0 ) ≠ ∅ → ( 𝐹 supp 0 ) ≠ ∅ ) )
77 73 76 syl5bi ⊢ ( 𝜑 → ( 𝑊 ≠ ∅ → ( 𝐹 supp 0 ) ≠ ∅ ) )
78 77 imp ⊢ ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) → ( 𝐹 supp 0 ) ≠ ∅ )
79 78 adantr ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( ¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑊 ) ) , 𝑊 ) ) ) → ( 𝐹 supp 0 ) ≠ ∅ )
80 11 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( ¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑊 ) ) , 𝑊 ) ) ) → ( 𝐹 supp 0 ) ⊆ ran 𝐻 )
81 14 frnd ⊢ ( 𝜑 → ran 𝐻 ⊆ 𝐴 )
82 81 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( ¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑊 ) ) , 𝑊 ) ) ) → ran 𝐻 ⊆ 𝐴 )
83 80 82 sstrd ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( ¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑊 ) ) , 𝑊 ) ) ) → ( 𝐹 supp 0 ) ⊆ 𝐴 )
84 1 2 3 4 60 61 62 63 72 79 83 gsumval3eu ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( ¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑊 ) ) , 𝑊 ) ) ) → ∃! 𝑥 ∃ 𝑔 ( 𝑔 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) ∧ 𝑥 = ( seq 1 ( + , ( 𝐹 ∘ 𝑔 ) ) ‘ ( ♯ ‘ ( 𝐹 supp 0 ) ) ) ) )
85 iota1 ⊢ ( ∃! 𝑥 ∃ 𝑔 ( 𝑔 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) ∧ 𝑥 = ( seq 1 ( + , ( 𝐹 ∘ 𝑔 ) ) ‘ ( ♯ ‘ ( 𝐹 supp 0 ) ) ) ) → ( ∃ 𝑔 ( 𝑔 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) ∧ 𝑥 = ( seq 1 ( + , ( 𝐹 ∘ 𝑔 ) ) ‘ ( ♯ ‘ ( 𝐹 supp 0 ) ) ) ) ↔ ( ℩ 𝑥 ∃ 𝑔 ( 𝑔 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) ∧ 𝑥 = ( seq 1 ( + , ( 𝐹 ∘ 𝑔 ) ) ‘ ( ♯ ‘ ( 𝐹 supp 0 ) ) ) ) ) = 𝑥 ) )
86 84 85 syl ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( ¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑊 ) ) , 𝑊 ) ) ) → ( ∃ 𝑔 ( 𝑔 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) ∧ 𝑥 = ( seq 1 ( + , ( 𝐹 ∘ 𝑔 ) ) ‘ ( ♯ ‘ ( 𝐹 supp 0 ) ) ) ) ↔ ( ℩ 𝑥 ∃ 𝑔 ( 𝑔 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) ∧ 𝑥 = ( seq 1 ( + , ( 𝐹 ∘ 𝑔 ) ) ‘ ( ♯ ‘ ( 𝐹 supp 0 ) ) ) ) ) = 𝑥 ) )
87 eqid ⊢ ( 𝐹 supp 0 ) = ( 𝐹 supp 0 )
88 simprl ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( ¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑊 ) ) , 𝑊 ) ) ) → ¬ 𝐴 ∈ ran ... )
89 1 2 3 4 60 61 62 63 72 79 87 88 gsumval3a ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( ¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑊 ) ) , 𝑊 ) ) ) → ( 𝐺 Σg 𝐹 ) = ( ℩ 𝑥 ∃ 𝑔 ( 𝑔 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) ∧ 𝑥 = ( seq 1 ( + , ( 𝐹 ∘ 𝑔 ) ) ‘ ( ♯ ‘ ( 𝐹 supp 0 ) ) ) ) ) )
90 89 eqeq1d ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( ¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑊 ) ) , 𝑊 ) ) ) → ( ( 𝐺 Σg 𝐹 ) = 𝑥 ↔ ( ℩ 𝑥 ∃ 𝑔 ( 𝑔 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) ∧ 𝑥 = ( seq 1 ( + , ( 𝐹 ∘ 𝑔 ) ) ‘ ( ♯ ‘ ( 𝐹 supp 0 ) ) ) ) ) = 𝑥 ) )
91 86 90 bitr4d ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( ¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑊 ) ) , 𝑊 ) ) ) → ( ∃ 𝑔 ( 𝑔 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) ∧ 𝑥 = ( seq 1 ( + , ( 𝐹 ∘ 𝑔 ) ) ‘ ( ♯ ‘ ( 𝐹 supp 0 ) ) ) ) ↔ ( 𝐺 Σg 𝐹 ) = 𝑥 ) )
92 91 alrimiv ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( ¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑊 ) ) , 𝑊 ) ) ) → ∀ 𝑥 ( ∃ 𝑔 ( 𝑔 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) ∧ 𝑥 = ( seq 1 ( + , ( 𝐹 ∘ 𝑔 ) ) ‘ ( ♯ ‘ ( 𝐹 supp 0 ) ) ) ) ↔ ( 𝐺 Σg 𝐹 ) = 𝑥 ) )
93 fvex ⊢ ( seq 1 ( + , ( 𝐹 ∘ ( 𝐻 ∘ 𝑓 ) ) ) ‘ ( ♯ ‘ 𝑊 ) ) ∈ V
94 eqeq1 ⊢ ( 𝑥 = ( seq 1 ( + , ( 𝐹 ∘ ( 𝐻 ∘ 𝑓 ) ) ) ‘ ( ♯ ‘ 𝑊 ) ) → ( 𝑥 = ( seq 1 ( + , ( 𝐹 ∘ 𝑔 ) ) ‘ ( ♯ ‘ ( 𝐹 supp 0 ) ) ) ↔ ( seq 1 ( + , ( 𝐹 ∘ ( 𝐻 ∘ 𝑓 ) ) ) ‘ ( ♯ ‘ 𝑊 ) ) = ( seq 1 ( + , ( 𝐹 ∘ 𝑔 ) ) ‘ ( ♯ ‘ ( 𝐹 supp 0 ) ) ) ) )
95 94 anbi2d ⊢ ( 𝑥 = ( seq 1 ( + , ( 𝐹 ∘ ( 𝐻 ∘ 𝑓 ) ) ) ‘ ( ♯ ‘ 𝑊 ) ) → ( ( 𝑔 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) ∧ 𝑥 = ( seq 1 ( + , ( 𝐹 ∘ 𝑔 ) ) ‘ ( ♯ ‘ ( 𝐹 supp 0 ) ) ) ) ↔ ( 𝑔 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) ∧ ( seq 1 ( + , ( 𝐹 ∘ ( 𝐻 ∘ 𝑓 ) ) ) ‘ ( ♯ ‘ 𝑊 ) ) = ( seq 1 ( + , ( 𝐹 ∘ 𝑔 ) ) ‘ ( ♯ ‘ ( 𝐹 supp 0 ) ) ) ) ) )
96 95 exbidv ⊢ ( 𝑥 = ( seq 1 ( + , ( 𝐹 ∘ ( 𝐻 ∘ 𝑓 ) ) ) ‘ ( ♯ ‘ 𝑊 ) ) → ( ∃ 𝑔 ( 𝑔 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) ∧ 𝑥 = ( seq 1 ( + , ( 𝐹 ∘ 𝑔 ) ) ‘ ( ♯ ‘ ( 𝐹 supp 0 ) ) ) ) ↔ ∃ 𝑔 ( 𝑔 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) ∧ ( seq 1 ( + , ( 𝐹 ∘ ( 𝐻 ∘ 𝑓 ) ) ) ‘ ( ♯ ‘ 𝑊 ) ) = ( seq 1 ( + , ( 𝐹 ∘ 𝑔 ) ) ‘ ( ♯ ‘ ( 𝐹 supp 0 ) ) ) ) ) )
97 eqeq2 ⊢ ( 𝑥 = ( seq 1 ( + , ( 𝐹 ∘ ( 𝐻 ∘ 𝑓 ) ) ) ‘ ( ♯ ‘ 𝑊 ) ) → ( ( 𝐺 Σg 𝐹 ) = 𝑥 ↔ ( 𝐺 Σg 𝐹 ) = ( seq 1 ( + , ( 𝐹 ∘ ( 𝐻 ∘ 𝑓 ) ) ) ‘ ( ♯ ‘ 𝑊 ) ) ) )
98 96 97 bibi12d ⊢ ( 𝑥 = ( seq 1 ( + , ( 𝐹 ∘ ( 𝐻 ∘ 𝑓 ) ) ) ‘ ( ♯ ‘ 𝑊 ) ) → ( ( ∃ 𝑔 ( 𝑔 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) ∧ 𝑥 = ( seq 1 ( + , ( 𝐹 ∘ 𝑔 ) ) ‘ ( ♯ ‘ ( 𝐹 supp 0 ) ) ) ) ↔ ( 𝐺 Σg 𝐹 ) = 𝑥 ) ↔ ( ∃ 𝑔 ( 𝑔 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) ∧ ( seq 1 ( + , ( 𝐹 ∘ ( 𝐻 ∘ 𝑓 ) ) ) ‘ ( ♯ ‘ 𝑊 ) ) = ( seq 1 ( + , ( 𝐹 ∘ 𝑔 ) ) ‘ ( ♯ ‘ ( 𝐹 supp 0 ) ) ) ) ↔ ( 𝐺 Σg 𝐹 ) = ( seq 1 ( + , ( 𝐹 ∘ ( 𝐻 ∘ 𝑓 ) ) ) ‘ ( ♯ ‘ 𝑊 ) ) ) ) )
99 93 98 spcv ⊢ ( ∀ 𝑥 ( ∃ 𝑔 ( 𝑔 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) ∧ 𝑥 = ( seq 1 ( + , ( 𝐹 ∘ 𝑔 ) ) ‘ ( ♯ ‘ ( 𝐹 supp 0 ) ) ) ) ↔ ( 𝐺 Σg 𝐹 ) = 𝑥 ) → ( ∃ 𝑔 ( 𝑔 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) ∧ ( seq 1 ( + , ( 𝐹 ∘ ( 𝐻 ∘ 𝑓 ) ) ) ‘ ( ♯ ‘ 𝑊 ) ) = ( seq 1 ( + , ( 𝐹 ∘ 𝑔 ) ) ‘ ( ♯ ‘ ( 𝐹 supp 0 ) ) ) ) ↔ ( 𝐺 Σg 𝐹 ) = ( seq 1 ( + , ( 𝐹 ∘ ( 𝐻 ∘ 𝑓 ) ) ) ‘ ( ♯ ‘ 𝑊 ) ) ) )
100 92 99 syl ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( ¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑊 ) ) , 𝑊 ) ) ) → ( ∃ 𝑔 ( 𝑔 : ( 1 ... ( ♯ ‘ ( 𝐹 supp 0 ) ) ) –1-1-onto→ ( 𝐹 supp 0 ) ∧ ( seq 1 ( + , ( 𝐹 ∘ ( 𝐻 ∘ 𝑓 ) ) ) ‘ ( ♯ ‘ 𝑊 ) ) = ( seq 1 ( + , ( 𝐹 ∘ 𝑔 ) ) ‘ ( ♯ ‘ ( 𝐹 supp 0 ) ) ) ) ↔ ( 𝐺 Σg 𝐹 ) = ( seq 1 ( + , ( 𝐹 ∘ ( 𝐻 ∘ 𝑓 ) ) ) ‘ ( ♯ ‘ 𝑊 ) ) ) )
101 59 100 mpbid ⊢ ( ( ( 𝜑 ∧ 𝑊 ≠ ∅ ) ∧ ( ¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑊 ) ) , 𝑊 ) ) ) → ( 𝐺 Σg 𝐹 ) = ( seq 1 ( + , ( 𝐹 ∘ ( 𝐻 ∘ 𝑓 ) ) ) ‘ ( ♯ ‘ 𝑊 ) ) )