coe1fzgsumd

Description: Value of an evaluated coefficient in a finite group sum of polynomials. (Contributed by AV, 8-Oct-2019)

	Ref	Expression
Hypotheses	coe1fzgsumd.p	⊢ 𝑃 = ( Poly₁ ‘ 𝑅 )
	coe1fzgsumd.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
	coe1fzgsumd.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
	coe1fzgsumd.k	⊢ ( 𝜑 → 𝐾 ∈ ℕ₀ )
	coe1fzgsumd.m	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑁 𝑀 ∈ 𝐵 )
	coe1fzgsumd.n	⊢ ( 𝜑 → 𝑁 ∈ Fin )
Assertion	coe1fzgsumd	⊢ ( 𝜑 → ( ( coe₁ ‘ ( 𝑃 Σ_g ( 𝑥 ∈ 𝑁 ↦ 𝑀 ) ) ) ‘ 𝐾 ) = ( 𝑅 Σ_g ( 𝑥 ∈ 𝑁 ↦ ( ( coe₁ ‘ 𝑀 ) ‘ 𝐾 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		coe1fzgsumd.p	⊢ 𝑃 = ( Poly₁ ‘ 𝑅 )
2		coe1fzgsumd.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
3		coe1fzgsumd.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
4		coe1fzgsumd.k	⊢ ( 𝜑 → 𝐾 ∈ ℕ₀ )
5		coe1fzgsumd.m	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑁 𝑀 ∈ 𝐵 )
6		coe1fzgsumd.n	⊢ ( 𝜑 → 𝑁 ∈ Fin )
7		raleq	⊢ ( 𝑛 = ∅ → ( ∀ 𝑥 ∈ 𝑛 𝑀 ∈ 𝐵 ↔ ∀ 𝑥 ∈ ∅ 𝑀 ∈ 𝐵 ) )
8	7	anbi2d	⊢ ( 𝑛 = ∅ → ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝑛 𝑀 ∈ 𝐵 ) ↔ ( 𝜑 ∧ ∀ 𝑥 ∈ ∅ 𝑀 ∈ 𝐵 ) ) )
9		mpteq1	⊢ ( 𝑛 = ∅ → ( 𝑥 ∈ 𝑛 ↦ 𝑀 ) = ( 𝑥 ∈ ∅ ↦ 𝑀 ) )
10	9	oveq2d	⊢ ( 𝑛 = ∅ → ( 𝑃 Σ_g ( 𝑥 ∈ 𝑛 ↦ 𝑀 ) ) = ( 𝑃 Σ_g ( 𝑥 ∈ ∅ ↦ 𝑀 ) ) )
11	10	fveq2d	⊢ ( 𝑛 = ∅ → ( coe₁ ‘ ( 𝑃 Σ_g ( 𝑥 ∈ 𝑛 ↦ 𝑀 ) ) ) = ( coe₁ ‘ ( 𝑃 Σ_g ( 𝑥 ∈ ∅ ↦ 𝑀 ) ) ) )
12	11	fveq1d	⊢ ( 𝑛 = ∅ → ( ( coe₁ ‘ ( 𝑃 Σ_g ( 𝑥 ∈ 𝑛 ↦ 𝑀 ) ) ) ‘ 𝐾 ) = ( ( coe₁ ‘ ( 𝑃 Σ_g ( 𝑥 ∈ ∅ ↦ 𝑀 ) ) ) ‘ 𝐾 ) )
13		mpteq1	⊢ ( 𝑛 = ∅ → ( 𝑥 ∈ 𝑛 ↦ ( ( coe₁ ‘ 𝑀 ) ‘ 𝐾 ) ) = ( 𝑥 ∈ ∅ ↦ ( ( coe₁ ‘ 𝑀 ) ‘ 𝐾 ) ) )
14	13	oveq2d	⊢ ( 𝑛 = ∅ → ( 𝑅 Σ_g ( 𝑥 ∈ 𝑛 ↦ ( ( coe₁ ‘ 𝑀 ) ‘ 𝐾 ) ) ) = ( 𝑅 Σ_g ( 𝑥 ∈ ∅ ↦ ( ( coe₁ ‘ 𝑀 ) ‘ 𝐾 ) ) ) )
15	12 14	eqeq12d	⊢ ( 𝑛 = ∅ → ( ( ( coe₁ ‘ ( 𝑃 Σ_g ( 𝑥 ∈ 𝑛 ↦ 𝑀 ) ) ) ‘ 𝐾 ) = ( 𝑅 Σ_g ( 𝑥 ∈ 𝑛 ↦ ( ( coe₁ ‘ 𝑀 ) ‘ 𝐾 ) ) ) ↔ ( ( coe₁ ‘ ( 𝑃 Σ_g ( 𝑥 ∈ ∅ ↦ 𝑀 ) ) ) ‘ 𝐾 ) = ( 𝑅 Σ_g ( 𝑥 ∈ ∅ ↦ ( ( coe₁ ‘ 𝑀 ) ‘ 𝐾 ) ) ) ) )
16	8 15	imbi12d	⊢ ( 𝑛 = ∅ → ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝑛 𝑀 ∈ 𝐵 ) → ( ( coe₁ ‘ ( 𝑃 Σ_g ( 𝑥 ∈ 𝑛 ↦ 𝑀 ) ) ) ‘ 𝐾 ) = ( 𝑅 Σ_g ( 𝑥 ∈ 𝑛 ↦ ( ( coe₁ ‘ 𝑀 ) ‘ 𝐾 ) ) ) ) ↔ ( ( 𝜑 ∧ ∀ 𝑥 ∈ ∅ 𝑀 ∈ 𝐵 ) → ( ( coe₁ ‘ ( 𝑃 Σ_g ( 𝑥 ∈ ∅ ↦ 𝑀 ) ) ) ‘ 𝐾 ) = ( 𝑅 Σ_g ( 𝑥 ∈ ∅ ↦ ( ( coe₁ ‘ 𝑀 ) ‘ 𝐾 ) ) ) ) ) )
17		raleq	⊢ ( 𝑛 = 𝑚 → ( ∀ 𝑥 ∈ 𝑛 𝑀 ∈ 𝐵 ↔ ∀ 𝑥 ∈ 𝑚 𝑀 ∈ 𝐵 ) )
18	17	anbi2d	⊢ ( 𝑛 = 𝑚 → ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝑛 𝑀 ∈ 𝐵 ) ↔ ( 𝜑 ∧ ∀ 𝑥 ∈ 𝑚 𝑀 ∈ 𝐵 ) ) )
19		mpteq1	⊢ ( 𝑛 = 𝑚 → ( 𝑥 ∈ 𝑛 ↦ 𝑀 ) = ( 𝑥 ∈ 𝑚 ↦ 𝑀 ) )
20	19	oveq2d	⊢ ( 𝑛 = 𝑚 → ( 𝑃 Σ_g ( 𝑥 ∈ 𝑛 ↦ 𝑀 ) ) = ( 𝑃 Σ_g ( 𝑥 ∈ 𝑚 ↦ 𝑀 ) ) )
21	20	fveq2d	⊢ ( 𝑛 = 𝑚 → ( coe₁ ‘ ( 𝑃 Σ_g ( 𝑥 ∈ 𝑛 ↦ 𝑀 ) ) ) = ( coe₁ ‘ ( 𝑃 Σ_g ( 𝑥 ∈ 𝑚 ↦ 𝑀 ) ) ) )
22	21	fveq1d	⊢ ( 𝑛 = 𝑚 → ( ( coe₁ ‘ ( 𝑃 Σ_g ( 𝑥 ∈ 𝑛 ↦ 𝑀 ) ) ) ‘ 𝐾 ) = ( ( coe₁ ‘ ( 𝑃 Σ_g ( 𝑥 ∈ 𝑚 ↦ 𝑀 ) ) ) ‘ 𝐾 ) )
23		mpteq1	⊢ ( 𝑛 = 𝑚 → ( 𝑥 ∈ 𝑛 ↦ ( ( coe₁ ‘ 𝑀 ) ‘ 𝐾 ) ) = ( 𝑥 ∈ 𝑚 ↦ ( ( coe₁ ‘ 𝑀 ) ‘ 𝐾 ) ) )
24	23	oveq2d	⊢ ( 𝑛 = 𝑚 → ( 𝑅 Σ_g ( 𝑥 ∈ 𝑛 ↦ ( ( coe₁ ‘ 𝑀 ) ‘ 𝐾 ) ) ) = ( 𝑅 Σ_g ( 𝑥 ∈ 𝑚 ↦ ( ( coe₁ ‘ 𝑀 ) ‘ 𝐾 ) ) ) )
25	22 24	eqeq12d	⊢ ( 𝑛 = 𝑚 → ( ( ( coe₁ ‘ ( 𝑃 Σ_g ( 𝑥 ∈ 𝑛 ↦ 𝑀 ) ) ) ‘ 𝐾 ) = ( 𝑅 Σ_g ( 𝑥 ∈ 𝑛 ↦ ( ( coe₁ ‘ 𝑀 ) ‘ 𝐾 ) ) ) ↔ ( ( coe₁ ‘ ( 𝑃 Σ_g ( 𝑥 ∈ 𝑚 ↦ 𝑀 ) ) ) ‘ 𝐾 ) = ( 𝑅 Σ_g ( 𝑥 ∈ 𝑚 ↦ ( ( coe₁ ‘ 𝑀 ) ‘ 𝐾 ) ) ) ) )
26	18 25	imbi12d	⊢ ( 𝑛 = 𝑚 → ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝑛 𝑀 ∈ 𝐵 ) → ( ( coe₁ ‘ ( 𝑃 Σ_g ( 𝑥 ∈ 𝑛 ↦ 𝑀 ) ) ) ‘ 𝐾 ) = ( 𝑅 Σ_g ( 𝑥 ∈ 𝑛 ↦ ( ( coe₁ ‘ 𝑀 ) ‘ 𝐾 ) ) ) ) ↔ ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝑚 𝑀 ∈ 𝐵 ) → ( ( coe₁ ‘ ( 𝑃 Σ_g ( 𝑥 ∈ 𝑚 ↦ 𝑀 ) ) ) ‘ 𝐾 ) = ( 𝑅 Σ_g ( 𝑥 ∈ 𝑚 ↦ ( ( coe₁ ‘ 𝑀 ) ‘ 𝐾 ) ) ) ) ) )
27		raleq	⊢ ( 𝑛 = ( 𝑚 ∪ { 𝑎 } ) → ( ∀ 𝑥 ∈ 𝑛 𝑀 ∈ 𝐵 ↔ ∀ 𝑥 ∈ ( 𝑚 ∪ { 𝑎 } ) 𝑀 ∈ 𝐵 ) )
28	27	anbi2d	⊢ ( 𝑛 = ( 𝑚 ∪ { 𝑎 } ) → ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝑛 𝑀 ∈ 𝐵 ) ↔ ( 𝜑 ∧ ∀ 𝑥 ∈ ( 𝑚 ∪ { 𝑎 } ) 𝑀 ∈ 𝐵 ) ) )
29		mpteq1	⊢ ( 𝑛 = ( 𝑚 ∪ { 𝑎 } ) → ( 𝑥 ∈ 𝑛 ↦ 𝑀 ) = ( 𝑥 ∈ ( 𝑚 ∪ { 𝑎 } ) ↦ 𝑀 ) )
30	29	oveq2d	⊢ ( 𝑛 = ( 𝑚 ∪ { 𝑎 } ) → ( 𝑃 Σ_g ( 𝑥 ∈ 𝑛 ↦ 𝑀 ) ) = ( 𝑃 Σ_g ( 𝑥 ∈ ( 𝑚 ∪ { 𝑎 } ) ↦ 𝑀 ) ) )
31	30	fveq2d	⊢ ( 𝑛 = ( 𝑚 ∪ { 𝑎 } ) → ( coe₁ ‘ ( 𝑃 Σ_g ( 𝑥 ∈ 𝑛 ↦ 𝑀 ) ) ) = ( coe₁ ‘ ( 𝑃 Σ_g ( 𝑥 ∈ ( 𝑚 ∪ { 𝑎 } ) ↦ 𝑀 ) ) ) )
32	31	fveq1d	⊢ ( 𝑛 = ( 𝑚 ∪ { 𝑎 } ) → ( ( coe₁ ‘ ( 𝑃 Σ_g ( 𝑥 ∈ 𝑛 ↦ 𝑀 ) ) ) ‘ 𝐾 ) = ( ( coe₁ ‘ ( 𝑃 Σ_g ( 𝑥 ∈ ( 𝑚 ∪ { 𝑎 } ) ↦ 𝑀 ) ) ) ‘ 𝐾 ) )
33		mpteq1	⊢ ( 𝑛 = ( 𝑚 ∪ { 𝑎 } ) → ( 𝑥 ∈ 𝑛 ↦ ( ( coe₁ ‘ 𝑀 ) ‘ 𝐾 ) ) = ( 𝑥 ∈ ( 𝑚 ∪ { 𝑎 } ) ↦ ( ( coe₁ ‘ 𝑀 ) ‘ 𝐾 ) ) )
34	33	oveq2d	⊢ ( 𝑛 = ( 𝑚 ∪ { 𝑎 } ) → ( 𝑅 Σ_g ( 𝑥 ∈ 𝑛 ↦ ( ( coe₁ ‘ 𝑀 ) ‘ 𝐾 ) ) ) = ( 𝑅 Σ_g ( 𝑥 ∈ ( 𝑚 ∪ { 𝑎 } ) ↦ ( ( coe₁ ‘ 𝑀 ) ‘ 𝐾 ) ) ) )
35	32 34	eqeq12d	⊢ ( 𝑛 = ( 𝑚 ∪ { 𝑎 } ) → ( ( ( coe₁ ‘ ( 𝑃 Σ_g ( 𝑥 ∈ 𝑛 ↦ 𝑀 ) ) ) ‘ 𝐾 ) = ( 𝑅 Σ_g ( 𝑥 ∈ 𝑛 ↦ ( ( coe₁ ‘ 𝑀 ) ‘ 𝐾 ) ) ) ↔ ( ( coe₁ ‘ ( 𝑃 Σ_g ( 𝑥 ∈ ( 𝑚 ∪ { 𝑎 } ) ↦ 𝑀 ) ) ) ‘ 𝐾 ) = ( 𝑅 Σ_g ( 𝑥 ∈ ( 𝑚 ∪ { 𝑎 } ) ↦ ( ( coe₁ ‘ 𝑀 ) ‘ 𝐾 ) ) ) ) )
36	28 35	imbi12d	⊢ ( 𝑛 = ( 𝑚 ∪ { 𝑎 } ) → ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝑛 𝑀 ∈ 𝐵 ) → ( ( coe₁ ‘ ( 𝑃 Σ_g ( 𝑥 ∈ 𝑛 ↦ 𝑀 ) ) ) ‘ 𝐾 ) = ( 𝑅 Σ_g ( 𝑥 ∈ 𝑛 ↦ ( ( coe₁ ‘ 𝑀 ) ‘ 𝐾 ) ) ) ) ↔ ( ( 𝜑 ∧ ∀ 𝑥 ∈ ( 𝑚 ∪ { 𝑎 } ) 𝑀 ∈ 𝐵 ) → ( ( coe₁ ‘ ( 𝑃 Σ_g ( 𝑥 ∈ ( 𝑚 ∪ { 𝑎 } ) ↦ 𝑀 ) ) ) ‘ 𝐾 ) = ( 𝑅 Σ_g ( 𝑥 ∈ ( 𝑚 ∪ { 𝑎 } ) ↦ ( ( coe₁ ‘ 𝑀 ) ‘ 𝐾 ) ) ) ) ) )
37		raleq	⊢ ( 𝑛 = 𝑁 → ( ∀ 𝑥 ∈ 𝑛 𝑀 ∈ 𝐵 ↔ ∀ 𝑥 ∈ 𝑁 𝑀 ∈ 𝐵 ) )
38	37	anbi2d	⊢ ( 𝑛 = 𝑁 → ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝑛 𝑀 ∈ 𝐵 ) ↔ ( 𝜑 ∧ ∀ 𝑥 ∈ 𝑁 𝑀 ∈ 𝐵 ) ) )
39		mpteq1	⊢ ( 𝑛 = 𝑁 → ( 𝑥 ∈ 𝑛 ↦ 𝑀 ) = ( 𝑥 ∈ 𝑁 ↦ 𝑀 ) )
40	39	oveq2d	⊢ ( 𝑛 = 𝑁 → ( 𝑃 Σ_g ( 𝑥 ∈ 𝑛 ↦ 𝑀 ) ) = ( 𝑃 Σ_g ( 𝑥 ∈ 𝑁 ↦ 𝑀 ) ) )
41	40	fveq2d	⊢ ( 𝑛 = 𝑁 → ( coe₁ ‘ ( 𝑃 Σ_g ( 𝑥 ∈ 𝑛 ↦ 𝑀 ) ) ) = ( coe₁ ‘ ( 𝑃 Σ_g ( 𝑥 ∈ 𝑁 ↦ 𝑀 ) ) ) )
42	41	fveq1d	⊢ ( 𝑛 = 𝑁 → ( ( coe₁ ‘ ( 𝑃 Σ_g ( 𝑥 ∈ 𝑛 ↦ 𝑀 ) ) ) ‘ 𝐾 ) = ( ( coe₁ ‘ ( 𝑃 Σ_g ( 𝑥 ∈ 𝑁 ↦ 𝑀 ) ) ) ‘ 𝐾 ) )
43		mpteq1	⊢ ( 𝑛 = 𝑁 → ( 𝑥 ∈ 𝑛 ↦ ( ( coe₁ ‘ 𝑀 ) ‘ 𝐾 ) ) = ( 𝑥 ∈ 𝑁 ↦ ( ( coe₁ ‘ 𝑀 ) ‘ 𝐾 ) ) )
44	43	oveq2d	⊢ ( 𝑛 = 𝑁 → ( 𝑅 Σ_g ( 𝑥 ∈ 𝑛 ↦ ( ( coe₁ ‘ 𝑀 ) ‘ 𝐾 ) ) ) = ( 𝑅 Σ_g ( 𝑥 ∈ 𝑁 ↦ ( ( coe₁ ‘ 𝑀 ) ‘ 𝐾 ) ) ) )
45	42 44	eqeq12d	⊢ ( 𝑛 = 𝑁 → ( ( ( coe₁ ‘ ( 𝑃 Σ_g ( 𝑥 ∈ 𝑛 ↦ 𝑀 ) ) ) ‘ 𝐾 ) = ( 𝑅 Σ_g ( 𝑥 ∈ 𝑛 ↦ ( ( coe₁ ‘ 𝑀 ) ‘ 𝐾 ) ) ) ↔ ( ( coe₁ ‘ ( 𝑃 Σ_g ( 𝑥 ∈ 𝑁 ↦ 𝑀 ) ) ) ‘ 𝐾 ) = ( 𝑅 Σ_g ( 𝑥 ∈ 𝑁 ↦ ( ( coe₁ ‘ 𝑀 ) ‘ 𝐾 ) ) ) ) )
46	38 45	imbi12d	⊢ ( 𝑛 = 𝑁 → ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝑛 𝑀 ∈ 𝐵 ) → ( ( coe₁ ‘ ( 𝑃 Σ_g ( 𝑥 ∈ 𝑛 ↦ 𝑀 ) ) ) ‘ 𝐾 ) = ( 𝑅 Σ_g ( 𝑥 ∈ 𝑛 ↦ ( ( coe₁ ‘ 𝑀 ) ‘ 𝐾 ) ) ) ) ↔ ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝑁 𝑀 ∈ 𝐵 ) → ( ( coe₁ ‘ ( 𝑃 Σ_g ( 𝑥 ∈ 𝑁 ↦ 𝑀 ) ) ) ‘ 𝐾 ) = ( 𝑅 Σ_g ( 𝑥 ∈ 𝑁 ↦ ( ( coe₁ ‘ 𝑀 ) ‘ 𝐾 ) ) ) ) ) )
47		mpt0	⊢ ( 𝑥 ∈ ∅ ↦ 𝑀 ) = ∅
48	47	oveq2i	⊢ ( 𝑃 Σ_g ( 𝑥 ∈ ∅ ↦ 𝑀 ) ) = ( 𝑃 Σ_g ∅ )
49		eqid	⊢ ( 0_g ‘ 𝑃 ) = ( 0_g ‘ 𝑃 )
50	49	gsum0	⊢ ( 𝑃 Σ_g ∅ ) = ( 0_g ‘ 𝑃 )
51	48 50	eqtri	⊢ ( 𝑃 Σ_g ( 𝑥 ∈ ∅ ↦ 𝑀 ) ) = ( 0_g ‘ 𝑃 )
52	51	fveq2i	⊢ ( coe₁ ‘ ( 𝑃 Σ_g ( 𝑥 ∈ ∅ ↦ 𝑀 ) ) ) = ( coe₁ ‘ ( 0_g ‘ 𝑃 ) )
53	52	a1i	⊢ ( 𝜑 → ( coe₁ ‘ ( 𝑃 Σ_g ( 𝑥 ∈ ∅ ↦ 𝑀 ) ) ) = ( coe₁ ‘ ( 0_g ‘ 𝑃 ) ) )
54	53	fveq1d	⊢ ( 𝜑 → ( ( coe₁ ‘ ( 𝑃 Σ_g ( 𝑥 ∈ ∅ ↦ 𝑀 ) ) ) ‘ 𝐾 ) = ( ( coe₁ ‘ ( 0_g ‘ 𝑃 ) ) ‘ 𝐾 ) )
55		eqid	⊢ ( 0_g ‘ 𝑅 ) = ( 0_g ‘ 𝑅 )
56	1 49 55	coe1z	⊢ ( 𝑅 ∈ Ring → ( coe₁ ‘ ( 0_g ‘ 𝑃 ) ) = ( ℕ₀ × { ( 0_g ‘ 𝑅 ) } ) )
57	3 56	syl	⊢ ( 𝜑 → ( coe₁ ‘ ( 0_g ‘ 𝑃 ) ) = ( ℕ₀ × { ( 0_g ‘ 𝑅 ) } ) )
58	57	fveq1d	⊢ ( 𝜑 → ( ( coe₁ ‘ ( 0_g ‘ 𝑃 ) ) ‘ 𝐾 ) = ( ( ℕ₀ × { ( 0_g ‘ 𝑅 ) } ) ‘ 𝐾 ) )
59		fvex	⊢ ( 0_g ‘ 𝑅 ) ∈ V
60		fvconst2g	⊢ ( ( ( 0_g ‘ 𝑅 ) ∈ V ∧ 𝐾 ∈ ℕ₀ ) → ( ( ℕ₀ × { ( 0_g ‘ 𝑅 ) } ) ‘ 𝐾 ) = ( 0_g ‘ 𝑅 ) )
61	59 4 60	sylancr	⊢ ( 𝜑 → ( ( ℕ₀ × { ( 0_g ‘ 𝑅 ) } ) ‘ 𝐾 ) = ( 0_g ‘ 𝑅 ) )
62	54 58 61	3eqtrd	⊢ ( 𝜑 → ( ( coe₁ ‘ ( 𝑃 Σ_g ( 𝑥 ∈ ∅ ↦ 𝑀 ) ) ) ‘ 𝐾 ) = ( 0_g ‘ 𝑅 ) )
63		mpt0	⊢ ( 𝑥 ∈ ∅ ↦ ( ( coe₁ ‘ 𝑀 ) ‘ 𝐾 ) ) = ∅
64	63	oveq2i	⊢ ( 𝑅 Σ_g ( 𝑥 ∈ ∅ ↦ ( ( coe₁ ‘ 𝑀 ) ‘ 𝐾 ) ) ) = ( 𝑅 Σ_g ∅ )
65	55	gsum0	⊢ ( 𝑅 Σ_g ∅ ) = ( 0_g ‘ 𝑅 )
66	64 65	eqtri	⊢ ( 𝑅 Σ_g ( 𝑥 ∈ ∅ ↦ ( ( coe₁ ‘ 𝑀 ) ‘ 𝐾 ) ) ) = ( 0_g ‘ 𝑅 )
67	62 66	eqtr4di	⊢ ( 𝜑 → ( ( coe₁ ‘ ( 𝑃 Σ_g ( 𝑥 ∈ ∅ ↦ 𝑀 ) ) ) ‘ 𝐾 ) = ( 𝑅 Σ_g ( 𝑥 ∈ ∅ ↦ ( ( coe₁ ‘ 𝑀 ) ‘ 𝐾 ) ) ) )
68	67	adantr	⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ ∅ 𝑀 ∈ 𝐵 ) → ( ( coe₁ ‘ ( 𝑃 Σ_g ( 𝑥 ∈ ∅ ↦ 𝑀 ) ) ) ‘ 𝐾 ) = ( 𝑅 Σ_g ( 𝑥 ∈ ∅ ↦ ( ( coe₁ ‘ 𝑀 ) ‘ 𝐾 ) ) ) )
69	1 2 3 4	coe1fzgsumdlem	⊢ ( ( 𝑚 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑚 ∧ 𝜑 ) → ( ( ∀ 𝑥 ∈ 𝑚 𝑀 ∈ 𝐵 → ( ( coe₁ ‘ ( 𝑃 Σ_g ( 𝑥 ∈ 𝑚 ↦ 𝑀 ) ) ) ‘ 𝐾 ) = ( 𝑅 Σ_g ( 𝑥 ∈ 𝑚 ↦ ( ( coe₁ ‘ 𝑀 ) ‘ 𝐾 ) ) ) ) → ( ∀ 𝑥 ∈ ( 𝑚 ∪ { 𝑎 } ) 𝑀 ∈ 𝐵 → ( ( coe₁ ‘ ( 𝑃 Σ_g ( 𝑥 ∈ ( 𝑚 ∪ { 𝑎 } ) ↦ 𝑀 ) ) ) ‘ 𝐾 ) = ( 𝑅 Σ_g ( 𝑥 ∈ ( 𝑚 ∪ { 𝑎 } ) ↦ ( ( coe₁ ‘ 𝑀 ) ‘ 𝐾 ) ) ) ) ) )
70	69	3expia	⊢ ( ( 𝑚 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑚 ) → ( 𝜑 → ( ( ∀ 𝑥 ∈ 𝑚 𝑀 ∈ 𝐵 → ( ( coe₁ ‘ ( 𝑃 Σ_g ( 𝑥 ∈ 𝑚 ↦ 𝑀 ) ) ) ‘ 𝐾 ) = ( 𝑅 Σ_g ( 𝑥 ∈ 𝑚 ↦ ( ( coe₁ ‘ 𝑀 ) ‘ 𝐾 ) ) ) ) → ( ∀ 𝑥 ∈ ( 𝑚 ∪ { 𝑎 } ) 𝑀 ∈ 𝐵 → ( ( coe₁ ‘ ( 𝑃 Σ_g ( 𝑥 ∈ ( 𝑚 ∪ { 𝑎 } ) ↦ 𝑀 ) ) ) ‘ 𝐾 ) = ( 𝑅 Σ_g ( 𝑥 ∈ ( 𝑚 ∪ { 𝑎 } ) ↦ ( ( coe₁ ‘ 𝑀 ) ‘ 𝐾 ) ) ) ) ) ) )
71	70	a2d	⊢ ( ( 𝑚 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑚 ) → ( ( 𝜑 → ( ∀ 𝑥 ∈ 𝑚 𝑀 ∈ 𝐵 → ( ( coe₁ ‘ ( 𝑃 Σ_g ( 𝑥 ∈ 𝑚 ↦ 𝑀 ) ) ) ‘ 𝐾 ) = ( 𝑅 Σ_g ( 𝑥 ∈ 𝑚 ↦ ( ( coe₁ ‘ 𝑀 ) ‘ 𝐾 ) ) ) ) ) → ( 𝜑 → ( ∀ 𝑥 ∈ ( 𝑚 ∪ { 𝑎 } ) 𝑀 ∈ 𝐵 → ( ( coe₁ ‘ ( 𝑃 Σ_g ( 𝑥 ∈ ( 𝑚 ∪ { 𝑎 } ) ↦ 𝑀 ) ) ) ‘ 𝐾 ) = ( 𝑅 Σ_g ( 𝑥 ∈ ( 𝑚 ∪ { 𝑎 } ) ↦ ( ( coe₁ ‘ 𝑀 ) ‘ 𝐾 ) ) ) ) ) ) )
72		impexp	⊢ ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝑚 𝑀 ∈ 𝐵 ) → ( ( coe₁ ‘ ( 𝑃 Σ_g ( 𝑥 ∈ 𝑚 ↦ 𝑀 ) ) ) ‘ 𝐾 ) = ( 𝑅 Σ_g ( 𝑥 ∈ 𝑚 ↦ ( ( coe₁ ‘ 𝑀 ) ‘ 𝐾 ) ) ) ) ↔ ( 𝜑 → ( ∀ 𝑥 ∈ 𝑚 𝑀 ∈ 𝐵 → ( ( coe₁ ‘ ( 𝑃 Σ_g ( 𝑥 ∈ 𝑚 ↦ 𝑀 ) ) ) ‘ 𝐾 ) = ( 𝑅 Σ_g ( 𝑥 ∈ 𝑚 ↦ ( ( coe₁ ‘ 𝑀 ) ‘ 𝐾 ) ) ) ) ) )
73		impexp	⊢ ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ ( 𝑚 ∪ { 𝑎 } ) 𝑀 ∈ 𝐵 ) → ( ( coe₁ ‘ ( 𝑃 Σ_g ( 𝑥 ∈ ( 𝑚 ∪ { 𝑎 } ) ↦ 𝑀 ) ) ) ‘ 𝐾 ) = ( 𝑅 Σ_g ( 𝑥 ∈ ( 𝑚 ∪ { 𝑎 } ) ↦ ( ( coe₁ ‘ 𝑀 ) ‘ 𝐾 ) ) ) ) ↔ ( 𝜑 → ( ∀ 𝑥 ∈ ( 𝑚 ∪ { 𝑎 } ) 𝑀 ∈ 𝐵 → ( ( coe₁ ‘ ( 𝑃 Σ_g ( 𝑥 ∈ ( 𝑚 ∪ { 𝑎 } ) ↦ 𝑀 ) ) ) ‘ 𝐾 ) = ( 𝑅 Σ_g ( 𝑥 ∈ ( 𝑚 ∪ { 𝑎 } ) ↦ ( ( coe₁ ‘ 𝑀 ) ‘ 𝐾 ) ) ) ) ) )
74	71 72 73	3imtr4g	⊢ ( ( 𝑚 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑚 ) → ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝑚 𝑀 ∈ 𝐵 ) → ( ( coe₁ ‘ ( 𝑃 Σ_g ( 𝑥 ∈ 𝑚 ↦ 𝑀 ) ) ) ‘ 𝐾 ) = ( 𝑅 Σ_g ( 𝑥 ∈ 𝑚 ↦ ( ( coe₁ ‘ 𝑀 ) ‘ 𝐾 ) ) ) ) → ( ( 𝜑 ∧ ∀ 𝑥 ∈ ( 𝑚 ∪ { 𝑎 } ) 𝑀 ∈ 𝐵 ) → ( ( coe₁ ‘ ( 𝑃 Σ_g ( 𝑥 ∈ ( 𝑚 ∪ { 𝑎 } ) ↦ 𝑀 ) ) ) ‘ 𝐾 ) = ( 𝑅 Σ_g ( 𝑥 ∈ ( 𝑚 ∪ { 𝑎 } ) ↦ ( ( coe₁ ‘ 𝑀 ) ‘ 𝐾 ) ) ) ) ) )
75	16 26 36 46 68 74	findcard2s	⊢ ( 𝑁 ∈ Fin → ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝑁 𝑀 ∈ 𝐵 ) → ( ( coe₁ ‘ ( 𝑃 Σ_g ( 𝑥 ∈ 𝑁 ↦ 𝑀 ) ) ) ‘ 𝐾 ) = ( 𝑅 Σ_g ( 𝑥 ∈ 𝑁 ↦ ( ( coe₁ ‘ 𝑀 ) ‘ 𝐾 ) ) ) ) )
76	75	expd	⊢ ( 𝑁 ∈ Fin → ( 𝜑 → ( ∀ 𝑥 ∈ 𝑁 𝑀 ∈ 𝐵 → ( ( coe₁ ‘ ( 𝑃 Σ_g ( 𝑥 ∈ 𝑁 ↦ 𝑀 ) ) ) ‘ 𝐾 ) = ( 𝑅 Σ_g ( 𝑥 ∈ 𝑁 ↦ ( ( coe₁ ‘ 𝑀 ) ‘ 𝐾 ) ) ) ) ) )
77	6 76	mpcom	⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝑁 𝑀 ∈ 𝐵 → ( ( coe₁ ‘ ( 𝑃 Σ_g ( 𝑥 ∈ 𝑁 ↦ 𝑀 ) ) ) ‘ 𝐾 ) = ( 𝑅 Σ_g ( 𝑥 ∈ 𝑁 ↦ ( ( coe₁ ‘ 𝑀 ) ‘ 𝐾 ) ) ) ) )
78	5 77	mpd	⊢ ( 𝜑 → ( ( coe₁ ‘ ( 𝑃 Σ_g ( 𝑥 ∈ 𝑁 ↦ 𝑀 ) ) ) ‘ 𝐾 ) = ( 𝑅 Σ_g ( 𝑥 ∈ 𝑁 ↦ ( ( coe₁ ‘ 𝑀 ) ‘ 𝐾 ) ) ) )

Metamath Proof Explorer

Theorem coe1fzgsumd

Proof