Theorem fta1glem1

Description: Lemma for fta1g . (Contributed by Mario Carneiro, 7-Jun-2016)

	Ref	Expression
Hypotheses	fta1g.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
	fta1g.b	$$⊢B={\mathrm{Base}}_P$$
	fta1g.d	$$⊢D={\mathrm{deg}}_1\left(R\right)$$
	fta1g.o	$$⊢O={\mathrm{eval}}_1\left(R\right)$$
	fta1g.w	$$⊢W=0_R$$
	fta1g.z	$$⊢\underset{\dot{}}{0}=0_P$$
	fta1g.1	$$⊢\phi \to R\in \mathrm{IDomn}$$
	fta1g.2	$$⊢\phi \to F\in B$$
	fta1glem.k	$$⊢K={\mathrm{Base}}_R$$
	fta1glem.x	$$⊢X={\mathrm{var}}_1\left(R\right)$$
	fta1glem.m	$$⊢\underset{\dot{}}{-}={-}_P$$
	fta1glem.a	$$⊢A=\mathrm{algSc}\left(P\right)$$
	fta1glem.g	$$⊢G=X\underset{\dot{}}{-}A\left(T\right)$$
	fta1glem.3	$$⊢\phi \to N\in {\mathbb{N}}_0$$
	fta1glem.4	$$⊢\phi \to D\left(F\right)=N+1$$
	fta1glem.5	$$⊢\phi \to T\in {O\left(F\right)}^{-1}\left[\left\{W\right\}\right]$$
Assertion	fta1glem1	$$⊢\phi \to D\left(F{quot}_{\mathrm{1p}}\left(R\right)G\right)=N$$

Proof

Step	Hyp	Ref	Expression
1		fta1g.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
2		fta1g.b	$$⊢B={\mathrm{Base}}_P$$
3		fta1g.d	$$⊢D={\mathrm{deg}}_1\left(R\right)$$
4		fta1g.o	$$⊢O={\mathrm{eval}}_1\left(R\right)$$
5		fta1g.w	$$⊢W=0_R$$
6		fta1g.z	$$⊢\underset{\dot{}}{0}=0_P$$
7		fta1g.1	$$⊢\phi \to R\in \mathrm{IDomn}$$
8		fta1g.2	$$⊢\phi \to F\in B$$
9		fta1glem.k	$$⊢K={\mathrm{Base}}_R$$
10		fta1glem.x	$$⊢X={\mathrm{var}}_1\left(R\right)$$
11		fta1glem.m	$$⊢\underset{\dot{}}{-}={-}_P$$
12		fta1glem.a	$$⊢A=\mathrm{algSc}\left(P\right)$$
13		fta1glem.g	$$⊢G=X\underset{\dot{}}{-}A\left(T\right)$$
14		fta1glem.3	$$⊢\phi \to N\in {\mathbb{N}}_0$$
15		fta1glem.4	$$⊢\phi \to D\left(F\right)=N+1$$
16		fta1glem.5	$$⊢\phi \to T\in {O\left(F\right)}^{-1}\left[\left\{W\right\}\right]$$
17		1cnd	$$⊢\phi \to 1\in ℂ$$
18		isidom	$$⊢R\in \mathrm{IDomn}\leftrightarrow \left(R\in \mathrm{CRing}\wedge R\in \mathrm{Domn}\right)$$
19		domnnzr	$$⊢R\in \mathrm{Domn}\to R\in \mathrm{NzRing}$$
20	18 19	simplbiim	$$⊢R\in \mathrm{IDomn}\to R\in \mathrm{NzRing}$$
21	7 20	syl	$$⊢\phi \to R\in \mathrm{NzRing}$$
22		nzrring	$$⊢R\in \mathrm{NzRing}\to R\in \mathrm{Ring}$$
23	21 22	syl	$$⊢\phi \to R\in \mathrm{Ring}$$
24	18	simplbi	$$⊢R\in \mathrm{IDomn}\to R\in \mathrm{CRing}$$
25	7 24	syl	$$⊢\phi \to R\in \mathrm{CRing}$$
26		eqid	$$⊢R{\uparrow }_{𝑠}K=R{\uparrow }_{𝑠}K$$
27		eqid	$$⊢{\mathrm{Base}}_{\left(R{\uparrow }_{𝑠}K\right)}={\mathrm{Base}}_{\left(R{\uparrow }_{𝑠}K\right)}$$
28	9	fvexi	$$⊢K\in \mathrm{V}$$
29	28	a1i	$$⊢\phi \to K\in \mathrm{V}$$
30	4 1 26 9	evl1rhm	$$⊢R\in \mathrm{CRing}\to O\in \left(P\mathrm{RingHom}\left(R{\uparrow }_{𝑠}K\right)\right)$$
31	25 30	syl	$$⊢\phi \to O\in \left(P\mathrm{RingHom}\left(R{\uparrow }_{𝑠}K\right)\right)$$
32	2 27	rhmf	$$⊢O\in \left(P\mathrm{RingHom}\left(R{\uparrow }_{𝑠}K\right)\right)\to O:B⟶{\mathrm{Base}}_{\left(R{\uparrow }_{𝑠}K\right)}$$
33	31 32	syl	$$⊢\phi \to O:B⟶{\mathrm{Base}}_{\left(R{\uparrow }_{𝑠}K\right)}$$
34	33 8	ffvelcdmd	$$⊢\phi \to O\left(F\right)\in {\mathrm{Base}}_{\left(R{\uparrow }_{𝑠}K\right)}$$
35	26 9 27 7 29 34	pwselbas	$$⊢\phi \to O\left(F\right):K⟶K$$
36	35	ffnd	$$⊢\phi \to O\left(F\right)FnK$$
37		fniniseg	$$⊢O\left(F\right)FnK\to \left(T\in {O\left(F\right)}^{-1}\left[\left\{W\right\}\right]\leftrightarrow \left(T\in K\wedge O\left(F\right)\left(T\right)=W\right)\right)$$
38	36 37	syl	$$⊢\phi \to \left(T\in {O\left(F\right)}^{-1}\left[\left\{W\right\}\right]\leftrightarrow \left(T\in K\wedge O\left(F\right)\left(T\right)=W\right)\right)$$
39	16 38	mpbid	$$⊢\phi \to \left(T\in K\wedge O\left(F\right)\left(T\right)=W\right)$$
40	39	simpld	$$⊢\phi \to T\in K$$
41		eqid	$$⊢{Monic}_{\mathrm{1p}}\left(R\right)={Monic}_{\mathrm{1p}}\left(R\right)$$
42	1 2 9 10 11 12 13 4 21 25 40 41 3 5	ply1remlem	$$⊢\phi \to \left(G\in {Monic}_{\mathrm{1p}}\left(R\right)\wedge D\left(G\right)=1\wedge {O\left(G\right)}^{-1}\left[\left\{W\right\}\right]=\left\{T\right\}\right)$$
43	42	simp1d	$$⊢\phi \to G\in {Monic}_{\mathrm{1p}}\left(R\right)$$
44		eqid	$$⊢{Unic}_{\mathrm{1p}}\left(R\right)={Unic}_{\mathrm{1p}}\left(R\right)$$
45	44 41	mon1puc1p	$$⊢\left(R\in \mathrm{Ring}\wedge G\in {Monic}_{\mathrm{1p}}\left(R\right)\right)\to G\in {Unic}_{\mathrm{1p}}\left(R\right)$$
46	23 43 45	syl2anc	$$⊢\phi \to G\in {Unic}_{\mathrm{1p}}\left(R\right)$$
47		eqid	$$⊢{quot}_{\mathrm{1p}}\left(R\right)={quot}_{\mathrm{1p}}\left(R\right)$$
48	47 1 2 44	q1pcl	$$⊢\left(R\in \mathrm{Ring}\wedge F\in B\wedge G\in {Unic}_{\mathrm{1p}}\left(R\right)\right)\to F{quot}_{\mathrm{1p}}\left(R\right)G\in B$$
49	23 8 46 48	syl3anc	$$⊢\phi \to F{quot}_{\mathrm{1p}}\left(R\right)G\in B$$
50		peano2nn0	$$⊢N\in {\mathbb{N}}_0\to N+1\in {\mathbb{N}}_0$$
51	14 50	syl	$$⊢\phi \to N+1\in {\mathbb{N}}_0$$
52	15 51	eqeltrd	$$⊢\phi \to D\left(F\right)\in {\mathbb{N}}_0$$
53	3 1 6 2	deg1nn0clb	$$⊢\left(R\in \mathrm{Ring}\wedge F\in B\right)\to \left(F\ne \underset{\dot{}}{0}\leftrightarrow D\left(F\right)\in {\mathbb{N}}_0\right)$$
54	23 8 53	syl2anc	$$⊢\phi \to \left(F\ne \underset{\dot{}}{0}\leftrightarrow D\left(F\right)\in {\mathbb{N}}_0\right)$$
55	52 54	mpbird	$$⊢\phi \to F\ne \underset{\dot{}}{0}$$
56	39	simprd	$$⊢\phi \to O\left(F\right)\left(T\right)=W$$
57		eqid	$$⊢{\parallel }_r\left(P\right)={\parallel }_r\left(P\right)$$
58	1 2 9 10 11 12 13 4 21 25 40 8 5 57	facth1	$$⊢\phi \to \left(G{\parallel }_r\left(P\right)F\leftrightarrow O\left(F\right)\left(T\right)=W\right)$$
59	56 58	mpbird	$$⊢\phi \to G{\parallel }_r\left(P\right)F$$
60		eqid	$$⊢{\cdot }_P={\cdot }_P$$
61	1 57 2 44 60 47	dvdsq1p	$$⊢\left(R\in \mathrm{Ring}\wedge F\in B\wedge G\in {Unic}_{\mathrm{1p}}\left(R\right)\right)\to \left(G{\parallel }_r\left(P\right)F\leftrightarrow F=\left(F{quot}_{\mathrm{1p}}\left(R\right)G\right){\cdot }_{P}G\right)$$
62	23 8 46 61	syl3anc	$$⊢\phi \to \left(G{\parallel }_r\left(P\right)F\leftrightarrow F=\left(F{quot}_{\mathrm{1p}}\left(R\right)G\right){\cdot }_{P}G\right)$$
63	59 62	mpbid	$$⊢\phi \to F=\left(F{quot}_{\mathrm{1p}}\left(R\right)G\right){\cdot }_{P}G$$
64	63	eqcomd	$$⊢\phi \to \left(F{quot}_{\mathrm{1p}}\left(R\right)G\right){\cdot }_{P}G=F$$
65	1	ply1crng	$$⊢R\in \mathrm{CRing}\to P\in \mathrm{CRing}$$
66	25 65	syl	$$⊢\phi \to P\in \mathrm{CRing}$$
67		crngring	$$⊢P\in \mathrm{CRing}\to P\in \mathrm{Ring}$$
68	66 67	syl	$$⊢\phi \to P\in \mathrm{Ring}$$
69	1 2 41	mon1pcl	$$⊢G\in {Monic}_{\mathrm{1p}}\left(R\right)\to G\in B$$
70	43 69	syl	$$⊢\phi \to G\in B$$
71	2 60 6	ringlz	$$⊢\left(P\in \mathrm{Ring}\wedge G\in B\right)\to \underset{\dot{}}{0}{\cdot }_{P}G=\underset{\dot{}}{0}$$
72	68 70 71	syl2anc	$$⊢\phi \to \underset{\dot{}}{0}{\cdot }_{P}G=\underset{\dot{}}{0}$$
73	55 64 72	3netr4d	$$⊢\phi \to \left(F{quot}_{\mathrm{1p}}\left(R\right)G\right){\cdot }_{P}G\ne \underset{\dot{}}{0}{\cdot }_{P}G$$
74		oveq1	$$⊢F{quot}_{\mathrm{1p}}\left(R\right)G=\underset{\dot{}}{0}\to \left(F{quot}_{\mathrm{1p}}\left(R\right)G\right){\cdot }_{P}G=\underset{\dot{}}{0}{\cdot }_{P}G$$
75	74	necon3i	$$⊢\left(F{quot}_{\mathrm{1p}}\left(R\right)G\right){\cdot }_{P}G\ne \underset{\dot{}}{0}{\cdot }_{P}G\to F{quot}_{\mathrm{1p}}\left(R\right)G\ne \underset{\dot{}}{0}$$
76	73 75	syl	$$⊢\phi \to F{quot}_{\mathrm{1p}}\left(R\right)G\ne \underset{\dot{}}{0}$$
77	3 1 6 2	deg1nn0cl	$$⊢\left(R\in \mathrm{Ring}\wedge F{quot}_{\mathrm{1p}}\left(R\right)G\in B\wedge F{quot}_{\mathrm{1p}}\left(R\right)G\ne \underset{\dot{}}{0}\right)\to D\left(F{quot}_{\mathrm{1p}}\left(R\right)G\right)\in {\mathbb{N}}_0$$
78	23 49 76 77	syl3anc	$$⊢\phi \to D\left(F{quot}_{\mathrm{1p}}\left(R\right)G\right)\in {\mathbb{N}}_0$$
79	78	nn0cnd	$$⊢\phi \to D\left(F{quot}_{\mathrm{1p}}\left(R\right)G\right)\in ℂ$$
80	14	nn0cnd	$$⊢\phi \to N\in ℂ$$
81	2 60	crngcom	$$⊢\left(P\in \mathrm{CRing}\wedge F{quot}_{\mathrm{1p}}\left(R\right)G\in B\wedge G\in B\right)\to \left(F{quot}_{\mathrm{1p}}\left(R\right)G\right){\cdot }_{P}G=G{\cdot }_P\left(F{quot}_{\mathrm{1p}}\left(R\right)G\right)$$
82	66 49 70 81	syl3anc	$$⊢\phi \to \left(F{quot}_{\mathrm{1p}}\left(R\right)G\right){\cdot }_{P}G=G{\cdot }_P\left(F{quot}_{\mathrm{1p}}\left(R\right)G\right)$$
83	63 82	eqtrd	$$⊢\phi \to F=G{\cdot }_P\left(F{quot}_{\mathrm{1p}}\left(R\right)G\right)$$
84	83	fveq2d	$$⊢\phi \to D\left(F\right)=D\left(G{\cdot }_P\left(F{quot}_{\mathrm{1p}}\left(R\right)G\right)\right)$$
85		eqid	$$⊢\mathrm{RLReg}\left(R\right)=\mathrm{RLReg}\left(R\right)$$
86	42	simp2d	$$⊢\phi \to D\left(G\right)=1$$
87		1nn0	$$⊢1\in {\mathbb{N}}_0$$
88	86 87	eqeltrdi	$$⊢\phi \to D\left(G\right)\in {\mathbb{N}}_0$$
89	3 1 6 2	deg1nn0clb	$$⊢\left(R\in \mathrm{Ring}\wedge G\in B\right)\to \left(G\ne \underset{\dot{}}{0}\leftrightarrow D\left(G\right)\in {\mathbb{N}}_0\right)$$
90	23 70 89	syl2anc	$$⊢\phi \to \left(G\ne \underset{\dot{}}{0}\leftrightarrow D\left(G\right)\in {\mathbb{N}}_0\right)$$
91	88 90	mpbird	$$⊢\phi \to G\ne \underset{\dot{}}{0}$$
92		eqid	$$⊢\mathrm{Unit}\left(R\right)=\mathrm{Unit}\left(R\right)$$
93	85 92	unitrrg	$$⊢R\in \mathrm{Ring}\to \mathrm{Unit}\left(R\right)\subseteq \mathrm{RLReg}\left(R\right)$$
94	23 93	syl	$$⊢\phi \to \mathrm{Unit}\left(R\right)\subseteq \mathrm{RLReg}\left(R\right)$$
95	3 92 44	uc1pldg	$$⊢G\in {Unic}_{\mathrm{1p}}\left(R\right)\to {\mathrm{coe}}_1\left(G\right)\left(D\left(G\right)\right)\in \mathrm{Unit}\left(R\right)$$
96	46 95	syl	$$⊢\phi \to {\mathrm{coe}}_1\left(G\right)\left(D\left(G\right)\right)\in \mathrm{Unit}\left(R\right)$$
97	94 96	sseldd	$$⊢\phi \to {\mathrm{coe}}_1\left(G\right)\left(D\left(G\right)\right)\in \mathrm{RLReg}\left(R\right)$$
98	3 1 85 2 60 6 23 70 91 97 49 76	deg1mul2	$$⊢\phi \to D\left(G{\cdot }_P\left(F{quot}_{\mathrm{1p}}\left(R\right)G\right)\right)=D\left(G\right)+D\left(F{quot}_{\mathrm{1p}}\left(R\right)G\right)$$
99	84 15 98	3eqtr3d	$$⊢\phi \to N+1=D\left(G\right)+D\left(F{quot}_{\mathrm{1p}}\left(R\right)G\right)$$
100		ax-1cn	$$⊢1\in ℂ$$
101		addcom	$$⊢\left(N\in ℂ\wedge 1\in ℂ\right)\to N+1=1+N$$
102	80 100 101	sylancl	$$⊢\phi \to N+1=1+N$$
103	86	oveq1d	$$⊢\phi \to D\left(G\right)+D\left(F{quot}_{\mathrm{1p}}\left(R\right)G\right)=1+D\left(F{quot}_{\mathrm{1p}}\left(R\right)G\right)$$
104	99 102 103	3eqtr3rd	$$⊢\phi \to 1+D\left(F{quot}_{\mathrm{1p}}\left(R\right)G\right)=1+N$$
105	17 79 80 104	addcanad	$$⊢\phi \to D\left(F{quot}_{\mathrm{1p}}\left(R\right)G\right)=N$$