fta1glem1

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

Proof

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

Metamath Proof Explorer

Theorem fta1glem1

Proof