evl1gsumdlem

Description: Lemma for evl1gsumd (induction step). (Contributed by AV, 17-Sep-2019)

	Ref	Expression
Hypotheses	evl1gsumd.q	$⊢ O = {eval}_{1} (R)$
	evl1gsumd.p	$⊢ P = {Poly}_{1} (R)$
	evl1gsumd.b	$⊢ B = {Base}_{R}$
	evl1gsumd.u	$⊢ U = {Base}_{P}$
	evl1gsumd.r	$⊢ φ \to R \in CRing$
	evl1gsumd.y	$⊢ φ \to Y \in B$
Assertion	evl1gsumdlem	$⊢ (m \in Fin \land \neg a \in m \land φ) \to ((\forall x \in m M \in U \to O (\underset{x \in m}{\sum_{P}} M) (Y) = \underset{x \in m}{\sum_{R}} O (M) (Y)) \to (\forall x \in (m \cup \{a\}) M \in U \to O (\underset{x \in m \cup \{a\}}{\sum_{P}} M) (Y) = \underset{x \in m \cup \{a\}}{\sum_{R}} O (M) (Y)))$

Proof

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

Metamath Proof Explorer

Theorem evl1gsumdlem

Proof