coe1fzgsumdlem

Description: Lemma for coe1fzgsumd (induction step). (Contributed by AV, 8-Oct-2019)

	Ref	Expression
Hypotheses	coe1fzgsumd.p	⊢ 𝑃 = ( Poly₁ ‘ 𝑅 )
	coe1fzgsumd.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
	coe1fzgsumd.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
	coe1fzgsumd.k	⊢ ( 𝜑 → 𝐾 ∈ ℕ₀ )
Assertion	coe1fzgsumdlem	⊢ ( ( 𝑚 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑚 ∧ 𝜑 ) → ( ( ∀ 𝑥 ∈ 𝑚 𝑀 ∈ 𝐵 → ( ( coe₁ ‘ ( 𝑃 Σ_g ( 𝑥 ∈ 𝑚 ↦ 𝑀 ) ) ) ‘ 𝐾 ) = ( 𝑅 Σ_g ( 𝑥 ∈ 𝑚 ↦ ( ( coe₁ ‘ 𝑀 ) ‘ 𝐾 ) ) ) ) → ( ∀ 𝑥 ∈ ( 𝑚 ∪ { 𝑎 } ) 𝑀 ∈ 𝐵 → ( ( 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		ralunb	⊢ ( ∀ 𝑥 ∈ ( 𝑚 ∪ { 𝑎 } ) 𝑀 ∈ 𝐵 ↔ ( ∀ 𝑥 ∈ 𝑚 𝑀 ∈ 𝐵 ∧ ∀ 𝑥 ∈ { 𝑎 } 𝑀 ∈ 𝐵 ) )
6		nfcv	⊢ Ⅎ 𝑦 𝑀
7		nfcsb1v	⊢ Ⅎ 𝑥 ⦋ 𝑦 / 𝑥 ⦌ 𝑀
8		csbeq1a	⊢ ( 𝑥 = 𝑦 → 𝑀 = ⦋ 𝑦 / 𝑥 ⦌ 𝑀 )
9	6 7 8	cbvmpt	⊢ ( 𝑥 ∈ ( 𝑚 ∪ { 𝑎 } ) ↦ 𝑀 ) = ( 𝑦 ∈ ( 𝑚 ∪ { 𝑎 } ) ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝑀 )
10	9	oveq2i	⊢ ( 𝑃 Σ_g ( 𝑥 ∈ ( 𝑚 ∪ { 𝑎 } ) ↦ 𝑀 ) ) = ( 𝑃 Σ_g ( 𝑦 ∈ ( 𝑚 ∪ { 𝑎 } ) ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝑀 ) )
11		eqid	⊢ ( +_g ‘ 𝑃 ) = ( +_g ‘ 𝑃 )
12	1	ply1ring	⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ Ring )
13	3 12	syl	⊢ ( 𝜑 → 𝑃 ∈ Ring )
14		ringcmn	⊢ ( 𝑃 ∈ Ring → 𝑃 ∈ CMnd )
15	13 14	syl	⊢ ( 𝜑 → 𝑃 ∈ CMnd )
16	15	3ad2ant3	⊢ ( ( 𝑚 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑚 ∧ 𝜑 ) → 𝑃 ∈ CMnd )
17	16	ad2antrr	⊢ ( ( ( ( 𝑚 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑚 ∧ 𝜑 ) ∧ ∀ 𝑥 ∈ 𝑚 𝑀 ∈ 𝐵 ) ∧ ∀ 𝑥 ∈ { 𝑎 } 𝑀 ∈ 𝐵 ) → 𝑃 ∈ CMnd )
18		simpll1	⊢ ( ( ( ( 𝑚 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑚 ∧ 𝜑 ) ∧ ∀ 𝑥 ∈ 𝑚 𝑀 ∈ 𝐵 ) ∧ ∀ 𝑥 ∈ { 𝑎 } 𝑀 ∈ 𝐵 ) → 𝑚 ∈ Fin )
19		rspcsbela	⊢ ( ( 𝑦 ∈ 𝑚 ∧ ∀ 𝑥 ∈ 𝑚 𝑀 ∈ 𝐵 ) → ⦋ 𝑦 / 𝑥 ⦌ 𝑀 ∈ 𝐵 )
20	19	expcom	⊢ ( ∀ 𝑥 ∈ 𝑚 𝑀 ∈ 𝐵 → ( 𝑦 ∈ 𝑚 → ⦋ 𝑦 / 𝑥 ⦌ 𝑀 ∈ 𝐵 ) )
21	20	adantl	⊢ ( ( ( 𝑚 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑚 ∧ 𝜑 ) ∧ ∀ 𝑥 ∈ 𝑚 𝑀 ∈ 𝐵 ) → ( 𝑦 ∈ 𝑚 → ⦋ 𝑦 / 𝑥 ⦌ 𝑀 ∈ 𝐵 ) )
22	21	adantr	⊢ ( ( ( ( 𝑚 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑚 ∧ 𝜑 ) ∧ ∀ 𝑥 ∈ 𝑚 𝑀 ∈ 𝐵 ) ∧ ∀ 𝑥 ∈ { 𝑎 } 𝑀 ∈ 𝐵 ) → ( 𝑦 ∈ 𝑚 → ⦋ 𝑦 / 𝑥 ⦌ 𝑀 ∈ 𝐵 ) )
23	22	imp	⊢ ( ( ( ( ( 𝑚 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑚 ∧ 𝜑 ) ∧ ∀ 𝑥 ∈ 𝑚 𝑀 ∈ 𝐵 ) ∧ ∀ 𝑥 ∈ { 𝑎 } 𝑀 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝑚 ) → ⦋ 𝑦 / 𝑥 ⦌ 𝑀 ∈ 𝐵 )
24		vex	⊢ 𝑎 ∈ V
25	24	a1i	⊢ ( ( ( ( 𝑚 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑚 ∧ 𝜑 ) ∧ ∀ 𝑥 ∈ 𝑚 𝑀 ∈ 𝐵 ) ∧ ∀ 𝑥 ∈ { 𝑎 } 𝑀 ∈ 𝐵 ) → 𝑎 ∈ V )
26		simpll2	⊢ ( ( ( ( 𝑚 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑚 ∧ 𝜑 ) ∧ ∀ 𝑥 ∈ 𝑚 𝑀 ∈ 𝐵 ) ∧ ∀ 𝑥 ∈ { 𝑎 } 𝑀 ∈ 𝐵 ) → ¬ 𝑎 ∈ 𝑚 )
27		vsnid	⊢ 𝑎 ∈ { 𝑎 }
28		rspcsbela	⊢ ( ( 𝑎 ∈ { 𝑎 } ∧ ∀ 𝑥 ∈ { 𝑎 } 𝑀 ∈ 𝐵 ) → ⦋ 𝑎 / 𝑥 ⦌ 𝑀 ∈ 𝐵 )
29	27 28	mpan	⊢ ( ∀ 𝑥 ∈ { 𝑎 } 𝑀 ∈ 𝐵 → ⦋ 𝑎 / 𝑥 ⦌ 𝑀 ∈ 𝐵 )
30	29	adantl	⊢ ( ( ( ( 𝑚 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑚 ∧ 𝜑 ) ∧ ∀ 𝑥 ∈ 𝑚 𝑀 ∈ 𝐵 ) ∧ ∀ 𝑥 ∈ { 𝑎 } 𝑀 ∈ 𝐵 ) → ⦋ 𝑎 / 𝑥 ⦌ 𝑀 ∈ 𝐵 )
31		csbeq1	⊢ ( 𝑦 = 𝑎 → ⦋ 𝑦 / 𝑥 ⦌ 𝑀 = ⦋ 𝑎 / 𝑥 ⦌ 𝑀 )
32	2 11 17 18 23 25 26 30 31	gsumunsn	⊢ ( ( ( ( 𝑚 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑚 ∧ 𝜑 ) ∧ ∀ 𝑥 ∈ 𝑚 𝑀 ∈ 𝐵 ) ∧ ∀ 𝑥 ∈ { 𝑎 } 𝑀 ∈ 𝐵 ) → ( 𝑃 Σ_g ( 𝑦 ∈ ( 𝑚 ∪ { 𝑎 } ) ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝑀 ) ) = ( ( 𝑃 Σ_g ( 𝑦 ∈ 𝑚 ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝑀 ) ) ( +_g ‘ 𝑃 ) ⦋ 𝑎 / 𝑥 ⦌ 𝑀 ) )
33	10 32	eqtrid	⊢ ( ( ( ( 𝑚 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑚 ∧ 𝜑 ) ∧ ∀ 𝑥 ∈ 𝑚 𝑀 ∈ 𝐵 ) ∧ ∀ 𝑥 ∈ { 𝑎 } 𝑀 ∈ 𝐵 ) → ( 𝑃 Σ_g ( 𝑥 ∈ ( 𝑚 ∪ { 𝑎 } ) ↦ 𝑀 ) ) = ( ( 𝑃 Σ_g ( 𝑦 ∈ 𝑚 ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝑀 ) ) ( +_g ‘ 𝑃 ) ⦋ 𝑎 / 𝑥 ⦌ 𝑀 ) )
34	6 7 8	cbvmpt	⊢ ( 𝑥 ∈ 𝑚 ↦ 𝑀 ) = ( 𝑦 ∈ 𝑚 ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝑀 )
35	34	eqcomi	⊢ ( 𝑦 ∈ 𝑚 ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝑀 ) = ( 𝑥 ∈ 𝑚 ↦ 𝑀 )
36	35	oveq2i	⊢ ( 𝑃 Σ_g ( 𝑦 ∈ 𝑚 ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝑀 ) ) = ( 𝑃 Σ_g ( 𝑥 ∈ 𝑚 ↦ 𝑀 ) )
37	36	oveq1i	⊢ ( ( 𝑃 Σ_g ( 𝑦 ∈ 𝑚 ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝑀 ) ) ( +_g ‘ 𝑃 ) ⦋ 𝑎 / 𝑥 ⦌ 𝑀 ) = ( ( 𝑃 Σ_g ( 𝑥 ∈ 𝑚 ↦ 𝑀 ) ) ( +_g ‘ 𝑃 ) ⦋ 𝑎 / 𝑥 ⦌ 𝑀 )
38	33 37	eqtrdi	⊢ ( ( ( ( 𝑚 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑚 ∧ 𝜑 ) ∧ ∀ 𝑥 ∈ 𝑚 𝑀 ∈ 𝐵 ) ∧ ∀ 𝑥 ∈ { 𝑎 } 𝑀 ∈ 𝐵 ) → ( 𝑃 Σ_g ( 𝑥 ∈ ( 𝑚 ∪ { 𝑎 } ) ↦ 𝑀 ) ) = ( ( 𝑃 Σ_g ( 𝑥 ∈ 𝑚 ↦ 𝑀 ) ) ( +_g ‘ 𝑃 ) ⦋ 𝑎 / 𝑥 ⦌ 𝑀 ) )
39	38	fveq2d	⊢ ( ( ( ( 𝑚 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑚 ∧ 𝜑 ) ∧ ∀ 𝑥 ∈ 𝑚 𝑀 ∈ 𝐵 ) ∧ ∀ 𝑥 ∈ { 𝑎 } 𝑀 ∈ 𝐵 ) → ( coe₁ ‘ ( 𝑃 Σ_g ( 𝑥 ∈ ( 𝑚 ∪ { 𝑎 } ) ↦ 𝑀 ) ) ) = ( coe₁ ‘ ( ( 𝑃 Σ_g ( 𝑥 ∈ 𝑚 ↦ 𝑀 ) ) ( +_g ‘ 𝑃 ) ⦋ 𝑎 / 𝑥 ⦌ 𝑀 ) ) )
40	39	fveq1d	⊢ ( ( ( ( 𝑚 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑚 ∧ 𝜑 ) ∧ ∀ 𝑥 ∈ 𝑚 𝑀 ∈ 𝐵 ) ∧ ∀ 𝑥 ∈ { 𝑎 } 𝑀 ∈ 𝐵 ) → ( ( coe₁ ‘ ( 𝑃 Σ_g ( 𝑥 ∈ ( 𝑚 ∪ { 𝑎 } ) ↦ 𝑀 ) ) ) ‘ 𝐾 ) = ( ( coe₁ ‘ ( ( 𝑃 Σ_g ( 𝑥 ∈ 𝑚 ↦ 𝑀 ) ) ( +_g ‘ 𝑃 ) ⦋ 𝑎 / 𝑥 ⦌ 𝑀 ) ) ‘ 𝐾 ) )
41	3	3ad2ant3	⊢ ( ( 𝑚 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑚 ∧ 𝜑 ) → 𝑅 ∈ Ring )
42	41	ad2antrr	⊢ ( ( ( ( 𝑚 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑚 ∧ 𝜑 ) ∧ ∀ 𝑥 ∈ 𝑚 𝑀 ∈ 𝐵 ) ∧ ∀ 𝑥 ∈ { 𝑎 } 𝑀 ∈ 𝐵 ) → 𝑅 ∈ Ring )
43		simplr	⊢ ( ( ( ( 𝑚 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑚 ∧ 𝜑 ) ∧ ∀ 𝑥 ∈ 𝑚 𝑀 ∈ 𝐵 ) ∧ ∀ 𝑥 ∈ { 𝑎 } 𝑀 ∈ 𝐵 ) → ∀ 𝑥 ∈ 𝑚 𝑀 ∈ 𝐵 )
44	2 17 18 43	gsummptcl	⊢ ( ( ( ( 𝑚 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑚 ∧ 𝜑 ) ∧ ∀ 𝑥 ∈ 𝑚 𝑀 ∈ 𝐵 ) ∧ ∀ 𝑥 ∈ { 𝑎 } 𝑀 ∈ 𝐵 ) → ( 𝑃 Σ_g ( 𝑥 ∈ 𝑚 ↦ 𝑀 ) ) ∈ 𝐵 )
45	4	3ad2ant3	⊢ ( ( 𝑚 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑚 ∧ 𝜑 ) → 𝐾 ∈ ℕ₀ )
46	45	ad2antrr	⊢ ( ( ( ( 𝑚 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑚 ∧ 𝜑 ) ∧ ∀ 𝑥 ∈ 𝑚 𝑀 ∈ 𝐵 ) ∧ ∀ 𝑥 ∈ { 𝑎 } 𝑀 ∈ 𝐵 ) → 𝐾 ∈ ℕ₀ )
47		eqid	⊢ ( +_g ‘ 𝑅 ) = ( +_g ‘ 𝑅 )
48	1 2 11 47	coe1addfv	⊢ ( ( ( 𝑅 ∈ Ring ∧ ( 𝑃 Σ_g ( 𝑥 ∈ 𝑚 ↦ 𝑀 ) ) ∈ 𝐵 ∧ ⦋ 𝑎 / 𝑥 ⦌ 𝑀 ∈ 𝐵 ) ∧ 𝐾 ∈ ℕ₀ ) → ( ( coe₁ ‘ ( ( 𝑃 Σ_g ( 𝑥 ∈ 𝑚 ↦ 𝑀 ) ) ( +_g ‘ 𝑃 ) ⦋ 𝑎 / 𝑥 ⦌ 𝑀 ) ) ‘ 𝐾 ) = ( ( ( coe₁ ‘ ( 𝑃 Σ_g ( 𝑥 ∈ 𝑚 ↦ 𝑀 ) ) ) ‘ 𝐾 ) ( +_g ‘ 𝑅 ) ( ( coe₁ ‘ ⦋ 𝑎 / 𝑥 ⦌ 𝑀 ) ‘ 𝐾 ) ) )
49	42 44 30 46 48	syl31anc	⊢ ( ( ( ( 𝑚 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑚 ∧ 𝜑 ) ∧ ∀ 𝑥 ∈ 𝑚 𝑀 ∈ 𝐵 ) ∧ ∀ 𝑥 ∈ { 𝑎 } 𝑀 ∈ 𝐵 ) → ( ( coe₁ ‘ ( ( 𝑃 Σ_g ( 𝑥 ∈ 𝑚 ↦ 𝑀 ) ) ( +_g ‘ 𝑃 ) ⦋ 𝑎 / 𝑥 ⦌ 𝑀 ) ) ‘ 𝐾 ) = ( ( ( coe₁ ‘ ( 𝑃 Σ_g ( 𝑥 ∈ 𝑚 ↦ 𝑀 ) ) ) ‘ 𝐾 ) ( +_g ‘ 𝑅 ) ( ( coe₁ ‘ ⦋ 𝑎 / 𝑥 ⦌ 𝑀 ) ‘ 𝐾 ) ) )
50	40 49	eqtrd	⊢ ( ( ( ( 𝑚 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑚 ∧ 𝜑 ) ∧ ∀ 𝑥 ∈ 𝑚 𝑀 ∈ 𝐵 ) ∧ ∀ 𝑥 ∈ { 𝑎 } 𝑀 ∈ 𝐵 ) → ( ( coe₁ ‘ ( 𝑃 Σ_g ( 𝑥 ∈ ( 𝑚 ∪ { 𝑎 } ) ↦ 𝑀 ) ) ) ‘ 𝐾 ) = ( ( ( coe₁ ‘ ( 𝑃 Σ_g ( 𝑥 ∈ 𝑚 ↦ 𝑀 ) ) ) ‘ 𝐾 ) ( +_g ‘ 𝑅 ) ( ( coe₁ ‘ ⦋ 𝑎 / 𝑥 ⦌ 𝑀 ) ‘ 𝐾 ) ) )
51		oveq1	⊢ ( ( ( coe₁ ‘ ( 𝑃 Σ_g ( 𝑥 ∈ 𝑚 ↦ 𝑀 ) ) ) ‘ 𝐾 ) = ( 𝑅 Σ_g ( 𝑥 ∈ 𝑚 ↦ ( ( coe₁ ‘ 𝑀 ) ‘ 𝐾 ) ) ) → ( ( ( coe₁ ‘ ( 𝑃 Σ_g ( 𝑥 ∈ 𝑚 ↦ 𝑀 ) ) ) ‘ 𝐾 ) ( +_g ‘ 𝑅 ) ( ( coe₁ ‘ ⦋ 𝑎 / 𝑥 ⦌ 𝑀 ) ‘ 𝐾 ) ) = ( ( 𝑅 Σ_g ( 𝑥 ∈ 𝑚 ↦ ( ( coe₁ ‘ 𝑀 ) ‘ 𝐾 ) ) ) ( +_g ‘ 𝑅 ) ( ( coe₁ ‘ ⦋ 𝑎 / 𝑥 ⦌ 𝑀 ) ‘ 𝐾 ) ) )
52	50 51	sylan9eq	⊢ ( ( ( ( ( 𝑚 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑚 ∧ 𝜑 ) ∧ ∀ 𝑥 ∈ 𝑚 𝑀 ∈ 𝐵 ) ∧ ∀ 𝑥 ∈ { 𝑎 } 𝑀 ∈ 𝐵 ) ∧ ( ( coe₁ ‘ ( 𝑃 Σ_g ( 𝑥 ∈ 𝑚 ↦ 𝑀 ) ) ) ‘ 𝐾 ) = ( 𝑅 Σ_g ( 𝑥 ∈ 𝑚 ↦ ( ( coe₁ ‘ 𝑀 ) ‘ 𝐾 ) ) ) ) → ( ( coe₁ ‘ ( 𝑃 Σ_g ( 𝑥 ∈ ( 𝑚 ∪ { 𝑎 } ) ↦ 𝑀 ) ) ) ‘ 𝐾 ) = ( ( 𝑅 Σ_g ( 𝑥 ∈ 𝑚 ↦ ( ( coe₁ ‘ 𝑀 ) ‘ 𝐾 ) ) ) ( +_g ‘ 𝑅 ) ( ( coe₁ ‘ ⦋ 𝑎 / 𝑥 ⦌ 𝑀 ) ‘ 𝐾 ) ) )
53		nfcv	⊢ Ⅎ 𝑦 ( ( coe₁ ‘ 𝑀 ) ‘ 𝐾 )
54		nfcsb1v	⊢ Ⅎ 𝑥 ⦋ 𝑦 / 𝑥 ⦌ ( ( coe₁ ‘ 𝑀 ) ‘ 𝐾 )
55		csbeq1a	⊢ ( 𝑥 = 𝑦 → ( ( coe₁ ‘ 𝑀 ) ‘ 𝐾 ) = ⦋ 𝑦 / 𝑥 ⦌ ( ( coe₁ ‘ 𝑀 ) ‘ 𝐾 ) )
56	53 54 55	cbvmpt	⊢ ( 𝑥 ∈ ( 𝑚 ∪ { 𝑎 } ) ↦ ( ( coe₁ ‘ 𝑀 ) ‘ 𝐾 ) ) = ( 𝑦 ∈ ( 𝑚 ∪ { 𝑎 } ) ↦ ⦋ 𝑦 / 𝑥 ⦌ ( ( coe₁ ‘ 𝑀 ) ‘ 𝐾 ) )
57	56	oveq2i	⊢ ( 𝑅 Σ_g ( 𝑥 ∈ ( 𝑚 ∪ { 𝑎 } ) ↦ ( ( coe₁ ‘ 𝑀 ) ‘ 𝐾 ) ) ) = ( 𝑅 Σ_g ( 𝑦 ∈ ( 𝑚 ∪ { 𝑎 } ) ↦ ⦋ 𝑦 / 𝑥 ⦌ ( ( coe₁ ‘ 𝑀 ) ‘ 𝐾 ) ) )
58		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
59		ringcmn	⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ CMnd )
60	3 59	syl	⊢ ( 𝜑 → 𝑅 ∈ CMnd )
61	60	3ad2ant3	⊢ ( ( 𝑚 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑚 ∧ 𝜑 ) → 𝑅 ∈ CMnd )
62	61	ad2antrr	⊢ ( ( ( ( 𝑚 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑚 ∧ 𝜑 ) ∧ ∀ 𝑥 ∈ 𝑚 𝑀 ∈ 𝐵 ) ∧ ∀ 𝑥 ∈ { 𝑎 } 𝑀 ∈ 𝐵 ) → 𝑅 ∈ CMnd )
63		csbfv12	⊢ ⦋ 𝑦 / 𝑥 ⦌ ( ( coe₁ ‘ 𝑀 ) ‘ 𝐾 ) = ( ⦋ 𝑦 / 𝑥 ⦌ ( coe₁ ‘ 𝑀 ) ‘ ⦋ 𝑦 / 𝑥 ⦌ 𝐾 )
64		csbfv2g	⊢ ( 𝑦 ∈ V → ⦋ 𝑦 / 𝑥 ⦌ ( coe₁ ‘ 𝑀 ) = ( coe₁ ‘ ⦋ 𝑦 / 𝑥 ⦌ 𝑀 ) )
65	64	elv	⊢ ⦋ 𝑦 / 𝑥 ⦌ ( coe₁ ‘ 𝑀 ) = ( coe₁ ‘ ⦋ 𝑦 / 𝑥 ⦌ 𝑀 )
66		csbconstg	⊢ ( 𝑦 ∈ V → ⦋ 𝑦 / 𝑥 ⦌ 𝐾 = 𝐾 )
67	66	elv	⊢ ⦋ 𝑦 / 𝑥 ⦌ 𝐾 = 𝐾
68	65 67	fveq12i	⊢ ( ⦋ 𝑦 / 𝑥 ⦌ ( coe₁ ‘ 𝑀 ) ‘ ⦋ 𝑦 / 𝑥 ⦌ 𝐾 ) = ( ( coe₁ ‘ ⦋ 𝑦 / 𝑥 ⦌ 𝑀 ) ‘ 𝐾 )
69	63 68	eqtri	⊢ ⦋ 𝑦 / 𝑥 ⦌ ( ( coe₁ ‘ 𝑀 ) ‘ 𝐾 ) = ( ( coe₁ ‘ ⦋ 𝑦 / 𝑥 ⦌ 𝑀 ) ‘ 𝐾 )
70		eqid	⊢ ( coe₁ ‘ ⦋ 𝑦 / 𝑥 ⦌ 𝑀 ) = ( coe₁ ‘ ⦋ 𝑦 / 𝑥 ⦌ 𝑀 )
71	70 2 1 58	coe1f	⊢ ( ⦋ 𝑦 / 𝑥 ⦌ 𝑀 ∈ 𝐵 → ( coe₁ ‘ ⦋ 𝑦 / 𝑥 ⦌ 𝑀 ) : ℕ₀ ⟶ ( Base ‘ 𝑅 ) )
72	23 71	syl	⊢ ( ( ( ( ( 𝑚 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑚 ∧ 𝜑 ) ∧ ∀ 𝑥 ∈ 𝑚 𝑀 ∈ 𝐵 ) ∧ ∀ 𝑥 ∈ { 𝑎 } 𝑀 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝑚 ) → ( coe₁ ‘ ⦋ 𝑦 / 𝑥 ⦌ 𝑀 ) : ℕ₀ ⟶ ( Base ‘ 𝑅 ) )
73	45	adantr	⊢ ( ( ( 𝑚 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑚 ∧ 𝜑 ) ∧ ∀ 𝑥 ∈ 𝑚 𝑀 ∈ 𝐵 ) → 𝐾 ∈ ℕ₀ )
74	73	ad2antrr	⊢ ( ( ( ( ( 𝑚 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑚 ∧ 𝜑 ) ∧ ∀ 𝑥 ∈ 𝑚 𝑀 ∈ 𝐵 ) ∧ ∀ 𝑥 ∈ { 𝑎 } 𝑀 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝑚 ) → 𝐾 ∈ ℕ₀ )
75	72 74	ffvelrnd	⊢ ( ( ( ( ( 𝑚 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑚 ∧ 𝜑 ) ∧ ∀ 𝑥 ∈ 𝑚 𝑀 ∈ 𝐵 ) ∧ ∀ 𝑥 ∈ { 𝑎 } 𝑀 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝑚 ) → ( ( coe₁ ‘ ⦋ 𝑦 / 𝑥 ⦌ 𝑀 ) ‘ 𝐾 ) ∈ ( Base ‘ 𝑅 ) )
76	69 75	eqeltrid	⊢ ( ( ( ( ( 𝑚 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑚 ∧ 𝜑 ) ∧ ∀ 𝑥 ∈ 𝑚 𝑀 ∈ 𝐵 ) ∧ ∀ 𝑥 ∈ { 𝑎 } 𝑀 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝑚 ) → ⦋ 𝑦 / 𝑥 ⦌ ( ( coe₁ ‘ 𝑀 ) ‘ 𝐾 ) ∈ ( Base ‘ 𝑅 ) )
77		eqid	⊢ ( coe₁ ‘ ⦋ 𝑎 / 𝑥 ⦌ 𝑀 ) = ( coe₁ ‘ ⦋ 𝑎 / 𝑥 ⦌ 𝑀 )
78	77 2 1 58	coe1f	⊢ ( ⦋ 𝑎 / 𝑥 ⦌ 𝑀 ∈ 𝐵 → ( coe₁ ‘ ⦋ 𝑎 / 𝑥 ⦌ 𝑀 ) : ℕ₀ ⟶ ( Base ‘ 𝑅 ) )
79	30 78	syl	⊢ ( ( ( ( 𝑚 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑚 ∧ 𝜑 ) ∧ ∀ 𝑥 ∈ 𝑚 𝑀 ∈ 𝐵 ) ∧ ∀ 𝑥 ∈ { 𝑎 } 𝑀 ∈ 𝐵 ) → ( coe₁ ‘ ⦋ 𝑎 / 𝑥 ⦌ 𝑀 ) : ℕ₀ ⟶ ( Base ‘ 𝑅 ) )
80	79 46	ffvelrnd	⊢ ( ( ( ( 𝑚 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑚 ∧ 𝜑 ) ∧ ∀ 𝑥 ∈ 𝑚 𝑀 ∈ 𝐵 ) ∧ ∀ 𝑥 ∈ { 𝑎 } 𝑀 ∈ 𝐵 ) → ( ( coe₁ ‘ ⦋ 𝑎 / 𝑥 ⦌ 𝑀 ) ‘ 𝐾 ) ∈ ( Base ‘ 𝑅 ) )
81		nfcv	⊢ Ⅎ 𝑥 𝑎
82		nfcv	⊢ Ⅎ 𝑥 coe₁
83		nfcsb1v	⊢ Ⅎ 𝑥 ⦋ 𝑎 / 𝑥 ⦌ 𝑀
84	82 83	nffv	⊢ Ⅎ 𝑥 ( coe₁ ‘ ⦋ 𝑎 / 𝑥 ⦌ 𝑀 )
85		nfcv	⊢ Ⅎ 𝑥 𝐾
86	84 85	nffv	⊢ Ⅎ 𝑥 ( ( coe₁ ‘ ⦋ 𝑎 / 𝑥 ⦌ 𝑀 ) ‘ 𝐾 )
87		csbeq1a	⊢ ( 𝑥 = 𝑎 → 𝑀 = ⦋ 𝑎 / 𝑥 ⦌ 𝑀 )
88	87	fveq2d	⊢ ( 𝑥 = 𝑎 → ( coe₁ ‘ 𝑀 ) = ( coe₁ ‘ ⦋ 𝑎 / 𝑥 ⦌ 𝑀 ) )
89	88	fveq1d	⊢ ( 𝑥 = 𝑎 → ( ( coe₁ ‘ 𝑀 ) ‘ 𝐾 ) = ( ( coe₁ ‘ ⦋ 𝑎 / 𝑥 ⦌ 𝑀 ) ‘ 𝐾 ) )
90	81 86 89	csbhypf	⊢ ( 𝑦 = 𝑎 → ⦋ 𝑦 / 𝑥 ⦌ ( ( coe₁ ‘ 𝑀 ) ‘ 𝐾 ) = ( ( coe₁ ‘ ⦋ 𝑎 / 𝑥 ⦌ 𝑀 ) ‘ 𝐾 ) )
91	58 47 62 18 76 25 26 80 90	gsumunsn	⊢ ( ( ( ( 𝑚 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑚 ∧ 𝜑 ) ∧ ∀ 𝑥 ∈ 𝑚 𝑀 ∈ 𝐵 ) ∧ ∀ 𝑥 ∈ { 𝑎 } 𝑀 ∈ 𝐵 ) → ( 𝑅 Σ_g ( 𝑦 ∈ ( 𝑚 ∪ { 𝑎 } ) ↦ ⦋ 𝑦 / 𝑥 ⦌ ( ( coe₁ ‘ 𝑀 ) ‘ 𝐾 ) ) ) = ( ( 𝑅 Σ_g ( 𝑦 ∈ 𝑚 ↦ ⦋ 𝑦 / 𝑥 ⦌ ( ( coe₁ ‘ 𝑀 ) ‘ 𝐾 ) ) ) ( +_g ‘ 𝑅 ) ( ( coe₁ ‘ ⦋ 𝑎 / 𝑥 ⦌ 𝑀 ) ‘ 𝐾 ) ) )
92	57 91	eqtrid	⊢ ( ( ( ( 𝑚 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑚 ∧ 𝜑 ) ∧ ∀ 𝑥 ∈ 𝑚 𝑀 ∈ 𝐵 ) ∧ ∀ 𝑥 ∈ { 𝑎 } 𝑀 ∈ 𝐵 ) → ( 𝑅 Σ_g ( 𝑥 ∈ ( 𝑚 ∪ { 𝑎 } ) ↦ ( ( coe₁ ‘ 𝑀 ) ‘ 𝐾 ) ) ) = ( ( 𝑅 Σ_g ( 𝑦 ∈ 𝑚 ↦ ⦋ 𝑦 / 𝑥 ⦌ ( ( coe₁ ‘ 𝑀 ) ‘ 𝐾 ) ) ) ( +_g ‘ 𝑅 ) ( ( coe₁ ‘ ⦋ 𝑎 / 𝑥 ⦌ 𝑀 ) ‘ 𝐾 ) ) )
93	53 54 55	cbvmpt	⊢ ( 𝑥 ∈ 𝑚 ↦ ( ( coe₁ ‘ 𝑀 ) ‘ 𝐾 ) ) = ( 𝑦 ∈ 𝑚 ↦ ⦋ 𝑦 / 𝑥 ⦌ ( ( coe₁ ‘ 𝑀 ) ‘ 𝐾 ) )
94	93	eqcomi	⊢ ( 𝑦 ∈ 𝑚 ↦ ⦋ 𝑦 / 𝑥 ⦌ ( ( coe₁ ‘ 𝑀 ) ‘ 𝐾 ) ) = ( 𝑥 ∈ 𝑚 ↦ ( ( coe₁ ‘ 𝑀 ) ‘ 𝐾 ) )
95	94	oveq2i	⊢ ( 𝑅 Σ_g ( 𝑦 ∈ 𝑚 ↦ ⦋ 𝑦 / 𝑥 ⦌ ( ( coe₁ ‘ 𝑀 ) ‘ 𝐾 ) ) ) = ( 𝑅 Σ_g ( 𝑥 ∈ 𝑚 ↦ ( ( coe₁ ‘ 𝑀 ) ‘ 𝐾 ) ) )
96	95	oveq1i	⊢ ( ( 𝑅 Σ_g ( 𝑦 ∈ 𝑚 ↦ ⦋ 𝑦 / 𝑥 ⦌ ( ( coe₁ ‘ 𝑀 ) ‘ 𝐾 ) ) ) ( +_g ‘ 𝑅 ) ( ( coe₁ ‘ ⦋ 𝑎 / 𝑥 ⦌ 𝑀 ) ‘ 𝐾 ) ) = ( ( 𝑅 Σ_g ( 𝑥 ∈ 𝑚 ↦ ( ( coe₁ ‘ 𝑀 ) ‘ 𝐾 ) ) ) ( +_g ‘ 𝑅 ) ( ( coe₁ ‘ ⦋ 𝑎 / 𝑥 ⦌ 𝑀 ) ‘ 𝐾 ) )
97	92 96	eqtr2di	⊢ ( ( ( ( 𝑚 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑚 ∧ 𝜑 ) ∧ ∀ 𝑥 ∈ 𝑚 𝑀 ∈ 𝐵 ) ∧ ∀ 𝑥 ∈ { 𝑎 } 𝑀 ∈ 𝐵 ) → ( ( 𝑅 Σ_g ( 𝑥 ∈ 𝑚 ↦ ( ( coe₁ ‘ 𝑀 ) ‘ 𝐾 ) ) ) ( +_g ‘ 𝑅 ) ( ( coe₁ ‘ ⦋ 𝑎 / 𝑥 ⦌ 𝑀 ) ‘ 𝐾 ) ) = ( 𝑅 Σ_g ( 𝑥 ∈ ( 𝑚 ∪ { 𝑎 } ) ↦ ( ( coe₁ ‘ 𝑀 ) ‘ 𝐾 ) ) ) )
98	97	adantr	⊢ ( ( ( ( ( 𝑚 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑚 ∧ 𝜑 ) ∧ ∀ 𝑥 ∈ 𝑚 𝑀 ∈ 𝐵 ) ∧ ∀ 𝑥 ∈ { 𝑎 } 𝑀 ∈ 𝐵 ) ∧ ( ( coe₁ ‘ ( 𝑃 Σ_g ( 𝑥 ∈ 𝑚 ↦ 𝑀 ) ) ) ‘ 𝐾 ) = ( 𝑅 Σ_g ( 𝑥 ∈ 𝑚 ↦ ( ( coe₁ ‘ 𝑀 ) ‘ 𝐾 ) ) ) ) → ( ( 𝑅 Σ_g ( 𝑥 ∈ 𝑚 ↦ ( ( coe₁ ‘ 𝑀 ) ‘ 𝐾 ) ) ) ( +_g ‘ 𝑅 ) ( ( coe₁ ‘ ⦋ 𝑎 / 𝑥 ⦌ 𝑀 ) ‘ 𝐾 ) ) = ( 𝑅 Σ_g ( 𝑥 ∈ ( 𝑚 ∪ { 𝑎 } ) ↦ ( ( coe₁ ‘ 𝑀 ) ‘ 𝐾 ) ) ) )
99	52 98	eqtrd	⊢ ( ( ( ( ( 𝑚 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑚 ∧ 𝜑 ) ∧ ∀ 𝑥 ∈ 𝑚 𝑀 ∈ 𝐵 ) ∧ ∀ 𝑥 ∈ { 𝑎 } 𝑀 ∈ 𝐵 ) ∧ ( ( coe₁ ‘ ( 𝑃 Σ_g ( 𝑥 ∈ 𝑚 ↦ 𝑀 ) ) ) ‘ 𝐾 ) = ( 𝑅 Σ_g ( 𝑥 ∈ 𝑚 ↦ ( ( coe₁ ‘ 𝑀 ) ‘ 𝐾 ) ) ) ) → ( ( coe₁ ‘ ( 𝑃 Σ_g ( 𝑥 ∈ ( 𝑚 ∪ { 𝑎 } ) ↦ 𝑀 ) ) ) ‘ 𝐾 ) = ( 𝑅 Σ_g ( 𝑥 ∈ ( 𝑚 ∪ { 𝑎 } ) ↦ ( ( coe₁ ‘ 𝑀 ) ‘ 𝐾 ) ) ) )
100	99	exp31	⊢ ( ( ( 𝑚 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑚 ∧ 𝜑 ) ∧ ∀ 𝑥 ∈ 𝑚 𝑀 ∈ 𝐵 ) → ( ∀ 𝑥 ∈ { 𝑎 } 𝑀 ∈ 𝐵 → ( ( ( coe₁ ‘ ( 𝑃 Σ_g ( 𝑥 ∈ 𝑚 ↦ 𝑀 ) ) ) ‘ 𝐾 ) = ( 𝑅 Σ_g ( 𝑥 ∈ 𝑚 ↦ ( ( coe₁ ‘ 𝑀 ) ‘ 𝐾 ) ) ) → ( ( coe₁ ‘ ( 𝑃 Σ_g ( 𝑥 ∈ ( 𝑚 ∪ { 𝑎 } ) ↦ 𝑀 ) ) ) ‘ 𝐾 ) = ( 𝑅 Σ_g ( 𝑥 ∈ ( 𝑚 ∪ { 𝑎 } ) ↦ ( ( coe₁ ‘ 𝑀 ) ‘ 𝐾 ) ) ) ) ) )
101	100	com23	⊢ ( ( ( 𝑚 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑚 ∧ 𝜑 ) ∧ ∀ 𝑥 ∈ 𝑚 𝑀 ∈ 𝐵 ) → ( ( ( coe₁ ‘ ( 𝑃 Σ_g ( 𝑥 ∈ 𝑚 ↦ 𝑀 ) ) ) ‘ 𝐾 ) = ( 𝑅 Σ_g ( 𝑥 ∈ 𝑚 ↦ ( ( coe₁ ‘ 𝑀 ) ‘ 𝐾 ) ) ) → ( ∀ 𝑥 ∈ { 𝑎 } 𝑀 ∈ 𝐵 → ( ( coe₁ ‘ ( 𝑃 Σ_g ( 𝑥 ∈ ( 𝑚 ∪ { 𝑎 } ) ↦ 𝑀 ) ) ) ‘ 𝐾 ) = ( 𝑅 Σ_g ( 𝑥 ∈ ( 𝑚 ∪ { 𝑎 } ) ↦ ( ( coe₁ ‘ 𝑀 ) ‘ 𝐾 ) ) ) ) ) )
102	101	ex	⊢ ( ( 𝑚 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑚 ∧ 𝜑 ) → ( ∀ 𝑥 ∈ 𝑚 𝑀 ∈ 𝐵 → ( ( ( coe₁ ‘ ( 𝑃 Σ_g ( 𝑥 ∈ 𝑚 ↦ 𝑀 ) ) ) ‘ 𝐾 ) = ( 𝑅 Σ_g ( 𝑥 ∈ 𝑚 ↦ ( ( coe₁ ‘ 𝑀 ) ‘ 𝐾 ) ) ) → ( ∀ 𝑥 ∈ { 𝑎 } 𝑀 ∈ 𝐵 → ( ( coe₁ ‘ ( 𝑃 Σ_g ( 𝑥 ∈ ( 𝑚 ∪ { 𝑎 } ) ↦ 𝑀 ) ) ) ‘ 𝐾 ) = ( 𝑅 Σ_g ( 𝑥 ∈ ( 𝑚 ∪ { 𝑎 } ) ↦ ( ( coe₁ ‘ 𝑀 ) ‘ 𝐾 ) ) ) ) ) ) )
103	102	a2d	⊢ ( ( 𝑚 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑚 ∧ 𝜑 ) → ( ( ∀ 𝑥 ∈ 𝑚 𝑀 ∈ 𝐵 → ( ( coe₁ ‘ ( 𝑃 Σ_g ( 𝑥 ∈ 𝑚 ↦ 𝑀 ) ) ) ‘ 𝐾 ) = ( 𝑅 Σ_g ( 𝑥 ∈ 𝑚 ↦ ( ( coe₁ ‘ 𝑀 ) ‘ 𝐾 ) ) ) ) → ( ∀ 𝑥 ∈ 𝑚 𝑀 ∈ 𝐵 → ( ∀ 𝑥 ∈ { 𝑎 } 𝑀 ∈ 𝐵 → ( ( coe₁ ‘ ( 𝑃 Σ_g ( 𝑥 ∈ ( 𝑚 ∪ { 𝑎 } ) ↦ 𝑀 ) ) ) ‘ 𝐾 ) = ( 𝑅 Σ_g ( 𝑥 ∈ ( 𝑚 ∪ { 𝑎 } ) ↦ ( ( coe₁ ‘ 𝑀 ) ‘ 𝐾 ) ) ) ) ) ) )
104	103	imp4b	⊢ ( ( ( 𝑚 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑚 ∧ 𝜑 ) ∧ ( ∀ 𝑥 ∈ 𝑚 𝑀 ∈ 𝐵 → ( ( coe₁ ‘ ( 𝑃 Σ_g ( 𝑥 ∈ 𝑚 ↦ 𝑀 ) ) ) ‘ 𝐾 ) = ( 𝑅 Σ_g ( 𝑥 ∈ 𝑚 ↦ ( ( coe₁ ‘ 𝑀 ) ‘ 𝐾 ) ) ) ) ) → ( ( ∀ 𝑥 ∈ 𝑚 𝑀 ∈ 𝐵 ∧ ∀ 𝑥 ∈ { 𝑎 } 𝑀 ∈ 𝐵 ) → ( ( coe₁ ‘ ( 𝑃 Σ_g ( 𝑥 ∈ ( 𝑚 ∪ { 𝑎 } ) ↦ 𝑀 ) ) ) ‘ 𝐾 ) = ( 𝑅 Σ_g ( 𝑥 ∈ ( 𝑚 ∪ { 𝑎 } ) ↦ ( ( coe₁ ‘ 𝑀 ) ‘ 𝐾 ) ) ) ) )
105	5 104	syl5bi	⊢ ( ( ( 𝑚 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑚 ∧ 𝜑 ) ∧ ( ∀ 𝑥 ∈ 𝑚 𝑀 ∈ 𝐵 → ( ( coe₁ ‘ ( 𝑃 Σ_g ( 𝑥 ∈ 𝑚 ↦ 𝑀 ) ) ) ‘ 𝐾 ) = ( 𝑅 Σ_g ( 𝑥 ∈ 𝑚 ↦ ( ( coe₁ ‘ 𝑀 ) ‘ 𝐾 ) ) ) ) ) → ( ∀ 𝑥 ∈ ( 𝑚 ∪ { 𝑎 } ) 𝑀 ∈ 𝐵 → ( ( coe₁ ‘ ( 𝑃 Σ_g ( 𝑥 ∈ ( 𝑚 ∪ { 𝑎 } ) ↦ 𝑀 ) ) ) ‘ 𝐾 ) = ( 𝑅 Σ_g ( 𝑥 ∈ ( 𝑚 ∪ { 𝑎 } ) ↦ ( ( coe₁ ‘ 𝑀 ) ‘ 𝐾 ) ) ) ) )
106	105	ex	⊢ ( ( 𝑚 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑚 ∧ 𝜑 ) → ( ( ∀ 𝑥 ∈ 𝑚 𝑀 ∈ 𝐵 → ( ( coe₁ ‘ ( 𝑃 Σ_g ( 𝑥 ∈ 𝑚 ↦ 𝑀 ) ) ) ‘ 𝐾 ) = ( 𝑅 Σ_g ( 𝑥 ∈ 𝑚 ↦ ( ( coe₁ ‘ 𝑀 ) ‘ 𝐾 ) ) ) ) → ( ∀ 𝑥 ∈ ( 𝑚 ∪ { 𝑎 } ) 𝑀 ∈ 𝐵 → ( ( coe₁ ‘ ( 𝑃 Σ_g ( 𝑥 ∈ ( 𝑚 ∪ { 𝑎 } ) ↦ 𝑀 ) ) ) ‘ 𝐾 ) = ( 𝑅 Σ_g ( 𝑥 ∈ ( 𝑚 ∪ { 𝑎 } ) ↦ ( ( coe₁ ‘ 𝑀 ) ‘ 𝐾 ) ) ) ) ) )

Metamath Proof Explorer

Theorem coe1fzgsumdlem

Proof