Metamath Proof Explorer

Theorem gsumhashmul

Description: Express a group sum by grouping by nonzero values. (Contributed by Thierry Arnoux, 22-Jun-2024)

Ref Expression
Hypotheses gsumhashmul.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
gsumhashmul.z ⊢ 0 = ( 0g ‘ 𝐺 )
gsumhashmul.x ⊢ · = ( .g ‘ 𝐺 )
gsumhashmul.g ⊢ ( 𝜑 → 𝐺 ∈ CMnd )
gsumhashmul.f ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
gsumhashmul.1 ⊢ ( 𝜑 → 𝐹 finSupp 0 )
Assertion gsumhashmul ( 𝜑 → ( 𝐺 Σg 𝐹 ) = ( 𝐺 Σg ( 𝑥 ∈ ( ran 𝐹 ∖ { 0 } ) ↦ ( ( ♯ ‘ ( ◡ 𝐹 “ { 𝑥 } ) ) · 𝑥 ) ) ) )

Proof

Step Hyp Ref Expression
1 gsumhashmul.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 gsumhashmul.z ⊢ 0 = ( 0g ‘ 𝐺 )
3 gsumhashmul.x ⊢ · = ( .g ‘ 𝐺 )
4 gsumhashmul.g ⊢ ( 𝜑 → 𝐺 ∈ CMnd )
5 gsumhashmul.f ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
6 gsumhashmul.1 ⊢ ( 𝜑 → 𝐹 finSupp 0 )
7 suppssdm ⊢ ( 𝐹 supp 0 ) ⊆ dom 𝐹
8 7 5 fssdm ⊢ ( 𝜑 → ( 𝐹 supp 0 ) ⊆ 𝐴 )
9 5 8 feqresmpt ⊢ ( 𝜑 → ( 𝐹 ↾ ( 𝐹 supp 0 ) ) = ( 𝑥 ∈ ( 𝐹 supp 0 ) ↦ ( 𝐹 ‘ 𝑥 ) ) )
10 9 oveq2d ⊢ ( 𝜑 → ( 𝐺 Σg ( 𝐹 ↾ ( 𝐹 supp 0 ) ) ) = ( 𝐺 Σg ( 𝑥 ∈ ( 𝐹 supp 0 ) ↦ ( 𝐹 ‘ 𝑥 ) ) ) )
11 relfsupp ⊢ Rel finSupp
12 11 brrelex1i ⊢ ( 𝐹 finSupp 0 → 𝐹 ∈ V )
13 6 12 syl ⊢ ( 𝜑 → 𝐹 ∈ V )
14 5 ffnd ⊢ ( 𝜑 → 𝐹 Fn 𝐴 )
15 13 14 fndmexd ⊢ ( 𝜑 → 𝐴 ∈ V )
16 ssidd ⊢ ( 𝜑 → ( 𝐹 supp 0 ) ⊆ ( 𝐹 supp 0 ) )
17 1 2 4 15 5 16 6 gsumres ⊢ ( 𝜑 → ( 𝐺 Σg ( 𝐹 ↾ ( 𝐹 supp 0 ) ) ) = ( 𝐺 Σg 𝐹 ) )
18 nfcv ⊢ Ⅎ 𝑥 ( 𝐹 ‘ ( 1st ‘ 𝑧 ) )
19 fveq2 ⊢ ( 𝑥 = ( 1st ‘ 𝑧 ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ ( 1st ‘ 𝑧 ) ) )
20 6 fsuppimpd ⊢ ( 𝜑 → ( 𝐹 supp 0 ) ∈ Fin )
21 ssidd ⊢ ( 𝜑 → 𝐵 ⊆ 𝐵 )
22 5 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐹 supp 0 ) ) → 𝐹 : 𝐴 ⟶ 𝐵 )
23 8 sselda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐹 supp 0 ) ) → 𝑥 ∈ 𝐴 )
24 22 23 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐹 supp 0 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 )
25 5 ffund ⊢ ( 𝜑 → Fun 𝐹 )
26 funrel ⊢ ( Fun 𝐹 → Rel 𝐹 )
27 reldif ⊢ ( Rel 𝐹 → Rel ( 𝐹 ∖ ( V × { 0 } ) ) )
28 25 26 27 3syl ⊢ ( 𝜑 → Rel ( 𝐹 ∖ ( V × { 0 } ) ) )
29 1stdm ⊢ ( ( Rel ( 𝐹 ∖ ( V × { 0 } ) ) ∧ 𝑧 ∈ ( 𝐹 ∖ ( V × { 0 } ) ) ) → ( 1st ‘ 𝑧 ) ∈ dom ( 𝐹 ∖ ( V × { 0 } ) ) )
30 28 29 sylan ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐹 ∖ ( V × { 0 } ) ) ) → ( 1st ‘ 𝑧 ) ∈ dom ( 𝐹 ∖ ( V × { 0 } ) ) )
31 2 fvexi ⊢ 0 ∈ V
32 31 a1i ⊢ ( 𝜑 → 0 ∈ V )
33 fressupp ⊢ ( ( Fun 𝐹 ∧ 𝐹 ∈ V ∧ 0 ∈ V ) → ( 𝐹 ↾ ( 𝐹 supp 0 ) ) = ( 𝐹 ∖ ( V × { 0 } ) ) )
34 25 13 32 33 syl3anc ⊢ ( 𝜑 → ( 𝐹 ↾ ( 𝐹 supp 0 ) ) = ( 𝐹 ∖ ( V × { 0 } ) ) )
35 34 dmeqd ⊢ ( 𝜑 → dom ( 𝐹 ↾ ( 𝐹 supp 0 ) ) = dom ( 𝐹 ∖ ( V × { 0 } ) ) )
36 7 a1i ⊢ ( 𝜑 → ( 𝐹 supp 0 ) ⊆ dom 𝐹 )
37 ssdmres ⊢ ( ( 𝐹 supp 0 ) ⊆ dom 𝐹 ↔ dom ( 𝐹 ↾ ( 𝐹 supp 0 ) ) = ( 𝐹 supp 0 ) )
38 36 37 sylib ⊢ ( 𝜑 → dom ( 𝐹 ↾ ( 𝐹 supp 0 ) ) = ( 𝐹 supp 0 ) )
39 35 38 eqtr3d ⊢ ( 𝜑 → dom ( 𝐹 ∖ ( V × { 0 } ) ) = ( 𝐹 supp 0 ) )
40 39 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐹 ∖ ( V × { 0 } ) ) ) → dom ( 𝐹 ∖ ( V × { 0 } ) ) = ( 𝐹 supp 0 ) )
41 30 40 eleqtrd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐹 ∖ ( V × { 0 } ) ) ) → ( 1st ‘ 𝑧 ) ∈ ( 𝐹 supp 0 ) )
42 25 funresd ⊢ ( 𝜑 → Fun ( 𝐹 ↾ ( 𝐹 supp 0 ) ) )
43 42 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐹 supp 0 ) ) → Fun ( 𝐹 ↾ ( 𝐹 supp 0 ) ) )
44 38 eleq2d ⊢ ( 𝜑 → ( 𝑥 ∈ dom ( 𝐹 ↾ ( 𝐹 supp 0 ) ) ↔ 𝑥 ∈ ( 𝐹 supp 0 ) ) )
45 44 biimpar ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐹 supp 0 ) ) → 𝑥 ∈ dom ( 𝐹 ↾ ( 𝐹 supp 0 ) ) )
46 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐹 supp 0 ) ) → 𝑥 ∈ ( 𝐹 supp 0 ) )
47 46 fvresd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐹 supp 0 ) ) → ( ( 𝐹 ↾ ( 𝐹 supp 0 ) ) ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
48 funopfvb ⊢ ( ( Fun ( 𝐹 ↾ ( 𝐹 supp 0 ) ) ∧ 𝑥 ∈ dom ( 𝐹 ↾ ( 𝐹 supp 0 ) ) ) → ( ( ( 𝐹 ↾ ( 𝐹 supp 0 ) ) ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) ↔ ⟨ 𝑥 , ( 𝐹 ‘ 𝑥 ) ⟩ ∈ ( 𝐹 ↾ ( 𝐹 supp 0 ) ) ) )
49 48 biimpa ⊢ ( ( ( Fun ( 𝐹 ↾ ( 𝐹 supp 0 ) ) ∧ 𝑥 ∈ dom ( 𝐹 ↾ ( 𝐹 supp 0 ) ) ) ∧ ( ( 𝐹 ↾ ( 𝐹 supp 0 ) ) ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) ) → ⟨ 𝑥 , ( 𝐹 ‘ 𝑥 ) ⟩ ∈ ( 𝐹 ↾ ( 𝐹 supp 0 ) ) )
50 43 45 47 49 syl21anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐹 supp 0 ) ) → ⟨ 𝑥 , ( 𝐹 ‘ 𝑥 ) ⟩ ∈ ( 𝐹 ↾ ( 𝐹 supp 0 ) ) )
51 34 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐹 supp 0 ) ) → ( 𝐹 ↾ ( 𝐹 supp 0 ) ) = ( 𝐹 ∖ ( V × { 0 } ) ) )
52 50 51 eleqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐹 supp 0 ) ) → ⟨ 𝑥 , ( 𝐹 ‘ 𝑥 ) ⟩ ∈ ( 𝐹 ∖ ( V × { 0 } ) ) )
53 eqeq2 ⊢ ( 𝑣 = ⟨ 𝑥 , ( 𝐹 ‘ 𝑥 ) ⟩ → ( 𝑧 = 𝑣 ↔ 𝑧 = ⟨ 𝑥 , ( 𝐹 ‘ 𝑥 ) ⟩ ) )
54 53 bibi2d ⊢ ( 𝑣 = ⟨ 𝑥 , ( 𝐹 ‘ 𝑥 ) ⟩ → ( ( 𝑥 = ( 1st ‘ 𝑧 ) ↔ 𝑧 = 𝑣 ) ↔ ( 𝑥 = ( 1st ‘ 𝑧 ) ↔ 𝑧 = ⟨ 𝑥 , ( 𝐹 ‘ 𝑥 ) ⟩ ) ) )
55 54 ralbidv ⊢ ( 𝑣 = ⟨ 𝑥 , ( 𝐹 ‘ 𝑥 ) ⟩ → ( ∀ 𝑧 ∈ ( 𝐹 ∖ ( V × { 0 } ) ) ( 𝑥 = ( 1st ‘ 𝑧 ) ↔ 𝑧 = 𝑣 ) ↔ ∀ 𝑧 ∈ ( 𝐹 ∖ ( V × { 0 } ) ) ( 𝑥 = ( 1st ‘ 𝑧 ) ↔ 𝑧 = ⟨ 𝑥 , ( 𝐹 ‘ 𝑥 ) ⟩ ) ) )
56 55 adantl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐹 supp 0 ) ) ∧ 𝑣 = ⟨ 𝑥 , ( 𝐹 ‘ 𝑥 ) ⟩ ) → ( ∀ 𝑧 ∈ ( 𝐹 ∖ ( V × { 0 } ) ) ( 𝑥 = ( 1st ‘ 𝑧 ) ↔ 𝑧 = 𝑣 ) ↔ ∀ 𝑧 ∈ ( 𝐹 ∖ ( V × { 0 } ) ) ( 𝑥 = ( 1st ‘ 𝑧 ) ↔ 𝑧 = ⟨ 𝑥 , ( 𝐹 ‘ 𝑥 ) ⟩ ) ) )
57 fvexd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐹 supp 0 ) ) ∧ 𝑧 ∈ ( 𝐹 ∖ ( V × { 0 } ) ) ) ∧ 𝑥 = ( 1st ‘ 𝑧 ) ) → ( 2nd ‘ 𝑧 ) ∈ V )
58 28 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐹 supp 0 ) ) ∧ 𝑧 ∈ ( 𝐹 ∖ ( V × { 0 } ) ) ) ∧ 𝑥 = ( 1st ‘ 𝑧 ) ) → Rel ( 𝐹 ∖ ( V × { 0 } ) ) )
59 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐹 supp 0 ) ) ∧ 𝑧 ∈ ( 𝐹 ∖ ( V × { 0 } ) ) ) ∧ 𝑥 = ( 1st ‘ 𝑧 ) ) → 𝑧 ∈ ( 𝐹 ∖ ( V × { 0 } ) ) )
60 1st2nd ⊢ ( ( Rel ( 𝐹 ∖ ( V × { 0 } ) ) ∧ 𝑧 ∈ ( 𝐹 ∖ ( V × { 0 } ) ) ) → 𝑧 = ⟨ ( 1st ‘ 𝑧 ) , ( 2nd ‘ 𝑧 ) ⟩ )
61 58 59 60 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐹 supp 0 ) ) ∧ 𝑧 ∈ ( 𝐹 ∖ ( V × { 0 } ) ) ) ∧ 𝑥 = ( 1st ‘ 𝑧 ) ) → 𝑧 = ⟨ ( 1st ‘ 𝑧 ) , ( 2nd ‘ 𝑧 ) ⟩ )
62 opeq1 ⊢ ( 𝑥 = ( 1st ‘ 𝑧 ) → ⟨ 𝑥 , ( 2nd ‘ 𝑧 ) ⟩ = ⟨ ( 1st ‘ 𝑧 ) , ( 2nd ‘ 𝑧 ) ⟩ )
63 62 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐹 supp 0 ) ) ∧ 𝑧 ∈ ( 𝐹 ∖ ( V × { 0 } ) ) ) ∧ 𝑥 = ( 1st ‘ 𝑧 ) ) → ⟨ 𝑥 , ( 2nd ‘ 𝑧 ) ⟩ = ⟨ ( 1st ‘ 𝑧 ) , ( 2nd ‘ 𝑧 ) ⟩ )
64 61 63 eqtr4d ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐹 supp 0 ) ) ∧ 𝑧 ∈ ( 𝐹 ∖ ( V × { 0 } ) ) ) ∧ 𝑥 = ( 1st ‘ 𝑧 ) ) → 𝑧 = ⟨ 𝑥 , ( 2nd ‘ 𝑧 ) ⟩ )
65 difssd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐹 supp 0 ) ) → ( 𝐹 ∖ ( V × { 0 } ) ) ⊆ 𝐹 )
66 65 sselda ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐹 supp 0 ) ) ∧ 𝑧 ∈ ( 𝐹 ∖ ( V × { 0 } ) ) ) → 𝑧 ∈ 𝐹 )
67 66 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐹 supp 0 ) ) ∧ 𝑧 ∈ ( 𝐹 ∖ ( V × { 0 } ) ) ) ∧ 𝑥 = ( 1st ‘ 𝑧 ) ) → 𝑧 ∈ 𝐹 )
68 64 67 eqeltrrd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐹 supp 0 ) ) ∧ 𝑧 ∈ ( 𝐹 ∖ ( V × { 0 } ) ) ) ∧ 𝑥 = ( 1st ‘ 𝑧 ) ) → ⟨ 𝑥 , ( 2nd ‘ 𝑧 ) ⟩ ∈ 𝐹 )
69 64 68 jca ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐹 supp 0 ) ) ∧ 𝑧 ∈ ( 𝐹 ∖ ( V × { 0 } ) ) ) ∧ 𝑥 = ( 1st ‘ 𝑧 ) ) → ( 𝑧 = ⟨ 𝑥 , ( 2nd ‘ 𝑧 ) ⟩ ∧ ⟨ 𝑥 , ( 2nd ‘ 𝑧 ) ⟩ ∈ 𝐹 ) )
70 opeq2 ⊢ ( 𝑦 = ( 2nd ‘ 𝑧 ) → ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑥 , ( 2nd ‘ 𝑧 ) ⟩ )
71 70 eqeq2d ⊢ ( 𝑦 = ( 2nd ‘ 𝑧 ) → ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ↔ 𝑧 = ⟨ 𝑥 , ( 2nd ‘ 𝑧 ) ⟩ ) )
72 70 eleq1d ⊢ ( 𝑦 = ( 2nd ‘ 𝑧 ) → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ↔ ⟨ 𝑥 , ( 2nd ‘ 𝑧 ) ⟩ ∈ 𝐹 ) )
73 71 72 anbi12d ⊢ ( 𝑦 = ( 2nd ‘ 𝑧 ) → ( ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ) ↔ ( 𝑧 = ⟨ 𝑥 , ( 2nd ‘ 𝑧 ) ⟩ ∧ ⟨ 𝑥 , ( 2nd ‘ 𝑧 ) ⟩ ∈ 𝐹 ) ) )
74 57 69 73 spcedv ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐹 supp 0 ) ) ∧ 𝑧 ∈ ( 𝐹 ∖ ( V × { 0 } ) ) ) ∧ 𝑥 = ( 1st ‘ 𝑧 ) ) → ∃ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ) )
75 vex ⊢ 𝑥 ∈ V
76 75 elsnres ⊢ ( 𝑧 ∈ ( 𝐹 ↾ { 𝑥 } ) ↔ ∃ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ) )
77 74 76 sylibr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐹 supp 0 ) ) ∧ 𝑧 ∈ ( 𝐹 ∖ ( V × { 0 } ) ) ) ∧ 𝑥 = ( 1st ‘ 𝑧 ) ) → 𝑧 ∈ ( 𝐹 ↾ { 𝑥 } ) )
78 14 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐹 supp 0 ) ) ∧ 𝑧 ∈ ( 𝐹 ∖ ( V × { 0 } ) ) ) ∧ 𝑥 = ( 1st ‘ 𝑧 ) ) → 𝐹 Fn 𝐴 )
79 23 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐹 supp 0 ) ) ∧ 𝑧 ∈ ( 𝐹 ∖ ( V × { 0 } ) ) ) ∧ 𝑥 = ( 1st ‘ 𝑧 ) ) → 𝑥 ∈ 𝐴 )
80 fnressn ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ↾ { 𝑥 } ) = { ⟨ 𝑥 , ( 𝐹 ‘ 𝑥 ) ⟩ } )
81 78 79 80 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐹 supp 0 ) ) ∧ 𝑧 ∈ ( 𝐹 ∖ ( V × { 0 } ) ) ) ∧ 𝑥 = ( 1st ‘ 𝑧 ) ) → ( 𝐹 ↾ { 𝑥 } ) = { ⟨ 𝑥 , ( 𝐹 ‘ 𝑥 ) ⟩ } )
82 77 81 eleqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐹 supp 0 ) ) ∧ 𝑧 ∈ ( 𝐹 ∖ ( V × { 0 } ) ) ) ∧ 𝑥 = ( 1st ‘ 𝑧 ) ) → 𝑧 ∈ { ⟨ 𝑥 , ( 𝐹 ‘ 𝑥 ) ⟩ } )
83 elsni ⊢ ( 𝑧 ∈ { ⟨ 𝑥 , ( 𝐹 ‘ 𝑥 ) ⟩ } → 𝑧 = ⟨ 𝑥 , ( 𝐹 ‘ 𝑥 ) ⟩ )
84 82 83 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐹 supp 0 ) ) ∧ 𝑧 ∈ ( 𝐹 ∖ ( V × { 0 } ) ) ) ∧ 𝑥 = ( 1st ‘ 𝑧 ) ) → 𝑧 = ⟨ 𝑥 , ( 𝐹 ‘ 𝑥 ) ⟩ )
85 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐹 supp 0 ) ) ∧ 𝑧 ∈ ( 𝐹 ∖ ( V × { 0 } ) ) ) ∧ 𝑧 = ⟨ 𝑥 , ( 𝐹 ‘ 𝑥 ) ⟩ ) → 𝑧 = ⟨ 𝑥 , ( 𝐹 ‘ 𝑥 ) ⟩ )
86 85 fveq2d ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐹 supp 0 ) ) ∧ 𝑧 ∈ ( 𝐹 ∖ ( V × { 0 } ) ) ) ∧ 𝑧 = ⟨ 𝑥 , ( 𝐹 ‘ 𝑥 ) ⟩ ) → ( 1st ‘ 𝑧 ) = ( 1st ‘ ⟨ 𝑥 , ( 𝐹 ‘ 𝑥 ) ⟩ ) )
87 fvex ⊢ ( 𝐹 ‘ 𝑥 ) ∈ V
88 75 87 op1st ⊢ ( 1st ‘ ⟨ 𝑥 , ( 𝐹 ‘ 𝑥 ) ⟩ ) = 𝑥
89 86 88 eqtr2di ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐹 supp 0 ) ) ∧ 𝑧 ∈ ( 𝐹 ∖ ( V × { 0 } ) ) ) ∧ 𝑧 = ⟨ 𝑥 , ( 𝐹 ‘ 𝑥 ) ⟩ ) → 𝑥 = ( 1st ‘ 𝑧 ) )
90 84 89 impbida ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐹 supp 0 ) ) ∧ 𝑧 ∈ ( 𝐹 ∖ ( V × { 0 } ) ) ) → ( 𝑥 = ( 1st ‘ 𝑧 ) ↔ 𝑧 = ⟨ 𝑥 , ( 𝐹 ‘ 𝑥 ) ⟩ ) )
91 90 ralrimiva ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐹 supp 0 ) ) → ∀ 𝑧 ∈ ( 𝐹 ∖ ( V × { 0 } ) ) ( 𝑥 = ( 1st ‘ 𝑧 ) ↔ 𝑧 = ⟨ 𝑥 , ( 𝐹 ‘ 𝑥 ) ⟩ ) )
92 52 56 91 rspcedvd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐹 supp 0 ) ) → ∃ 𝑣 ∈ ( 𝐹 ∖ ( V × { 0 } ) ) ∀ 𝑧 ∈ ( 𝐹 ∖ ( V × { 0 } ) ) ( 𝑥 = ( 1st ‘ 𝑧 ) ↔ 𝑧 = 𝑣 ) )
93 reu6 ⊢ ( ∃! 𝑧 ∈ ( 𝐹 ∖ ( V × { 0 } ) ) 𝑥 = ( 1st ‘ 𝑧 ) ↔ ∃ 𝑣 ∈ ( 𝐹 ∖ ( V × { 0 } ) ) ∀ 𝑧 ∈ ( 𝐹 ∖ ( V × { 0 } ) ) ( 𝑥 = ( 1st ‘ 𝑧 ) ↔ 𝑧 = 𝑣 ) )
94 92 93 sylibr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐹 supp 0 ) ) → ∃! 𝑧 ∈ ( 𝐹 ∖ ( V × { 0 } ) ) 𝑥 = ( 1st ‘ 𝑧 ) )
95 18 1 2 19 4 20 21 24 41 94 gsummptf1o ⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑥 ∈ ( 𝐹 supp 0 ) ↦ ( 𝐹 ‘ 𝑥 ) ) ) = ( 𝐺 Σg ( 𝑧 ∈ ( 𝐹 ∖ ( V × { 0 } ) ) ↦ ( 𝐹 ‘ ( 1st ‘ 𝑧 ) ) ) ) )
96 10 17 95 3eqtr3d ⊢ ( 𝜑 → ( 𝐺 Σg 𝐹 ) = ( 𝐺 Σg ( 𝑧 ∈ ( 𝐹 ∖ ( V × { 0 } ) ) ↦ ( 𝐹 ‘ ( 1st ‘ 𝑧 ) ) ) ) )
97 simpr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐹 ∖ ( V × { 0 } ) ) ) → 𝑧 ∈ ( 𝐹 ∖ ( V × { 0 } ) ) )
98 97 eldifad ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐹 ∖ ( V × { 0 } ) ) ) → 𝑧 ∈ 𝐹 )
99 funfv1st2nd ⊢ ( ( Fun 𝐹 ∧ 𝑧 ∈ 𝐹 ) → ( 𝐹 ‘ ( 1st ‘ 𝑧 ) ) = ( 2nd ‘ 𝑧 ) )
100 25 98 99 syl2an2r ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐹 ∖ ( V × { 0 } ) ) ) → ( 𝐹 ‘ ( 1st ‘ 𝑧 ) ) = ( 2nd ‘ 𝑧 ) )
101 100 mpteq2dva ⊢ ( 𝜑 → ( 𝑧 ∈ ( 𝐹 ∖ ( V × { 0 } ) ) ↦ ( 𝐹 ‘ ( 1st ‘ 𝑧 ) ) ) = ( 𝑧 ∈ ( 𝐹 ∖ ( V × { 0 } ) ) ↦ ( 2nd ‘ 𝑧 ) ) )
102 101 oveq2d ⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑧 ∈ ( 𝐹 ∖ ( V × { 0 } ) ) ↦ ( 𝐹 ‘ ( 1st ‘ 𝑧 ) ) ) ) = ( 𝐺 Σg ( 𝑧 ∈ ( 𝐹 ∖ ( V × { 0 } ) ) ↦ ( 2nd ‘ 𝑧 ) ) ) )
103 96 102 eqtrd ⊢ ( 𝜑 → ( 𝐺 Σg 𝐹 ) = ( 𝐺 Σg ( 𝑧 ∈ ( 𝐹 ∖ ( V × { 0 } ) ) ↦ ( 2nd ‘ 𝑧 ) ) ) )
104 nfcv ⊢ Ⅎ 𝑧 ( 1st ‘ 𝑡 )
105 fvex ⊢ ( 2nd ‘ 𝑡 ) ∈ V
106 fvex ⊢ ( 1st ‘ 𝑡 ) ∈ V
107 105 106 op2ndd ⊢ ( 𝑧 = ⟨ ( 2nd ‘ 𝑡 ) , ( 1st ‘ 𝑡 ) ⟩ → ( 2nd ‘ 𝑧 ) = ( 1st ‘ 𝑡 ) )
108 resfnfinfin ⊢ ( ( 𝐹 Fn 𝐴 ∧ ( 𝐹 supp 0 ) ∈ Fin ) → ( 𝐹 ↾ ( 𝐹 supp 0 ) ) ∈ Fin )
109 14 20 108 syl2anc ⊢ ( 𝜑 → ( 𝐹 ↾ ( 𝐹 supp 0 ) ) ∈ Fin )
110 34 109 eqeltrrd ⊢ ( 𝜑 → ( 𝐹 ∖ ( V × { 0 } ) ) ∈ Fin )
111 34 rneqd ⊢ ( 𝜑 → ran ( 𝐹 ↾ ( 𝐹 supp 0 ) ) = ran ( 𝐹 ∖ ( V × { 0 } ) ) )
112 rnresss ⊢ ran ( 𝐹 ↾ ( 𝐹 supp 0 ) ) ⊆ ran 𝐹
113 5 frnd ⊢ ( 𝜑 → ran 𝐹 ⊆ 𝐵 )
114 112 113 sstrid ⊢ ( 𝜑 → ran ( 𝐹 ↾ ( 𝐹 supp 0 ) ) ⊆ 𝐵 )
115 111 114 eqsstrrd ⊢ ( 𝜑 → ran ( 𝐹 ∖ ( V × { 0 } ) ) ⊆ 𝐵 )
116 2ndrn ⊢ ( ( Rel ( 𝐹 ∖ ( V × { 0 } ) ) ∧ 𝑧 ∈ ( 𝐹 ∖ ( V × { 0 } ) ) ) → ( 2nd ‘ 𝑧 ) ∈ ran ( 𝐹 ∖ ( V × { 0 } ) ) )
117 28 116 sylan ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐹 ∖ ( V × { 0 } ) ) ) → ( 2nd ‘ 𝑧 ) ∈ ran ( 𝐹 ∖ ( V × { 0 } ) ) )
118 relcnv ⊢ Rel ◡ 𝐹
119 reldif ⊢ ( Rel ◡ 𝐹 → Rel ( ◡ 𝐹 ∖ ( { 0 } × V ) ) )
120 118 119 mp1i ⊢ ( 𝜑 → Rel ( ◡ 𝐹 ∖ ( { 0 } × V ) ) )
121 1st2nd ⊢ ( ( Rel ( ◡ 𝐹 ∖ ( { 0 } × V ) ) ∧ 𝑡 ∈ ( ◡ 𝐹 ∖ ( { 0 } × V ) ) ) → 𝑡 = ⟨ ( 1st ‘ 𝑡 ) , ( 2nd ‘ 𝑡 ) ⟩ )
122 120 121 sylan ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( ◡ 𝐹 ∖ ( { 0 } × V ) ) ) → 𝑡 = ⟨ ( 1st ‘ 𝑡 ) , ( 2nd ‘ 𝑡 ) ⟩ )
123 cnvdif ⊢ ◡ ( 𝐹 ∖ ( V × { 0 } ) ) = ( ◡ 𝐹 ∖ ◡ ( V × { 0 } ) )
124 cnvxp ⊢ ◡ ( V × { 0 } ) = ( { 0 } × V )
125 124 difeq2i ⊢ ( ◡ 𝐹 ∖ ◡ ( V × { 0 } ) ) = ( ◡ 𝐹 ∖ ( { 0 } × V ) )
126 123 125 eqtri ⊢ ◡ ( 𝐹 ∖ ( V × { 0 } ) ) = ( ◡ 𝐹 ∖ ( { 0 } × V ) )
127 126 eqimss2i ⊢ ( ◡ 𝐹 ∖ ( { 0 } × V ) ) ⊆ ◡ ( 𝐹 ∖ ( V × { 0 } ) )
128 127 a1i ⊢ ( 𝜑 → ( ◡ 𝐹 ∖ ( { 0 } × V ) ) ⊆ ◡ ( 𝐹 ∖ ( V × { 0 } ) ) )
129 128 sselda ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( ◡ 𝐹 ∖ ( { 0 } × V ) ) ) → 𝑡 ∈ ◡ ( 𝐹 ∖ ( V × { 0 } ) ) )
130 122 129 eqeltrrd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( ◡ 𝐹 ∖ ( { 0 } × V ) ) ) → ⟨ ( 1st ‘ 𝑡 ) , ( 2nd ‘ 𝑡 ) ⟩ ∈ ◡ ( 𝐹 ∖ ( V × { 0 } ) ) )
131 106 105 opelcnv ⊢ ( ⟨ ( 1st ‘ 𝑡 ) , ( 2nd ‘ 𝑡 ) ⟩ ∈ ◡ ( 𝐹 ∖ ( V × { 0 } ) ) ↔ ⟨ ( 2nd ‘ 𝑡 ) , ( 1st ‘ 𝑡 ) ⟩ ∈ ( 𝐹 ∖ ( V × { 0 } ) ) )
132 130 131 sylib ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( ◡ 𝐹 ∖ ( { 0 } × V ) ) ) → ⟨ ( 2nd ‘ 𝑡 ) , ( 1st ‘ 𝑡 ) ⟩ ∈ ( 𝐹 ∖ ( V × { 0 } ) ) )
133 28 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐹 ∖ ( V × { 0 } ) ) ) → Rel ( 𝐹 ∖ ( V × { 0 } ) ) )
134 eqidd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐹 ∖ ( V × { 0 } ) ) ) → ∪ ◡ { 𝑧 } = ∪ ◡ { 𝑧 } )
135 cnvf1olem ⊢ ( ( Rel ( 𝐹 ∖ ( V × { 0 } ) ) ∧ ( 𝑧 ∈ ( 𝐹 ∖ ( V × { 0 } ) ) ∧ ∪ ◡ { 𝑧 } = ∪ ◡ { 𝑧 } ) ) → ( ∪ ◡ { 𝑧 } ∈ ◡ ( 𝐹 ∖ ( V × { 0 } ) ) ∧ 𝑧 = ∪ ◡ { ∪ ◡ { 𝑧 } } ) )
136 135 simpld ⊢ ( ( Rel ( 𝐹 ∖ ( V × { 0 } ) ) ∧ ( 𝑧 ∈ ( 𝐹 ∖ ( V × { 0 } ) ) ∧ ∪ ◡ { 𝑧 } = ∪ ◡ { 𝑧 } ) ) → ∪ ◡ { 𝑧 } ∈ ◡ ( 𝐹 ∖ ( V × { 0 } ) ) )
137 133 97 134 136 syl12anc ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐹 ∖ ( V × { 0 } ) ) ) → ∪ ◡ { 𝑧 } ∈ ◡ ( 𝐹 ∖ ( V × { 0 } ) ) )
138 137 126 eleqtrdi ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐹 ∖ ( V × { 0 } ) ) ) → ∪ ◡ { 𝑧 } ∈ ( ◡ 𝐹 ∖ ( { 0 } × V ) ) )
139 eqeq2 ⊢ ( 𝑢 = ∪ ◡ { 𝑧 } → ( 𝑡 = 𝑢 ↔ 𝑡 = ∪ ◡ { 𝑧 } ) )
140 139 bibi2d ⊢ ( 𝑢 = ∪ ◡ { 𝑧 } → ( ( 𝑧 = ⟨ ( 2nd ‘ 𝑡 ) , ( 1st ‘ 𝑡 ) ⟩ ↔ 𝑡 = 𝑢 ) ↔ ( 𝑧 = ⟨ ( 2nd ‘ 𝑡 ) , ( 1st ‘ 𝑡 ) ⟩ ↔ 𝑡 = ∪ ◡ { 𝑧 } ) ) )
141 140 ralbidv ⊢ ( 𝑢 = ∪ ◡ { 𝑧 } → ( ∀ 𝑡 ∈ ( ◡ 𝐹 ∖ ( { 0 } × V ) ) ( 𝑧 = ⟨ ( 2nd ‘ 𝑡 ) , ( 1st ‘ 𝑡 ) ⟩ ↔ 𝑡 = 𝑢 ) ↔ ∀ 𝑡 ∈ ( ◡ 𝐹 ∖ ( { 0 } × V ) ) ( 𝑧 = ⟨ ( 2nd ‘ 𝑡 ) , ( 1st ‘ 𝑡 ) ⟩ ↔ 𝑡 = ∪ ◡ { 𝑧 } ) ) )
142 141 adantl ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐹 ∖ ( V × { 0 } ) ) ) ∧ 𝑢 = ∪ ◡ { 𝑧 } ) → ( ∀ 𝑡 ∈ ( ◡ 𝐹 ∖ ( { 0 } × V ) ) ( 𝑧 = ⟨ ( 2nd ‘ 𝑡 ) , ( 1st ‘ 𝑡 ) ⟩ ↔ 𝑡 = 𝑢 ) ↔ ∀ 𝑡 ∈ ( ◡ 𝐹 ∖ ( { 0 } × V ) ) ( 𝑧 = ⟨ ( 2nd ‘ 𝑡 ) , ( 1st ‘ 𝑡 ) ⟩ ↔ 𝑡 = ∪ ◡ { 𝑧 } ) ) )
143 118 119 mp1i ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐹 ∖ ( V × { 0 } ) ) ) ∧ 𝑡 ∈ ( ◡ 𝐹 ∖ ( { 0 } × V ) ) ) ∧ 𝑧 = ⟨ ( 2nd ‘ 𝑡 ) , ( 1st ‘ 𝑡 ) ⟩ ) → Rel ( ◡ 𝐹 ∖ ( { 0 } × V ) ) )
144 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐹 ∖ ( V × { 0 } ) ) ) ∧ 𝑡 ∈ ( ◡ 𝐹 ∖ ( { 0 } × V ) ) ) ∧ 𝑧 = ⟨ ( 2nd ‘ 𝑡 ) , ( 1st ‘ 𝑡 ) ⟩ ) → 𝑡 ∈ ( ◡ 𝐹 ∖ ( { 0 } × V ) ) )
145 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐹 ∖ ( V × { 0 } ) ) ) ∧ 𝑡 ∈ ( ◡ 𝐹 ∖ ( { 0 } × V ) ) ) ∧ 𝑧 = ⟨ ( 2nd ‘ 𝑡 ) , ( 1st ‘ 𝑡 ) ⟩ ) → 𝑧 = ⟨ ( 2nd ‘ 𝑡 ) , ( 1st ‘ 𝑡 ) ⟩ )
146 df-rel ⊢ ( Rel ( ◡ 𝐹 ∖ ( { 0 } × V ) ) ↔ ( ◡ 𝐹 ∖ ( { 0 } × V ) ) ⊆ ( V × V ) )
147 120 146 sylib ⊢ ( 𝜑 → ( ◡ 𝐹 ∖ ( { 0 } × V ) ) ⊆ ( V × V ) )
148 147 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐹 ∖ ( V × { 0 } ) ) ) ∧ 𝑡 ∈ ( ◡ 𝐹 ∖ ( { 0 } × V ) ) ) ∧ 𝑧 = ⟨ ( 2nd ‘ 𝑡 ) , ( 1st ‘ 𝑡 ) ⟩ ) → ( ◡ 𝐹 ∖ ( { 0 } × V ) ) ⊆ ( V × V ) )
149 148 144 sseldd ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐹 ∖ ( V × { 0 } ) ) ) ∧ 𝑡 ∈ ( ◡ 𝐹 ∖ ( { 0 } × V ) ) ) ∧ 𝑧 = ⟨ ( 2nd ‘ 𝑡 ) , ( 1st ‘ 𝑡 ) ⟩ ) → 𝑡 ∈ ( V × V ) )
150 2nd1st ⊢ ( 𝑡 ∈ ( V × V ) → ∪ ◡ { 𝑡 } = ⟨ ( 2nd ‘ 𝑡 ) , ( 1st ‘ 𝑡 ) ⟩ )
151 149 150 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐹 ∖ ( V × { 0 } ) ) ) ∧ 𝑡 ∈ ( ◡ 𝐹 ∖ ( { 0 } × V ) ) ) ∧ 𝑧 = ⟨ ( 2nd ‘ 𝑡 ) , ( 1st ‘ 𝑡 ) ⟩ ) → ∪ ◡ { 𝑡 } = ⟨ ( 2nd ‘ 𝑡 ) , ( 1st ‘ 𝑡 ) ⟩ )
152 145 151 eqtr4d ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐹 ∖ ( V × { 0 } ) ) ) ∧ 𝑡 ∈ ( ◡ 𝐹 ∖ ( { 0 } × V ) ) ) ∧ 𝑧 = ⟨ ( 2nd ‘ 𝑡 ) , ( 1st ‘ 𝑡 ) ⟩ ) → 𝑧 = ∪ ◡ { 𝑡 } )
153 cnvf1olem ⊢ ( ( Rel ( ◡ 𝐹 ∖ ( { 0 } × V ) ) ∧ ( 𝑡 ∈ ( ◡ 𝐹 ∖ ( { 0 } × V ) ) ∧ 𝑧 = ∪ ◡ { 𝑡 } ) ) → ( 𝑧 ∈ ◡ ( ◡ 𝐹 ∖ ( { 0 } × V ) ) ∧ 𝑡 = ∪ ◡ { 𝑧 } ) )
154 153 simprd ⊢ ( ( Rel ( ◡ 𝐹 ∖ ( { 0 } × V ) ) ∧ ( 𝑡 ∈ ( ◡ 𝐹 ∖ ( { 0 } × V ) ) ∧ 𝑧 = ∪ ◡ { 𝑡 } ) ) → 𝑡 = ∪ ◡ { 𝑧 } )
155 143 144 152 154 syl12anc ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐹 ∖ ( V × { 0 } ) ) ) ∧ 𝑡 ∈ ( ◡ 𝐹 ∖ ( { 0 } × V ) ) ) ∧ 𝑧 = ⟨ ( 2nd ‘ 𝑡 ) , ( 1st ‘ 𝑡 ) ⟩ ) → 𝑡 = ∪ ◡ { 𝑧 } )
156 28 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐹 ∖ ( V × { 0 } ) ) ) ∧ 𝑡 ∈ ( ◡ 𝐹 ∖ ( { 0 } × V ) ) ) ∧ 𝑡 = ∪ ◡ { 𝑧 } ) → Rel ( 𝐹 ∖ ( V × { 0 } ) ) )
157 97 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐹 ∖ ( V × { 0 } ) ) ) ∧ 𝑡 ∈ ( ◡ 𝐹 ∖ ( { 0 } × V ) ) ) ∧ 𝑡 = ∪ ◡ { 𝑧 } ) → 𝑧 ∈ ( 𝐹 ∖ ( V × { 0 } ) ) )
158 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐹 ∖ ( V × { 0 } ) ) ) ∧ 𝑡 ∈ ( ◡ 𝐹 ∖ ( { 0 } × V ) ) ) ∧ 𝑡 = ∪ ◡ { 𝑧 } ) → 𝑡 = ∪ ◡ { 𝑧 } )
159 cnvf1olem ⊢ ( ( Rel ( 𝐹 ∖ ( V × { 0 } ) ) ∧ ( 𝑧 ∈ ( 𝐹 ∖ ( V × { 0 } ) ) ∧ 𝑡 = ∪ ◡ { 𝑧 } ) ) → ( 𝑡 ∈ ◡ ( 𝐹 ∖ ( V × { 0 } ) ) ∧ 𝑧 = ∪ ◡ { 𝑡 } ) )
160 159 simprd ⊢ ( ( Rel ( 𝐹 ∖ ( V × { 0 } ) ) ∧ ( 𝑧 ∈ ( 𝐹 ∖ ( V × { 0 } ) ) ∧ 𝑡 = ∪ ◡ { 𝑧 } ) ) → 𝑧 = ∪ ◡ { 𝑡 } )
161 156 157 158 160 syl12anc ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐹 ∖ ( V × { 0 } ) ) ) ∧ 𝑡 ∈ ( ◡ 𝐹 ∖ ( { 0 } × V ) ) ) ∧ 𝑡 = ∪ ◡ { 𝑧 } ) → 𝑧 = ∪ ◡ { 𝑡 } )
162 147 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐹 ∖ ( V × { 0 } ) ) ) ∧ 𝑡 ∈ ( ◡ 𝐹 ∖ ( { 0 } × V ) ) ) ∧ 𝑡 = ∪ ◡ { 𝑧 } ) → ( ◡ 𝐹 ∖ ( { 0 } × V ) ) ⊆ ( V × V ) )
163 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐹 ∖ ( V × { 0 } ) ) ) ∧ 𝑡 ∈ ( ◡ 𝐹 ∖ ( { 0 } × V ) ) ) ∧ 𝑡 = ∪ ◡ { 𝑧 } ) → 𝑡 ∈ ( ◡ 𝐹 ∖ ( { 0 } × V ) ) )
164 162 163 sseldd ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐹 ∖ ( V × { 0 } ) ) ) ∧ 𝑡 ∈ ( ◡ 𝐹 ∖ ( { 0 } × V ) ) ) ∧ 𝑡 = ∪ ◡ { 𝑧 } ) → 𝑡 ∈ ( V × V ) )
165 164 150 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐹 ∖ ( V × { 0 } ) ) ) ∧ 𝑡 ∈ ( ◡ 𝐹 ∖ ( { 0 } × V ) ) ) ∧ 𝑡 = ∪ ◡ { 𝑧 } ) → ∪ ◡ { 𝑡 } = ⟨ ( 2nd ‘ 𝑡 ) , ( 1st ‘ 𝑡 ) ⟩ )
166 161 165 eqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐹 ∖ ( V × { 0 } ) ) ) ∧ 𝑡 ∈ ( ◡ 𝐹 ∖ ( { 0 } × V ) ) ) ∧ 𝑡 = ∪ ◡ { 𝑧 } ) → 𝑧 = ⟨ ( 2nd ‘ 𝑡 ) , ( 1st ‘ 𝑡 ) ⟩ )
167 155 166 impbida ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐹 ∖ ( V × { 0 } ) ) ) ∧ 𝑡 ∈ ( ◡ 𝐹 ∖ ( { 0 } × V ) ) ) → ( 𝑧 = ⟨ ( 2nd ‘ 𝑡 ) , ( 1st ‘ 𝑡 ) ⟩ ↔ 𝑡 = ∪ ◡ { 𝑧 } ) )
168 167 ralrimiva ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐹 ∖ ( V × { 0 } ) ) ) → ∀ 𝑡 ∈ ( ◡ 𝐹 ∖ ( { 0 } × V ) ) ( 𝑧 = ⟨ ( 2nd ‘ 𝑡 ) , ( 1st ‘ 𝑡 ) ⟩ ↔ 𝑡 = ∪ ◡ { 𝑧 } ) )
169 138 142 168 rspcedvd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐹 ∖ ( V × { 0 } ) ) ) → ∃ 𝑢 ∈ ( ◡ 𝐹 ∖ ( { 0 } × V ) ) ∀ 𝑡 ∈ ( ◡ 𝐹 ∖ ( { 0 } × V ) ) ( 𝑧 = ⟨ ( 2nd ‘ 𝑡 ) , ( 1st ‘ 𝑡 ) ⟩ ↔ 𝑡 = 𝑢 ) )
170 reu6 ⊢ ( ∃! 𝑡 ∈ ( ◡ 𝐹 ∖ ( { 0 } × V ) ) 𝑧 = ⟨ ( 2nd ‘ 𝑡 ) , ( 1st ‘ 𝑡 ) ⟩ ↔ ∃ 𝑢 ∈ ( ◡ 𝐹 ∖ ( { 0 } × V ) ) ∀ 𝑡 ∈ ( ◡ 𝐹 ∖ ( { 0 } × V ) ) ( 𝑧 = ⟨ ( 2nd ‘ 𝑡 ) , ( 1st ‘ 𝑡 ) ⟩ ↔ 𝑡 = 𝑢 ) )
171 169 170 sylibr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐹 ∖ ( V × { 0 } ) ) ) → ∃! 𝑡 ∈ ( ◡ 𝐹 ∖ ( { 0 } × V ) ) 𝑧 = ⟨ ( 2nd ‘ 𝑡 ) , ( 1st ‘ 𝑡 ) ⟩ )
172 104 1 2 107 4 110 115 117 132 171 gsummptf1o ⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑧 ∈ ( 𝐹 ∖ ( V × { 0 } ) ) ↦ ( 2nd ‘ 𝑧 ) ) ) = ( 𝐺 Σg ( 𝑡 ∈ ( ◡ 𝐹 ∖ ( { 0 } × V ) ) ↦ ( 1st ‘ 𝑡 ) ) ) )
173 fveq2 ⊢ ( 𝑡 = 𝑧 → ( 1st ‘ 𝑡 ) = ( 1st ‘ 𝑧 ) )
174 173 cbvmptv ⊢ ( 𝑡 ∈ ( ◡ 𝐹 ∖ ( { 0 } × V ) ) ↦ ( 1st ‘ 𝑡 ) ) = ( 𝑧 ∈ ( ◡ 𝐹 ∖ ( { 0 } × V ) ) ↦ ( 1st ‘ 𝑧 ) )
175 34 cnveqd ⊢ ( 𝜑 → ◡ ( 𝐹 ↾ ( 𝐹 supp 0 ) ) = ◡ ( 𝐹 ∖ ( V × { 0 } ) ) )
176 175 126 eqtr2di ⊢ ( 𝜑 → ( ◡ 𝐹 ∖ ( { 0 } × V ) ) = ◡ ( 𝐹 ↾ ( 𝐹 supp 0 ) ) )
177 176 mpteq1d ⊢ ( 𝜑 → ( 𝑧 ∈ ( ◡ 𝐹 ∖ ( { 0 } × V ) ) ↦ ( 1st ‘ 𝑧 ) ) = ( 𝑧 ∈ ◡ ( 𝐹 ↾ ( 𝐹 supp 0 ) ) ↦ ( 1st ‘ 𝑧 ) ) )
178 174 177 syl5eq ⊢ ( 𝜑 → ( 𝑡 ∈ ( ◡ 𝐹 ∖ ( { 0 } × V ) ) ↦ ( 1st ‘ 𝑡 ) ) = ( 𝑧 ∈ ◡ ( 𝐹 ↾ ( 𝐹 supp 0 ) ) ↦ ( 1st ‘ 𝑧 ) ) )
179 178 oveq2d ⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑡 ∈ ( ◡ 𝐹 ∖ ( { 0 } × V ) ) ↦ ( 1st ‘ 𝑡 ) ) ) = ( 𝐺 Σg ( 𝑧 ∈ ◡ ( 𝐹 ↾ ( 𝐹 supp 0 ) ) ↦ ( 1st ‘ 𝑧 ) ) ) )
180 103 172 179 3eqtrd ⊢ ( 𝜑 → ( 𝐺 Σg 𝐹 ) = ( 𝐺 Σg ( 𝑧 ∈ ◡ ( 𝐹 ↾ ( 𝐹 supp 0 ) ) ↦ ( 1st ‘ 𝑧 ) ) ) )
181 nfcv ⊢ Ⅎ 𝑦 ( 1st ‘ 𝑧 )
182 nfv ⊢ Ⅎ 𝑥 𝜑
183 vex ⊢ 𝑦 ∈ V
184 75 183 op1std ⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( 1st ‘ 𝑧 ) = 𝑥 )
185 relcnv ⊢ Rel ◡ ( 𝐹 ↾ ( 𝐹 supp 0 ) )
186 185 a1i ⊢ ( 𝜑 → Rel ◡ ( 𝐹 ↾ ( 𝐹 supp 0 ) ) )
187 cnvfi ⊢ ( ( 𝐹 ↾ ( 𝐹 supp 0 ) ) ∈ Fin → ◡ ( 𝐹 ↾ ( 𝐹 supp 0 ) ) ∈ Fin )
188 109 187 syl ⊢ ( 𝜑 → ◡ ( 𝐹 ↾ ( 𝐹 supp 0 ) ) ∈ Fin )
189 113 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ◡ ( 𝐹 ↾ ( 𝐹 supp 0 ) ) ) → ran 𝐹 ⊆ 𝐵 )
190 185 a1i ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ◡ ( 𝐹 ↾ ( 𝐹 supp 0 ) ) ) → Rel ◡ ( 𝐹 ↾ ( 𝐹 supp 0 ) ) )
191 simpr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ◡ ( 𝐹 ↾ ( 𝐹 supp 0 ) ) ) → 𝑧 ∈ ◡ ( 𝐹 ↾ ( 𝐹 supp 0 ) ) )
192 1stdm ⊢ ( ( Rel ◡ ( 𝐹 ↾ ( 𝐹 supp 0 ) ) ∧ 𝑧 ∈ ◡ ( 𝐹 ↾ ( 𝐹 supp 0 ) ) ) → ( 1st ‘ 𝑧 ) ∈ dom ◡ ( 𝐹 ↾ ( 𝐹 supp 0 ) ) )
193 190 191 192 syl2anc ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ◡ ( 𝐹 ↾ ( 𝐹 supp 0 ) ) ) → ( 1st ‘ 𝑧 ) ∈ dom ◡ ( 𝐹 ↾ ( 𝐹 supp 0 ) ) )
194 df-rn ⊢ ran ( 𝐹 ↾ ( 𝐹 supp 0 ) ) = dom ◡ ( 𝐹 ↾ ( 𝐹 supp 0 ) )
195 193 194 eleqtrrdi ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ◡ ( 𝐹 ↾ ( 𝐹 supp 0 ) ) ) → ( 1st ‘ 𝑧 ) ∈ ran ( 𝐹 ↾ ( 𝐹 supp 0 ) ) )
196 112 195 sselid ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ◡ ( 𝐹 ↾ ( 𝐹 supp 0 ) ) ) → ( 1st ‘ 𝑧 ) ∈ ran 𝐹 )
197 189 196 sseldd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ◡ ( 𝐹 ↾ ( 𝐹 supp 0 ) ) ) → ( 1st ‘ 𝑧 ) ∈ 𝐵 )
198 181 182 1 184 186 188 4 197 gsummpt2d ⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑧 ∈ ◡ ( 𝐹 ↾ ( 𝐹 supp 0 ) ) ↦ ( 1st ‘ 𝑧 ) ) ) = ( 𝐺 Σg ( 𝑥 ∈ dom ◡ ( 𝐹 ↾ ( 𝐹 supp 0 ) ) ↦ ( 𝐺 Σg ( 𝑦 ∈ ( ◡ ( 𝐹 ↾ ( 𝐹 supp 0 ) ) “ { 𝑥 } ) ↦ 𝑥 ) ) ) ) )
199 df-ima ⊢ ( 𝐹 “ ( 𝐹 supp 0 ) ) = ran ( 𝐹 ↾ ( 𝐹 supp 0 ) )
200 supppreima ⊢ ( ( Fun 𝐹 ∧ 𝐹 ∈ V ∧ 0 ∈ V ) → ( 𝐹 supp 0 ) = ( ◡ 𝐹 “ ( ran 𝐹 ∖ { 0 } ) ) )
201 25 13 32 200 syl3anc ⊢ ( 𝜑 → ( 𝐹 supp 0 ) = ( ◡ 𝐹 “ ( ran 𝐹 ∖ { 0 } ) ) )
202 201 imaeq2d ⊢ ( 𝜑 → ( 𝐹 “ ( 𝐹 supp 0 ) ) = ( 𝐹 “ ( ◡ 𝐹 “ ( ran 𝐹 ∖ { 0 } ) ) ) )
203 199 202 eqtr3id ⊢ ( 𝜑 → ran ( 𝐹 ↾ ( 𝐹 supp 0 ) ) = ( 𝐹 “ ( ◡ 𝐹 “ ( ran 𝐹 ∖ { 0 } ) ) ) )
204 funimacnv ⊢ ( Fun 𝐹 → ( 𝐹 “ ( ◡ 𝐹 “ ( ran 𝐹 ∖ { 0 } ) ) ) = ( ( ran 𝐹 ∖ { 0 } ) ∩ ran 𝐹 ) )
205 25 204 syl ⊢ ( 𝜑 → ( 𝐹 “ ( ◡ 𝐹 “ ( ran 𝐹 ∖ { 0 } ) ) ) = ( ( ran 𝐹 ∖ { 0 } ) ∩ ran 𝐹 ) )
206 difssd ⊢ ( 𝜑 → ( ran 𝐹 ∖ { 0 } ) ⊆ ran 𝐹 )
207 df-ss ⊢ ( ( ran 𝐹 ∖ { 0 } ) ⊆ ran 𝐹 ↔ ( ( ran 𝐹 ∖ { 0 } ) ∩ ran 𝐹 ) = ( ran 𝐹 ∖ { 0 } ) )
208 206 207 sylib ⊢ ( 𝜑 → ( ( ran 𝐹 ∖ { 0 } ) ∩ ran 𝐹 ) = ( ran 𝐹 ∖ { 0 } ) )
209 203 205 208 3eqtrd ⊢ ( 𝜑 → ran ( 𝐹 ↾ ( 𝐹 supp 0 ) ) = ( ran 𝐹 ∖ { 0 } ) )
210 194 209 eqtr3id ⊢ ( 𝜑 → dom ◡ ( 𝐹 ↾ ( 𝐹 supp 0 ) ) = ( ran 𝐹 ∖ { 0 } ) )
211 4 cmnmndd ⊢ ( 𝜑 → 𝐺 ∈ Mnd )
212 211 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ dom ◡ ( 𝐹 ↾ ( 𝐹 supp 0 ) ) ) → 𝐺 ∈ Mnd )
213 109 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ dom ◡ ( 𝐹 ↾ ( 𝐹 supp 0 ) ) ) → ( 𝐹 ↾ ( 𝐹 supp 0 ) ) ∈ Fin )
214 imafi2 ⊢ ( ◡ ( 𝐹 ↾ ( 𝐹 supp 0 ) ) ∈ Fin → ( ◡ ( 𝐹 ↾ ( 𝐹 supp 0 ) ) “ { 𝑥 } ) ∈ Fin )
215 213 187 214 3syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ dom ◡ ( 𝐹 ↾ ( 𝐹 supp 0 ) ) ) → ( ◡ ( 𝐹 ↾ ( 𝐹 supp 0 ) ) “ { 𝑥 } ) ∈ Fin )
216 194 114 eqsstrrid ⊢ ( 𝜑 → dom ◡ ( 𝐹 ↾ ( 𝐹 supp 0 ) ) ⊆ 𝐵 )
217 216 sselda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ dom ◡ ( 𝐹 ↾ ( 𝐹 supp 0 ) ) ) → 𝑥 ∈ 𝐵 )
218 1 3 gsumconst ⊢ ( ( 𝐺 ∈ Mnd ∧ ( ◡ ( 𝐹 ↾ ( 𝐹 supp 0 ) ) “ { 𝑥 } ) ∈ Fin ∧ 𝑥 ∈ 𝐵 ) → ( 𝐺 Σg ( 𝑦 ∈ ( ◡ ( 𝐹 ↾ ( 𝐹 supp 0 ) ) “ { 𝑥 } ) ↦ 𝑥 ) ) = ( ( ♯ ‘ ( ◡ ( 𝐹 ↾ ( 𝐹 supp 0 ) ) “ { 𝑥 } ) ) · 𝑥 ) )
219 212 215 217 218 syl3anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ dom ◡ ( 𝐹 ↾ ( 𝐹 supp 0 ) ) ) → ( 𝐺 Σg ( 𝑦 ∈ ( ◡ ( 𝐹 ↾ ( 𝐹 supp 0 ) ) “ { 𝑥 } ) ↦ 𝑥 ) ) = ( ( ♯ ‘ ( ◡ ( 𝐹 ↾ ( 𝐹 supp 0 ) ) “ { 𝑥 } ) ) · 𝑥 ) )
220 cnvresima ⊢ ( ◡ ( 𝐹 ↾ ( 𝐹 supp 0 ) ) “ { 𝑥 } ) = ( ( ◡ 𝐹 “ { 𝑥 } ) ∩ ( 𝐹 supp 0 ) )
221 210 eleq2d ⊢ ( 𝜑 → ( 𝑥 ∈ dom ◡ ( 𝐹 ↾ ( 𝐹 supp 0 ) ) ↔ 𝑥 ∈ ( ran 𝐹 ∖ { 0 } ) ) )
222 221 biimpa ⊢ ( ( 𝜑 ∧ 𝑥 ∈ dom ◡ ( 𝐹 ↾ ( 𝐹 supp 0 ) ) ) → 𝑥 ∈ ( ran 𝐹 ∖ { 0 } ) )
223 222 snssd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ dom ◡ ( 𝐹 ↾ ( 𝐹 supp 0 ) ) ) → { 𝑥 } ⊆ ( ran 𝐹 ∖ { 0 } ) )
224 sspreima ⊢ ( ( Fun 𝐹 ∧ { 𝑥 } ⊆ ( ran 𝐹 ∖ { 0 } ) ) → ( ◡ 𝐹 “ { 𝑥 } ) ⊆ ( ◡ 𝐹 “ ( ran 𝐹 ∖ { 0 } ) ) )
225 25 223 224 syl2an2r ⊢ ( ( 𝜑 ∧ 𝑥 ∈ dom ◡ ( 𝐹 ↾ ( 𝐹 supp 0 ) ) ) → ( ◡ 𝐹 “ { 𝑥 } ) ⊆ ( ◡ 𝐹 “ ( ran 𝐹 ∖ { 0 } ) ) )
226 201 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ dom ◡ ( 𝐹 ↾ ( 𝐹 supp 0 ) ) ) → ( 𝐹 supp 0 ) = ( ◡ 𝐹 “ ( ran 𝐹 ∖ { 0 } ) ) )
227 225 226 sseqtrrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ dom ◡ ( 𝐹 ↾ ( 𝐹 supp 0 ) ) ) → ( ◡ 𝐹 “ { 𝑥 } ) ⊆ ( 𝐹 supp 0 ) )
228 df-ss ⊢ ( ( ◡ 𝐹 “ { 𝑥 } ) ⊆ ( 𝐹 supp 0 ) ↔ ( ( ◡ 𝐹 “ { 𝑥 } ) ∩ ( 𝐹 supp 0 ) ) = ( ◡ 𝐹 “ { 𝑥 } ) )
229 227 228 sylib ⊢ ( ( 𝜑 ∧ 𝑥 ∈ dom ◡ ( 𝐹 ↾ ( 𝐹 supp 0 ) ) ) → ( ( ◡ 𝐹 “ { 𝑥 } ) ∩ ( 𝐹 supp 0 ) ) = ( ◡ 𝐹 “ { 𝑥 } ) )
230 220 229 eqtr2id ⊢ ( ( 𝜑 ∧ 𝑥 ∈ dom ◡ ( 𝐹 ↾ ( 𝐹 supp 0 ) ) ) → ( ◡ 𝐹 “ { 𝑥 } ) = ( ◡ ( 𝐹 ↾ ( 𝐹 supp 0 ) ) “ { 𝑥 } ) )
231 230 fveq2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ dom ◡ ( 𝐹 ↾ ( 𝐹 supp 0 ) ) ) → ( ♯ ‘ ( ◡ 𝐹 “ { 𝑥 } ) ) = ( ♯ ‘ ( ◡ ( 𝐹 ↾ ( 𝐹 supp 0 ) ) “ { 𝑥 } ) ) )
232 231 oveq1d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ dom ◡ ( 𝐹 ↾ ( 𝐹 supp 0 ) ) ) → ( ( ♯ ‘ ( ◡ 𝐹 “ { 𝑥 } ) ) · 𝑥 ) = ( ( ♯ ‘ ( ◡ ( 𝐹 ↾ ( 𝐹 supp 0 ) ) “ { 𝑥 } ) ) · 𝑥 ) )
233 219 232 eqtr4d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ dom ◡ ( 𝐹 ↾ ( 𝐹 supp 0 ) ) ) → ( 𝐺 Σg ( 𝑦 ∈ ( ◡ ( 𝐹 ↾ ( 𝐹 supp 0 ) ) “ { 𝑥 } ) ↦ 𝑥 ) ) = ( ( ♯ ‘ ( ◡ 𝐹 “ { 𝑥 } ) ) · 𝑥 ) )
234 210 233 mpteq12dva ⊢ ( 𝜑 → ( 𝑥 ∈ dom ◡ ( 𝐹 ↾ ( 𝐹 supp 0 ) ) ↦ ( 𝐺 Σg ( 𝑦 ∈ ( ◡ ( 𝐹 ↾ ( 𝐹 supp 0 ) ) “ { 𝑥 } ) ↦ 𝑥 ) ) ) = ( 𝑥 ∈ ( ran 𝐹 ∖ { 0 } ) ↦ ( ( ♯ ‘ ( ◡ 𝐹 “ { 𝑥 } ) ) · 𝑥 ) ) )
235 234 oveq2d ⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑥 ∈ dom ◡ ( 𝐹 ↾ ( 𝐹 supp 0 ) ) ↦ ( 𝐺 Σg ( 𝑦 ∈ ( ◡ ( 𝐹 ↾ ( 𝐹 supp 0 ) ) “ { 𝑥 } ) ↦ 𝑥 ) ) ) ) = ( 𝐺 Σg ( 𝑥 ∈ ( ran 𝐹 ∖ { 0 } ) ↦ ( ( ♯ ‘ ( ◡ 𝐹 “ { 𝑥 } ) ) · 𝑥 ) ) ) )
236 180 198 235 3eqtrd ⊢ ( 𝜑 → ( 𝐺 Σg 𝐹 ) = ( 𝐺 Σg ( 𝑥 ∈ ( ran 𝐹 ∖ { 0 } ) ↦ ( ( ♯ ‘ ( ◡ 𝐹 “ { 𝑥 } ) ) · 𝑥 ) ) ) )