mplcoe5lem

	Ref	Expression
Hypotheses	mplcoe1.p	$⊢ P = I mPoly R$
	mplcoe1.d	$⊢ D = \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}$
	mplcoe1.z	$⊢ \underset{˙}{0} = 0_{R}$
	mplcoe1.o	$⊢ \underset{˙}{1} = 1_{R}$
	mplcoe1.i	$⊢ φ \to I \in W$
	mplcoe2.g	$⊢ G = {mulGrp}_{P}$
	mplcoe2.m	$⊢ \underset{˙}{\times} = \cdot_{G}$
	mplcoe2.v	$⊢ V = I mVar R$
	mplcoe5.r	$⊢ φ \to R \in Ring$
	mplcoe5.y	$⊢ φ \to Y \in D$
	mplcoe5.c	$⊢ φ \to \forall x \in I \forall y \in I V (y) +_{G} V (x) = V (x) +_{G} V (y)$
	mplcoe5.s	$⊢ φ \to S \subseteq I$
Assertion	mplcoe5lem	$⊢ φ \to ran (k \in S ⟼ Y (k) \underset{˙}{\times} V (k)) \subseteq Cntz (G) (ran (k \in S ⟼ Y (k) \underset{˙}{\times} V (k)))$

Proof

Step	Hyp	Ref	Expression
1		mplcoe1.p	$⊢ P = I mPoly R$
2		mplcoe1.d	$⊢ D = \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}$
3		mplcoe1.z	$⊢ \underset{˙}{0} = 0_{R}$
4		mplcoe1.o	$⊢ \underset{˙}{1} = 1_{R}$
5		mplcoe1.i	$⊢ φ \to I \in W$
6		mplcoe2.g	$⊢ G = {mulGrp}_{P}$
7		mplcoe2.m	$⊢ \underset{˙}{\times} = \cdot_{G}$
8		mplcoe2.v	$⊢ V = I mVar R$
9		mplcoe5.r	$⊢ φ \to R \in Ring$
10		mplcoe5.y	$⊢ φ \to Y \in D$
11		mplcoe5.c	$⊢ φ \to \forall x \in I \forall y \in I V (y) +_{G} V (x) = V (x) +_{G} V (y)$
12		mplcoe5.s	$⊢ φ \to S \subseteq I$
13		vex	$⊢ x \in V$
14		eqid	$⊢ (k \in S ⟼ Y (k) \underset{˙}{\times} V (k)) = (k \in S ⟼ Y (k) \underset{˙}{\times} V (k))$
15	14	elrnmpt	$⊢ x \in V \to (x \in ran (k \in S ⟼ Y (k) \underset{˙}{\times} V (k)) \leftrightarrow \exists k \in S x = Y (k) \underset{˙}{\times} V (k))$
16	13 15	mp1i	$⊢ φ \to (x \in ran (k \in S ⟼ Y (k) \underset{˙}{\times} V (k)) \leftrightarrow \exists k \in S x = Y (k) \underset{˙}{\times} V (k))$
17		vex	$⊢ y \in V$
18	14	elrnmpt	$⊢ y \in V \to (y \in ran (k \in S ⟼ Y (k) \underset{˙}{\times} V (k)) \leftrightarrow \exists k \in S y = Y (k) \underset{˙}{\times} V (k))$
19	17 18	mp1i	$⊢ φ \to (y \in ran (k \in S ⟼ Y (k) \underset{˙}{\times} V (k)) \leftrightarrow \exists k \in S y = Y (k) \underset{˙}{\times} V (k))$
20		fveq2	$⊢ k = l \to Y (k) = Y (l)$
21		fveq2	$⊢ k = l \to V (k) = V (l)$
22	20 21	oveq12d	$⊢ k = l \to Y (k) \underset{˙}{\times} V (k) = Y (l) \underset{˙}{\times} V (l)$
23	22	eqeq2d	$⊢ k = l \to (y = Y (k) \underset{˙}{\times} V (k) \leftrightarrow y = Y (l) \underset{˙}{\times} V (l))$
24	23	cbvrexvw	$⊢ \exists k \in S y = Y (k) \underset{˙}{\times} V (k) \leftrightarrow \exists l \in S y = Y (l) \underset{˙}{\times} V (l)$
25		eqid	$⊢ {Base}_{P} = {Base}_{P}$
26		eqid	$⊢ \cdot_{P} = \cdot_{P}$
27	6 26	mgpplusg	$⊢ \cdot_{P} = +_{G}$
28	27	eqcomi	$⊢ +_{G} = \cdot_{P}$
29	1	mplring	$⊢ (I \in W \land R \in Ring) \to P \in Ring$
30	5 9 29	syl2anc	$⊢ φ \to P \in Ring$
31		ringsrg	$⊢ P \in Ring \to P \in SRing$
32	30 31	syl	$⊢ φ \to P \in SRing$
33	32	adantr	$⊢ (φ \land l \in S) \to P \in SRing$
34	33	adantr	$⊢ ((φ \land l \in S) \land k \in S) \to P \in SRing$
35	6 25	mgpbas	$⊢ {Base}_{P} = {Base}_{G}$
36	6	ringmgp	$⊢ P \in Ring \to G \in Mnd$
37	30 36	syl	$⊢ φ \to G \in Mnd$
38	37	adantr	$⊢ (φ \land l \in S) \to G \in Mnd$
39	12	sseld	$⊢ φ \to (l \in S \to l \in I)$
40	39	imdistani	$⊢ (φ \land l \in S) \to (φ \land l \in I)$
41	2	psrbag	$⊢ I \in W \to (Y \in D \leftrightarrow (Y : I ⟶ ℕ_{0} \land Y^{-1} [ℕ] \in Fin))$
42	5 41	syl	$⊢ φ \to (Y \in D \leftrightarrow (Y : I ⟶ ℕ_{0} \land Y^{-1} [ℕ] \in Fin))$
43	10 42	mpbid	$⊢ φ \to (Y : I ⟶ ℕ_{0} \land Y^{-1} [ℕ] \in Fin)$
44	43	simpld	$⊢ φ \to Y : I ⟶ ℕ_{0}$
45	44	ffvelcdmda	$⊢ (φ \land l \in I) \to Y (l) \in ℕ_{0}$
46	40 45	syl	$⊢ (φ \land l \in S) \to Y (l) \in ℕ_{0}$
47	5	adantr	$⊢ (φ \land l \in S) \to I \in W$
48	9	adantr	$⊢ (φ \land l \in S) \to R \in Ring$
49	12	sselda	$⊢ (φ \land l \in S) \to l \in I$
50	1 8 25 47 48 49	mvrcl	$⊢ (φ \land l \in S) \to V (l) \in {Base}_{P}$
51	35 7 38 46 50	mulgnn0cld	$⊢ (φ \land l \in S) \to Y (l) \underset{˙}{\times} V (l) \in {Base}_{P}$
52	51	adantr	$⊢ ((φ \land l \in S) \land k \in S) \to Y (l) \underset{˙}{\times} V (l) \in {Base}_{P}$
53	5	adantr	$⊢ (φ \land k \in S) \to I \in W$
54	9	adantr	$⊢ (φ \land k \in S) \to R \in Ring$
55	12	sselda	$⊢ (φ \land k \in S) \to k \in I$
56	1 8 25 53 54 55	mvrcl	$⊢ (φ \land k \in S) \to V (k) \in {Base}_{P}$
57	56	adantlr	$⊢ ((φ \land l \in S) \land k \in S) \to V (k) \in {Base}_{P}$
58	44	ffvelcdmda	$⊢ (φ \land k \in I) \to Y (k) \in ℕ_{0}$
59	55 58	syldan	$⊢ (φ \land k \in S) \to Y (k) \in ℕ_{0}$
60	59	adantlr	$⊢ ((φ \land l \in S) \land k \in S) \to Y (k) \in ℕ_{0}$
61	50	adantr	$⊢ ((φ \land l \in S) \land k \in S) \to V (l) \in {Base}_{P}$
62	46	adantr	$⊢ ((φ \land l \in S) \land k \in S) \to Y (l) \in ℕ_{0}$
63		fveq2	$⊢ x = l \to V (x) = V (l)$
64	63	oveq2d	$⊢ x = l \to V (y) +_{G} V (x) = V (y) +_{G} V (l)$
65	63	oveq1d	$⊢ x = l \to V (x) +_{G} V (y) = V (l) +_{G} V (y)$
66	64 65	eqeq12d	$⊢ x = l \to (V (y) +_{G} V (x) = V (x) +_{G} V (y) \leftrightarrow V (y) +_{G} V (l) = V (l) +_{G} V (y))$
67		fveq2	$⊢ y = k \to V (y) = V (k)$
68	67	oveq1d	$⊢ y = k \to V (y) +_{G} V (l) = V (k) +_{G} V (l)$
69	67	oveq2d	$⊢ y = k \to V (l) +_{G} V (y) = V (l) +_{G} V (k)$
70	68 69	eqeq12d	$⊢ y = k \to (V (y) +_{G} V (l) = V (l) +_{G} V (y) \leftrightarrow V (k) +_{G} V (l) = V (l) +_{G} V (k))$
71	66 70	rspc2v	$⊢ (l \in I \land k \in I) \to (\forall x \in I \forall y \in I V (y) +_{G} V (x) = V (x) +_{G} V (y) \to V (k) +_{G} V (l) = V (l) +_{G} V (k))$
72	49 55	anim12dan	$⊢ (φ \land (l \in S \land k \in S)) \to (l \in I \land k \in I)$
73	71 72	syl11	$⊢ \forall x \in I \forall y \in I V (y) +_{G} V (x) = V (x) +_{G} V (y) \to ((φ \land (l \in S \land k \in S)) \to V (k) +_{G} V (l) = V (l) +_{G} V (k))$
74	73	expd	$⊢ \forall x \in I \forall y \in I V (y) +_{G} V (x) = V (x) +_{G} V (y) \to (φ \to ((l \in S \land k \in S) \to V (k) +_{G} V (l) = V (l) +_{G} V (k)))$
75	11 74	mpcom	$⊢ φ \to ((l \in S \land k \in S) \to V (k) +_{G} V (l) = V (l) +_{G} V (k))$
76	75	impl	$⊢ ((φ \land l \in S) \land k \in S) \to V (k) +_{G} V (l) = V (l) +_{G} V (k)$
77	25 28 6 7 34 57 61 62 76	srgpcomp	$⊢ ((φ \land l \in S) \land k \in S) \to (Y (l) \underset{˙}{\times} V (l)) +_{G} V (k) = V (k) +_{G} (Y (l) \underset{˙}{\times} V (l))$
78	25 28 6 7 34 52 57 60 77	srgpcomp	$⊢ ((φ \land l \in S) \land k \in S) \to (Y (k) \underset{˙}{\times} V (k)) +_{G} (Y (l) \underset{˙}{\times} V (l)) = (Y (l) \underset{˙}{\times} V (l)) +_{G} (Y (k) \underset{˙}{\times} V (k))$
79		oveq12	$⊢ (x = Y (k) \underset{˙}{\times} V (k) \land y = Y (l) \underset{˙}{\times} V (l)) \to x +_{G} y = (Y (k) \underset{˙}{\times} V (k)) +_{G} (Y (l) \underset{˙}{\times} V (l))$
80		oveq12	$⊢ (y = Y (l) \underset{˙}{\times} V (l) \land x = Y (k) \underset{˙}{\times} V (k)) \to y +_{G} x = (Y (l) \underset{˙}{\times} V (l)) +_{G} (Y (k) \underset{˙}{\times} V (k))$
81	80	ancoms	$⊢ (x = Y (k) \underset{˙}{\times} V (k) \land y = Y (l) \underset{˙}{\times} V (l)) \to y +_{G} x = (Y (l) \underset{˙}{\times} V (l)) +_{G} (Y (k) \underset{˙}{\times} V (k))$
82	79 81	eqeq12d	$⊢ (x = Y (k) \underset{˙}{\times} V (k) \land y = Y (l) \underset{˙}{\times} V (l)) \to (x +_{G} y = y +_{G} x \leftrightarrow (Y (k) \underset{˙}{\times} V (k)) +_{G} (Y (l) \underset{˙}{\times} V (l)) = (Y (l) \underset{˙}{\times} V (l)) +_{G} (Y (k) \underset{˙}{\times} V (k)))$
83	78 82	syl5ibrcom	$⊢ ((φ \land l \in S) \land k \in S) \to ((x = Y (k) \underset{˙}{\times} V (k) \land y = Y (l) \underset{˙}{\times} V (l)) \to x +_{G} y = y +_{G} x)$
84	83	expd	$⊢ ((φ \land l \in S) \land k \in S) \to (x = Y (k) \underset{˙}{\times} V (k) \to (y = Y (l) \underset{˙}{\times} V (l) \to x +_{G} y = y +_{G} x))$
85	84	rexlimdva	$⊢ (φ \land l \in S) \to (\exists k \in S x = Y (k) \underset{˙}{\times} V (k) \to (y = Y (l) \underset{˙}{\times} V (l) \to x +_{G} y = y +_{G} x))$
86	85	com23	$⊢ (φ \land l \in S) \to (y = Y (l) \underset{˙}{\times} V (l) \to (\exists k \in S x = Y (k) \underset{˙}{\times} V (k) \to x +_{G} y = y +_{G} x))$
87	86	rexlimdva	$⊢ φ \to (\exists l \in S y = Y (l) \underset{˙}{\times} V (l) \to (\exists k \in S x = Y (k) \underset{˙}{\times} V (k) \to x +_{G} y = y +_{G} x))$
88	24 87	biimtrid	$⊢ φ \to (\exists k \in S y = Y (k) \underset{˙}{\times} V (k) \to (\exists k \in S x = Y (k) \underset{˙}{\times} V (k) \to x +_{G} y = y +_{G} x))$
89	19 88	sylbid	$⊢ φ \to (y \in ran (k \in S ⟼ Y (k) \underset{˙}{\times} V (k)) \to (\exists k \in S x = Y (k) \underset{˙}{\times} V (k) \to x +_{G} y = y +_{G} x))$
90	89	com23	$⊢ φ \to (\exists k \in S x = Y (k) \underset{˙}{\times} V (k) \to (y \in ran (k \in S ⟼ Y (k) \underset{˙}{\times} V (k)) \to x +_{G} y = y +_{G} x))$
91	16 90	sylbid	$⊢ φ \to (x \in ran (k \in S ⟼ Y (k) \underset{˙}{\times} V (k)) \to (y \in ran (k \in S ⟼ Y (k) \underset{˙}{\times} V (k)) \to x +_{G} y = y +_{G} x))$
92	91	imp32	$⊢ (φ \land (x \in ran (k \in S ⟼ Y (k) \underset{˙}{\times} V (k)) \land y \in ran (k \in S ⟼ Y (k) \underset{˙}{\times} V (k)))) \to x +_{G} y = y +_{G} x$
93	92	ralrimivva	$⊢ φ \to \forall x \in ran (k \in S ⟼ Y (k) \underset{˙}{\times} V (k)) \forall y \in ran (k \in S ⟼ Y (k) \underset{˙}{\times} V (k)) x +_{G} y = y +_{G} x$
94		eqid	$⊢ {Base}_{G} = {Base}_{G}$
95	37	adantr	$⊢ (φ \land k \in S) \to G \in Mnd$
96	12	sseld	$⊢ φ \to (k \in S \to k \in I)$
97	96	imdistani	$⊢ (φ \land k \in S) \to (φ \land k \in I)$
98	97 58	syl	$⊢ (φ \land k \in S) \to Y (k) \in ℕ_{0}$
99	56 35	eleqtrdi	$⊢ (φ \land k \in S) \to V (k) \in {Base}_{G}$
100	94 7 95 98 99	mulgnn0cld	$⊢ (φ \land k \in S) \to Y (k) \underset{˙}{\times} V (k) \in {Base}_{G}$
101	100	fmpttd	$⊢ φ \to (k \in S ⟼ Y (k) \underset{˙}{\times} V (k)) : S ⟶ {Base}_{G}$
102	101	frnd	$⊢ φ \to ran (k \in S ⟼ Y (k) \underset{˙}{\times} V (k)) \subseteq {Base}_{G}$
103		eqid	$⊢ +_{G} = +_{G}$
104		eqid	$⊢ Cntz (G) = Cntz (G)$
105	94 103 104	sscntz	$⊢ (ran (k \in S ⟼ Y (k) \underset{˙}{\times} V (k)) \subseteq {Base}_{G} \land ran (k \in S ⟼ Y (k) \underset{˙}{\times} V (k)) \subseteq {Base}_{G}) \to (ran (k \in S ⟼ Y (k) \underset{˙}{\times} V (k)) \subseteq Cntz (G) (ran (k \in S ⟼ Y (k) \underset{˙}{\times} V (k))) \leftrightarrow \forall x \in ran (k \in S ⟼ Y (k) \underset{˙}{\times} V (k)) \forall y \in ran (k \in S ⟼ Y (k) \underset{˙}{\times} V (k)) x +_{G} y = y +_{G} x)$
106	102 102 105	syl2anc	$⊢ φ \to (ran (k \in S ⟼ Y (k) \underset{˙}{\times} V (k)) \subseteq Cntz (G) (ran (k \in S ⟼ Y (k) \underset{˙}{\times} V (k))) \leftrightarrow \forall x \in ran (k \in S ⟼ Y (k) \underset{˙}{\times} V (k)) \forall y \in ran (k \in S ⟼ Y (k) \underset{˙}{\times} V (k)) x +_{G} y = y +_{G} x)$
107	93 106	mpbird	$⊢ φ \to ran (k \in S ⟼ Y (k) \underset{˙}{\times} V (k)) \subseteq Cntz (G) (ran (k \in S ⟼ Y (k) \underset{˙}{\times} V (k)))$

Metamath Proof Explorer

Theorem mplcoe5lem

Proof