evl1gprodd

Description: Polynomial evaluation builder for a finite group product of polynomials. (Contributed by metakunt, 29-Apr-2025)

	Ref	Expression
Hypotheses	evl1gprodd.1	$⊢ O = {eval}_{1} (R)$
	evl1gprodd.2	$⊢ P = {Poly}_{1} (R)$
	evl1gprodd.3	$⊢ Q = {mulGrp}_{P}$
	evl1gprodd.4	$⊢ B = {Base}_{R}$
	evl1gprodd.5	$⊢ U = {Base}_{P}$
	evl1gprodd.6	$⊢ S = {mulGrp}_{R}$
	evl1gprodd.7	$⊢ φ \to R \in CRing$
	evl1gprodd.8	$⊢ φ \to Y \in B$
	evl1gprodd.9	$⊢ φ \to \forall x \in N M \in U$
	evl1gprodd.10	$⊢ φ \to N \in Fin$
Assertion	evl1gprodd	$⊢ φ \to O (\underset{x \in N}{\sum_{Q}} M) (Y) = \underset{x \in N}{\sum_{S}} O (M) (Y)$

Proof

Step	Hyp	Ref	Expression
1		evl1gprodd.1	$⊢ O = {eval}_{1} (R)$
2		evl1gprodd.2	$⊢ P = {Poly}_{1} (R)$
3		evl1gprodd.3	$⊢ Q = {mulGrp}_{P}$
4		evl1gprodd.4	$⊢ B = {Base}_{R}$
5		evl1gprodd.5	$⊢ U = {Base}_{P}$
6		evl1gprodd.6	$⊢ S = {mulGrp}_{R}$
7		evl1gprodd.7	$⊢ φ \to R \in CRing$
8		evl1gprodd.8	$⊢ φ \to Y \in B$
9		evl1gprodd.9	$⊢ φ \to \forall x \in N M \in U$
10		evl1gprodd.10	$⊢ φ \to N \in Fin$
11		mpteq1	$⊢ a = \emptyset \to (x \in a ⟼ M) = (x \in \emptyset ⟼ M)$
12	11	oveq2d	$⊢ a = \emptyset \to \underset{x \in a}{\sum_{Q}} M = \underset{x \in \emptyset}{\sum_{Q}} M$
13	12	fveq2d	$⊢ a = \emptyset \to O (\underset{x \in a}{\sum_{Q}} M) = O (\underset{x \in \emptyset}{\sum_{Q}} M)$
14	13	fveq1d	$⊢ a = \emptyset \to O (\underset{x \in a}{\sum_{Q}} M) (Y) = O (\underset{x \in \emptyset}{\sum_{Q}} M) (Y)$
15		mpteq1	$⊢ a = \emptyset \to (x \in a ⟼ O (M) (Y)) = (x \in \emptyset ⟼ O (M) (Y))$
16	15	oveq2d	$⊢ a = \emptyset \to \underset{x \in a}{\sum_{S}} O (M) (Y) = \underset{x \in \emptyset}{\sum_{S}} O (M) (Y)$
17	14 16	eqeq12d	$⊢ a = \emptyset \to (O (\underset{x \in a}{\sum_{Q}} M) (Y) = \underset{x \in a}{\sum_{S}} O (M) (Y) \leftrightarrow O (\underset{x \in \emptyset}{\sum_{Q}} M) (Y) = \underset{x \in \emptyset}{\sum_{S}} O (M) (Y))$
18		mpteq1	$⊢ a = b \to (x \in a ⟼ M) = (x \in b ⟼ M)$
19	18	oveq2d	$⊢ a = b \to \underset{x \in a}{\sum_{Q}} M = \underset{x \in b}{\sum_{Q}} M$
20	19	fveq2d	$⊢ a = b \to O (\underset{x \in a}{\sum_{Q}} M) = O (\underset{x \in b}{\sum_{Q}} M)$
21	20	fveq1d	$⊢ a = b \to O (\underset{x \in a}{\sum_{Q}} M) (Y) = O (\underset{x \in b}{\sum_{Q}} M) (Y)$
22		mpteq1	$⊢ a = b \to (x \in a ⟼ O (M) (Y)) = (x \in b ⟼ O (M) (Y))$
23	22	oveq2d	$⊢ a = b \to \underset{x \in a}{\sum_{S}} O (M) (Y) = \underset{x \in b}{\sum_{S}} O (M) (Y)$
24	21 23	eqeq12d	$⊢ a = b \to (O (\underset{x \in a}{\sum_{Q}} M) (Y) = \underset{x \in a}{\sum_{S}} O (M) (Y) \leftrightarrow O (\underset{x \in b}{\sum_{Q}} M) (Y) = \underset{x \in b}{\sum_{S}} O (M) (Y))$
25		mpteq1	$⊢ a = b \cup \{c\} \to (x \in a ⟼ M) = (x \in (b \cup \{c\}) ⟼ M)$
26	25	oveq2d	$⊢ a = b \cup \{c\} \to \underset{x \in a}{\sum_{Q}} M = \underset{x \in b \cup \{c\}}{\sum_{Q}} M$
27	26	fveq2d	$⊢ a = b \cup \{c\} \to O (\underset{x \in a}{\sum_{Q}} M) = O (\underset{x \in b \cup \{c\}}{\sum_{Q}} M)$
28	27	fveq1d	$⊢ a = b \cup \{c\} \to O (\underset{x \in a}{\sum_{Q}} M) (Y) = O (\underset{x \in b \cup \{c\}}{\sum_{Q}} M) (Y)$
29		mpteq1	$⊢ a = b \cup \{c\} \to (x \in a ⟼ O (M) (Y)) = (x \in (b \cup \{c\}) ⟼ O (M) (Y))$
30	29	oveq2d	$⊢ a = b \cup \{c\} \to \underset{x \in a}{\sum_{S}} O (M) (Y) = \underset{x \in b \cup \{c\}}{\sum_{S}} O (M) (Y)$
31	28 30	eqeq12d	$⊢ a = b \cup \{c\} \to (O (\underset{x \in a}{\sum_{Q}} M) (Y) = \underset{x \in a}{\sum_{S}} O (M) (Y) \leftrightarrow O (\underset{x \in b \cup \{c\}}{\sum_{Q}} M) (Y) = \underset{x \in b \cup \{c\}}{\sum_{S}} O (M) (Y))$
32		mpteq1	$⊢ a = N \to (x \in a ⟼ M) = (x \in N ⟼ M)$
33	32	oveq2d	$⊢ a = N \to \underset{x \in a}{\sum_{Q}} M = \underset{x \in N}{\sum_{Q}} M$
34	33	fveq2d	$⊢ a = N \to O (\underset{x \in a}{\sum_{Q}} M) = O (\underset{x \in N}{\sum_{Q}} M)$
35	34	fveq1d	$⊢ a = N \to O (\underset{x \in a}{\sum_{Q}} M) (Y) = O (\underset{x \in N}{\sum_{Q}} M) (Y)$
36		mpteq1	$⊢ a = N \to (x \in a ⟼ O (M) (Y)) = (x \in N ⟼ O (M) (Y))$
37	36	oveq2d	$⊢ a = N \to \underset{x \in a}{\sum_{S}} O (M) (Y) = \underset{x \in N}{\sum_{S}} O (M) (Y)$
38	35 37	eqeq12d	$⊢ a = N \to (O (\underset{x \in a}{\sum_{Q}} M) (Y) = \underset{x \in a}{\sum_{S}} O (M) (Y) \leftrightarrow O (\underset{x \in N}{\sum_{Q}} M) (Y) = \underset{x \in N}{\sum_{S}} O (M) (Y))$
39		mpt0	$⊢ (x \in \emptyset ⟼ M) = \emptyset$
40	39	a1i	$⊢ φ \to (x \in \emptyset ⟼ M) = \emptyset$
41	40	oveq2d	$⊢ φ \to \underset{x \in \emptyset}{\sum_{Q}} M = \sum_{Q} \emptyset$
42	41	fveq2d	$⊢ φ \to O (\underset{x \in \emptyset}{\sum_{Q}} M) = O (\sum_{Q} \emptyset)$
43	42	fveq1d	$⊢ φ \to O (\underset{x \in \emptyset}{\sum_{Q}} M) (Y) = O (\sum_{Q} \emptyset) (Y)$
44		mpt0	$⊢ (x \in \emptyset ⟼ O (M) (Y)) = \emptyset$
45	44	a1i	$⊢ φ \to (x \in \emptyset ⟼ O (M) (Y)) = \emptyset$
46	45	oveq2d	$⊢ φ \to \underset{x \in \emptyset}{\sum_{S}} O (M) (Y) = \sum_{S} \emptyset$
47		eqid	$⊢ 0_{S} = 0_{S}$
48	47	gsum0	$⊢ \sum_{S} \emptyset = 0_{S}$
49	48	a1i	$⊢ φ \to \sum_{S} \emptyset = 0_{S}$
50		eqid	$⊢ 1_{R} = 1_{R}$
51	6 50	ringidval	$⊢ 1_{R} = 0_{S}$
52	51	eqcomi	$⊢ 0_{S} = 1_{R}$
53	52	a1i	$⊢ φ \to 0_{S} = 1_{R}$
54		eqid	$⊢ algSc (P) = algSc (P)$
55	7	crngringd	$⊢ φ \to R \in Ring$
56	6	ringmgp	$⊢ R \in Ring \to S \in Mnd$
57	55 56	syl	$⊢ φ \to S \in Mnd$
58		eqid	$⊢ {Base}_{S} = {Base}_{S}$
59	58 47	mndidcl	$⊢ S \in Mnd \to 0_{S} \in {Base}_{S}$
60	57 59	syl	$⊢ φ \to 0_{S} \in {Base}_{S}$
61		eqid	$⊢ {Base}_{R} = {Base}_{R}$
62	6 61	mgpbas	$⊢ {Base}_{R} = {Base}_{S}$
63	4 62	eqtri	$⊢ B = {Base}_{S}$
64	60 63	eleqtrrdi	$⊢ φ \to 0_{S} \in B$
65	51	a1i	$⊢ φ \to 1_{R} = 0_{S}$
66	65	eleq1d	$⊢ φ \to (1_{R} \in B \leftrightarrow 0_{S} \in B)$
67	64 66	mpbird	$⊢ φ \to 1_{R} \in B$
68	1 2 4 54 5 7 67 8	evl1scad	$⊢ φ \to (algSc (P) (1_{R}) \in U \land O (algSc (P) (1_{R})) (Y) = 1_{R})$
69	68	simprd	$⊢ φ \to O (algSc (P) (1_{R})) (Y) = 1_{R}$
70	69	eqcomd	$⊢ φ \to 1_{R} = O (algSc (P) (1_{R})) (Y)$
71		eqid	$⊢ 1_{P} = 1_{P}$
72	2 54 50 71	ply1scl1	$⊢ R \in Ring \to algSc (P) (1_{R}) = 1_{P}$
73	55 72	syl	$⊢ φ \to algSc (P) (1_{R}) = 1_{P}$
74	3 71	ringidval	$⊢ 1_{P} = 0_{Q}$
75	74	a1i	$⊢ φ \to 1_{P} = 0_{Q}$
76	73 75	eqtrd	$⊢ φ \to algSc (P) (1_{R}) = 0_{Q}$
77	76	fveq2d	$⊢ φ \to O (algSc (P) (1_{R})) = O (0_{Q})$
78	77	fveq1d	$⊢ φ \to O (algSc (P) (1_{R})) (Y) = O (0_{Q}) (Y)$
79	70 78	eqtrd	$⊢ φ \to 1_{R} = O (0_{Q}) (Y)$
80	53 79	eqtrd	$⊢ φ \to 0_{S} = O (0_{Q}) (Y)$
81		eqid	$⊢ 0_{Q} = 0_{Q}$
82	81	gsum0	$⊢ \sum_{Q} \emptyset = 0_{Q}$
83	82	a1i	$⊢ φ \to \sum_{Q} \emptyset = 0_{Q}$
84	83	eqcomd	$⊢ φ \to 0_{Q} = \sum_{Q} \emptyset$
85	84	fveq2d	$⊢ φ \to O (0_{Q}) = O (\sum_{Q} \emptyset)$
86	85	fveq1d	$⊢ φ \to O (0_{Q}) (Y) = O (\sum_{Q} \emptyset) (Y)$
87	49 80 86	3eqtrd	$⊢ φ \to \sum_{S} \emptyset = O (\sum_{Q} \emptyset) (Y)$
88	46 87	eqtr2d	$⊢ φ \to O (\sum_{Q} \emptyset) (Y) = \underset{x \in \emptyset}{\sum_{S}} O (M) (Y)$
89	43 88	eqtrd	$⊢ φ \to O (\underset{x \in \emptyset}{\sum_{Q}} M) (Y) = \underset{x \in \emptyset}{\sum_{S}} O (M) (Y)$
90		nfcv	$⊢ \underline{Ⅎ} y M$
91		nfcsb1v	$⊢ \underline{Ⅎ} x ⦋ y / x ⦌ M$
92		csbeq1a	$⊢ x = y \to M = ⦋ y / x ⦌ M$
93	90 91 92	cbvmpt	$⊢ (x \in (b \cup \{c\}) ⟼ M) = (y \in (b \cup \{c\}) ⟼ ⦋ y / x ⦌ M)$
94	93	a1i	$⊢ ((φ \land (b \subseteq N \land c \in (N ∖ b))) \land O (\underset{x \in b}{\sum_{Q}} M) (Y) = \underset{x \in b}{\sum_{S}} O (M) (Y)) \to (x \in (b \cup \{c\}) ⟼ M) = (y \in (b \cup \{c\}) ⟼ ⦋ y / x ⦌ M)$
95	94	oveq2d	$⊢ ((φ \land (b \subseteq N \land c \in (N ∖ b))) \land O (\underset{x \in b}{\sum_{Q}} M) (Y) = \underset{x \in b}{\sum_{S}} O (M) (Y)) \to \underset{x \in b \cup \{c\}}{\sum_{Q}} M = \underset{y \in b \cup \{c\}}{\sum_{Q}} ⦋ y / x ⦌ M$
96	95	fveq2d	$⊢ ((φ \land (b \subseteq N \land c \in (N ∖ b))) \land O (\underset{x \in b}{\sum_{Q}} M) (Y) = \underset{x \in b}{\sum_{S}} O (M) (Y)) \to O (\underset{x \in b \cup \{c\}}{\sum_{Q}} M) = O (\underset{y \in b \cup \{c\}}{\sum_{Q}} ⦋ y / x ⦌ M)$
97	96	fveq1d	$⊢ ((φ \land (b \subseteq N \land c \in (N ∖ b))) \land O (\underset{x \in b}{\sum_{Q}} M) (Y) = \underset{x \in b}{\sum_{S}} O (M) (Y)) \to O (\underset{x \in b \cup \{c\}}{\sum_{Q}} M) (Y) = O (\underset{y \in b \cup \{c\}}{\sum_{Q}} ⦋ y / x ⦌ M) (Y)$
98		eqid	$⊢ {Base}_{Q} = {Base}_{Q}$
99		eqid	$⊢ \cdot_{P} = \cdot_{P}$
100	3 99	mgpplusg	$⊢ \cdot_{P} = +_{Q}$
101	2	ply1crng	$⊢ R \in CRing \to P \in CRing$
102	7 101	syl	$⊢ φ \to P \in CRing$
103	3	crngmgp	$⊢ P \in CRing \to Q \in CMnd$
104	102 103	syl	$⊢ φ \to Q \in CMnd$
105	104	adantr	$⊢ (φ \land (b \subseteq N \land c \in (N ∖ b))) \to Q \in CMnd$
106	105	adantr	$⊢ ((φ \land (b \subseteq N \land c \in (N ∖ b))) \land O (\underset{x \in b}{\sum_{Q}} M) (Y) = \underset{x \in b}{\sum_{S}} O (M) (Y)) \to Q \in CMnd$
107	10	ad2antrr	$⊢ ((φ \land (b \subseteq N \land c \in (N ∖ b))) \land O (\underset{x \in b}{\sum_{Q}} M) (Y) = \underset{x \in b}{\sum_{S}} O (M) (Y)) \to N \in Fin$
108		simplrl	$⊢ ((φ \land (b \subseteq N \land c \in (N ∖ b))) \land O (\underset{x \in b}{\sum_{Q}} M) (Y) = \underset{x \in b}{\sum_{S}} O (M) (Y)) \to b \subseteq N$
109	107 108	ssfid	$⊢ ((φ \land (b \subseteq N \land c \in (N ∖ b))) \land O (\underset{x \in b}{\sum_{Q}} M) (Y) = \underset{x \in b}{\sum_{S}} O (M) (Y)) \to b \in Fin$
110	9	ad3antrrr	$⊢ (((φ \land (b \subseteq N \land c \in (N ∖ b))) \land O (\underset{x \in b}{\sum_{Q}} M) (Y) = \underset{x \in b}{\sum_{S}} O (M) (Y)) \land y \in b) \to \forall x \in N M \in U$
111	108	sselda	$⊢ (((φ \land (b \subseteq N \land c \in (N ∖ b))) \land O (\underset{x \in b}{\sum_{Q}} M) (Y) = \underset{x \in b}{\sum_{S}} O (M) (Y)) \land y \in b) \to y \in N$
112		rspcsbela	$⊢ (y \in N \land \forall x \in N M \in U) \to ⦋ y / x ⦌ M \in U$
113	112	expcom	$⊢ \forall x \in N M \in U \to (y \in N \to ⦋ y / x ⦌ M \in U)$
114	113	imp	$⊢ (\forall x \in N M \in U \land y \in N) \to ⦋ y / x ⦌ M \in U$
115	110 111 114	syl2anc	$⊢ (((φ \land (b \subseteq N \land c \in (N ∖ b))) \land O (\underset{x \in b}{\sum_{Q}} M) (Y) = \underset{x \in b}{\sum_{S}} O (M) (Y)) \land y \in b) \to ⦋ y / x ⦌ M \in U$
116	3 5	mgpbas	$⊢ U = {Base}_{Q}$
117	116	eqcomi	$⊢ {Base}_{Q} = U$
118	117	a1i	$⊢ φ \to {Base}_{Q} = U$
119	118	adantr	$⊢ (φ \land (b \subseteq N \land c \in (N ∖ b))) \to {Base}_{Q} = U$
120	119	adantr	$⊢ ((φ \land (b \subseteq N \land c \in (N ∖ b))) \land O (\underset{x \in b}{\sum_{Q}} M) (Y) = \underset{x \in b}{\sum_{S}} O (M) (Y)) \to {Base}_{Q} = U$
121	120	adantr	$⊢ (((φ \land (b \subseteq N \land c \in (N ∖ b))) \land O (\underset{x \in b}{\sum_{Q}} M) (Y) = \underset{x \in b}{\sum_{S}} O (M) (Y)) \land y \in b) \to {Base}_{Q} = U$
122	121	eleq2d	$⊢ (((φ \land (b \subseteq N \land c \in (N ∖ b))) \land O (\underset{x \in b}{\sum_{Q}} M) (Y) = \underset{x \in b}{\sum_{S}} O (M) (Y)) \land y \in b) \to (⦋ y / x ⦌ M \in {Base}_{Q} \leftrightarrow ⦋ y / x ⦌ M \in U)$
123	115 122	mpbird	$⊢ (((φ \land (b \subseteq N \land c \in (N ∖ b))) \land O (\underset{x \in b}{\sum_{Q}} M) (Y) = \underset{x \in b}{\sum_{S}} O (M) (Y)) \land y \in b) \to ⦋ y / x ⦌ M \in {Base}_{Q}$
124		simplrr	$⊢ ((φ \land (b \subseteq N \land c \in (N ∖ b))) \land O (\underset{x \in b}{\sum_{Q}} M) (Y) = \underset{x \in b}{\sum_{S}} O (M) (Y)) \to c \in (N ∖ b)$
125	124	eldifbd	$⊢ ((φ \land (b \subseteq N \land c \in (N ∖ b))) \land O (\underset{x \in b}{\sum_{Q}} M) (Y) = \underset{x \in b}{\sum_{S}} O (M) (Y)) \to \neg c \in b$
126	124	eldifad	$⊢ ((φ \land (b \subseteq N \land c \in (N ∖ b))) \land O (\underset{x \in b}{\sum_{Q}} M) (Y) = \underset{x \in b}{\sum_{S}} O (M) (Y)) \to c \in N$
127	9	ad2antrr	$⊢ ((φ \land (b \subseteq N \land c \in (N ∖ b))) \land O (\underset{x \in b}{\sum_{Q}} M) (Y) = \underset{x \in b}{\sum_{S}} O (M) (Y)) \to \forall x \in N M \in U$
128		rspcsbela	$⊢ (c \in N \land \forall x \in N M \in U) \to ⦋ c / x ⦌ M \in U$
129	126 127 128	syl2anc	$⊢ ((φ \land (b \subseteq N \land c \in (N ∖ b))) \land O (\underset{x \in b}{\sum_{Q}} M) (Y) = \underset{x \in b}{\sum_{S}} O (M) (Y)) \to ⦋ c / x ⦌ M \in U$
130	120	eleq2d	$⊢ ((φ \land (b \subseteq N \land c \in (N ∖ b))) \land O (\underset{x \in b}{\sum_{Q}} M) (Y) = \underset{x \in b}{\sum_{S}} O (M) (Y)) \to (⦋ c / x ⦌ M \in {Base}_{Q} \leftrightarrow ⦋ c / x ⦌ M \in U)$
131	129 130	mpbird	$⊢ ((φ \land (b \subseteq N \land c \in (N ∖ b))) \land O (\underset{x \in b}{\sum_{Q}} M) (Y) = \underset{x \in b}{\sum_{S}} O (M) (Y)) \to ⦋ c / x ⦌ M \in {Base}_{Q}$
132		csbeq1	$⊢ y = c \to ⦋ y / x ⦌ M = ⦋ c / x ⦌ M$
133	98 100 106 109 123 124 125 131 132	gsumunsn	$⊢ ((φ \land (b \subseteq N \land c \in (N ∖ b))) \land O (\underset{x \in b}{\sum_{Q}} M) (Y) = \underset{x \in b}{\sum_{S}} O (M) (Y)) \to \underset{y \in b \cup \{c\}}{\sum_{Q}} ⦋ y / x ⦌ M = (\underset{y \in b}{\sum_{Q}}, ⦋ y / x ⦌ M) \cdot_{P} ⦋ c / x ⦌ M$
134	133	fveq2d	$⊢ ((φ \land (b \subseteq N \land c \in (N ∖ b))) \land O (\underset{x \in b}{\sum_{Q}} M) (Y) = \underset{x \in b}{\sum_{S}} O (M) (Y)) \to O (\underset{y \in b \cup \{c\}}{\sum_{Q}} ⦋ y / x ⦌ M) = O ((\underset{y \in b}{\sum_{Q}}, ⦋ y / x ⦌ M) \cdot_{P} ⦋ c / x ⦌ M)$
135	134	fveq1d	$⊢ ((φ \land (b \subseteq N \land c \in (N ∖ b))) \land O (\underset{x \in b}{\sum_{Q}} M) (Y) = \underset{x \in b}{\sum_{S}} O (M) (Y)) \to O (\underset{y \in b \cup \{c\}}{\sum_{Q}} ⦋ y / x ⦌ M) (Y) = O ((\underset{y \in b}{\sum_{Q}}, ⦋ y / x ⦌ M) \cdot_{P} ⦋ c / x ⦌ M) (Y)$
136	7	ad2antrr	$⊢ ((φ \land (b \subseteq N \land c \in (N ∖ b))) \land O (\underset{x \in b}{\sum_{Q}} M) (Y) = \underset{x \in b}{\sum_{S}} O (M) (Y)) \to R \in CRing$
137	8	ad2antrr	$⊢ ((φ \land (b \subseteq N \land c \in (N ∖ b))) \land O (\underset{x \in b}{\sum_{Q}} M) (Y) = \underset{x \in b}{\sum_{S}} O (M) (Y)) \to Y \in B$
138	115	ralrimiva	$⊢ ((φ \land (b \subseteq N \land c \in (N ∖ b))) \land O (\underset{x \in b}{\sum_{Q}} M) (Y) = \underset{x \in b}{\sum_{S}} O (M) (Y)) \to \forall y \in b ⦋ y / x ⦌ M \in U$
139	116 106 109 138	gsummptcl	$⊢ ((φ \land (b \subseteq N \land c \in (N ∖ b))) \land O (\underset{x \in b}{\sum_{Q}} M) (Y) = \underset{x \in b}{\sum_{S}} O (M) (Y)) \to \underset{y \in b}{\sum_{Q}} ⦋ y / x ⦌ M \in U$
140	92	equcoms	$⊢ y = x \to M = ⦋ y / x ⦌ M$
141	140	eqcomd	$⊢ y = x \to ⦋ y / x ⦌ M = M$
142	91 90 141	cbvmpt	$⊢ (y \in b ⟼ ⦋ y / x ⦌ M) = (x \in b ⟼ M)$
143	142	a1i	$⊢ ((φ \land (b \subseteq N \land c \in (N ∖ b))) \land O (\underset{x \in b}{\sum_{Q}} M) (Y) = \underset{x \in b}{\sum_{S}} O (M) (Y)) \to (y \in b ⟼ ⦋ y / x ⦌ M) = (x \in b ⟼ M)$
144	143	oveq2d	$⊢ ((φ \land (b \subseteq N \land c \in (N ∖ b))) \land O (\underset{x \in b}{\sum_{Q}} M) (Y) = \underset{x \in b}{\sum_{S}} O (M) (Y)) \to \underset{y \in b}{\sum_{Q}} ⦋ y / x ⦌ M = \underset{x \in b}{\sum_{Q}} M$
145	144	fveq2d	$⊢ ((φ \land (b \subseteq N \land c \in (N ∖ b))) \land O (\underset{x \in b}{\sum_{Q}} M) (Y) = \underset{x \in b}{\sum_{S}} O (M) (Y)) \to O (\underset{y \in b}{\sum_{Q}} ⦋ y / x ⦌ M) = O (\underset{x \in b}{\sum_{Q}} M)$
146	145	fveq1d	$⊢ ((φ \land (b \subseteq N \land c \in (N ∖ b))) \land O (\underset{x \in b}{\sum_{Q}} M) (Y) = \underset{x \in b}{\sum_{S}} O (M) (Y)) \to O (\underset{y \in b}{\sum_{Q}} ⦋ y / x ⦌ M) (Y) = O (\underset{x \in b}{\sum_{Q}} M) (Y)$
147	139 146	jca	$⊢ ((φ \land (b \subseteq N \land c \in (N ∖ b))) \land O (\underset{x \in b}{\sum_{Q}} M) (Y) = \underset{x \in b}{\sum_{S}} O (M) (Y)) \to (\underset{y \in b}{\sum_{Q}} ⦋ y / x ⦌ M \in U \land O (\underset{y \in b}{\sum_{Q}} ⦋ y / x ⦌ M) (Y) = O (\underset{x \in b}{\sum_{Q}} M) (Y))$
148		eqidd	$⊢ ((φ \land (b \subseteq N \land c \in (N ∖ b))) \land O (\underset{x \in b}{\sum_{Q}} M) (Y) = \underset{x \in b}{\sum_{S}} O (M) (Y)) \to O (⦋ c / x ⦌ M) (Y) = O (⦋ c / x ⦌ M) (Y)$
149	129 148	jca	$⊢ ((φ \land (b \subseteq N \land c \in (N ∖ b))) \land O (\underset{x \in b}{\sum_{Q}} M) (Y) = \underset{x \in b}{\sum_{S}} O (M) (Y)) \to (⦋ c / x ⦌ M \in U \land O (⦋ c / x ⦌ M) (Y) = O (⦋ c / x ⦌ M) (Y))$
150		eqid	$⊢ \cdot_{R} = \cdot_{R}$
151	1 2 4 5 136 137 147 149 99 150	evl1muld	$⊢ ((φ \land (b \subseteq N \land c \in (N ∖ b))) \land O (\underset{x \in b}{\sum_{Q}} M) (Y) = \underset{x \in b}{\sum_{S}} O (M) (Y)) \to ((\underset{y \in b}{\sum_{Q}}, ⦋ y / x ⦌ M) \cdot_{P} ⦋ c / x ⦌ M \in U \land O ((\underset{y \in b}{\sum_{Q}}, ⦋ y / x ⦌ M) \cdot_{P} ⦋ c / x ⦌ M) (Y) = O (\underset{x \in b}{\sum_{Q}} M) (Y) \cdot_{R} O (⦋ c / x ⦌ M) (Y))$
152	151	simprd	$⊢ ((φ \land (b \subseteq N \land c \in (N ∖ b))) \land O (\underset{x \in b}{\sum_{Q}} M) (Y) = \underset{x \in b}{\sum_{S}} O (M) (Y)) \to O ((\underset{y \in b}{\sum_{Q}}, ⦋ y / x ⦌ M) \cdot_{P} ⦋ c / x ⦌ M) (Y) = O (\underset{x \in b}{\sum_{Q}} M) (Y) \cdot_{R} O (⦋ c / x ⦌ M) (Y)$
153	135 152	eqtrd	$⊢ ((φ \land (b \subseteq N \land c \in (N ∖ b))) \land O (\underset{x \in b}{\sum_{Q}} M) (Y) = \underset{x \in b}{\sum_{S}} O (M) (Y)) \to O (\underset{y \in b \cup \{c\}}{\sum_{Q}} ⦋ y / x ⦌ M) (Y) = O (\underset{x \in b}{\sum_{Q}} M) (Y) \cdot_{R} O (⦋ c / x ⦌ M) (Y)$
154	97 153	eqtrd	$⊢ ((φ \land (b \subseteq N \land c \in (N ∖ b))) \land O (\underset{x \in b}{\sum_{Q}} M) (Y) = \underset{x \in b}{\sum_{S}} O (M) (Y)) \to O (\underset{x \in b \cup \{c\}}{\sum_{Q}} M) (Y) = O (\underset{x \in b}{\sum_{Q}} M) (Y) \cdot_{R} O (⦋ c / x ⦌ M) (Y)$
155	6 150	mgpplusg	$⊢ \cdot_{R} = +_{S}$
156		eqid	$⊢ {mulGrp}_{R} = {mulGrp}_{R}$
157	156	crngmgp	$⊢ R \in CRing \to {mulGrp}_{R} \in CMnd$
158	7 157	syl	$⊢ φ \to {mulGrp}_{R} \in CMnd$
159	6 158	eqeltrid	$⊢ φ \to S \in CMnd$
160	159	adantr	$⊢ (φ \land (b \subseteq N \land c \in (N ∖ b))) \to S \in CMnd$
161	160	adantr	$⊢ ((φ \land (b \subseteq N \land c \in (N ∖ b))) \land O (\underset{x \in b}{\sum_{Q}} M) (Y) = \underset{x \in b}{\sum_{S}} O (M) (Y)) \to S \in CMnd$
162		csbfv12	$⊢ ⦋ y / x ⦌ O (M) (Y) = ⦋ y / x ⦌ O (M) (⦋ y / x ⦌ Y)$
163		csbfv2g	$⊢ y \in V \to ⦋ y / x ⦌ O (M) = O (⦋ y / x ⦌ M)$
164	163	elv	$⊢ ⦋ y / x ⦌ O (M) = O (⦋ y / x ⦌ M)$
165		vex	$⊢ y \in V$
166		nfcv	$⊢ \underline{Ⅎ} x Y$
167	165 166	csbgfi	$⊢ ⦋ y / x ⦌ Y = Y$
168	164 167	fveq12i	$⊢ ⦋ y / x ⦌ O (M) (⦋ y / x ⦌ Y) = O (⦋ y / x ⦌ M) (Y)$
169	162 168	eqtri	$⊢ ⦋ y / x ⦌ O (M) (Y) = O (⦋ y / x ⦌ M) (Y)$
170	62	eqcomi	$⊢ {Base}_{S} = {Base}_{R}$
171	7	ad3antrrr	$⊢ (((φ \land (b \subseteq N \land c \in (N ∖ b))) \land O (\underset{x \in b}{\sum_{Q}} M) (Y) = \underset{x \in b}{\sum_{S}} O (M) (Y)) \land y \in b) \to R \in CRing$
172	8	ad3antrrr	$⊢ (((φ \land (b \subseteq N \land c \in (N ∖ b))) \land O (\underset{x \in b}{\sum_{Q}} M) (Y) = \underset{x \in b}{\sum_{S}} O (M) (Y)) \land y \in b) \to Y \in B$
173	63	eqcomi	$⊢ {Base}_{S} = B$
174	173	a1i	$⊢ (((φ \land (b \subseteq N \land c \in (N ∖ b))) \land O (\underset{x \in b}{\sum_{Q}} M) (Y) = \underset{x \in b}{\sum_{S}} O (M) (Y)) \land y \in b) \to {Base}_{S} = B$
175	174	eleq2d	$⊢ (((φ \land (b \subseteq N \land c \in (N ∖ b))) \land O (\underset{x \in b}{\sum_{Q}} M) (Y) = \underset{x \in b}{\sum_{S}} O (M) (Y)) \land y \in b) \to (Y \in {Base}_{S} \leftrightarrow Y \in B)$
176	172 175	mpbird	$⊢ (((φ \land (b \subseteq N \land c \in (N ∖ b))) \land O (\underset{x \in b}{\sum_{Q}} M) (Y) = \underset{x \in b}{\sum_{S}} O (M) (Y)) \land y \in b) \to Y \in {Base}_{S}$
177	1 2 170 5 171 176 115	fveval1fvcl	$⊢ (((φ \land (b \subseteq N \land c \in (N ∖ b))) \land O (\underset{x \in b}{\sum_{Q}} M) (Y) = \underset{x \in b}{\sum_{S}} O (M) (Y)) \land y \in b) \to O (⦋ y / x ⦌ M) (Y) \in {Base}_{S}$
178	169 177	eqeltrid	$⊢ (((φ \land (b \subseteq N \land c \in (N ∖ b))) \land O (\underset{x \in b}{\sum_{Q}} M) (Y) = \underset{x \in b}{\sum_{S}} O (M) (Y)) \land y \in b) \to ⦋ y / x ⦌ O (M) (Y) \in {Base}_{S}$
179	1 2 4 5 136 137 129	fveval1fvcl	$⊢ ((φ \land (b \subseteq N \land c \in (N ∖ b))) \land O (\underset{x \in b}{\sum_{Q}} M) (Y) = \underset{x \in b}{\sum_{S}} O (M) (Y)) \to O (⦋ c / x ⦌ M) (Y) \in B$
180	179 63	eleqtrdi	$⊢ ((φ \land (b \subseteq N \land c \in (N ∖ b))) \land O (\underset{x \in b}{\sum_{Q}} M) (Y) = \underset{x \in b}{\sum_{S}} O (M) (Y)) \to O (⦋ c / x ⦌ M) (Y) \in {Base}_{S}$
181		nfcv	$⊢ \underline{Ⅎ} x c$
182		nfcv	$⊢ \underline{Ⅎ} x O$
183	181	nfcsb1	$⊢ \underline{Ⅎ} x ⦋ c / x ⦌ M$
184	182 183	nffv	$⊢ \underline{Ⅎ} x O (⦋ c / x ⦌ M)$
185	184 166	nffv	$⊢ \underline{Ⅎ} x O (⦋ c / x ⦌ M) (Y)$
186		csbeq1a	$⊢ x = c \to M = ⦋ c / x ⦌ M$
187	186	fveq2d	$⊢ x = c \to O (M) = O (⦋ c / x ⦌ M)$
188	187	fveq1d	$⊢ x = c \to O (M) (Y) = O (⦋ c / x ⦌ M) (Y)$
189	181 185 188	csbhypf	$⊢ y = c \to ⦋ y / x ⦌ O (M) (Y) = O (⦋ c / x ⦌ M) (Y)$
190	58 155 161 109 178 124 125 180 189	gsumunsn	$⊢ ((φ \land (b \subseteq N \land c \in (N ∖ b))) \land O (\underset{x \in b}{\sum_{Q}} M) (Y) = \underset{x \in b}{\sum_{S}} O (M) (Y)) \to \underset{y \in b \cup \{c\}}{\sum_{S}} ⦋ y / x ⦌ O (M) (Y) = (\underset{y \in b}{\sum_{S}}, ⦋ y / x ⦌ O (M) (Y)) \cdot_{R} O (⦋ c / x ⦌ M) (Y)$
191		simpr	$⊢ ((φ \land (b \subseteq N \land c \in (N ∖ b))) \land O (\underset{x \in b}{\sum_{Q}} M) (Y) = \underset{x \in b}{\sum_{S}} O (M) (Y)) \to O (\underset{x \in b}{\sum_{Q}} M) (Y) = \underset{x \in b}{\sum_{S}} O (M) (Y)$
192		nfcv	$⊢ \underline{Ⅎ} y O (M) (Y)$
193		nfcsb1v	$⊢ \underline{Ⅎ} x ⦋ y / x ⦌ O (M) (Y)$
194		csbeq1a	$⊢ x = y \to O (M) (Y) = ⦋ y / x ⦌ O (M) (Y)$
195	192 193 194	cbvmpt	$⊢ (x \in b ⟼ O (M) (Y)) = (y \in b ⟼ ⦋ y / x ⦌ O (M) (Y))$
196	195	a1i	$⊢ ((φ \land (b \subseteq N \land c \in (N ∖ b))) \land O (\underset{x \in b}{\sum_{Q}} M) (Y) = \underset{x \in b}{\sum_{S}} O (M) (Y)) \to (x \in b ⟼ O (M) (Y)) = (y \in b ⟼ ⦋ y / x ⦌ O (M) (Y))$
197	196	oveq2d	$⊢ ((φ \land (b \subseteq N \land c \in (N ∖ b))) \land O (\underset{x \in b}{\sum_{Q}} M) (Y) = \underset{x \in b}{\sum_{S}} O (M) (Y)) \to \underset{x \in b}{\sum_{S}} O (M) (Y) = \underset{y \in b}{\sum_{S}} ⦋ y / x ⦌ O (M) (Y)$
198	191 197	eqtr2d	$⊢ ((φ \land (b \subseteq N \land c \in (N ∖ b))) \land O (\underset{x \in b}{\sum_{Q}} M) (Y) = \underset{x \in b}{\sum_{S}} O (M) (Y)) \to \underset{y \in b}{\sum_{S}} ⦋ y / x ⦌ O (M) (Y) = O (\underset{x \in b}{\sum_{Q}} M) (Y)$
199	198	oveq1d	$⊢ ((φ \land (b \subseteq N \land c \in (N ∖ b))) \land O (\underset{x \in b}{\sum_{Q}} M) (Y) = \underset{x \in b}{\sum_{S}} O (M) (Y)) \to (\underset{y \in b}{\sum_{S}}, ⦋ y / x ⦌ O (M) (Y)) \cdot_{R} O (⦋ c / x ⦌ M) (Y) = O (\underset{x \in b}{\sum_{Q}} M) (Y) \cdot_{R} O (⦋ c / x ⦌ M) (Y)$
200	190 199	eqtrd	$⊢ ((φ \land (b \subseteq N \land c \in (N ∖ b))) \land O (\underset{x \in b}{\sum_{Q}} M) (Y) = \underset{x \in b}{\sum_{S}} O (M) (Y)) \to \underset{y \in b \cup \{c\}}{\sum_{S}} ⦋ y / x ⦌ O (M) (Y) = O (\underset{x \in b}{\sum_{Q}} M) (Y) \cdot_{R} O (⦋ c / x ⦌ M) (Y)$
201	200	eqcomd	$⊢ ((φ \land (b \subseteq N \land c \in (N ∖ b))) \land O (\underset{x \in b}{\sum_{Q}} M) (Y) = \underset{x \in b}{\sum_{S}} O (M) (Y)) \to O (\underset{x \in b}{\sum_{Q}} M) (Y) \cdot_{R} O (⦋ c / x ⦌ M) (Y) = \underset{y \in b \cup \{c\}}{\sum_{S}} ⦋ y / x ⦌ O (M) (Y)$
202	154 201	eqtrd	$⊢ ((φ \land (b \subseteq N \land c \in (N ∖ b))) \land O (\underset{x \in b}{\sum_{Q}} M) (Y) = \underset{x \in b}{\sum_{S}} O (M) (Y)) \to O (\underset{x \in b \cup \{c\}}{\sum_{Q}} M) (Y) = \underset{y \in b \cup \{c\}}{\sum_{S}} ⦋ y / x ⦌ O (M) (Y)$
203	192 193 194	cbvmpt	$⊢ (x \in (b \cup \{c\}) ⟼ O (M) (Y)) = (y \in (b \cup \{c\}) ⟼ ⦋ y / x ⦌ O (M) (Y))$
204	203	eqcomi	$⊢ (y \in (b \cup \{c\}) ⟼ ⦋ y / x ⦌ O (M) (Y)) = (x \in (b \cup \{c\}) ⟼ O (M) (Y))$
205	204	a1i	$⊢ ((φ \land (b \subseteq N \land c \in (N ∖ b))) \land O (\underset{x \in b}{\sum_{Q}} M) (Y) = \underset{x \in b}{\sum_{S}} O (M) (Y)) \to (y \in (b \cup \{c\}) ⟼ ⦋ y / x ⦌ O (M) (Y)) = (x \in (b \cup \{c\}) ⟼ O (M) (Y))$
206	205	oveq2d	$⊢ ((φ \land (b \subseteq N \land c \in (N ∖ b))) \land O (\underset{x \in b}{\sum_{Q}} M) (Y) = \underset{x \in b}{\sum_{S}} O (M) (Y)) \to \underset{y \in b \cup \{c\}}{\sum_{S}} ⦋ y / x ⦌ O (M) (Y) = \underset{x \in b \cup \{c\}}{\sum_{S}} O (M) (Y)$
207	202 206	eqtrd	$⊢ ((φ \land (b \subseteq N \land c \in (N ∖ b))) \land O (\underset{x \in b}{\sum_{Q}} M) (Y) = \underset{x \in b}{\sum_{S}} O (M) (Y)) \to O (\underset{x \in b \cup \{c\}}{\sum_{Q}} M) (Y) = \underset{x \in b \cup \{c\}}{\sum_{S}} O (M) (Y)$
208	207	ex	$⊢ (φ \land (b \subseteq N \land c \in (N ∖ b))) \to (O (\underset{x \in b}{\sum_{Q}} M) (Y) = \underset{x \in b}{\sum_{S}} O (M) (Y) \to O (\underset{x \in b \cup \{c\}}{\sum_{Q}} M) (Y) = \underset{x \in b \cup \{c\}}{\sum_{S}} O (M) (Y))$
209	17 24 31 38 89 208 10	findcard2d	$⊢ φ \to O (\underset{x \in N}{\sum_{Q}} M) (Y) = \underset{x \in N}{\sum_{S}} O (M) (Y)$

Metamath Proof Explorer

Theorem evl1gprodd

Proof