coe1fzgsumdlem

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

	Ref	Expression
Hypotheses	coe1fzgsumd.p	$⊢ P = {Poly}_{1} (R)$
	coe1fzgsumd.b	$⊢ B = {Base}_{P}$
	coe1fzgsumd.r	$⊢ φ \to R \in Ring$
	coe1fzgsumd.k	$⊢ φ \to K \in ℕ_{0}$
Assertion	coe1fzgsumdlem	$⊢ (m \in Fin \land \neg a \in m \land φ) \to ((\forall x \in m M \in B \to {coe}_{1} (\underset{x \in m}{\sum_{P}} M) (K) = \underset{x \in m}{\sum_{R}} {coe}_{1} (M) (K)) \to (\forall x \in (m \cup \{a\}) M \in B \to {coe}_{1} (\underset{x \in m \cup \{a\}}{\sum_{P}} M) (K) = \underset{x \in m \cup \{a\}}{\sum_{R}} {coe}_{1} (M) (K)))$

Proof

Step	Hyp	Ref	Expression
1		coe1fzgsumd.p	$⊢ P = {Poly}_{1} (R)$
2		coe1fzgsumd.b	$⊢ B = {Base}_{P}$
3		coe1fzgsumd.r	$⊢ φ \to R \in Ring$
4		coe1fzgsumd.k	$⊢ φ \to K \in ℕ_{0}$
5		ralunb	$⊢ \forall x \in (m \cup \{a\}) M \in B \leftrightarrow (\forall x \in m M \in B \land \forall x \in \{a\} M \in B)$
6		nfcv	$⊢ \underline{Ⅎ} y M$
7		nfcsb1v	$⊢ \underline{Ⅎ} x ⦋ y / x ⦌ M$
8		csbeq1a	$⊢ x = y \to M = ⦋ y / x ⦌ M$
9	6 7 8	cbvmpt	$⊢ (x \in (m \cup \{a\}) ⟼ M) = (y \in (m \cup \{a\}) ⟼ ⦋ y / x ⦌ M)$
10	9	oveq2i	$⊢ \underset{x \in m \cup \{a\}}{\sum_{P}} M = \underset{y \in m \cup \{a\}}{\sum_{P}} ⦋ y / x ⦌ M$
11		eqid	$⊢ +_{P} = +_{P}$
12	1	ply1ring	$⊢ R \in Ring \to P \in Ring$
13	3 12	syl	$⊢ φ \to P \in Ring$
14		ringcmn	$⊢ P \in Ring \to P \in CMnd$
15	13 14	syl	$⊢ φ \to P \in CMnd$
16	15	3ad2ant3	$⊢ (m \in Fin \land \neg a \in m \land φ) \to P \in CMnd$
17	16	ad2antrr	$⊢ (((m \in Fin \land \neg a \in m \land φ) \land \forall x \in m M \in B) \land \forall x \in \{a\} M \in B) \to P \in CMnd$
18		simpll1	$⊢ (((m \in Fin \land \neg a \in m \land φ) \land \forall x \in m M \in B) \land \forall x \in \{a\} M \in B) \to m \in Fin$
19		rspcsbela	$⊢ (y \in m \land \forall x \in m M \in B) \to ⦋ y / x ⦌ M \in B$
20	19	expcom	$⊢ \forall x \in m M \in B \to (y \in m \to ⦋ y / x ⦌ M \in B)$
21	20	adantl	$⊢ ((m \in Fin \land \neg a \in m \land φ) \land \forall x \in m M \in B) \to (y \in m \to ⦋ y / x ⦌ M \in B)$
22	21	adantr	$⊢ (((m \in Fin \land \neg a \in m \land φ) \land \forall x \in m M \in B) \land \forall x \in \{a\} M \in B) \to (y \in m \to ⦋ y / x ⦌ M \in B)$
23	22	imp	$⊢ ((((m \in Fin \land \neg a \in m \land φ) \land \forall x \in m M \in B) \land \forall x \in \{a\} M \in B) \land y \in m) \to ⦋ y / x ⦌ M \in B$
24		vex	$⊢ a \in V$
25	24	a1i	$⊢ (((m \in Fin \land \neg a \in m \land φ) \land \forall x \in m M \in B) \land \forall x \in \{a\} M \in B) \to a \in V$
26		simpll2	$⊢ (((m \in Fin \land \neg a \in m \land φ) \land \forall x \in m M \in B) \land \forall x \in \{a\} M \in B) \to \neg a \in m$
27		vsnid	$⊢ a \in \{a\}$
28		rspcsbela	$⊢ (a \in \{a\} \land \forall x \in \{a\} M \in B) \to ⦋ a / x ⦌ M \in B$
29	27 28	mpan	$⊢ \forall x \in \{a\} M \in B \to ⦋ a / x ⦌ M \in B$
30	29	adantl	$⊢ (((m \in Fin \land \neg a \in m \land φ) \land \forall x \in m M \in B) \land \forall x \in \{a\} M \in B) \to ⦋ a / x ⦌ M \in B$
31		csbeq1	$⊢ y = a \to ⦋ y / x ⦌ M = ⦋ a / x ⦌ M$
32	2 11 17 18 23 25 26 30 31	gsumunsn	$⊢ (((m \in Fin \land \neg a \in m \land φ) \land \forall x \in m M \in B) \land \forall x \in \{a\} M \in B) \to \underset{y \in m \cup \{a\}}{\sum_{P}} ⦋ y / x ⦌ M = (\underset{y \in m}{\sum_{P}}, ⦋ y / x ⦌ M) +_{P} ⦋ a / x ⦌ M$
33	10 32	eqtrid	$⊢ (((m \in Fin \land \neg a \in m \land φ) \land \forall x \in m M \in B) \land \forall x \in \{a\} M \in B) \to \underset{x \in m \cup \{a\}}{\sum_{P}} M = (\underset{y \in m}{\sum_{P}}, ⦋ y / x ⦌ M) +_{P} ⦋ a / x ⦌ M$
34	6 7 8	cbvmpt	$⊢ (x \in m ⟼ M) = (y \in m ⟼ ⦋ y / x ⦌ M)$
35	34	eqcomi	$⊢ (y \in m ⟼ ⦋ y / x ⦌ M) = (x \in m ⟼ M)$
36	35	oveq2i	$⊢ \underset{y \in m}{\sum_{P}} ⦋ y / x ⦌ M = \underset{x \in m}{\sum_{P}} M$
37	36	oveq1i	$⊢ (\underset{y \in m}{\sum_{P}}, ⦋ y / x ⦌ M) +_{P} ⦋ a / x ⦌ M = (\underset{x \in m}{\sum_{P}}, M) +_{P} ⦋ a / x ⦌ M$
38	33 37	eqtrdi	$⊢ (((m \in Fin \land \neg a \in m \land φ) \land \forall x \in m M \in B) \land \forall x \in \{a\} M \in B) \to \underset{x \in m \cup \{a\}}{\sum_{P}} M = (\underset{x \in m}{\sum_{P}}, M) +_{P} ⦋ a / x ⦌ M$
39	38	fveq2d	$⊢ (((m \in Fin \land \neg a \in m \land φ) \land \forall x \in m M \in B) \land \forall x \in \{a\} M \in B) \to {coe}_{1} (\underset{x \in m \cup \{a\}}{\sum_{P}} M) = {coe}_{1} ((\underset{x \in m}{\sum_{P}}, M) +_{P} ⦋ a / x ⦌ M)$
40	39	fveq1d	$⊢ (((m \in Fin \land \neg a \in m \land φ) \land \forall x \in m M \in B) \land \forall x \in \{a\} M \in B) \to {coe}_{1} (\underset{x \in m \cup \{a\}}{\sum_{P}} M) (K) = {coe}_{1} ((\underset{x \in m}{\sum_{P}}, M) +_{P} ⦋ a / x ⦌ M) (K)$
41	3	3ad2ant3	$⊢ (m \in Fin \land \neg a \in m \land φ) \to R \in Ring$
42	41	ad2antrr	$⊢ (((m \in Fin \land \neg a \in m \land φ) \land \forall x \in m M \in B) \land \forall x \in \{a\} M \in B) \to R \in Ring$
43		simplr	$⊢ (((m \in Fin \land \neg a \in m \land φ) \land \forall x \in m M \in B) \land \forall x \in \{a\} M \in B) \to \forall x \in m M \in B$
44	2 17 18 43	gsummptcl	$⊢ (((m \in Fin \land \neg a \in m \land φ) \land \forall x \in m M \in B) \land \forall x \in \{a\} M \in B) \to \underset{x \in m}{\sum_{P}} M \in B$
45	4	3ad2ant3	$⊢ (m \in Fin \land \neg a \in m \land φ) \to K \in ℕ_{0}$
46	45	ad2antrr	$⊢ (((m \in Fin \land \neg a \in m \land φ) \land \forall x \in m M \in B) \land \forall x \in \{a\} M \in B) \to K \in ℕ_{0}$
47		eqid	$⊢ +_{R} = +_{R}$
48	1 2 11 47	coe1addfv	$⊢ ((R \in Ring \land \underset{x \in m}{\sum_{P}} M \in B \land ⦋ a / x ⦌ M \in B) \land K \in ℕ_{0}) \to {coe}_{1} ((\underset{x \in m}{\sum_{P}}, M) +_{P} ⦋ a / x ⦌ M) (K) = {coe}_{1} (\underset{x \in m}{\sum_{P}} M) (K) +_{R} {coe}_{1} (⦋ a / x ⦌ M) (K)$
49	42 44 30 46 48	syl31anc	$⊢ (((m \in Fin \land \neg a \in m \land φ) \land \forall x \in m M \in B) \land \forall x \in \{a\} M \in B) \to {coe}_{1} ((\underset{x \in m}{\sum_{P}}, M) +_{P} ⦋ a / x ⦌ M) (K) = {coe}_{1} (\underset{x \in m}{\sum_{P}} M) (K) +_{R} {coe}_{1} (⦋ a / x ⦌ M) (K)$
50	40 49	eqtrd	$⊢ (((m \in Fin \land \neg a \in m \land φ) \land \forall x \in m M \in B) \land \forall x \in \{a\} M \in B) \to {coe}_{1} (\underset{x \in m \cup \{a\}}{\sum_{P}} M) (K) = {coe}_{1} (\underset{x \in m}{\sum_{P}} M) (K) +_{R} {coe}_{1} (⦋ a / x ⦌ M) (K)$
51		oveq1	$⊢ {coe}_{1} (\underset{x \in m}{\sum_{P}} M) (K) = \underset{x \in m}{\sum_{R}} {coe}_{1} (M) (K) \to {coe}_{1} (\underset{x \in m}{\sum_{P}} M) (K) +_{R} {coe}_{1} (⦋ a / x ⦌ M) (K) = (\underset{x \in m}{\sum_{R}}, {coe}_{1} (M) (K)) +_{R} {coe}_{1} (⦋ a / x ⦌ M) (K)$
52	50 51	sylan9eq	$⊢ ((((m \in Fin \land \neg a \in m \land φ) \land \forall x \in m M \in B) \land \forall x \in \{a\} M \in B) \land {coe}_{1} (\underset{x \in m}{\sum_{P}} M) (K) = \underset{x \in m}{\sum_{R}} {coe}_{1} (M) (K)) \to {coe}_{1} (\underset{x \in m \cup \{a\}}{\sum_{P}} M) (K) = (\underset{x \in m}{\sum_{R}}, {coe}_{1} (M) (K)) +_{R} {coe}_{1} (⦋ a / x ⦌ M) (K)$
53		nfcv	$⊢ \underline{Ⅎ} y {coe}_{1} (M) (K)$
54		nfcsb1v	$⊢ \underline{Ⅎ} x ⦋ y / x ⦌ {coe}_{1} (M) (K)$
55		csbeq1a	$⊢ x = y \to {coe}_{1} (M) (K) = ⦋ y / x ⦌ {coe}_{1} (M) (K)$
56	53 54 55	cbvmpt	$⊢ (x \in (m \cup \{a\}) ⟼ {coe}_{1} (M) (K)) = (y \in (m \cup \{a\}) ⟼ ⦋ y / x ⦌ {coe}_{1} (M) (K))$
57	56	oveq2i	$⊢ \underset{x \in m \cup \{a\}}{\sum_{R}} {coe}_{1} (M) (K) = \underset{y \in m \cup \{a\}}{\sum_{R}} ⦋ y / x ⦌ {coe}_{1} (M) (K)$
58		eqid	$⊢ {Base}_{R} = {Base}_{R}$
59		ringcmn	$⊢ R \in Ring \to R \in CMnd$
60	3 59	syl	$⊢ φ \to R \in CMnd$
61	60	3ad2ant3	$⊢ (m \in Fin \land \neg a \in m \land φ) \to R \in CMnd$
62	61	ad2antrr	$⊢ (((m \in Fin \land \neg a \in m \land φ) \land \forall x \in m M \in B) \land \forall x \in \{a\} M \in B) \to R \in CMnd$
63		csbfv12	$⊢ ⦋ y / x ⦌ {coe}_{1} (M) (K) = ⦋ y / x ⦌ {coe}_{1} (M) (⦋ y / x ⦌ K)$
64		csbfv2g	$⊢ y \in V \to ⦋ y / x ⦌ {coe}_{1} (M) = {coe}_{1} (⦋ y / x ⦌ M)$
65	64	elv	$⊢ ⦋ y / x ⦌ {coe}_{1} (M) = {coe}_{1} (⦋ y / x ⦌ M)$
66		csbconstg	$⊢ y \in V \to ⦋ y / x ⦌ K = K$
67	66	elv	$⊢ ⦋ y / x ⦌ K = K$
68	65 67	fveq12i	$⊢ ⦋ y / x ⦌ {coe}_{1} (M) (⦋ y / x ⦌ K) = {coe}_{1} (⦋ y / x ⦌ M) (K)$
69	63 68	eqtri	$⊢ ⦋ y / x ⦌ {coe}_{1} (M) (K) = {coe}_{1} (⦋ y / x ⦌ M) (K)$
70		eqid	$⊢ {coe}_{1} (⦋ y / x ⦌ M) = {coe}_{1} (⦋ y / x ⦌ M)$
71	70 2 1 58	coe1f	$⊢ ⦋ y / x ⦌ M \in B \to {coe}_{1} (⦋ y / x ⦌ M) : ℕ_{0} ⟶ {Base}_{R}$
72	23 71	syl	$⊢ ((((m \in Fin \land \neg a \in m \land φ) \land \forall x \in m M \in B) \land \forall x \in \{a\} M \in B) \land y \in m) \to {coe}_{1} (⦋ y / x ⦌ M) : ℕ_{0} ⟶ {Base}_{R}$
73	45	adantr	$⊢ ((m \in Fin \land \neg a \in m \land φ) \land \forall x \in m M \in B) \to K \in ℕ_{0}$
74	73	ad2antrr	$⊢ ((((m \in Fin \land \neg a \in m \land φ) \land \forall x \in m M \in B) \land \forall x \in \{a\} M \in B) \land y \in m) \to K \in ℕ_{0}$
75	72 74	ffvelcdmd	$⊢ ((((m \in Fin \land \neg a \in m \land φ) \land \forall x \in m M \in B) \land \forall x \in \{a\} M \in B) \land y \in m) \to {coe}_{1} (⦋ y / x ⦌ M) (K) \in {Base}_{R}$
76	69 75	eqeltrid	$⊢ ((((m \in Fin \land \neg a \in m \land φ) \land \forall x \in m M \in B) \land \forall x \in \{a\} M \in B) \land y \in m) \to ⦋ y / x ⦌ {coe}_{1} (M) (K) \in {Base}_{R}$
77		eqid	$⊢ {coe}_{1} (⦋ a / x ⦌ M) = {coe}_{1} (⦋ a / x ⦌ M)$
78	77 2 1 58	coe1f	$⊢ ⦋ a / x ⦌ M \in B \to {coe}_{1} (⦋ a / x ⦌ M) : ℕ_{0} ⟶ {Base}_{R}$
79	30 78	syl	$⊢ (((m \in Fin \land \neg a \in m \land φ) \land \forall x \in m M \in B) \land \forall x \in \{a\} M \in B) \to {coe}_{1} (⦋ a / x ⦌ M) : ℕ_{0} ⟶ {Base}_{R}$
80	79 46	ffvelcdmd	$⊢ (((m \in Fin \land \neg a \in m \land φ) \land \forall x \in m M \in B) \land \forall x \in \{a\} M \in B) \to {coe}_{1} (⦋ a / x ⦌ M) (K) \in {Base}_{R}$
81		nfcv	$⊢ \underline{Ⅎ} x a$
82		nfcv	$⊢ \underline{Ⅎ} x {coe}_{1}$
83		nfcsb1v	$⊢ \underline{Ⅎ} x ⦋ a / x ⦌ M$
84	82 83	nffv	$⊢ \underline{Ⅎ} x {coe}_{1} (⦋ a / x ⦌ M)$
85		nfcv	$⊢ \underline{Ⅎ} x K$
86	84 85	nffv	$⊢ \underline{Ⅎ} x {coe}_{1} (⦋ a / x ⦌ M) (K)$
87		csbeq1a	$⊢ x = a \to M = ⦋ a / x ⦌ M$
88	87	fveq2d	$⊢ x = a \to {coe}_{1} (M) = {coe}_{1} (⦋ a / x ⦌ M)$
89	88	fveq1d	$⊢ x = a \to {coe}_{1} (M) (K) = {coe}_{1} (⦋ a / x ⦌ M) (K)$
90	81 86 89	csbhypf	$⊢ y = a \to ⦋ y / x ⦌ {coe}_{1} (M) (K) = {coe}_{1} (⦋ a / x ⦌ M) (K)$
91	58 47 62 18 76 25 26 80 90	gsumunsn	$⊢ (((m \in Fin \land \neg a \in m \land φ) \land \forall x \in m M \in B) \land \forall x \in \{a\} M \in B) \to \underset{y \in m \cup \{a\}}{\sum_{R}} ⦋ y / x ⦌ {coe}_{1} (M) (K) = (\underset{y \in m}{\sum_{R}}, ⦋ y / x ⦌ {coe}_{1} (M) (K)) +_{R} {coe}_{1} (⦋ a / x ⦌ M) (K)$
92	57 91	eqtrid	$⊢ (((m \in Fin \land \neg a \in m \land φ) \land \forall x \in m M \in B) \land \forall x \in \{a\} M \in B) \to \underset{x \in m \cup \{a\}}{\sum_{R}} {coe}_{1} (M) (K) = (\underset{y \in m}{\sum_{R}}, ⦋ y / x ⦌ {coe}_{1} (M) (K)) +_{R} {coe}_{1} (⦋ a / x ⦌ M) (K)$
93	53 54 55	cbvmpt	$⊢ (x \in m ⟼ {coe}_{1} (M) (K)) = (y \in m ⟼ ⦋ y / x ⦌ {coe}_{1} (M) (K))$
94	93	eqcomi	$⊢ (y \in m ⟼ ⦋ y / x ⦌ {coe}_{1} (M) (K)) = (x \in m ⟼ {coe}_{1} (M) (K))$
95	94	oveq2i	$⊢ \underset{y \in m}{\sum_{R}} ⦋ y / x ⦌ {coe}_{1} (M) (K) = \underset{x \in m}{\sum_{R}} {coe}_{1} (M) (K)$
96	95	oveq1i	$⊢ (\underset{y \in m}{\sum_{R}}, ⦋ y / x ⦌ {coe}_{1} (M) (K)) +_{R} {coe}_{1} (⦋ a / x ⦌ M) (K) = (\underset{x \in m}{\sum_{R}}, {coe}_{1} (M) (K)) +_{R} {coe}_{1} (⦋ a / x ⦌ M) (K)$
97	92 96	eqtr2di	$⊢ (((m \in Fin \land \neg a \in m \land φ) \land \forall x \in m M \in B) \land \forall x \in \{a\} M \in B) \to (\underset{x \in m}{\sum_{R}}, {coe}_{1} (M) (K)) +_{R} {coe}_{1} (⦋ a / x ⦌ M) (K) = \underset{x \in m \cup \{a\}}{\sum_{R}} {coe}_{1} (M) (K)$
98	97	adantr	$⊢ ((((m \in Fin \land \neg a \in m \land φ) \land \forall x \in m M \in B) \land \forall x \in \{a\} M \in B) \land {coe}_{1} (\underset{x \in m}{\sum_{P}} M) (K) = \underset{x \in m}{\sum_{R}} {coe}_{1} (M) (K)) \to (\underset{x \in m}{\sum_{R}}, {coe}_{1} (M) (K)) +_{R} {coe}_{1} (⦋ a / x ⦌ M) (K) = \underset{x \in m \cup \{a\}}{\sum_{R}} {coe}_{1} (M) (K)$
99	52 98	eqtrd	$⊢ ((((m \in Fin \land \neg a \in m \land φ) \land \forall x \in m M \in B) \land \forall x \in \{a\} M \in B) \land {coe}_{1} (\underset{x \in m}{\sum_{P}} M) (K) = \underset{x \in m}{\sum_{R}} {coe}_{1} (M) (K)) \to {coe}_{1} (\underset{x \in m \cup \{a\}}{\sum_{P}} M) (K) = \underset{x \in m \cup \{a\}}{\sum_{R}} {coe}_{1} (M) (K)$
100	99	exp31	$⊢ ((m \in Fin \land \neg a \in m \land φ) \land \forall x \in m M \in B) \to (\forall x \in \{a\} M \in B \to ({coe}_{1} (\underset{x \in m}{\sum_{P}} M) (K) = \underset{x \in m}{\sum_{R}} {coe}_{1} (M) (K) \to {coe}_{1} (\underset{x \in m \cup \{a\}}{\sum_{P}} M) (K) = \underset{x \in m \cup \{a\}}{\sum_{R}} {coe}_{1} (M) (K)))$
101	100	com23	$⊢ ((m \in Fin \land \neg a \in m \land φ) \land \forall x \in m M \in B) \to ({coe}_{1} (\underset{x \in m}{\sum_{P}} M) (K) = \underset{x \in m}{\sum_{R}} {coe}_{1} (M) (K) \to (\forall x \in \{a\} M \in B \to {coe}_{1} (\underset{x \in m \cup \{a\}}{\sum_{P}} M) (K) = \underset{x \in m \cup \{a\}}{\sum_{R}} {coe}_{1} (M) (K)))$
102	101	ex	$⊢ (m \in Fin \land \neg a \in m \land φ) \to (\forall x \in m M \in B \to ({coe}_{1} (\underset{x \in m}{\sum_{P}} M) (K) = \underset{x \in m}{\sum_{R}} {coe}_{1} (M) (K) \to (\forall x \in \{a\} M \in B \to {coe}_{1} (\underset{x \in m \cup \{a\}}{\sum_{P}} M) (K) = \underset{x \in m \cup \{a\}}{\sum_{R}} {coe}_{1} (M) (K))))$
103	102	a2d	$⊢ (m \in Fin \land \neg a \in m \land φ) \to ((\forall x \in m M \in B \to {coe}_{1} (\underset{x \in m}{\sum_{P}} M) (K) = \underset{x \in m}{\sum_{R}} {coe}_{1} (M) (K)) \to (\forall x \in m M \in B \to (\forall x \in \{a\} M \in B \to {coe}_{1} (\underset{x \in m \cup \{a\}}{\sum_{P}} M) (K) = \underset{x \in m \cup \{a\}}{\sum_{R}} {coe}_{1} (M) (K))))$
104	103	imp4b	$⊢ ((m \in Fin \land \neg a \in m \land φ) \land (\forall x \in m M \in B \to {coe}_{1} (\underset{x \in m}{\sum_{P}} M) (K) = \underset{x \in m}{\sum_{R}} {coe}_{1} (M) (K))) \to ((\forall x \in m M \in B \land \forall x \in \{a\} M \in B) \to {coe}_{1} (\underset{x \in m \cup \{a\}}{\sum_{P}} M) (K) = \underset{x \in m \cup \{a\}}{\sum_{R}} {coe}_{1} (M) (K))$
105	5 104	biimtrid	$⊢ ((m \in Fin \land \neg a \in m \land φ) \land (\forall x \in m M \in B \to {coe}_{1} (\underset{x \in m}{\sum_{P}} M) (K) = \underset{x \in m}{\sum_{R}} {coe}_{1} (M) (K))) \to (\forall x \in (m \cup \{a\}) M \in B \to {coe}_{1} (\underset{x \in m \cup \{a\}}{\sum_{P}} M) (K) = \underset{x \in m \cup \{a\}}{\sum_{R}} {coe}_{1} (M) (K))$
106	105	ex	$⊢ (m \in Fin \land \neg a \in m \land φ) \to ((\forall x \in m M \in B \to {coe}_{1} (\underset{x \in m}{\sum_{P}} M) (K) = \underset{x \in m}{\sum_{R}} {coe}_{1} (M) (K)) \to (\forall x \in (m \cup \{a\}) M \in B \to {coe}_{1} (\underset{x \in m \cup \{a\}}{\sum_{P}} M) (K) = \underset{x \in m \cup \{a\}}{\sum_{R}} {coe}_{1} (M) (K)))$

Metamath Proof Explorer

Theorem coe1fzgsumdlem

Proof