fta1glem2

	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\}]$
	fta1glem.6	$⊢ φ \to \forall g \in B (D (g) = N \to \|{O (g)}^{-1} [\{W\}]\| \leq D (g))$
Assertion	fta1glem2	$⊢ φ \to \|{O (F)}^{-1} [\{W\}]\| \leq D (F)$

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		fta1glem.6	$⊢ φ \to \forall g \in B (D (g) = N \to \|{O (g)}^{-1} [\{W\}]\| \leq D (g))$
18		eqid	$⊢ R ↑_{𝑠} K = R ↑_{𝑠} K$
19		eqid	$⊢ {Base}_{(R ↑_{𝑠} K)} = {Base}_{(R ↑_{𝑠} K)}$
20	9	fvexi	$⊢ K \in V$
21	20	a1i	$⊢ φ \to K \in V$
22		isidom	$⊢ R \in IDomn \leftrightarrow (R \in CRing \land R \in Domn)$
23	22	simplbi	$⊢ R \in IDomn \to R \in CRing$
24	7 23	syl	$⊢ φ \to R \in CRing$
25	4 1 18 9	evl1rhm	$⊢ R \in CRing \to O \in (P RingHom (R ↑_{𝑠} K))$
26	24 25	syl	$⊢ φ \to O \in (P RingHom (R ↑_{𝑠} K))$
27	2 19	rhmf	$⊢ O \in (P RingHom (R ↑_{𝑠} K)) \to O : B ⟶ {Base}_{(R ↑_{𝑠} K)}$
28	26 27	syl	$⊢ φ \to O : B ⟶ {Base}_{(R ↑_{𝑠} K)}$
29	28 8	ffvelrnd	$⊢ φ \to O (F) \in {Base}_{(R ↑_{𝑠} K)}$
30	18 9 19 7 21 29	pwselbas	$⊢ φ \to O (F) : K ⟶ K$
31	30	ffnd	$⊢ φ \to O (F) Fn K$
32		fniniseg	$⊢ O (F) Fn K \to (T \in {O (F)}^{-1} [\{W\}] \leftrightarrow (T \in K \land O (F) (T) = W))$
33	31 32	syl	$⊢ φ \to (T \in {O (F)}^{-1} [\{W\}] \leftrightarrow (T \in K \land O (F) (T) = W))$
34	16 33	mpbid	$⊢ φ \to (T \in K \land O (F) (T) = W)$
35	34	simprd	$⊢ φ \to O (F) (T) = W$
36	22	simprbi	$⊢ R \in IDomn \to R \in Domn$
37		domnnzr	$⊢ R \in Domn \to R \in NzRing$
38	36 37	syl	$⊢ R \in IDomn \to R \in NzRing$
39	7 38	syl	$⊢ φ \to R \in NzRing$
40	34	simpld	$⊢ φ \to T \in K$
41		eqid	$⊢ ∥_{r} (P) = ∥_{r} (P)$
42	1 2 9 10 11 12 13 4 39 24 40 8 5 41	facth1	$⊢ φ \to (G ∥_{r} (P) F \leftrightarrow O (F) (T) = W)$
43	35 42	mpbird	$⊢ φ \to G ∥_{r} (P) F$
44		nzrring	$⊢ R \in NzRing \to R \in Ring$
45	39 44	syl	$⊢ φ \to R \in Ring$
46		eqid	$⊢ {Monic}_{1p} (R) = {Monic}_{1p} (R)$
47	1 2 9 10 11 12 13 4 39 24 40 46 3 5	ply1remlem	$⊢ φ \to (G \in {Monic}_{1p} (R) \land D (G) = 1 \land {O (G)}^{-1} [\{W\}] = \{T\})$
48	47	simp1d	$⊢ φ \to G \in {Monic}_{1p} (R)$
49		eqid	$⊢ {Unic}_{1p} (R) = {Unic}_{1p} (R)$
50	49 46	mon1puc1p	$⊢ (R \in Ring \land G \in {Monic}_{1p} (R)) \to G \in {Unic}_{1p} (R)$
51	45 48 50	syl2anc	$⊢ φ \to G \in {Unic}_{1p} (R)$
52		eqid	$⊢ \cdot_{P} = \cdot_{P}$
53		eqid	$⊢ {quot}_{1p} (R) = {quot}_{1p} (R)$
54	1 41 2 49 52 53	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)$
55	45 8 51 54	syl3anc	$⊢ φ \to (G ∥_{r} (P) F \leftrightarrow F = (F {quot}_{1p} (R) G) \cdot_{P} G)$
56	43 55	mpbid	$⊢ φ \to F = (F {quot}_{1p} (R) G) \cdot_{P} G$
57	56	fveq2d	$⊢ φ \to O (F) = O ((F {quot}_{1p} (R) G) \cdot_{P} G)$
58	53 1 2 49	q1pcl	$⊢ (R \in Ring \land F \in B \land G \in {Unic}_{1p} (R)) \to F {quot}_{1p} (R) G \in B$
59	45 8 51 58	syl3anc	$⊢ φ \to F {quot}_{1p} (R) G \in B$
60	1 2 46	mon1pcl	$⊢ G \in {Monic}_{1p} (R) \to G \in B$
61	48 60	syl	$⊢ φ \to G \in B$
62		eqid	$⊢ \cdot_{(R ↑_{𝑠} K)} = \cdot_{(R ↑_{𝑠} K)}$
63	2 52 62	rhmmul	$⊢ (O \in (P RingHom (R ↑_{𝑠} K)) \land F {quot}_{1p} (R) G \in B \land G \in B) \to O ((F {quot}_{1p} (R) G) \cdot_{P} G) = O (F {quot}_{1p} (R) G) \cdot_{(R ↑_{𝑠} K)} O (G)$
64	26 59 61 63	syl3anc	$⊢ φ \to O ((F {quot}_{1p} (R) G) \cdot_{P} G) = O (F {quot}_{1p} (R) G) \cdot_{(R ↑_{𝑠} K)} O (G)$
65	28 59	ffvelrnd	$⊢ φ \to O (F {quot}_{1p} (R) G) \in {Base}_{(R ↑_{𝑠} K)}$
66	28 61	ffvelrnd	$⊢ φ \to O (G) \in {Base}_{(R ↑_{𝑠} K)}$
67		eqid	$⊢ \cdot_{R} = \cdot_{R}$
68	18 19 7 21 65 66 67 62	pwsmulrval	$⊢ φ \to O (F {quot}_{1p} (R) G) \cdot_{(R ↑_{𝑠} K)} O (G) = O (F {quot}_{1p} (R) G) {\cdot_{R}}_{f} O (G)$
69	57 64 68	3eqtrd	$⊢ φ \to O (F) = O (F {quot}_{1p} (R) G) {\cdot_{R}}_{f} O (G)$
70	69	fveq1d	$⊢ φ \to O (F) (x) = (O (F {quot}_{1p} (R) G) {\cdot_{R}}_{f} O (G)) (x)$
71	70	adantr	$⊢ (φ \land x \in K) \to O (F) (x) = (O (F {quot}_{1p} (R) G) {\cdot_{R}}_{f} O (G)) (x)$
72	18 9 19 7 21 65	pwselbas	$⊢ φ \to O (F {quot}_{1p} (R) G) : K ⟶ K$
73	72	ffnd	$⊢ φ \to O (F {quot}_{1p} (R) G) Fn K$
74	73	adantr	$⊢ (φ \land x \in K) \to O (F {quot}_{1p} (R) G) Fn K$
75	18 9 19 7 21 66	pwselbas	$⊢ φ \to O (G) : K ⟶ K$
76	75	ffnd	$⊢ φ \to O (G) Fn K$
77	76	adantr	$⊢ (φ \land x \in K) \to O (G) Fn K$
78	20	a1i	$⊢ (φ \land x \in K) \to K \in V$
79		simpr	$⊢ (φ \land x \in K) \to x \in K$
80		fnfvof	$⊢ ((O (F {quot}_{1p} (R) G) Fn K \land O (G) Fn K) \land (K \in V \land x \in K)) \to (O (F {quot}_{1p} (R) G) {\cdot_{R}}_{f} O (G)) (x) = O (F {quot}_{1p} (R) G) (x) \cdot_{R} O (G) (x)$
81	74 77 78 79 80	syl22anc	$⊢ (φ \land x \in K) \to (O (F {quot}_{1p} (R) G) {\cdot_{R}}_{f} O (G)) (x) = O (F {quot}_{1p} (R) G) (x) \cdot_{R} O (G) (x)$
82	71 81	eqtrd	$⊢ (φ \land x \in K) \to O (F) (x) = O (F {quot}_{1p} (R) G) (x) \cdot_{R} O (G) (x)$
83	82	eqeq1d	$⊢ (φ \land x \in K) \to (O (F) (x) = W \leftrightarrow O (F {quot}_{1p} (R) G) (x) \cdot_{R} O (G) (x) = W)$
84	7 36	syl	$⊢ φ \to R \in Domn$
85	84	adantr	$⊢ (φ \land x \in K) \to R \in Domn$
86	72	ffvelrnda	$⊢ (φ \land x \in K) \to O (F {quot}_{1p} (R) G) (x) \in K$
87	75	ffvelrnda	$⊢ (φ \land x \in K) \to O (G) (x) \in K$
88	9 67 5	domneq0	$⊢ (R \in Domn \land O (F {quot}_{1p} (R) G) (x) \in K \land O (G) (x) \in K) \to (O (F {quot}_{1p} (R) G) (x) \cdot_{R} O (G) (x) = W \leftrightarrow (O (F {quot}_{1p} (R) G) (x) = W \lor O (G) (x) = W))$
89	85 86 87 88	syl3anc	$⊢ (φ \land x \in K) \to (O (F {quot}_{1p} (R) G) (x) \cdot_{R} O (G) (x) = W \leftrightarrow (O (F {quot}_{1p} (R) G) (x) = W \lor O (G) (x) = W))$
90	83 89	bitrd	$⊢ (φ \land x \in K) \to (O (F) (x) = W \leftrightarrow (O (F {quot}_{1p} (R) G) (x) = W \lor O (G) (x) = W))$
91	90	pm5.32da	$⊢ φ \to ((x \in K \land O (F) (x) = W) \leftrightarrow (x \in K \land (O (F {quot}_{1p} (R) G) (x) = W \lor O (G) (x) = W)))$
92		andi	$⊢ (x \in K \land (O (F {quot}_{1p} (R) G) (x) = W \lor O (G) (x) = W)) \leftrightarrow ((x \in K \land O (F {quot}_{1p} (R) G) (x) = W) \lor (x \in K \land O (G) (x) = W))$
93	91 92	bitrdi	$⊢ φ \to ((x \in K \land O (F) (x) = W) \leftrightarrow ((x \in K \land O (F {quot}_{1p} (R) G) (x) = W) \lor (x \in K \land O (G) (x) = W)))$
94		fniniseg	$⊢ O (F) Fn K \to (x \in {O (F)}^{-1} [\{W\}] \leftrightarrow (x \in K \land O (F) (x) = W))$
95	31 94	syl	$⊢ φ \to (x \in {O (F)}^{-1} [\{W\}] \leftrightarrow (x \in K \land O (F) (x) = W))$
96		elun	$⊢ x \in ({O (F {quot}_{1p} (R) G)}^{-1} [\{W\}] \cup \{T\}) \leftrightarrow (x \in {O (F {quot}_{1p} (R) G)}^{-1} [\{W\}] \lor x \in \{T\})$
97		fniniseg	$⊢ O (F {quot}_{1p} (R) G) Fn K \to (x \in {O (F {quot}_{1p} (R) G)}^{-1} [\{W\}] \leftrightarrow (x \in K \land O (F {quot}_{1p} (R) G) (x) = W))$
98	73 97	syl	$⊢ φ \to (x \in {O (F {quot}_{1p} (R) G)}^{-1} [\{W\}] \leftrightarrow (x \in K \land O (F {quot}_{1p} (R) G) (x) = W))$
99	47	simp3d	$⊢ φ \to {O (G)}^{-1} [\{W\}] = \{T\}$
100	99	eleq2d	$⊢ φ \to (x \in {O (G)}^{-1} [\{W\}] \leftrightarrow x \in \{T\})$
101		fniniseg	$⊢ O (G) Fn K \to (x \in {O (G)}^{-1} [\{W\}] \leftrightarrow (x \in K \land O (G) (x) = W))$
102	76 101	syl	$⊢ φ \to (x \in {O (G)}^{-1} [\{W\}] \leftrightarrow (x \in K \land O (G) (x) = W))$
103	100 102	bitr3d	$⊢ φ \to (x \in \{T\} \leftrightarrow (x \in K \land O (G) (x) = W))$
104	98 103	orbi12d	$⊢ φ \to ((x \in {O (F {quot}_{1p} (R) G)}^{-1} [\{W\}] \lor x \in \{T\}) \leftrightarrow ((x \in K \land O (F {quot}_{1p} (R) G) (x) = W) \lor (x \in K \land O (G) (x) = W)))$
105	96 104	syl5bb	$⊢ φ \to (x \in ({O (F {quot}_{1p} (R) G)}^{-1} [\{W\}] \cup \{T\}) \leftrightarrow ((x \in K \land O (F {quot}_{1p} (R) G) (x) = W) \lor (x \in K \land O (G) (x) = W)))$
106	93 95 105	3bitr4d	$⊢ φ \to (x \in {O (F)}^{-1} [\{W\}] \leftrightarrow x \in ({O (F {quot}_{1p} (R) G)}^{-1} [\{W\}] \cup \{T\}))$
107	106	eqrdv	$⊢ φ \to {O (F)}^{-1} [\{W\}] = {O (F {quot}_{1p} (R) G)}^{-1} [\{W\}] \cup \{T\}$
108	107	fveq2d	$⊢ φ \to \|{O (F)}^{-1} [\{W\}]\| = \|{O (F {quot}_{1p} (R) G)}^{-1} [\{W\}] \cup \{T\}\|$
109		fvex	$⊢ O (F {quot}_{1p} (R) G) \in V$
110	109	cnvex	$⊢ {O (F {quot}_{1p} (R) G)}^{-1} \in V$
111	110	imaex	$⊢ {O (F {quot}_{1p} (R) G)}^{-1} [\{W\}] \in V$
112	111	a1i	$⊢ φ \to {O (F {quot}_{1p} (R) G)}^{-1} [\{W\}] \in V$
113	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16	fta1glem1	$⊢ φ \to D (F {quot}_{1p} (R) G) = N$
114		fveq2	$⊢ g = F {quot}_{1p} (R) G \to D (g) = D (F {quot}_{1p} (R) G)$
115	114	eqeq1d	$⊢ g = F {quot}_{1p} (R) G \to (D (g) = N \leftrightarrow D (F {quot}_{1p} (R) G) = N)$
116		fveq2	$⊢ g = F {quot}_{1p} (R) G \to O (g) = O (F {quot}_{1p} (R) G)$
117	116	cnveqd	$⊢ g = F {quot}_{1p} (R) G \to {O (g)}^{-1} = {O (F {quot}_{1p} (R) G)}^{-1}$
118	117	imaeq1d	$⊢ g = F {quot}_{1p} (R) G \to {O (g)}^{-1} [\{W\}] = {O (F {quot}_{1p} (R) G)}^{-1} [\{W\}]$
119	118	fveq2d	$⊢ g = F {quot}_{1p} (R) G \to \|{O (g)}^{-1} [\{W\}]\| = \|{O (F {quot}_{1p} (R) G)}^{-1} [\{W\}]\|$
120	119 114	breq12d	$⊢ g = F {quot}_{1p} (R) G \to (\|{O (g)}^{-1} [\{W\}]\| \leq D (g) \leftrightarrow \|{O (F {quot}_{1p} (R) G)}^{-1} [\{W\}]\| \leq D (F {quot}_{1p} (R) G))$
121	115 120	imbi12d	$⊢ g = F {quot}_{1p} (R) G \to ((D (g) = N \to \|{O (g)}^{-1} [\{W\}]\| \leq D (g)) \leftrightarrow (D (F {quot}_{1p} (R) G) = N \to \|{O (F {quot}_{1p} (R) G)}^{-1} [\{W\}]\| \leq D (F {quot}_{1p} (R) G)))$
122	121 17 59	rspcdva	$⊢ φ \to (D (F {quot}_{1p} (R) G) = N \to \|{O (F {quot}_{1p} (R) G)}^{-1} [\{W\}]\| \leq D (F {quot}_{1p} (R) G))$
123	113 122	mpd	$⊢ φ \to \|{O (F {quot}_{1p} (R) G)}^{-1} [\{W\}]\| \leq D (F {quot}_{1p} (R) G)$
124	123 113	breqtrd	$⊢ φ \to \|{O (F {quot}_{1p} (R) G)}^{-1} [\{W\}]\| \leq N$
125		hashbnd	$⊢ ({O (F {quot}_{1p} (R) G)}^{-1} [\{W\}] \in V \land N \in ℕ_{0} \land \|{O (F {quot}_{1p} (R) G)}^{-1} [\{W\}]\| \leq N) \to {O (F {quot}_{1p} (R) G)}^{-1} [\{W\}] \in Fin$
126	112 14 124 125	syl3anc	$⊢ φ \to {O (F {quot}_{1p} (R) G)}^{-1} [\{W\}] \in Fin$
127		snfi	$⊢ \{T\} \in Fin$
128		unfi	$⊢ ({O (F {quot}_{1p} (R) G)}^{-1} [\{W\}] \in Fin \land \{T\} \in Fin) \to {O (F {quot}_{1p} (R) G)}^{-1} [\{W\}] \cup \{T\} \in Fin$
129	126 127 128	sylancl	$⊢ φ \to {O (F {quot}_{1p} (R) G)}^{-1} [\{W\}] \cup \{T\} \in Fin$
130		hashcl	$⊢ {O (F {quot}_{1p} (R) G)}^{-1} [\{W\}] \cup \{T\} \in Fin \to \|{O (F {quot}_{1p} (R) G)}^{-1} [\{W\}] \cup \{T\}\| \in ℕ_{0}$
131	129 130	syl	$⊢ φ \to \|{O (F {quot}_{1p} (R) G)}^{-1} [\{W\}] \cup \{T\}\| \in ℕ_{0}$
132	131	nn0red	$⊢ φ \to \|{O (F {quot}_{1p} (R) G)}^{-1} [\{W\}] \cup \{T\}\| \in ℝ$
133		hashcl	$⊢ {O (F {quot}_{1p} (R) G)}^{-1} [\{W\}] \in Fin \to \|{O (F {quot}_{1p} (R) G)}^{-1} [\{W\}]\| \in ℕ_{0}$
134	126 133	syl	$⊢ φ \to \|{O (F {quot}_{1p} (R) G)}^{-1} [\{W\}]\| \in ℕ_{0}$
135	134	nn0red	$⊢ φ \to \|{O (F {quot}_{1p} (R) G)}^{-1} [\{W\}]\| \in ℝ$
136		peano2re	$⊢ \|{O (F {quot}_{1p} (R) G)}^{-1} [\{W\}]\| \in ℝ \to \|{O (F {quot}_{1p} (R) G)}^{-1} [\{W\}]\| + 1 \in ℝ$
137	135 136	syl	$⊢ φ \to \|{O (F {quot}_{1p} (R) G)}^{-1} [\{W\}]\| + 1 \in ℝ$
138		peano2nn0	$⊢ N \in ℕ_{0} \to N + 1 \in ℕ_{0}$
139	14 138	syl	$⊢ φ \to N + 1 \in ℕ_{0}$
140	15 139	eqeltrd	$⊢ φ \to D (F) \in ℕ_{0}$
141	140	nn0red	$⊢ φ \to D (F) \in ℝ$
142		hashun2	$⊢ ({O (F {quot}_{1p} (R) G)}^{-1} [\{W\}] \in Fin \land \{T\} \in Fin) \to \|{O (F {quot}_{1p} (R) G)}^{-1} [\{W\}] \cup \{T\}\| \leq \|{O (F {quot}_{1p} (R) G)}^{-1} [\{W\}]\| + \|\{T\}\|$
143	126 127 142	sylancl	$⊢ φ \to \|{O (F {quot}_{1p} (R) G)}^{-1} [\{W\}] \cup \{T\}\| \leq \|{O (F {quot}_{1p} (R) G)}^{-1} [\{W\}]\| + \|\{T\}\|$
144		hashsng	$⊢ T \in {O (F)}^{-1} [\{W\}] \to \|\{T\}\| = 1$
145	16 144	syl	$⊢ φ \to \|\{T\}\| = 1$
146	145	oveq2d	$⊢ φ \to \|{O (F {quot}_{1p} (R) G)}^{-1} [\{W\}]\| + \|\{T\}\| = \|{O (F {quot}_{1p} (R) G)}^{-1} [\{W\}]\| + 1$
147	143 146	breqtrd	$⊢ φ \to \|{O (F {quot}_{1p} (R) G)}^{-1} [\{W\}] \cup \{T\}\| \leq \|{O (F {quot}_{1p} (R) G)}^{-1} [\{W\}]\| + 1$
148	14	nn0red	$⊢ φ \to N \in ℝ$
149		1red	$⊢ φ \to 1 \in ℝ$
150	135 148 149 124	leadd1dd	$⊢ φ \to \|{O (F {quot}_{1p} (R) G)}^{-1} [\{W\}]\| + 1 \leq N + 1$
151	150 15	breqtrrd	$⊢ φ \to \|{O (F {quot}_{1p} (R) G)}^{-1} [\{W\}]\| + 1 \leq D (F)$
152	132 137 141 147 151	letrd	$⊢ φ \to \|{O (F {quot}_{1p} (R) G)}^{-1} [\{W\}] \cup \{T\}\| \leq D (F)$
153	108 152	eqbrtrd	$⊢ φ \to \|{O (F)}^{-1} [\{W\}]\| \leq D (F)$

Metamath Proof Explorer

Theorem fta1glem2

Proof