ply1dg1rt

Description: Express the root - B / A of a polynomial A x. X + B of degree 1 over a field. (Contributed by Thierry Arnoux, 8-Jun-2025)

	Ref	Expression
Hypotheses	ply1dg1rt.p	$⊢ P = {Poly}_{1} (R)$
	ply1dg1rt.u	$⊢ U = {Base}_{P}$
	ply1dg1rt.o	$⊢ O = {eval}_{1} (R)$
	ply1dg1rt.d	$⊢ D = \deg_{1} (R)$
	ply1dg1rt.0	$⊢ \underset{˙}{0} = 0_{R}$
	ply1dg1rt.r	$⊢ φ \to R \in Field$
	ply1dg1rt.g	$⊢ φ \to G \in U$
	ply1dg1rt.1	$⊢ φ \to D (G) = 1$
	ply1dg1rt.x	$⊢ N = {inv}_{g} (R)$
	ply1dg1rt.m	$⊢ \underset{˙}{\times} = /_{r} (R)$
	ply1dg1rt.c	$⊢ C = {coe}_{1} (G)$
	ply1dg1rt.a	$⊢ A = C (1)$
	ply1dg1rt.b	$⊢ B = C (0)$
	ply1dg1rt.z	$⊢ Z = N (B) \underset{˙}{\times} A$
Assertion	ply1dg1rt	$⊢ φ \to {O (G)}^{-1} [\{\underset{˙}{0}\}] = \{Z\}$

Proof

Step	Hyp	Ref	Expression
1		ply1dg1rt.p	$⊢ P = {Poly}_{1} (R)$
2		ply1dg1rt.u	$⊢ U = {Base}_{P}$
3		ply1dg1rt.o	$⊢ O = {eval}_{1} (R)$
4		ply1dg1rt.d	$⊢ D = \deg_{1} (R)$
5		ply1dg1rt.0	$⊢ \underset{˙}{0} = 0_{R}$
6		ply1dg1rt.r	$⊢ φ \to R \in Field$
7		ply1dg1rt.g	$⊢ φ \to G \in U$
8		ply1dg1rt.1	$⊢ φ \to D (G) = 1$
9		ply1dg1rt.x	$⊢ N = {inv}_{g} (R)$
10		ply1dg1rt.m	$⊢ \underset{˙}{\times} = /_{r} (R)$
11		ply1dg1rt.c	$⊢ C = {coe}_{1} (G)$
12		ply1dg1rt.a	$⊢ A = C (1)$
13		ply1dg1rt.b	$⊢ B = C (0)$
14		ply1dg1rt.z	$⊢ Z = N (B) \underset{˙}{\times} A$
15	6	fldcrngd	$⊢ φ \to R \in CRing$
16		eqid	$⊢ {Base}_{R} = {Base}_{R}$
17	3 1 2 15 16 7	evl1fvf	$⊢ φ \to O (G) : {Base}_{R} ⟶ {Base}_{R}$
18	17	ffnd	$⊢ φ \to O (G) Fn {Base}_{R}$
19		fniniseg2	$⊢ O (G) Fn {Base}_{R} \to {O (G)}^{-1} [\{\underset{˙}{0}\}] = \{x \in {Base}_{R} \| O (G) (x) = \underset{˙}{0}\}$
20	18 19	syl	$⊢ φ \to {O (G)}^{-1} [\{\underset{˙}{0}\}] = \{x \in {Base}_{R} \| O (G) (x) = \underset{˙}{0}\}$
21		fveqeq2	$⊢ x = Z \to (O (G) (x) = \underset{˙}{0} \leftrightarrow O (G) (Z) = \underset{˙}{0})$
22	15	crngringd	$⊢ φ \to R \in Ring$
23	15	crnggrpd	$⊢ φ \to R \in Grp$
24		0nn0	$⊢ 0 \in ℕ_{0}$
25	11 2 1 16	coe1fvalcl	$⊢ (G \in U \land 0 \in ℕ_{0}) \to C (0) \in {Base}_{R}$
26	7 24 25	sylancl	$⊢ φ \to C (0) \in {Base}_{R}$
27	13 26	eqeltrid	$⊢ φ \to B \in {Base}_{R}$
28	16 9 23 27	grpinvcld	$⊢ φ \to N (B) \in {Base}_{R}$
29	6	flddrngd	$⊢ φ \to R \in DivRing$
30		1nn0	$⊢ 1 \in ℕ_{0}$
31	11 2 1 16	coe1fvalcl	$⊢ (G \in U \land 1 \in ℕ_{0}) \to C (1) \in {Base}_{R}$
32	7 30 31	sylancl	$⊢ φ \to C (1) \in {Base}_{R}$
33	8	fveq2d	$⊢ φ \to C (D (G)) = C (1)$
34	8 30	eqeltrdi	$⊢ φ \to D (G) \in ℕ_{0}$
35		eqid	$⊢ 0_{P} = 0_{P}$
36	4 1 35 2	deg1nn0clb	$⊢ (R \in Ring \land G \in U) \to (G \neq 0_{P} \leftrightarrow D (G) \in ℕ_{0})$
37	36	biimpar	$⊢ ((R \in Ring \land G \in U) \land D (G) \in ℕ_{0}) \to G \neq 0_{P}$
38	22 7 34 37	syl21anc	$⊢ φ \to G \neq 0_{P}$
39	4 1 35 2 5 11	deg1ldg	$⊢ (R \in Ring \land G \in U \land G \neq 0_{P}) \to C (D (G)) \neq \underset{˙}{0}$
40	22 7 38 39	syl3anc	$⊢ φ \to C (D (G)) \neq \underset{˙}{0}$
41	33 40	eqnetrrd	$⊢ φ \to C (1) \neq \underset{˙}{0}$
42		eqid	$⊢ Unit (R) = Unit (R)$
43	16 42 5	drngunit	$⊢ R \in DivRing \to (C (1) \in Unit (R) \leftrightarrow (C (1) \in {Base}_{R} \land C (1) \neq \underset{˙}{0}))$
44	43	biimpar	$⊢ (R \in DivRing \land (C (1) \in {Base}_{R} \land C (1) \neq \underset{˙}{0})) \to C (1) \in Unit (R)$
45	29 32 41 44	syl12anc	$⊢ φ \to C (1) \in Unit (R)$
46	12 45	eqeltrid	$⊢ φ \to A \in Unit (R)$
47	16 42 10	dvrcl	$⊢ (R \in Ring \land N (B) \in {Base}_{R} \land A \in Unit (R)) \to N (B) \underset{˙}{\times} A \in {Base}_{R}$
48	22 28 46 47	syl3anc	$⊢ φ \to N (B) \underset{˙}{\times} A \in {Base}_{R}$
49	14 48	eqeltrid	$⊢ φ \to Z \in {Base}_{R}$
50		eqidd	$⊢ φ \to Z = Z$
51		eqeq1	$⊢ x = Z \to (x = Z \leftrightarrow Z = Z)$
52	51	imbi1d	$⊢ x = Z \to ((x = Z \to O (G) (Z) = \underset{˙}{0}) \leftrightarrow (Z = Z \to O (G) (Z) = \underset{˙}{0}))$
53		fveq2	$⊢ x = Z \to O (G) (x) = O (G) (Z)$
54	53	adantl	$⊢ ((φ \land x \in {Base}_{R}) \land x = Z) \to O (G) (x) = O (G) (Z)$
55	23	adantr	$⊢ (φ \land x \in {Base}_{R}) \to R \in Grp$
56		eqid	$⊢ \cdot_{R} = \cdot_{R}$
57	22	adantr	$⊢ (φ \land x \in {Base}_{R}) \to R \in Ring$
58	12 32	eqeltrid	$⊢ φ \to A \in {Base}_{R}$
59	58	adantr	$⊢ (φ \land x \in {Base}_{R}) \to A \in {Base}_{R}$
60		simpr	$⊢ (φ \land x \in {Base}_{R}) \to x \in {Base}_{R}$
61	16 56 57 59 60	ringcld	$⊢ (φ \land x \in {Base}_{R}) \to A \cdot_{R} x \in {Base}_{R}$
62	28	adantr	$⊢ (φ \land x \in {Base}_{R}) \to N (B) \in {Base}_{R}$
63	27	adantr	$⊢ (φ \land x \in {Base}_{R}) \to B \in {Base}_{R}$
64		eqid	$⊢ +_{R} = +_{R}$
65	16 64	grprcan	$⊢ (R \in Grp \land (A \cdot_{R} x \in {Base}_{R} \land N (B) \in {Base}_{R} \land B \in {Base}_{R})) \to ((A \cdot_{R} x) +_{R} B = N (B) +_{R} B \leftrightarrow A \cdot_{R} x = N (B))$
66	55 61 62 63 65	syl13anc	$⊢ (φ \land x \in {Base}_{R}) \to ((A \cdot_{R} x) +_{R} B = N (B) +_{R} B \leftrightarrow A \cdot_{R} x = N (B))$
67	15	adantr	$⊢ (φ \land x \in {Base}_{R}) \to R \in CRing$
68	48	adantr	$⊢ (φ \land x \in {Base}_{R}) \to N (B) \underset{˙}{\times} A \in {Base}_{R}$
69	16 56 67 68 59	crngcomd	$⊢ (φ \land x \in {Base}_{R}) \to (N (B) \underset{˙}{\times} A) \cdot_{R} A = A \cdot_{R} (N (B) \underset{˙}{\times} A)$
70	46	adantr	$⊢ (φ \land x \in {Base}_{R}) \to A \in Unit (R)$
71	16 42 10 56	dvrcan1	$⊢ (R \in Ring \land N (B) \in {Base}_{R} \land A \in Unit (R)) \to (N (B) \underset{˙}{\times} A) \cdot_{R} A = N (B)$
72	57 62 70 71	syl3anc	$⊢ (φ \land x \in {Base}_{R}) \to (N (B) \underset{˙}{\times} A) \cdot_{R} A = N (B)$
73	69 72	eqtr3d	$⊢ (φ \land x \in {Base}_{R}) \to A \cdot_{R} (N (B) \underset{˙}{\times} A) = N (B)$
74	73	eqeq2d	$⊢ (φ \land x \in {Base}_{R}) \to (A \cdot_{R} x = A \cdot_{R} (N (B) \underset{˙}{\times} A) \leftrightarrow A \cdot_{R} x = N (B))$
75		drngdomn	$⊢ R \in DivRing \to R \in Domn$
76	29 75	syl	$⊢ φ \to R \in Domn$
77		domnnzr	$⊢ R \in Domn \to R \in NzRing$
78	76 77	syl	$⊢ φ \to R \in NzRing$
79	78	adantr	$⊢ (φ \land x \in {Base}_{R}) \to R \in NzRing$
80	42 5 79 70	unitnz	$⊢ (φ \land x \in {Base}_{R}) \to A \neq \underset{˙}{0}$
81	59 80	eldifsnd	$⊢ (φ \land x \in {Base}_{R}) \to A \in ({Base}_{R} ∖ \{\underset{˙}{0}\})$
82	76	adantr	$⊢ (φ \land x \in {Base}_{R}) \to R \in Domn$
83	16 5 56 81 60 68 82	domnlcanb	$⊢ (φ \land x \in {Base}_{R}) \to (A \cdot_{R} x = A \cdot_{R} (N (B) \underset{˙}{\times} A) \leftrightarrow x = N (B) \underset{˙}{\times} A)$
84	66 74 83	3bitr2rd	$⊢ (φ \land x \in {Base}_{R}) \to (x = N (B) \underset{˙}{\times} A \leftrightarrow (A \cdot_{R} x) +_{R} B = N (B) +_{R} B)$
85	16 64 5 9 55 63	grplinvd	$⊢ (φ \land x \in {Base}_{R}) \to N (B) +_{R} B = \underset{˙}{0}$
86	85	eqeq2d	$⊢ (φ \land x \in {Base}_{R}) \to ((A \cdot_{R} x) +_{R} B = N (B) +_{R} B \leftrightarrow (A \cdot_{R} x) +_{R} B = \underset{˙}{0})$
87	84 86	bitr2d	$⊢ (φ \land x \in {Base}_{R}) \to ((A \cdot_{R} x) +_{R} B = \underset{˙}{0} \leftrightarrow x = N (B) \underset{˙}{\times} A)$
88	7	adantr	$⊢ (φ \land x \in {Base}_{R}) \to G \in U$
89	8	adantr	$⊢ (φ \land x \in {Base}_{R}) \to D (G) = 1$
90	1 3 16 2 56 64 11 4 12 13 67 88 89 60	evl1deg1	$⊢ (φ \land x \in {Base}_{R}) \to O (G) (x) = (A \cdot_{R} x) +_{R} B$
91	90	eqeq1d	$⊢ (φ \land x \in {Base}_{R}) \to (O (G) (x) = \underset{˙}{0} \leftrightarrow (A \cdot_{R} x) +_{R} B = \underset{˙}{0})$
92	14	eqeq2i	$⊢ x = Z \leftrightarrow x = N (B) \underset{˙}{\times} A$
93	92	a1i	$⊢ (φ \land x \in {Base}_{R}) \to (x = Z \leftrightarrow x = N (B) \underset{˙}{\times} A)$
94	87 91 93	3bitr4d	$⊢ (φ \land x \in {Base}_{R}) \to (O (G) (x) = \underset{˙}{0} \leftrightarrow x = Z)$
95	94	biimpar	$⊢ ((φ \land x \in {Base}_{R}) \land x = Z) \to O (G) (x) = \underset{˙}{0}$
96	54 95	eqtr3d	$⊢ ((φ \land x \in {Base}_{R}) \land x = Z) \to O (G) (Z) = \underset{˙}{0}$
97	96	ex	$⊢ (φ \land x \in {Base}_{R}) \to (x = Z \to O (G) (Z) = \underset{˙}{0})$
98	97	ralrimiva	$⊢ φ \to \forall x \in {Base}_{R} (x = Z \to O (G) (Z) = \underset{˙}{0})$
99	52 98 49	rspcdva	$⊢ φ \to (Z = Z \to O (G) (Z) = \underset{˙}{0})$
100	50 99	mpd	$⊢ φ \to O (G) (Z) = \underset{˙}{0}$
101	94	biimpa	$⊢ ((φ \land x \in {Base}_{R}) \land O (G) (x) = \underset{˙}{0}) \to x = Z$
102	21 49 100 101	rabeqsnd	$⊢ φ \to \{x \in {Base}_{R} \| O (G) (x) = \underset{˙}{0}\} = \{Z\}$
103	20 102	eqtrd	$⊢ φ \to {O (G)}^{-1} [\{\underset{˙}{0}\}] = \{Z\}$

Metamath Proof Explorer

Theorem ply1dg1rt

Proof