Metamath Proof Explorer

Theorem 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 = ( Poly1 ` R )
ply1dg1rt.u 
|- U = ( Base ` P )
ply1dg1rt.o 
|- O = ( eval1 ` R )
ply1dg1rt.d 
|- D = ( deg1 ` R )
ply1dg1rt.0 
|- .0. = ( 0g ` R )
ply1dg1rt.r 
|- ( ph -> R e. Field )
ply1dg1rt.g 
|- ( ph -> G e. U )
ply1dg1rt.1 
|- ( ph -> ( D ` G ) = 1 )
ply1dg1rt.x 
|- N = ( invg ` R )
ply1dg1rt.m 
|- ./ = ( /r ` R )
ply1dg1rt.c 
|- C = ( coe1 ` G )
ply1dg1rt.a 
|- A = ( C ` 1 )
ply1dg1rt.b 
|- B = ( C ` 0 )
ply1dg1rt.z 
|- Z = ( ( N ` B ) ./ A )
Assertion ply1dg1rt 
|- ( ph -> ( `' ( O ` G ) " { .0. } ) = { Z } )

Proof

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