fta1blem

	Ref	Expression
Hypotheses	fta1b.p	$⊢ P = {Poly}_{1} (R)$
	fta1b.b	$⊢ B = {Base}_{P}$
	fta1b.d	$⊢ D = \deg_{1} (R)$
	fta1b.o	$⊢ O = {eval}_{1} (R)$
	fta1b.w	$⊢ W = 0_{R}$
	fta1b.z	$⊢ \underset{˙}{0} = 0_{P}$
	fta1blem.k	$⊢ K = {Base}_{R}$
	fta1blem.t	$⊢ \underset{˙}{\times} = \cdot_{R}$
	fta1blem.x	$⊢ X = {var}_{1} (R)$
	fta1blem.s	$⊢ \underset{˙}{\cdot} = \cdot_{P}$
	fta1blem.1	$⊢ φ \to R \in CRing$
	fta1blem.2	$⊢ φ \to M \in K$
	fta1blem.3	$⊢ φ \to N \in K$
	fta1blem.4	$⊢ φ \to M \underset{˙}{\times} N = W$
	fta1blem.5	$⊢ φ \to M \neq W$
	fta1blem.6	$⊢ φ \to (M \underset{˙}{\cdot} X \in (B ∖ \{\underset{˙}{0}\}) \to \|{O (M \underset{˙}{\cdot} X)}^{-1} [\{W\}]\| \leq D (M \underset{˙}{\cdot} X))$
Assertion	fta1blem	$⊢ φ \to N = W$

Proof

Step	Hyp	Ref	Expression
1		fta1b.p	$⊢ P = {Poly}_{1} (R)$
2		fta1b.b	$⊢ B = {Base}_{P}$
3		fta1b.d	$⊢ D = \deg_{1} (R)$
4		fta1b.o	$⊢ O = {eval}_{1} (R)$
5		fta1b.w	$⊢ W = 0_{R}$
6		fta1b.z	$⊢ \underset{˙}{0} = 0_{P}$
7		fta1blem.k	$⊢ K = {Base}_{R}$
8		fta1blem.t	$⊢ \underset{˙}{\times} = \cdot_{R}$
9		fta1blem.x	$⊢ X = {var}_{1} (R)$
10		fta1blem.s	$⊢ \underset{˙}{\cdot} = \cdot_{P}$
11		fta1blem.1	$⊢ φ \to R \in CRing$
12		fta1blem.2	$⊢ φ \to M \in K$
13		fta1blem.3	$⊢ φ \to N \in K$
14		fta1blem.4	$⊢ φ \to M \underset{˙}{\times} N = W$
15		fta1blem.5	$⊢ φ \to M \neq W$
16		fta1blem.6	$⊢ φ \to (M \underset{˙}{\cdot} X \in (B ∖ \{\underset{˙}{0}\}) \to \|{O (M \underset{˙}{\cdot} X)}^{-1} [\{W\}]\| \leq D (M \underset{˙}{\cdot} X))$
17	4 9 7 1 2 11 13	evl1vard	$⊢ φ \to (X \in B \land O (X) (N) = N)$
18	4 1 7 2 11 13 17 12 10 8	evl1vsd	$⊢ φ \to (M \underset{˙}{\cdot} X \in B \land O (M \underset{˙}{\cdot} X) (N) = M \underset{˙}{\times} N)$
19	18	simprd	$⊢ φ \to O (M \underset{˙}{\cdot} X) (N) = M \underset{˙}{\times} N$
20	19 14	eqtrd	$⊢ φ \to O (M \underset{˙}{\cdot} X) (N) = W$
21		eqid	$⊢ R ↑_{𝑠} K = R ↑_{𝑠} K$
22		eqid	$⊢ {Base}_{(R ↑_{𝑠} K)} = {Base}_{(R ↑_{𝑠} K)}$
23	7	fvexi	$⊢ K \in V$
24	23	a1i	$⊢ φ \to K \in V$
25	4 1 21 7	evl1rhm	$⊢ R \in CRing \to O \in (P RingHom (R ↑_{𝑠} K))$
26	11 25	syl	$⊢ φ \to O \in (P RingHom (R ↑_{𝑠} K))$
27	2 22	rhmf	$⊢ O \in (P RingHom (R ↑_{𝑠} K)) \to O : B ⟶ {Base}_{(R ↑_{𝑠} K)}$
28	26 27	syl	$⊢ φ \to O : B ⟶ {Base}_{(R ↑_{𝑠} K)}$
29	18	simpld	$⊢ φ \to M \underset{˙}{\cdot} X \in B$
30	28 29	ffvelrnd	$⊢ φ \to O (M \underset{˙}{\cdot} X) \in {Base}_{(R ↑_{𝑠} K)}$
31	21 7 22 11 24 30	pwselbas	$⊢ φ \to O (M \underset{˙}{\cdot} X) : K ⟶ K$
32	31	ffnd	$⊢ φ \to O (M \underset{˙}{\cdot} X) Fn K$
33		fniniseg	$⊢ O (M \underset{˙}{\cdot} X) Fn K \to (N \in {O (M \underset{˙}{\cdot} X)}^{-1} [\{W\}] \leftrightarrow (N \in K \land O (M \underset{˙}{\cdot} X) (N) = W))$
34	32 33	syl	$⊢ φ \to (N \in {O (M \underset{˙}{\cdot} X)}^{-1} [\{W\}] \leftrightarrow (N \in K \land O (M \underset{˙}{\cdot} X) (N) = W))$
35	13 20 34	mpbir2and	$⊢ φ \to N \in {O (M \underset{˙}{\cdot} X)}^{-1} [\{W\}]$
36		fvex	$⊢ O (M \underset{˙}{\cdot} X) \in V$
37	36	cnvex	$⊢ {O (M \underset{˙}{\cdot} X)}^{-1} \in V$
38	37	imaex	$⊢ {O (M \underset{˙}{\cdot} X)}^{-1} [\{W\}] \in V$
39	38	a1i	$⊢ φ \to {O (M \underset{˙}{\cdot} X)}^{-1} [\{W\}] \in V$
40		1nn0	$⊢ 1 \in ℕ_{0}$
41	40	a1i	$⊢ φ \to 1 \in ℕ_{0}$
42		crngring	$⊢ R \in CRing \to R \in Ring$
43	11 42	syl	$⊢ φ \to R \in Ring$
44	9 1 2	vr1cl	$⊢ R \in Ring \to X \in B$
45	43 44	syl	$⊢ φ \to X \in B$
46		eqid	$⊢ {mulGrp}_{P} = {mulGrp}_{P}$
47	46 2	mgpbas	$⊢ B = {Base}_{{mulGrp}_{P}}$
48		eqid	$⊢ \cdot_{{mulGrp}_{P}} = \cdot_{{mulGrp}_{P}}$
49	47 48	mulg1	$⊢ X \in B \to 1 \cdot_{{mulGrp}_{P}} X = X$
50	45 49	syl	$⊢ φ \to 1 \cdot_{{mulGrp}_{P}} X = X$
51	50	oveq2d	$⊢ φ \to M \underset{˙}{\cdot} (1 \cdot_{{mulGrp}_{P}} X) = M \underset{˙}{\cdot} X$
52	5 7 1 9 10 46 48	coe1tmfv1	$⊢ (R \in Ring \land M \in K \land 1 \in ℕ_{0}) \to {coe}_{1} (M \underset{˙}{\cdot} (1 \cdot_{{mulGrp}_{P}} X)) (1) = M$
53	43 12 41 52	syl3anc	$⊢ φ \to {coe}_{1} (M \underset{˙}{\cdot} (1 \cdot_{{mulGrp}_{P}} X)) (1) = M$
54	1 6 5	coe1z	$⊢ R \in Ring \to {coe}_{1} (\underset{˙}{0}) = ℕ_{0} \times \{W\}$
55	43 54	syl	$⊢ φ \to {coe}_{1} (\underset{˙}{0}) = ℕ_{0} \times \{W\}$
56	55	fveq1d	$⊢ φ \to {coe}_{1} (\underset{˙}{0}) (1) = (ℕ_{0} \times \{W\}) (1)$
57	5	fvexi	$⊢ W \in V$
58	57	fvconst2	$⊢ 1 \in ℕ_{0} \to (ℕ_{0} \times \{W\}) (1) = W$
59	40 58	ax-mp	$⊢ (ℕ_{0} \times \{W\}) (1) = W$
60	56 59	eqtrdi	$⊢ φ \to {coe}_{1} (\underset{˙}{0}) (1) = W$
61	15 53 60	3netr4d	$⊢ φ \to {coe}_{1} (M \underset{˙}{\cdot} (1 \cdot_{{mulGrp}_{P}} X)) (1) \neq {coe}_{1} (\underset{˙}{0}) (1)$
62		fveq2	$⊢ M \underset{˙}{\cdot} (1 \cdot_{{mulGrp}_{P}} X) = \underset{˙}{0} \to {coe}_{1} (M \underset{˙}{\cdot} (1 \cdot_{{mulGrp}_{P}} X)) = {coe}_{1} (\underset{˙}{0})$
63	62	fveq1d	$⊢ M \underset{˙}{\cdot} (1 \cdot_{{mulGrp}_{P}} X) = \underset{˙}{0} \to {coe}_{1} (M \underset{˙}{\cdot} (1 \cdot_{{mulGrp}_{P}} X)) (1) = {coe}_{1} (\underset{˙}{0}) (1)$
64	63	necon3i	$⊢ {coe}_{1} (M \underset{˙}{\cdot} (1 \cdot_{{mulGrp}_{P}} X)) (1) \neq {coe}_{1} (\underset{˙}{0}) (1) \to M \underset{˙}{\cdot} (1 \cdot_{{mulGrp}_{P}} X) \neq \underset{˙}{0}$
65	61 64	syl	$⊢ φ \to M \underset{˙}{\cdot} (1 \cdot_{{mulGrp}_{P}} X) \neq \underset{˙}{0}$
66	51 65	eqnetrrd	$⊢ φ \to M \underset{˙}{\cdot} X \neq \underset{˙}{0}$
67		eldifsn	$⊢ M \underset{˙}{\cdot} X \in (B ∖ \{\underset{˙}{0}\}) \leftrightarrow (M \underset{˙}{\cdot} X \in B \land M \underset{˙}{\cdot} X \neq \underset{˙}{0})$
68	29 66 67	sylanbrc	$⊢ φ \to M \underset{˙}{\cdot} X \in (B ∖ \{\underset{˙}{0}\})$
69	68 16	mpd	$⊢ φ \to \|{O (M \underset{˙}{\cdot} X)}^{-1} [\{W\}]\| \leq D (M \underset{˙}{\cdot} X)$
70	51	fveq2d	$⊢ φ \to D (M \underset{˙}{\cdot} (1 \cdot_{{mulGrp}_{P}} X)) = D (M \underset{˙}{\cdot} X)$
71	3 7 1 9 10 46 48 5	deg1tm	$⊢ (R \in Ring \land (M \in K \land M \neq W) \land 1 \in ℕ_{0}) \to D (M \underset{˙}{\cdot} (1 \cdot_{{mulGrp}_{P}} X)) = 1$
72	43 12 15 41 71	syl121anc	$⊢ φ \to D (M \underset{˙}{\cdot} (1 \cdot_{{mulGrp}_{P}} X)) = 1$
73	70 72	eqtr3d	$⊢ φ \to D (M \underset{˙}{\cdot} X) = 1$
74	69 73	breqtrd	$⊢ φ \to \|{O (M \underset{˙}{\cdot} X)}^{-1} [\{W\}]\| \leq 1$
75		hashbnd	$⊢ ({O (M \underset{˙}{\cdot} X)}^{-1} [\{W\}] \in V \land 1 \in ℕ_{0} \land \|{O (M \underset{˙}{\cdot} X)}^{-1} [\{W\}]\| \leq 1) \to {O (M \underset{˙}{\cdot} X)}^{-1} [\{W\}] \in Fin$
76	39 41 74 75	syl3anc	$⊢ φ \to {O (M \underset{˙}{\cdot} X)}^{-1} [\{W\}] \in Fin$
77	7 5	ring0cl	$⊢ R \in Ring \to W \in K$
78	43 77	syl	$⊢ φ \to W \in K$
79		eqid	$⊢ algSc (P) = algSc (P)$
80	1 79 7 2	ply1sclf	$⊢ R \in Ring \to algSc (P) : K ⟶ B$
81	43 80	syl	$⊢ φ \to algSc (P) : K ⟶ B$
82	81 12	ffvelrnd	$⊢ φ \to algSc (P) (M) \in B$
83		eqid	$⊢ \cdot_{P} = \cdot_{P}$
84		eqid	$⊢ \cdot_{(R ↑_{𝑠} K)} = \cdot_{(R ↑_{𝑠} K)}$
85	2 83 84	rhmmul	$⊢ (O \in (P RingHom (R ↑_{𝑠} K)) \land algSc (P) (M) \in B \land X \in B) \to O (algSc (P) (M) \cdot_{P} X) = O (algSc (P) (M)) \cdot_{(R ↑_{𝑠} K)} O (X)$
86	26 82 45 85	syl3anc	$⊢ φ \to O (algSc (P) (M) \cdot_{P} X) = O (algSc (P) (M)) \cdot_{(R ↑_{𝑠} K)} O (X)$
87	1	ply1assa	$⊢ R \in CRing \to P \in AssAlg$
88	11 87	syl	$⊢ φ \to P \in AssAlg$
89	1	ply1sca	$⊢ R \in CRing \to R = Scalar (P)$
90	11 89	syl	$⊢ φ \to R = Scalar (P)$
91	90	fveq2d	$⊢ φ \to {Base}_{R} = {Base}_{Scalar (P)}$
92	7 91	eqtrid	$⊢ φ \to K = {Base}_{Scalar (P)}$
93	12 92	eleqtrd	$⊢ φ \to M \in {Base}_{Scalar (P)}$
94		eqid	$⊢ Scalar (P) = Scalar (P)$
95		eqid	$⊢ {Base}_{Scalar (P)} = {Base}_{Scalar (P)}$
96	79 94 95 2 83 10	asclmul1	$⊢ (P \in AssAlg \land M \in {Base}_{Scalar (P)} \land X \in B) \to algSc (P) (M) \cdot_{P} X = M \underset{˙}{\cdot} X$
97	88 93 45 96	syl3anc	$⊢ φ \to algSc (P) (M) \cdot_{P} X = M \underset{˙}{\cdot} X$
98	97	fveq2d	$⊢ φ \to O (algSc (P) (M) \cdot_{P} X) = O (M \underset{˙}{\cdot} X)$
99	28 82	ffvelrnd	$⊢ φ \to O (algSc (P) (M)) \in {Base}_{(R ↑_{𝑠} K)}$
100	28 45	ffvelrnd	$⊢ φ \to O (X) \in {Base}_{(R ↑_{𝑠} K)}$
101	21 22 11 24 99 100 8 84	pwsmulrval	$⊢ φ \to O (algSc (P) (M)) \cdot_{(R ↑_{𝑠} K)} O (X) = O (algSc (P) (M)) {\underset{˙}{\times}}_{f} O (X)$
102	4 1 7 79	evl1sca	$⊢ (R \in CRing \land M \in K) \to O (algSc (P) (M)) = K \times \{M\}$
103	11 12 102	syl2anc	$⊢ φ \to O (algSc (P) (M)) = K \times \{M\}$
104	4 9 7	evl1var	$⊢ R \in CRing \to O (X) = {I ↾}_{K}$
105	11 104	syl	$⊢ φ \to O (X) = {I ↾}_{K}$
106	103 105	oveq12d	$⊢ φ \to O (algSc (P) (M)) {\underset{˙}{\times}}_{f} O (X) = (K \times \{M\}) {\underset{˙}{\times}}_{f} ({I ↾}_{K})$
107	101 106	eqtrd	$⊢ φ \to O (algSc (P) (M)) \cdot_{(R ↑_{𝑠} K)} O (X) = (K \times \{M\}) {\underset{˙}{\times}}_{f} ({I ↾}_{K})$
108	86 98 107	3eqtr3d	$⊢ φ \to O (M \underset{˙}{\cdot} X) = (K \times \{M\}) {\underset{˙}{\times}}_{f} ({I ↾}_{K})$
109	108	fveq1d	$⊢ φ \to O (M \underset{˙}{\cdot} X) (W) = ((K \times \{M\}) {\underset{˙}{\times}}_{f} ({I ↾}_{K})) (W)$
110		fnconstg	$⊢ M \in K \to (K \times \{M\}) Fn K$
111	12 110	syl	$⊢ φ \to (K \times \{M\}) Fn K$
112		fnresi	$⊢ ({I ↾}_{K}) Fn K$
113	112	a1i	$⊢ φ \to ({I ↾}_{K}) Fn K$
114		fnfvof	$⊢ (((K \times \{M\}) Fn K \land ({I ↾}_{K}) Fn K) \land (K \in V \land W \in K)) \to ((K \times \{M\}) {\underset{˙}{\times}}_{f} ({I ↾}_{K})) (W) = (K \times \{M\}) (W) \underset{˙}{\times} ({I ↾}_{K}) (W)$
115	111 113 24 78 114	syl22anc	$⊢ φ \to ((K \times \{M\}) {\underset{˙}{\times}}_{f} ({I ↾}_{K})) (W) = (K \times \{M\}) (W) \underset{˙}{\times} ({I ↾}_{K}) (W)$
116		fvconst2g	$⊢ (M \in K \land W \in K) \to (K \times \{M\}) (W) = M$
117	12 78 116	syl2anc	$⊢ φ \to (K \times \{M\}) (W) = M$
118		fvresi	$⊢ W \in K \to ({I ↾}_{K}) (W) = W$
119	78 118	syl	$⊢ φ \to ({I ↾}_{K}) (W) = W$
120	117 119	oveq12d	$⊢ φ \to (K \times \{M\}) (W) \underset{˙}{\times} ({I ↾}_{K}) (W) = M \underset{˙}{\times} W$
121	7 8 5	ringrz	$⊢ (R \in Ring \land M \in K) \to M \underset{˙}{\times} W = W$
122	43 12 121	syl2anc	$⊢ φ \to M \underset{˙}{\times} W = W$
123	120 122	eqtrd	$⊢ φ \to (K \times \{M\}) (W) \underset{˙}{\times} ({I ↾}_{K}) (W) = W$
124	115 123	eqtrd	$⊢ φ \to ((K \times \{M\}) {\underset{˙}{\times}}_{f} ({I ↾}_{K})) (W) = W$
125	109 124	eqtrd	$⊢ φ \to O (M \underset{˙}{\cdot} X) (W) = W$
126		fniniseg	$⊢ O (M \underset{˙}{\cdot} X) Fn K \to (W \in {O (M \underset{˙}{\cdot} X)}^{-1} [\{W\}] \leftrightarrow (W \in K \land O (M \underset{˙}{\cdot} X) (W) = W))$
127	32 126	syl	$⊢ φ \to (W \in {O (M \underset{˙}{\cdot} X)}^{-1} [\{W\}] \leftrightarrow (W \in K \land O (M \underset{˙}{\cdot} X) (W) = W))$
128	78 125 127	mpbir2and	$⊢ φ \to W \in {O (M \underset{˙}{\cdot} X)}^{-1} [\{W\}]$
129	128	snssd	$⊢ φ \to \{W\} \subseteq {O (M \underset{˙}{\cdot} X)}^{-1} [\{W\}]$
130		hashsng	$⊢ W \in K \to \|\{W\}\| = 1$
131	78 130	syl	$⊢ φ \to \|\{W\}\| = 1$
132		ssdomg	$⊢ {O (M \underset{˙}{\cdot} X)}^{-1} [\{W\}] \in V \to (\{W\} \subseteq {O (M \underset{˙}{\cdot} X)}^{-1} [\{W\}] \to \{W\} ≼ {O (M \underset{˙}{\cdot} X)}^{-1} [\{W\}])$
133	38 129 132	mpsyl	$⊢ φ \to \{W\} ≼ {O (M \underset{˙}{\cdot} X)}^{-1} [\{W\}]$
134		snfi	$⊢ \{W\} \in Fin$
135		hashdom	$⊢ (\{W\} \in Fin \land {O (M \underset{˙}{\cdot} X)}^{-1} [\{W\}] \in V) \to (\|\{W\}\| \leq \|{O (M \underset{˙}{\cdot} X)}^{-1} [\{W\}]\| \leftrightarrow \{W\} ≼ {O (M \underset{˙}{\cdot} X)}^{-1} [\{W\}])$
136	134 38 135	mp2an	$⊢ \|\{W\}\| \leq \|{O (M \underset{˙}{\cdot} X)}^{-1} [\{W\}]\| \leftrightarrow \{W\} ≼ {O (M \underset{˙}{\cdot} X)}^{-1} [\{W\}]$
137	133 136	sylibr	$⊢ φ \to \|\{W\}\| \leq \|{O (M \underset{˙}{\cdot} X)}^{-1} [\{W\}]\|$
138	131 137	eqbrtrrd	$⊢ φ \to 1 \leq \|{O (M \underset{˙}{\cdot} X)}^{-1} [\{W\}]\|$
139		hashcl	$⊢ {O (M \underset{˙}{\cdot} X)}^{-1} [\{W\}] \in Fin \to \|{O (M \underset{˙}{\cdot} X)}^{-1} [\{W\}]\| \in ℕ_{0}$
140	76 139	syl	$⊢ φ \to \|{O (M \underset{˙}{\cdot} X)}^{-1} [\{W\}]\| \in ℕ_{0}$
141	140	nn0red	$⊢ φ \to \|{O (M \underset{˙}{\cdot} X)}^{-1} [\{W\}]\| \in ℝ$
142		1re	$⊢ 1 \in ℝ$
143		letri3	$⊢ (\|{O (M \underset{˙}{\cdot} X)}^{-1} [\{W\}]\| \in ℝ \land 1 \in ℝ) \to (\|{O (M \underset{˙}{\cdot} X)}^{-1} [\{W\}]\| = 1 \leftrightarrow (\|{O (M \underset{˙}{\cdot} X)}^{-1} [\{W\}]\| \leq 1 \land 1 \leq \|{O (M \underset{˙}{\cdot} X)}^{-1} [\{W\}]\|))$
144	141 142 143	sylancl	$⊢ φ \to (\|{O (M \underset{˙}{\cdot} X)}^{-1} [\{W\}]\| = 1 \leftrightarrow (\|{O (M \underset{˙}{\cdot} X)}^{-1} [\{W\}]\| \leq 1 \land 1 \leq \|{O (M \underset{˙}{\cdot} X)}^{-1} [\{W\}]\|))$
145	74 138 144	mpbir2and	$⊢ φ \to \|{O (M \underset{˙}{\cdot} X)}^{-1} [\{W\}]\| = 1$
146	131 145	eqtr4d	$⊢ φ \to \|\{W\}\| = \|{O (M \underset{˙}{\cdot} X)}^{-1} [\{W\}]\|$
147		hashen	$⊢ (\{W\} \in Fin \land {O (M \underset{˙}{\cdot} X)}^{-1} [\{W\}] \in Fin) \to (\|\{W\}\| = \|{O (M \underset{˙}{\cdot} X)}^{-1} [\{W\}]\| \leftrightarrow \{W\} \approx {O (M \underset{˙}{\cdot} X)}^{-1} [\{W\}])$
148	134 76 147	sylancr	$⊢ φ \to (\|\{W\}\| = \|{O (M \underset{˙}{\cdot} X)}^{-1} [\{W\}]\| \leftrightarrow \{W\} \approx {O (M \underset{˙}{\cdot} X)}^{-1} [\{W\}])$
149	146 148	mpbid	$⊢ φ \to \{W\} \approx {O (M \underset{˙}{\cdot} X)}^{-1} [\{W\}]$
150		fisseneq	$⊢ ({O (M \underset{˙}{\cdot} X)}^{-1} [\{W\}] \in Fin \land \{W\} \subseteq {O (M \underset{˙}{\cdot} X)}^{-1} [\{W\}] \land \{W\} \approx {O (M \underset{˙}{\cdot} X)}^{-1} [\{W\}]) \to \{W\} = {O (M \underset{˙}{\cdot} X)}^{-1} [\{W\}]$
151	76 129 149 150	syl3anc	$⊢ φ \to \{W\} = {O (M \underset{˙}{\cdot} X)}^{-1} [\{W\}]$
152	35 151	eleqtrrd	$⊢ φ \to N \in \{W\}$
153		elsni	$⊢ N \in \{W\} \to N = W$
154	152 153	syl	$⊢ φ \to N = W$

Metamath Proof Explorer

Theorem fta1blem

Proof