Theorem gsumval3a

Description: Value of the group sum operation over an index set with finite support. (Contributed by Mario Carneiro, 7-Dec-2014) (Revised by AV, 29-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 𝐹 ) )
	gsumval3a.t	⊢ ( 𝜑 → 𝑊 ∈ Fin )
	gsumval3a.n	⊢ ( 𝜑 → 𝑊 ≠ ∅ )
	gsumval3a.w	⊢ 𝑊 = ( 𝐹 supp 0 )
	gsumval3a.i	⊢ ( 𝜑 → ¬ 𝐴 ∈ ran ... )
Assertion	gsumval3a	⊢ ( 𝜑 → ( 𝐺 Σg 𝐹 ) = ( ℩ 𝑥 ∃ 𝑓 ( 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ 𝑊 ∧ 𝑥 = ( 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		gsumval3a.t	⊢ ( 𝜑 → 𝑊 ∈ Fin )
10		gsumval3a.n	⊢ ( 𝜑 → 𝑊 ≠ ∅ )
11		gsumval3a.w	⊢ 𝑊 = ( 𝐹 supp 0 )
12		gsumval3a.i	⊢ ( 𝜑 → ¬ 𝐴 ∈ ran ... )
13		eqid	⊢ { 𝑧 ∈ 𝐵 ∣ ∀ 𝑦 ∈ 𝐵 ( ( 𝑧 + 𝑦 ) = 𝑦 ∧ ( 𝑦 + 𝑧 ) = 𝑦 ) } = { 𝑧 ∈ 𝐵 ∣ ∀ 𝑦 ∈ 𝐵 ( ( 𝑧 + 𝑦 ) = 𝑦 ∧ ( 𝑦 + 𝑧 ) = 𝑦 ) }
14	11	a1i	⊢ ( 𝜑 → 𝑊 = ( 𝐹 supp 0 ) )
15	7 6	jca	⊢ ( 𝜑 → ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ∈ 𝑉 ) )
16		fex	⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ∈ 𝑉 ) → 𝐹 ∈ V )
17	15 16	syl	⊢ ( 𝜑 → 𝐹 ∈ V )
18	2	fvexi	⊢ 0 ∈ V
19		suppimacnv	⊢ ( ( 𝐹 ∈ V ∧ 0 ∈ V ) → ( 𝐹 supp 0 ) = ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) )
20	17 18 19	sylancl	⊢ ( 𝜑 → ( 𝐹 supp 0 ) = ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) )
21	1 2 3 13	gsumvallem2	⊢ ( 𝐺 ∈ Mnd → { 𝑧 ∈ 𝐵 ∣ ∀ 𝑦 ∈ 𝐵 ( ( 𝑧 + 𝑦 ) = 𝑦 ∧ ( 𝑦 + 𝑧 ) = 𝑦 ) } = { 0 } )
22	5 21	syl	⊢ ( 𝜑 → { 𝑧 ∈ 𝐵 ∣ ∀ 𝑦 ∈ 𝐵 ( ( 𝑧 + 𝑦 ) = 𝑦 ∧ ( 𝑦 + 𝑧 ) = 𝑦 ) } = { 0 } )
23	22	eqcomd	⊢ ( 𝜑 → { 0 } = { 𝑧 ∈ 𝐵 ∣ ∀ 𝑦 ∈ 𝐵 ( ( 𝑧 + 𝑦 ) = 𝑦 ∧ ( 𝑦 + 𝑧 ) = 𝑦 ) } )
24	23	difeq2d	⊢ ( 𝜑 → ( V ∖ { 0 } ) = ( V ∖ { 𝑧 ∈ 𝐵 ∣ ∀ 𝑦 ∈ 𝐵 ( ( 𝑧 + 𝑦 ) = 𝑦 ∧ ( 𝑦 + 𝑧 ) = 𝑦 ) } ) )
25	24	imaeq2d	⊢ ( 𝜑 → ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) = ( ◡ 𝐹 “ ( V ∖ { 𝑧 ∈ 𝐵 ∣ ∀ 𝑦 ∈ 𝐵 ( ( 𝑧 + 𝑦 ) = 𝑦 ∧ ( 𝑦 + 𝑧 ) = 𝑦 ) } ) ) )
26	14 20 25	3eqtrd	⊢ ( 𝜑 → 𝑊 = ( ◡ 𝐹 “ ( V ∖ { 𝑧 ∈ 𝐵 ∣ ∀ 𝑦 ∈ 𝐵 ( ( 𝑧 + 𝑦 ) = 𝑦 ∧ ( 𝑦 + 𝑧 ) = 𝑦 ) } ) ) )
27	1 2 3 13 26 5 6 7	gsumval	⊢ ( 𝜑 → ( 𝐺 Σg 𝐹 ) = if ( ran 𝐹 ⊆ { 𝑧 ∈ 𝐵 ∣ ∀ 𝑦 ∈ 𝐵 ( ( 𝑧 + 𝑦 ) = 𝑦 ∧ ( 𝑦 + 𝑧 ) = 𝑦 ) } , 0 , if ( 𝐴 ∈ ran ... , ( ℩ 𝑥 ∃ 𝑚 ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ( 𝐴 = ( 𝑚 ... 𝑛 ) ∧ 𝑥 = ( seq 𝑚 ( + , 𝐹 ) ‘ 𝑛 ) ) ) , ( ℩ 𝑥 ∃ 𝑓 ( 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ 𝑊 ∧ 𝑥 = ( seq 1 ( + , ( 𝐹 ∘ 𝑓 ) ) ‘ ( ♯ ‘ 𝑊 ) ) ) ) ) ) )
28	22	sseq2d	⊢ ( 𝜑 → ( ran 𝐹 ⊆ { 𝑧 ∈ 𝐵 ∣ ∀ 𝑦 ∈ 𝐵 ( ( 𝑧 + 𝑦 ) = 𝑦 ∧ ( 𝑦 + 𝑧 ) = 𝑦 ) } ↔ ran 𝐹 ⊆ { 0 } ) )
29	11	a1i	⊢ ( ( 𝜑 ∧ ran 𝐹 ⊆ { 0 } ) → 𝑊 = ( 𝐹 supp 0 ) )
30	15	adantr	⊢ ( ( 𝜑 ∧ ran 𝐹 ⊆ { 0 } ) → ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ∈ 𝑉 ) )
31	30 16	syl	⊢ ( ( 𝜑 ∧ ran 𝐹 ⊆ { 0 } ) → 𝐹 ∈ V )
32	31 18 19	sylancl	⊢ ( ( 𝜑 ∧ ran 𝐹 ⊆ { 0 } ) → ( 𝐹 supp 0 ) = ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) )
33	7	ffnd	⊢ ( 𝜑 → 𝐹 Fn 𝐴 )
34	33	adantr	⊢ ( ( 𝜑 ∧ ran 𝐹 ⊆ { 0 } ) → 𝐹 Fn 𝐴 )
35		simpr	⊢ ( ( 𝜑 ∧ ran 𝐹 ⊆ { 0 } ) → ran 𝐹 ⊆ { 0 } )
36		df-f	⊢ ( 𝐹 : 𝐴 ⟶ { 0 } ↔ ( 𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ { 0 } ) )
37	34 35 36	sylanbrc	⊢ ( ( 𝜑 ∧ ran 𝐹 ⊆ { 0 } ) → 𝐹 : 𝐴 ⟶ { 0 } )
38		disjdif	⊢ ( { 0 } ∩ ( V ∖ { 0 } ) ) = ∅
39		fimacnvdisj	⊢ ( ( 𝐹 : 𝐴 ⟶ { 0 } ∧ ( { 0 } ∩ ( V ∖ { 0 } ) ) = ∅ ) → ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) = ∅ )
40	37 38 39	sylancl	⊢ ( ( 𝜑 ∧ ran 𝐹 ⊆ { 0 } ) → ( ◡ 𝐹 “ ( V ∖ { 0 } ) ) = ∅ )
41	29 32 40	3eqtrd	⊢ ( ( 𝜑 ∧ ran 𝐹 ⊆ { 0 } ) → 𝑊 = ∅ )
42	41	ex	⊢ ( 𝜑 → ( ran 𝐹 ⊆ { 0 } → 𝑊 = ∅ ) )
43	28 42	sylbid	⊢ ( 𝜑 → ( ran 𝐹 ⊆ { 𝑧 ∈ 𝐵 ∣ ∀ 𝑦 ∈ 𝐵 ( ( 𝑧 + 𝑦 ) = 𝑦 ∧ ( 𝑦 + 𝑧 ) = 𝑦 ) } → 𝑊 = ∅ ) )
44	43	necon3ad	⊢ ( 𝜑 → ( 𝑊 ≠ ∅ → ¬ ran 𝐹 ⊆ { 𝑧 ∈ 𝐵 ∣ ∀ 𝑦 ∈ 𝐵 ( ( 𝑧 + 𝑦 ) = 𝑦 ∧ ( 𝑦 + 𝑧 ) = 𝑦 ) } ) )
45	10 44	mpd	⊢ ( 𝜑 → ¬ ran 𝐹 ⊆ { 𝑧 ∈ 𝐵 ∣ ∀ 𝑦 ∈ 𝐵 ( ( 𝑧 + 𝑦 ) = 𝑦 ∧ ( 𝑦 + 𝑧 ) = 𝑦 ) } )
46	45	iffalsed	⊢ ( 𝜑 → if ( ran 𝐹 ⊆ { 𝑧 ∈ 𝐵 ∣ ∀ 𝑦 ∈ 𝐵 ( ( 𝑧 + 𝑦 ) = 𝑦 ∧ ( 𝑦 + 𝑧 ) = 𝑦 ) } , 0 , if ( 𝐴 ∈ ran ... , ( ℩ 𝑥 ∃ 𝑚 ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ( 𝐴 = ( 𝑚 ... 𝑛 ) ∧ 𝑥 = ( seq 𝑚 ( + , 𝐹 ) ‘ 𝑛 ) ) ) , ( ℩ 𝑥 ∃ 𝑓 ( 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ 𝑊 ∧ 𝑥 = ( seq 1 ( + , ( 𝐹 ∘ 𝑓 ) ) ‘ ( ♯ ‘ 𝑊 ) ) ) ) ) ) = if ( 𝐴 ∈ ran ... , ( ℩ 𝑥 ∃ 𝑚 ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ( 𝐴 = ( 𝑚 ... 𝑛 ) ∧ 𝑥 = ( seq 𝑚 ( + , 𝐹 ) ‘ 𝑛 ) ) ) , ( ℩ 𝑥 ∃ 𝑓 ( 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ 𝑊 ∧ 𝑥 = ( seq 1 ( + , ( 𝐹 ∘ 𝑓 ) ) ‘ ( ♯ ‘ 𝑊 ) ) ) ) ) )
47	12	iffalsed	⊢ ( 𝜑 → if ( 𝐴 ∈ ran ... , ( ℩ 𝑥 ∃ 𝑚 ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ( 𝐴 = ( 𝑚 ... 𝑛 ) ∧ 𝑥 = ( seq 𝑚 ( + , 𝐹 ) ‘ 𝑛 ) ) ) , ( ℩ 𝑥 ∃ 𝑓 ( 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ 𝑊 ∧ 𝑥 = ( seq 1 ( + , ( 𝐹 ∘ 𝑓 ) ) ‘ ( ♯ ‘ 𝑊 ) ) ) ) ) = ( ℩ 𝑥 ∃ 𝑓 ( 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ 𝑊 ∧ 𝑥 = ( seq 1 ( + , ( 𝐹 ∘ 𝑓 ) ) ‘ ( ♯ ‘ 𝑊 ) ) ) ) )
48	27 46 47	3eqtrd	⊢ ( 𝜑 → ( 𝐺 Σg 𝐹 ) = ( ℩ 𝑥 ∃ 𝑓 ( 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ 𝑊 ∧ 𝑥 = ( seq 1 ( + , ( 𝐹 ∘ 𝑓 ) ) ‘ ( ♯ ‘ 𝑊 ) ) ) ) )