# Metamath Proof Explorer

## 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
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
fta1glem.a ${⊢}{A}=\mathrm{algSc}\left({P}\right)$
fta1glem.g
fta1glem.3 ${⊢}{\phi }\to {N}\in {ℕ}_{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
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
12 fta1glem.a ${⊢}{A}=\mathrm{algSc}\left({P}\right)$
13 fta1glem.g
14 fta1glem.3 ${⊢}{\phi }\to {N}\in {ℕ}_{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}↔\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}{↑}_{𝑠}{K}={R}{↑}_{𝑠}{K}$
27 eqid ${⊢}{\mathrm{Base}}_{\left({R}{↑}_{𝑠}{K}\right)}={\mathrm{Base}}_{\left({R}{↑}_{𝑠}{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}{↑}_{𝑠}{K}\right)\right)$
31 25 30 syl ${⊢}{\phi }\to {O}\in \left({P}\mathrm{RingHom}\left({R}{↑}_{𝑠}{K}\right)\right)$
32 2 27 rhmf ${⊢}{O}\in \left({P}\mathrm{RingHom}\left({R}{↑}_{𝑠}{K}\right)\right)\to {O}:{B}⟶{\mathrm{Base}}_{\left({R}{↑}_{𝑠}{K}\right)}$
33 31 32 syl ${⊢}{\phi }\to {O}:{B}⟶{\mathrm{Base}}_{\left({R}{↑}_{𝑠}{K}\right)}$
34 33 8 ffvelrnd ${⊢}{\phi }\to {O}\left({F}\right)\in {\mathrm{Base}}_{\left({R}{↑}_{𝑠}{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)Fn{K}$
37 fniniseg ${⊢}{O}\left({F}\right)Fn{K}\to \left({T}\in {{O}\left({F}\right)}^{-1}\left[\left\{{W}\right\}\right]↔\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]↔\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 {ℕ}_{0}\to {N}+1\in {ℕ}_{0}$
51 14 50 syl ${⊢}{\phi }\to {N}+1\in {ℕ}_{0}$
52 15 51 eqeltrd ${⊢}{\phi }\to {D}\left({F}\right)\in {ℕ}_{0}$
53 3 1 6 2 deg1nn0clb
54 23 8 53 syl2anc
55 52 54 mpbird
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}↔{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}↔{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}↔{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
72 68 70 71 syl2anc
73 55 64 72 3netr4d
74 oveq1
75 74 necon3i
76 73 75 syl
77 3 1 6 2 deg1nn0cl
78 23 49 76 77 syl3anc ${⊢}{\phi }\to {D}\left({F}{quot}_{\mathrm{1p}}\left({R}\right){G}\right)\in {ℕ}_{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 {ℕ}_{0}$
88 86 87 syl6eqel ${⊢}{\phi }\to {D}\left({G}\right)\in {ℕ}_{0}$
89 3 1 6 2 deg1nn0clb
90 23 70 89 syl2anc
91 88 90 mpbird
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}$