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 5 9	mplringd	$⊢ φ \to P \in Ring$
30		ringsrg	$⊢ P \in Ring \to P \in SRing$
31	29 30	syl	$⊢ φ \to P \in SRing$
32	31	adantr	$⊢ (φ \land l \in S) \to P \in SRing$
33	32	adantr	$⊢ ((φ \land l \in S) \land k \in S) \to P \in SRing$
34	6 25	mgpbas	$⊢ {Base}_{P} = {Base}_{G}$
35	6	ringmgp	$⊢ P \in Ring \to G \in Mnd$
36	29 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	ffvelcdmda	$⊢ (φ \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	34 7 37 45 49	mulgnn0cld	$⊢ (φ \land l \in S) \to Y (l) \underset{˙}{\times} V (l) \in {Base}_{P}$
51	50	adantr	$⊢ ((φ \land l \in S) \land k \in S) \to Y (l) \underset{˙}{\times} V (l) \in {Base}_{P}$
52	5	adantr	$⊢ (φ \land k \in S) \to I \in W$
53	9	adantr	$⊢ (φ \land k \in S) \to R \in Ring$
54	12	sselda	$⊢ (φ \land k \in S) \to k \in I$
55	1 8 25 52 53 54	mvrcl	$⊢ (φ \land k \in S) \to V (k) \in {Base}_{P}$
56	55	adantlr	$⊢ ((φ \land l \in S) \land k \in S) \to V (k) \in {Base}_{P}$
57	43	ffvelcdmda	$⊢ (φ \land k \in I) \to Y (k) \in ℕ_{0}$
58	54 57	syldan	$⊢ (φ \land k \in S) \to Y (k) \in ℕ_{0}$
59	58	adantlr	$⊢ ((φ \land l \in S) \land k \in S) \to Y (k) \in ℕ_{0}$
60	49	adantr	$⊢ ((φ \land l \in S) \land k \in S) \to V (l) \in {Base}_{P}$
61	45	adantr	$⊢ ((φ \land l \in S) \land k \in S) \to Y (l) \in ℕ_{0}$
62		fveq2	$⊢ x = l \to V (x) = V (l)$
63	62	oveq2d	$⊢ x = l \to V (y) +_{G} V (x) = V (y) +_{G} V (l)$
64	62	oveq1d	$⊢ x = l \to V (x) +_{G} V (y) = V (l) +_{G} V (y)$
65	63 64	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))$
66		fveq2	$⊢ y = k \to V (y) = V (k)$
67	66	oveq1d	$⊢ y = k \to V (y) +_{G} V (l) = V (k) +_{G} V (l)$
68	66	oveq2d	$⊢ y = k \to V (l) +_{G} V (y) = V (l) +_{G} V (k)$
69	67 68	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))$
70	65 69	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))$
71	48 54	anim12dan	$⊢ (φ \land (l \in S \land k \in S)) \to (l \in I \land k \in I)$
72	70 71	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))$
73	72	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)))$
74	11 73	mpcom	$⊢ φ \to ((l \in S \land k \in S) \to V (k) +_{G} V (l) = V (l) +_{G} V (k))$
75	74	impl	$⊢ ((φ \land l \in S) \land k \in S) \to V (k) +_{G} V (l) = V (l) +_{G} V (k)$
76	25 28 6 7 33 56 60 61 75	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))$
77	25 28 6 7 33 51 56 59 76	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))$
78		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))$
79		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))$
80	79	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))$
81	78 80	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)))$
82	77 81	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)$
83	82	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))$
84	83	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))$
85	84	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))$
86	85	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))$
87	24 86	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))$
88	19 87	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))$
89	88	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))$
90	16 89	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))$
91	90	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$
92	91	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$
93		eqid	$⊢ {Base}_{G} = {Base}_{G}$
94	36	adantr	$⊢ (φ \land k \in S) \to G \in Mnd$
95	12	sseld	$⊢ φ \to (k \in S \to k \in I)$
96	95	imdistani	$⊢ (φ \land k \in S) \to (φ \land k \in I)$
97	96 57	syl	$⊢ (φ \land k \in S) \to Y (k) \in ℕ_{0}$
98	55 34	eleqtrdi	$⊢ (φ \land k \in S) \to V (k) \in {Base}_{G}$
99	93 7 94 97 98	mulgnn0cld	$⊢ (φ \land k \in S) \to Y (k) \underset{˙}{\times} V (k) \in {Base}_{G}$
100	99	fmpttd	$⊢ φ \to (k \in S ⟼ Y (k) \underset{˙}{\times} V (k)) : S ⟶ {Base}_{G}$
101	100	frnd	$⊢ φ \to ran (k \in S ⟼ Y (k) \underset{˙}{\times} V (k)) \subseteq {Base}_{G}$
102		eqid	$⊢ +_{G} = +_{G}$
103		eqid	$⊢ Cntz (G) = Cntz (G)$
104	93 102 103	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)$
105	101 101 104	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)$
106	92 105	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