Theorem mplcoe3

Description: Decompose a monomial in one variable into a power of a variable. (Contributed by Mario Carneiro, 7-Jan-2015) (Proof shortened by AV, 18-Jul-2019)

	Ref	Expression
Hypotheses	mplcoe1.p	$$⊢P=I\mathrm{mPoly}R$$
	mplcoe1.d	$$⊢D=\left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
	mplcoe1.z	$$⊢\underset{\dot{}}{0}=0_R$$
	mplcoe1.o	$$⊢\underset{\dot{}}{1}=1_R$$
	mplcoe1.i	$$⊢\phi \to I\in W$$
	mplcoe2.g	$$⊢G={\mathrm{mulGrp}}_P$$
	mplcoe2.m	$$⊢\underset{\dot{}}{\times }={\cdot }_G$$
	mplcoe2.v	$$⊢V=I\mathrm{mVar}R$$
	mplcoe3.r	$$⊢\phi \to R\in \mathrm{Ring}$$
	mplcoe3.x	$$⊢\phi \to X\in I$$
	mplcoe3.n	$$⊢\phi \to N\in {\mathbb{N}}_0$$
Assertion	mplcoe3	$$⊢\phi \to \left(y\in D⟼if\left(y=\left(k\in I⟼if\left(k=X,N,0\right)\right),\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)=N\underset{\dot{}}{\times }V\left(X\right)$$

Proof

Step	Hyp	Ref	Expression
1		mplcoe1.p	$$⊢P=I\mathrm{mPoly}R$$
2		mplcoe1.d	$$⊢D=\left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
3		mplcoe1.z	$$⊢\underset{\dot{}}{0}=0_R$$
4		mplcoe1.o	$$⊢\underset{\dot{}}{1}=1_R$$
5		mplcoe1.i	$$⊢\phi \to I\in W$$
6		mplcoe2.g	$$⊢G={\mathrm{mulGrp}}_P$$
7		mplcoe2.m	$$⊢\underset{\dot{}}{\times }={\cdot }_G$$
8		mplcoe2.v	$$⊢V=I\mathrm{mVar}R$$
9		mplcoe3.r	$$⊢\phi \to R\in \mathrm{Ring}$$
10		mplcoe3.x	$$⊢\phi \to X\in I$$
11		mplcoe3.n	$$⊢\phi \to N\in {\mathbb{N}}_0$$
12		ifeq1	$$⊢x=0\to if\left(k=X,x,0\right)=if\left(k=X,0,0\right)$$
13		ifid	$$⊢if\left(k=X,0,0\right)=0$$
14	12 13	eqtrdi	$$⊢x=0\to if\left(k=X,x,0\right)=0$$
15	14	mpteq2dv	$$⊢x=0\to \left(k\in I⟼if\left(k=X,x,0\right)\right)=\left(k\in I⟼0\right)$$
16		fconstmpt	$$⊢I\times \left\{0\right\}=\left(k\in I⟼0\right)$$
17	15 16	eqtr4di	$$⊢x=0\to \left(k\in I⟼if\left(k=X,x,0\right)\right)=I\times \left\{0\right\}$$
18	17	eqeq2d	$$⊢x=0\to \left(y=\left(k\in I⟼if\left(k=X,x,0\right)\right)\leftrightarrow y=I\times \left\{0\right\}\right)$$
19	18	ifbid	$$⊢x=0\to if\left(y=\left(k\in I⟼if\left(k=X,x,0\right)\right),\underset{\dot{}}{1},\underset{\dot{}}{0}\right)=if\left(y=I\times \left\{0\right\},\underset{\dot{}}{1},\underset{\dot{}}{0}\right)$$
20	19	mpteq2dv	$$⊢x=0\to \left(y\in D⟼if\left(y=\left(k\in I⟼if\left(k=X,x,0\right)\right),\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)=\left(y\in D⟼if\left(y=I\times \left\{0\right\},\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)$$
21		oveq1	$$⊢x=0\to x\underset{\dot{}}{\times }V\left(X\right)=0\underset{\dot{}}{\times }V\left(X\right)$$
22	20 21	eqeq12d	$$⊢x=0\to \left(\left(y\in D⟼if\left(y=\left(k\in I⟼if\left(k=X,x,0\right)\right),\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)=x\underset{\dot{}}{\times }V\left(X\right)\leftrightarrow \left(y\in D⟼if\left(y=I\times \left\{0\right\},\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)=0\underset{\dot{}}{\times }V\left(X\right)\right)$$
23	22	imbi2d	$$⊢x=0\to \left(\left(\phi \to \left(y\in D⟼if\left(y=\left(k\in I⟼if\left(k=X,x,0\right)\right),\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)=x\underset{\dot{}}{\times }V\left(X\right)\right)\leftrightarrow \left(\phi \to \left(y\in D⟼if\left(y=I\times \left\{0\right\},\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)=0\underset{\dot{}}{\times }V\left(X\right)\right)\right)$$
24		ifeq1	$$⊢x=n\to if\left(k=X,x,0\right)=if\left(k=X,n,0\right)$$
25	24	mpteq2dv	$$⊢x=n\to \left(k\in I⟼if\left(k=X,x,0\right)\right)=\left(k\in I⟼if\left(k=X,n,0\right)\right)$$
26	25	eqeq2d	$$⊢x=n\to \left(y=\left(k\in I⟼if\left(k=X,x,0\right)\right)\leftrightarrow y=\left(k\in I⟼if\left(k=X,n,0\right)\right)\right)$$
27	26	ifbid	$$⊢x=n\to if\left(y=\left(k\in I⟼if\left(k=X,x,0\right)\right),\underset{\dot{}}{1},\underset{\dot{}}{0}\right)=if\left(y=\left(k\in I⟼if\left(k=X,n,0\right)\right),\underset{\dot{}}{1},\underset{\dot{}}{0}\right)$$
28	27	mpteq2dv	$$⊢x=n\to \left(y\in D⟼if\left(y=\left(k\in I⟼if\left(k=X,x,0\right)\right),\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)=\left(y\in D⟼if\left(y=\left(k\in I⟼if\left(k=X,n,0\right)\right),\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)$$
29		oveq1	$$⊢x=n\to x\underset{\dot{}}{\times }V\left(X\right)=n\underset{\dot{}}{\times }V\left(X\right)$$
30	28 29	eqeq12d	$$⊢x=n\to \left(\left(y\in D⟼if\left(y=\left(k\in I⟼if\left(k=X,x,0\right)\right),\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)=x\underset{\dot{}}{\times }V\left(X\right)\leftrightarrow \left(y\in D⟼if\left(y=\left(k\in I⟼if\left(k=X,n,0\right)\right),\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)=n\underset{\dot{}}{\times }V\left(X\right)\right)$$
31	30	imbi2d	$$⊢x=n\to \left(\left(\phi \to \left(y\in D⟼if\left(y=\left(k\in I⟼if\left(k=X,x,0\right)\right),\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)=x\underset{\dot{}}{\times }V\left(X\right)\right)\leftrightarrow \left(\phi \to \left(y\in D⟼if\left(y=\left(k\in I⟼if\left(k=X,n,0\right)\right),\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)=n\underset{\dot{}}{\times }V\left(X\right)\right)\right)$$
32		ifeq1	$$⊢x=n+1\to if\left(k=X,x,0\right)=if\left(k=X,n+1,0\right)$$
33	32	mpteq2dv	$$⊢x=n+1\to \left(k\in I⟼if\left(k=X,x,0\right)\right)=\left(k\in I⟼if\left(k=X,n+1,0\right)\right)$$
34	33	eqeq2d	$$⊢x=n+1\to \left(y=\left(k\in I⟼if\left(k=X,x,0\right)\right)\leftrightarrow y=\left(k\in I⟼if\left(k=X,n+1,0\right)\right)\right)$$
35	34	ifbid	$$⊢x=n+1\to if\left(y=\left(k\in I⟼if\left(k=X,x,0\right)\right),\underset{\dot{}}{1},\underset{\dot{}}{0}\right)=if\left(y=\left(k\in I⟼if\left(k=X,n+1,0\right)\right),\underset{\dot{}}{1},\underset{\dot{}}{0}\right)$$
36	35	mpteq2dv	$$⊢x=n+1\to \left(y\in D⟼if\left(y=\left(k\in I⟼if\left(k=X,x,0\right)\right),\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)=\left(y\in D⟼if\left(y=\left(k\in I⟼if\left(k=X,n+1,0\right)\right),\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)$$
37		oveq1	$$⊢x=n+1\to x\underset{\dot{}}{\times }V\left(X\right)=\left(n+1\right)\underset{\dot{}}{\times }V\left(X\right)$$
38	36 37	eqeq12d	$$⊢x=n+1\to \left(\left(y\in D⟼if\left(y=\left(k\in I⟼if\left(k=X,x,0\right)\right),\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)=x\underset{\dot{}}{\times }V\left(X\right)\leftrightarrow \left(y\in D⟼if\left(y=\left(k\in I⟼if\left(k=X,n+1,0\right)\right),\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)=\left(n+1\right)\underset{\dot{}}{\times }V\left(X\right)\right)$$
39	38	imbi2d	$$⊢x=n+1\to \left(\left(\phi \to \left(y\in D⟼if\left(y=\left(k\in I⟼if\left(k=X,x,0\right)\right),\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)=x\underset{\dot{}}{\times }V\left(X\right)\right)\leftrightarrow \left(\phi \to \left(y\in D⟼if\left(y=\left(k\in I⟼if\left(k=X,n+1,0\right)\right),\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)=\left(n+1\right)\underset{\dot{}}{\times }V\left(X\right)\right)\right)$$
40		ifeq1	$$⊢x=N\to if\left(k=X,x,0\right)=if\left(k=X,N,0\right)$$
41	40	mpteq2dv	$$⊢x=N\to \left(k\in I⟼if\left(k=X,x,0\right)\right)=\left(k\in I⟼if\left(k=X,N,0\right)\right)$$
42	41	eqeq2d	$$⊢x=N\to \left(y=\left(k\in I⟼if\left(k=X,x,0\right)\right)\leftrightarrow y=\left(k\in I⟼if\left(k=X,N,0\right)\right)\right)$$
43	42	ifbid	$$⊢x=N\to if\left(y=\left(k\in I⟼if\left(k=X,x,0\right)\right),\underset{\dot{}}{1},\underset{\dot{}}{0}\right)=if\left(y=\left(k\in I⟼if\left(k=X,N,0\right)\right),\underset{\dot{}}{1},\underset{\dot{}}{0}\right)$$
44	43	mpteq2dv	$$⊢x=N\to \left(y\in D⟼if\left(y=\left(k\in I⟼if\left(k=X,x,0\right)\right),\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)=\left(y\in D⟼if\left(y=\left(k\in I⟼if\left(k=X,N,0\right)\right),\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)$$
45		oveq1	$$⊢x=N\to x\underset{\dot{}}{\times }V\left(X\right)=N\underset{\dot{}}{\times }V\left(X\right)$$
46	44 45	eqeq12d	$$⊢x=N\to \left(\left(y\in D⟼if\left(y=\left(k\in I⟼if\left(k=X,x,0\right)\right),\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)=x\underset{\dot{}}{\times }V\left(X\right)\leftrightarrow \left(y\in D⟼if\left(y=\left(k\in I⟼if\left(k=X,N,0\right)\right),\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)=N\underset{\dot{}}{\times }V\left(X\right)\right)$$
47	46	imbi2d	$$⊢x=N\to \left(\left(\phi \to \left(y\in D⟼if\left(y=\left(k\in I⟼if\left(k=X,x,0\right)\right),\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)=x\underset{\dot{}}{\times }V\left(X\right)\right)\leftrightarrow \left(\phi \to \left(y\in D⟼if\left(y=\left(k\in I⟼if\left(k=X,N,0\right)\right),\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)=N\underset{\dot{}}{\times }V\left(X\right)\right)\right)$$
48		eqid	$$⊢{\mathrm{Base}}_P={\mathrm{Base}}_P$$
49	1 8 48 5 9 10	mvrcl	$$⊢\phi \to V\left(X\right)\in {\mathrm{Base}}_P$$
50	6 48	mgpbas	$$⊢{\mathrm{Base}}_P={\mathrm{Base}}_G$$
51		eqid	$$⊢1_P=1_P$$
52	6 51	ringidval	$$⊢1_P=0_G$$
53	50 52 7	mulg0	$$⊢V\left(X\right)\in {\mathrm{Base}}_P\to 0\underset{\dot{}}{\times }V\left(X\right)=1_P$$
54	49 53	syl	$$⊢\phi \to 0\underset{\dot{}}{\times }V\left(X\right)=1_P$$
55	1 2 3 4 51 5 9	mpl1	$$⊢\phi \to 1_P=\left(y\in D⟼if\left(y=I\times \left\{0\right\},\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)$$
56	54 55	eqtr2d	$$⊢\phi \to \left(y\in D⟼if\left(y=I\times \left\{0\right\},\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)=0\underset{\dot{}}{\times }V\left(X\right)$$
57		oveq1	$$⊢\left(y\in D⟼if\left(y=\left(k\in I⟼if\left(k=X,n,0\right)\right),\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)=n\underset{\dot{}}{\times }V\left(X\right)\to \left(y\in D⟼if\left(y=\left(k\in I⟼if\left(k=X,n,0\right)\right),\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right){\cdot }_{P}V\left(X\right)=\left(n\underset{\dot{}}{\times }V\left(X\right)\right){\cdot }_{P}V\left(X\right)$$
58	5	adantr	$$⊢\left(\phi \wedge n\in {\mathbb{N}}_0\right)\to I\in W$$
59	9	adantr	$$⊢\left(\phi \wedge n\in {\mathbb{N}}_0\right)\to R\in \mathrm{Ring}$$
60	2	snifpsrbag	$$⊢\left(I\in W\wedge n\in {\mathbb{N}}_0\right)\to \left(k\in I⟼if\left(k=X,n,0\right)\right)\in D$$
61	5 60	sylan	$$⊢\left(\phi \wedge n\in {\mathbb{N}}_0\right)\to \left(k\in I⟼if\left(k=X,n,0\right)\right)\in D$$
62		eqid	$$⊢{\cdot }_P={\cdot }_P$$
63		1nn0	$$⊢1\in {\mathbb{N}}_0$$
64	63	a1i	$$⊢n\in {\mathbb{N}}_0\to 1\in {\mathbb{N}}_0$$
65	2	snifpsrbag	$$⊢\left(I\in W\wedge 1\in {\mathbb{N}}_0\right)\to \left(k\in I⟼if\left(k=X,1,0\right)\right)\in D$$
66	5 64 65	syl2an	$$⊢\left(\phi \wedge n\in {\mathbb{N}}_0\right)\to \left(k\in I⟼if\left(k=X,1,0\right)\right)\in D$$
67	1 48 3 4 2 58 59 61 62 66	mplmonmul	$$⊢\left(\phi \wedge n\in {\mathbb{N}}_0\right)\to \left(y\in D⟼if\left(y=\left(k\in I⟼if\left(k=X,n,0\right)\right),\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right){\cdot }_P\left(y\in D⟼if\left(y=\left(k\in I⟼if\left(k=X,1,0\right)\right),\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)=\left(y\in D⟼if\left(y=\left(k\in I⟼if\left(k=X,n,0\right)\right){+}_f\left(k\in I⟼if\left(k=X,1,0\right)\right),\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)$$
68	10	adantr	$$⊢\left(\phi \wedge n\in {\mathbb{N}}_0\right)\to X\in I$$
69	8 2 3 4 58 59 68	mvrval	$$⊢\left(\phi \wedge n\in {\mathbb{N}}_0\right)\to V\left(X\right)=\left(y\in D⟼if\left(y=\left(k\in I⟼if\left(k=X,1,0\right)\right),\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)$$
70	69	eqcomd	$$⊢\left(\phi \wedge n\in {\mathbb{N}}_0\right)\to \left(y\in D⟼if\left(y=\left(k\in I⟼if\left(k=X,1,0\right)\right),\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)=V\left(X\right)$$
71	70	oveq2d	$$⊢\left(\phi \wedge n\in {\mathbb{N}}_0\right)\to \left(y\in D⟼if\left(y=\left(k\in I⟼if\left(k=X,n,0\right)\right),\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right){\cdot }_P\left(y\in D⟼if\left(y=\left(k\in I⟼if\left(k=X,1,0\right)\right),\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)=\left(y\in D⟼if\left(y=\left(k\in I⟼if\left(k=X,n,0\right)\right),\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right){\cdot }_{P}V\left(X\right)$$
72		simplr	$$⊢\left(\left(\phi \wedge n\in {\mathbb{N}}_0\right)\wedge k\in I\right)\to n\in {\mathbb{N}}_0$$
73		0nn0	$$⊢0\in {\mathbb{N}}_0$$
74		ifcl	$$⊢\left(n\in {\mathbb{N}}_0\wedge 0\in {\mathbb{N}}_0\right)\to if\left(k=X,n,0\right)\in {\mathbb{N}}_0$$
75	72 73 74	sylancl	$$⊢\left(\left(\phi \wedge n\in {\mathbb{N}}_0\right)\wedge k\in I\right)\to if\left(k=X,n,0\right)\in {\mathbb{N}}_0$$
76	63 73	ifcli	$$⊢if\left(k=X,1,0\right)\in {\mathbb{N}}_0$$
77	76	a1i	$$⊢\left(\left(\phi \wedge n\in {\mathbb{N}}_0\right)\wedge k\in I\right)\to if\left(k=X,1,0\right)\in {\mathbb{N}}_0$$
78		eqidd	$$⊢\left(\phi \wedge n\in {\mathbb{N}}_0\right)\to \left(k\in I⟼if\left(k=X,n,0\right)\right)=\left(k\in I⟼if\left(k=X,n,0\right)\right)$$
79		eqidd	$$⊢\left(\phi \wedge n\in {\mathbb{N}}_0\right)\to \left(k\in I⟼if\left(k=X,1,0\right)\right)=\left(k\in I⟼if\left(k=X,1,0\right)\right)$$
80	58 75 77 78 79	offval2	$$⊢\left(\phi \wedge n\in {\mathbb{N}}_0\right)\to \left(k\in I⟼if\left(k=X,n,0\right)\right){+}_f\left(k\in I⟼if\left(k=X,1,0\right)\right)=\left(k\in I⟼if\left(k=X,n,0\right)+if\left(k=X,1,0\right)\right)$$
81		iftrue	$$⊢k=X\to if\left(k=X,n,0\right)=n$$
82		iftrue	$$⊢k=X\to if\left(k=X,1,0\right)=1$$
83	81 82	oveq12d	$$⊢k=X\to if\left(k=X,n,0\right)+if\left(k=X,1,0\right)=n+1$$
84		iftrue	$$⊢k=X\to if\left(k=X,n+1,0\right)=n+1$$
85	83 84	eqtr4d	$$⊢k=X\to if\left(k=X,n,0\right)+if\left(k=X,1,0\right)=if\left(k=X,n+1,0\right)$$
86		00id	$$⊢0+0=0$$
87		iffalse	$$⊢\neg k=X\to if\left(k=X,n,0\right)=0$$
88		iffalse	$$⊢\neg k=X\to if\left(k=X,1,0\right)=0$$
89	87 88	oveq12d	$$⊢\neg k=X\to if\left(k=X,n,0\right)+if\left(k=X,1,0\right)=0+0$$
90		iffalse	$$⊢\neg k=X\to if\left(k=X,n+1,0\right)=0$$
91	86 89 90	3eqtr4a	$$⊢\neg k=X\to if\left(k=X,n,0\right)+if\left(k=X,1,0\right)=if\left(k=X,n+1,0\right)$$
92	85 91	pm2.61i	$$⊢if\left(k=X,n,0\right)+if\left(k=X,1,0\right)=if\left(k=X,n+1,0\right)$$
93	92	mpteq2i	$$⊢\left(k\in I⟼if\left(k=X,n,0\right)+if\left(k=X,1,0\right)\right)=\left(k\in I⟼if\left(k=X,n+1,0\right)\right)$$
94	80 93	eqtrdi	$$⊢\left(\phi \wedge n\in {\mathbb{N}}_0\right)\to \left(k\in I⟼if\left(k=X,n,0\right)\right){+}_f\left(k\in I⟼if\left(k=X,1,0\right)\right)=\left(k\in I⟼if\left(k=X,n+1,0\right)\right)$$
95	94	eqeq2d	$$⊢\left(\phi \wedge n\in {\mathbb{N}}_0\right)\to \left(y=\left(k\in I⟼if\left(k=X,n,0\right)\right){+}_f\left(k\in I⟼if\left(k=X,1,0\right)\right)\leftrightarrow y=\left(k\in I⟼if\left(k=X,n+1,0\right)\right)\right)$$
96	95	ifbid	$$⊢\left(\phi \wedge n\in {\mathbb{N}}_0\right)\to if\left(y=\left(k\in I⟼if\left(k=X,n,0\right)\right){+}_f\left(k\in I⟼if\left(k=X,1,0\right)\right),\underset{\dot{}}{1},\underset{\dot{}}{0}\right)=if\left(y=\left(k\in I⟼if\left(k=X,n+1,0\right)\right),\underset{\dot{}}{1},\underset{\dot{}}{0}\right)$$
97	96	mpteq2dv	$$⊢\left(\phi \wedge n\in {\mathbb{N}}_0\right)\to \left(y\in D⟼if\left(y=\left(k\in I⟼if\left(k=X,n,0\right)\right){+}_f\left(k\in I⟼if\left(k=X,1,0\right)\right),\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)=\left(y\in D⟼if\left(y=\left(k\in I⟼if\left(k=X,n+1,0\right)\right),\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)$$
98	67 71 97	3eqtr3rd	$$⊢\left(\phi \wedge n\in {\mathbb{N}}_0\right)\to \left(y\in D⟼if\left(y=\left(k\in I⟼if\left(k=X,n+1,0\right)\right),\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)=\left(y\in D⟼if\left(y=\left(k\in I⟼if\left(k=X,n,0\right)\right),\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right){\cdot }_{P}V\left(X\right)$$
99	1 5 9	mplringd	$$⊢\phi \to P\in \mathrm{Ring}$$
100	6	ringmgp	$$⊢P\in \mathrm{Ring}\to G\in \mathrm{Mnd}$$
101	99 100	syl	$$⊢\phi \to G\in \mathrm{Mnd}$$
102	101	adantr	$$⊢\left(\phi \wedge n\in {\mathbb{N}}_0\right)\to G\in \mathrm{Mnd}$$
103		simpr	$$⊢\left(\phi \wedge n\in {\mathbb{N}}_0\right)\to n\in {\mathbb{N}}_0$$
104	49	adantr	$$⊢\left(\phi \wedge n\in {\mathbb{N}}_0\right)\to V\left(X\right)\in {\mathrm{Base}}_P$$
105	6 62	mgpplusg	$$⊢{\cdot }_P={+}_G$$
106	50 7 105	mulgnn0p1	$$⊢\left(G\in \mathrm{Mnd}\wedge n\in {\mathbb{N}}_0\wedge V\left(X\right)\in {\mathrm{Base}}_P\right)\to \left(n+1\right)\underset{\dot{}}{\times }V\left(X\right)=\left(n\underset{\dot{}}{\times }V\left(X\right)\right){\cdot }_{P}V\left(X\right)$$
107	102 103 104 106	syl3anc	$$⊢\left(\phi \wedge n\in {\mathbb{N}}_0\right)\to \left(n+1\right)\underset{\dot{}}{\times }V\left(X\right)=\left(n\underset{\dot{}}{\times }V\left(X\right)\right){\cdot }_{P}V\left(X\right)$$
108	98 107	eqeq12d	$$⊢\left(\phi \wedge n\in {\mathbb{N}}_0\right)\to \left(\left(y\in D⟼if\left(y=\left(k\in I⟼if\left(k=X,n+1,0\right)\right),\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)=\left(n+1\right)\underset{\dot{}}{\times }V\left(X\right)\leftrightarrow \left(y\in D⟼if\left(y=\left(k\in I⟼if\left(k=X,n,0\right)\right),\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right){\cdot }_{P}V\left(X\right)=\left(n\underset{\dot{}}{\times }V\left(X\right)\right){\cdot }_{P}V\left(X\right)\right)$$
109	57 108	imbitrrid	$$⊢\left(\phi \wedge n\in {\mathbb{N}}_0\right)\to \left(\left(y\in D⟼if\left(y=\left(k\in I⟼if\left(k=X,n,0\right)\right),\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)=n\underset{\dot{}}{\times }V\left(X\right)\to \left(y\in D⟼if\left(y=\left(k\in I⟼if\left(k=X,n+1,0\right)\right),\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)=\left(n+1\right)\underset{\dot{}}{\times }V\left(X\right)\right)$$
110	109	expcom	$$⊢n\in {\mathbb{N}}_0\to \left(\phi \to \left(\left(y\in D⟼if\left(y=\left(k\in I⟼if\left(k=X,n,0\right)\right),\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)=n\underset{\dot{}}{\times }V\left(X\right)\to \left(y\in D⟼if\left(y=\left(k\in I⟼if\left(k=X,n+1,0\right)\right),\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)=\left(n+1\right)\underset{\dot{}}{\times }V\left(X\right)\right)\right)$$
111	110	a2d	$$⊢n\in {\mathbb{N}}_0\to \left(\left(\phi \to \left(y\in D⟼if\left(y=\left(k\in I⟼if\left(k=X,n,0\right)\right),\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)=n\underset{\dot{}}{\times }V\left(X\right)\right)\to \left(\phi \to \left(y\in D⟼if\left(y=\left(k\in I⟼if\left(k=X,n+1,0\right)\right),\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)=\left(n+1\right)\underset{\dot{}}{\times }V\left(X\right)\right)\right)$$
112	23 31 39 47 56 111	nn0ind	$$⊢N\in {\mathbb{N}}_0\to \left(\phi \to \left(y\in D⟼if\left(y=\left(k\in I⟼if\left(k=X,N,0\right)\right),\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)=N\underset{\dot{}}{\times }V\left(X\right)\right)$$
113	11 112	mpcom	$$⊢\phi \to \left(y\in D⟼if\left(y=\left(k\in I⟼if\left(k=X,N,0\right)\right),\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)=N\underset{\dot{}}{\times }V\left(X\right)$$