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	ringmgp	$⊢ P \in Ring \to G \in Mnd$
36	30 35	syl	$⊢ φ \to G \in Mnd$
37	36	adantr	$⊢ (φ \land l \in S) \to G \in Mnd$
38	12	sseld	$⊢ φ \to (l \in S \to l \in I)$
39	38	imdistani	$⊢ (φ \land l \in S) \to (φ \land l \in I)$
40	2	psrbag	$⊢ I \in W \to (Y \in D \leftrightarrow (Y : I ⟶ ℕ_{0} \land Y^{-1} [ℕ] \in Fin))$
41	5 40	syl	$⊢ φ \to (Y \in D \leftrightarrow (Y : I ⟶ ℕ_{0} \land Y^{-1} [ℕ] \in Fin))$
42	10 41	mpbid	$⊢ φ \to (Y : I ⟶ ℕ_{0} \land Y^{-1} [ℕ] \in Fin)$
43	42	simpld	$⊢ φ \to Y : I ⟶ ℕ_{0}$
44	43	ffvelrnda	$⊢ (φ \land l \in I) \to Y (l) \in ℕ_{0}$
45	39 44	syl	$⊢ (φ \land l \in S) \to Y (l) \in ℕ_{0}$
46	5	adantr	$⊢ (φ \land l \in S) \to I \in W$
47	9	adantr	$⊢ (φ \land l \in S) \to R \in Ring$
48	12	sselda	$⊢ (φ \land l \in S) \to l \in I$
49	1 8 25 46 47 48	mvrcl	$⊢ (φ \land l \in S) \to V (l) \in {Base}_{P}$
50	6 25	mgpbas	$⊢ {Base}_{P} = {Base}_{G}$
51	50 7	mulgnn0cl	$⊢ (G \in Mnd \land Y (l) \in ℕ_{0} \land V (l) \in {Base}_{P}) \to Y (l) \underset{˙}{\times} V (l) \in {Base}_{P}$
52	37 45 49 51	syl3anc	$⊢ (φ \land l \in S) \to Y (l) \underset{˙}{\times} V (l) \in {Base}_{P}$
53	52	adantr	$⊢ ((φ \land l \in S) \land k \in S) \to Y (l) \underset{˙}{\times} V (l) \in {Base}_{P}$
54	5	adantr	$⊢ (φ \land k \in S) \to I \in W$
55	9	adantr	$⊢ (φ \land k \in S) \to R \in Ring$
56	12	sselda	$⊢ (φ \land k \in S) \to k \in I$
57	1 8 25 54 55 56	mvrcl	$⊢ (φ \land k \in S) \to V (k) \in {Base}_{P}$
58	57	adantlr	$⊢ ((φ \land l \in S) \land k \in S) \to V (k) \in {Base}_{P}$
59	43	ffvelrnda	$⊢ (φ \land k \in I) \to Y (k) \in ℕ_{0}$
60	56 59	syldan	$⊢ (φ \land k \in S) \to Y (k) \in ℕ_{0}$
61	60	adantlr	$⊢ ((φ \land l \in S) \land k \in S) \to Y (k) \in ℕ_{0}$
62	49	adantr	$⊢ ((φ \land l \in S) \land k \in S) \to V (l) \in {Base}_{P}$
63	45	adantr	$⊢ ((φ \land l \in S) \land k \in S) \to Y (l) \in ℕ_{0}$
64		fveq2	$⊢ x = l \to V (x) = V (l)$
65	64	oveq2d	$⊢ x = l \to V (y) +_{G} V (x) = V (y) +_{G} V (l)$
66	64	oveq1d	$⊢ x = l \to V (x) +_{G} V (y) = V (l) +_{G} V (y)$
67	65 66	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))$
68		fveq2	$⊢ y = k \to V (y) = V (k)$
69	68	oveq1d	$⊢ y = k \to V (y) +_{G} V (l) = V (k) +_{G} V (l)$
70	68	oveq2d	$⊢ y = k \to V (l) +_{G} V (y) = V (l) +_{G} V (k)$
71	69 70	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))$
72	67 71	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))$
73	48 56	anim12dan	$⊢ (φ \land (l \in S \land k \in S)) \to (l \in I \land k \in I)$
74	72 73	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))$
75	74	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)))$
76	11 75	mpcom	$⊢ φ \to ((l \in S \land k \in S) \to V (k) +_{G} V (l) = V (l) +_{G} V (k))$
77	76	impl	$⊢ ((φ \land l \in S) \land k \in S) \to V (k) +_{G} V (l) = V (l) +_{G} V (k)$
78	25 28 6 7 34 58 62 63 77	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))$
79	25 28 6 7 34 53 58 61 78	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))$
80		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))$
81		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))$
82	81	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))$
83	80 82	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)))$
84	79 83	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)$
85	84	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))$
86	85	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))$
87	86	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))$
88	87	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))$
89	24 88	syl5bi	$⊢ φ \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))$
90	19 89	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))$
91	90	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))$
92	16 91	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))$
93	92	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$
94	93	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$
95	36	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 59	syl	$⊢ (φ \land k \in S) \to Y (k) \in ℕ_{0}$
99	57 50	eleqtrdi	$⊢ (φ \land k \in S) \to V (k) \in {Base}_{G}$
100		eqid	$⊢ {Base}_{G} = {Base}_{G}$
101	100 7	mulgnn0cl	$⊢ (G \in Mnd \land Y (k) \in ℕ_{0} \land V (k) \in {Base}_{G}) \to Y (k) \underset{˙}{\times} V (k) \in {Base}_{G}$
102	95 98 99 101	syl3anc	$⊢ (φ \land k \in S) \to Y (k) \underset{˙}{\times} V (k) \in {Base}_{G}$
103	102	fmpttd	$⊢ φ \to (k \in S ⟼ Y (k) \underset{˙}{\times} V (k)) : S ⟶ {Base}_{G}$
104	103	frnd	$⊢ φ \to ran (k \in S ⟼ Y (k) \underset{˙}{\times} V (k)) \subseteq {Base}_{G}$
105		eqid	$⊢ +_{G} = +_{G}$
106		eqid	$⊢ Cntz (G) = Cntz (G)$
107	100 105 106	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)$
108	104 104 107	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)$
109	94 108	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