Metamath Proof Explorer

Theorem idomrootle

Description: No element of an integral domain can have more than N N -th roots. (Contributed by Stefan O'Rear, 11-Sep-2015)

Ref Expression
Hypotheses idomrootle.b 
|- B = ( Base ` R )
idomrootle.e 
|- .^ = ( .g ` ( mulGrp ` R ) )
Assertion idomrootle 
|- ( ( R e. IDomn /\ X e. B /\ N e. NN ) -> ( # ` { y e. B | ( N .^ y ) = X } ) <_ N )

Proof

Step Hyp Ref Expression
1 idomrootle.b 
 |-  B = ( Base ` R )
2 idomrootle.e 
 |-  .^ = ( .g ` ( mulGrp ` R ) )
3 eqid 
 |-  ( Poly1 ` R ) = ( Poly1 ` R )
4 eqid 
 |-  ( Base ` ( Poly1 ` R ) ) = ( Base ` ( Poly1 ` R ) )
5 eqid 
 |-  ( deg1 ` R ) = ( deg1 ` R )
6 eqid 
 |-  ( eval1 ` R ) = ( eval1 ` R )
7 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
8 eqid 
 |-  ( 0g ` ( Poly1 ` R ) ) = ( 0g ` ( Poly1 ` R ) )
9 simp1 
 |-  ( ( R e. IDomn /\ X e. B /\ N e. NN ) -> R e. IDomn )
10 isidom 
 |-  ( R e. IDomn <-> ( R e. CRing /\ R e. Domn ) )
11 10 simplbi 
 |-  ( R e. IDomn -> R e. CRing )
12 9 11 syl 
 |-  ( ( R e. IDomn /\ X e. B /\ N e. NN ) -> R e. CRing )
13 crngring 
 |-  ( R e. CRing -> R e. Ring )
14 12 13 syl 
 |-  ( ( R e. IDomn /\ X e. B /\ N e. NN ) -> R e. Ring )
15 3 ply1ring 
 |-  ( R e. Ring -> ( Poly1 ` R ) e. Ring )
16 14 15 syl 
 |-  ( ( R e. IDomn /\ X e. B /\ N e. NN ) -> ( Poly1 ` R ) e. Ring )
17 ringgrp 
 |-  ( ( Poly1 ` R ) e. Ring -> ( Poly1 ` R ) e. Grp )
18 16 17 syl 
 |-  ( ( R e. IDomn /\ X e. B /\ N e. NN ) -> ( Poly1 ` R ) e. Grp )
19 eqid 
 |-  ( mulGrp ` ( Poly1 ` R ) ) = ( mulGrp ` ( Poly1 ` R ) )
20 19 ringmgp 
 |-  ( ( Poly1 ` R ) e. Ring -> ( mulGrp ` ( Poly1 ` R ) ) e. Mnd )
21 16 20 syl 
 |-  ( ( R e. IDomn /\ X e. B /\ N e. NN ) -> ( mulGrp ` ( Poly1 ` R ) ) e. Mnd )
22 mndmgm 
 |-  ( ( mulGrp ` ( Poly1 ` R ) ) e. Mnd -> ( mulGrp ` ( Poly1 ` R ) ) e. Mgm )
23 21 22 syl 
 |-  ( ( R e. IDomn /\ X e. B /\ N e. NN ) -> ( mulGrp ` ( Poly1 ` R ) ) e. Mgm )
24 simp3 
 |-  ( ( R e. IDomn /\ X e. B /\ N e. NN ) -> N e. NN )
25 eqid 
 |-  ( var1 ` R ) = ( var1 ` R )
26 25 3 4 vr1cl 
 |-  ( R e. Ring -> ( var1 ` R ) e. ( Base ` ( Poly1 ` R ) ) )
27 14 26 syl 
 |-  ( ( R e. IDomn /\ X e. B /\ N e. NN ) -> ( var1 ` R ) e. ( Base ` ( Poly1 ` R ) ) )
28 19 4 mgpbas 
 |-  ( Base ` ( Poly1 ` R ) ) = ( Base ` ( mulGrp ` ( Poly1 ` R ) ) )
29 eqid 
 |-  ( .g ` ( mulGrp ` ( Poly1 ` R ) ) ) = ( .g ` ( mulGrp ` ( Poly1 ` R ) ) )
30 28 29 mulgnncl 
 |-  ( ( ( mulGrp ` ( Poly1 ` R ) ) e. Mgm /\ N e. NN /\ ( var1 ` R ) e. ( Base ` ( Poly1 ` R ) ) ) -> ( N ( .g ` ( mulGrp ` ( Poly1 ` R ) ) ) ( var1 ` R ) ) e. ( Base ` ( Poly1 ` R ) ) )
31 23 24 27 30 syl3anc 
 |-  ( ( R e. IDomn /\ X e. B /\ N e. NN ) -> ( N ( .g ` ( mulGrp ` ( Poly1 ` R ) ) ) ( var1 ` R ) ) e. ( Base ` ( Poly1 ` R ) ) )
32 eqid 
 |-  ( algSc ` ( Poly1 ` R ) ) = ( algSc ` ( Poly1 ` R ) )
33 3 32 1 4 ply1sclf 
 |-  ( R e. Ring -> ( algSc ` ( Poly1 ` R ) ) : B --> ( Base ` ( Poly1 ` R ) ) )
34 14 33 syl 
 |-  ( ( R e. IDomn /\ X e. B /\ N e. NN ) -> ( algSc ` ( Poly1 ` R ) ) : B --> ( Base ` ( Poly1 ` R ) ) )
35 simp2 
 |-  ( ( R e. IDomn /\ X e. B /\ N e. NN ) -> X e. B )
36 34 35 ffvelcdmd 
 |-  ( ( R e. IDomn /\ X e. B /\ N e. NN ) -> ( ( algSc ` ( Poly1 ` R ) ) ` X ) e. ( Base ` ( Poly1 ` R ) ) )
37 eqid 
 |-  ( -g ` ( Poly1 ` R ) ) = ( -g ` ( Poly1 ` R ) )
38 4 37 grpsubcl 
 |-  ( ( ( Poly1 ` R ) e. Grp /\ ( N ( .g ` ( mulGrp ` ( Poly1 ` R ) ) ) ( var1 ` R ) ) e. ( Base ` ( Poly1 ` R ) ) /\ ( ( algSc ` ( Poly1 ` R ) ) ` X ) e. ( Base ` ( Poly1 ` R ) ) ) -> ( ( N ( .g ` ( mulGrp ` ( Poly1 ` R ) ) ) ( var1 ` R ) ) ( -g ` ( Poly1 ` R ) ) ( ( algSc ` ( Poly1 ` R ) ) ` X ) ) e. ( Base ` ( Poly1 ` R ) ) )
39 18 31 36 38 syl3anc 
 |-  ( ( R e. IDomn /\ X e. B /\ N e. NN ) -> ( ( N ( .g ` ( mulGrp ` ( Poly1 ` R ) ) ) ( var1 ` R ) ) ( -g ` ( Poly1 ` R ) ) ( ( algSc ` ( Poly1 ` R ) ) ` X ) ) e. ( Base ` ( Poly1 ` R ) ) )
40 5 3 4 deg1xrcl 
 |-  ( ( ( algSc ` ( Poly1 ` R ) ) ` X ) e. ( Base ` ( Poly1 ` R ) ) -> ( ( deg1 ` R ) ` ( ( algSc ` ( Poly1 ` R ) ) ` X ) ) e. RR* )
41 36 40 syl 
 |-  ( ( R e. IDomn /\ X e. B /\ N e. NN ) -> ( ( deg1 ` R ) ` ( ( algSc ` ( Poly1 ` R ) ) ` X ) ) e. RR* )
42 0xr 
 |-  0 e. RR*
43 42 a1i 
 |-  ( ( R e. IDomn /\ X e. B /\ N e. NN ) -> 0 e. RR* )
44 nnre 
 |-  ( N e. NN -> N e. RR )
45 44 rexrd 
 |-  ( N e. NN -> N e. RR* )
46 45 3ad2ant3 
 |-  ( ( R e. IDomn /\ X e. B /\ N e. NN ) -> N e. RR* )
47 5 3 1 32 deg1sclle 
 |-  ( ( R e. Ring /\ X e. B ) -> ( ( deg1 ` R ) ` ( ( algSc ` ( Poly1 ` R ) ) ` X ) ) <_ 0 )
48 14 35 47 syl2anc 
 |-  ( ( R e. IDomn /\ X e. B /\ N e. NN ) -> ( ( deg1 ` R ) ` ( ( algSc ` ( Poly1 ` R ) ) ` X ) ) <_ 0 )
49 nngt0 
 |-  ( N e. NN -> 0 < N )
50 49 3ad2ant3 
 |-  ( ( R e. IDomn /\ X e. B /\ N e. NN ) -> 0 < N )
51 41 43 46 48 50 xrlelttrd 
 |-  ( ( R e. IDomn /\ X e. B /\ N e. NN ) -> ( ( deg1 ` R ) ` ( ( algSc ` ( Poly1 ` R ) ) ` X ) ) < N )
52 10 simprbi 
 |-  ( R e. IDomn -> R e. Domn )
53 domnnzr 
 |-  ( R e. Domn -> R e. NzRing )
54 52 53 syl 
 |-  ( R e. IDomn -> R e. NzRing )
55 9 54 syl 
 |-  ( ( R e. IDomn /\ X e. B /\ N e. NN ) -> R e. NzRing )
56 nnnn0 
 |-  ( N e. NN -> N e. NN0 )
57 56 3ad2ant3 
 |-  ( ( R e. IDomn /\ X e. B /\ N e. NN ) -> N e. NN0 )
58 5 3 25 19 29 deg1pw 
 |-  ( ( R e. NzRing /\ N e. NN0 ) -> ( ( deg1 ` R ) ` ( N ( .g ` ( mulGrp ` ( Poly1 ` R ) ) ) ( var1 ` R ) ) ) = N )
59 55 57 58 syl2anc 
 |-  ( ( R e. IDomn /\ X e. B /\ N e. NN ) -> ( ( deg1 ` R ) ` ( N ( .g ` ( mulGrp ` ( Poly1 ` R ) ) ) ( var1 ` R ) ) ) = N )
60 51 59 breqtrrd 
 |-  ( ( R e. IDomn /\ X e. B /\ N e. NN ) -> ( ( deg1 ` R ) ` ( ( algSc ` ( Poly1 ` R ) ) ` X ) ) < ( ( deg1 ` R ) ` ( N ( .g ` ( mulGrp ` ( Poly1 ` R ) ) ) ( var1 ` R ) ) ) )
61 3 5 14 4 37 31 36 60 deg1sub 
 |-  ( ( R e. IDomn /\ X e. B /\ N e. NN ) -> ( ( deg1 ` R ) ` ( ( N ( .g ` ( mulGrp ` ( Poly1 ` R ) ) ) ( var1 ` R ) ) ( -g ` ( Poly1 ` R ) ) ( ( algSc ` ( Poly1 ` R ) ) ` X ) ) ) = ( ( deg1 ` R ) ` ( N ( .g ` ( mulGrp ` ( Poly1 ` R ) ) ) ( var1 ` R ) ) ) )
62 61 59 eqtrd 
 |-  ( ( R e. IDomn /\ X e. B /\ N e. NN ) -> ( ( deg1 ` R ) ` ( ( N ( .g ` ( mulGrp ` ( Poly1 ` R ) ) ) ( var1 ` R ) ) ( -g ` ( Poly1 ` R ) ) ( ( algSc ` ( Poly1 ` R ) ) ` X ) ) ) = N )
63 62 57 eqeltrd 
 |-  ( ( R e. IDomn /\ X e. B /\ N e. NN ) -> ( ( deg1 ` R ) ` ( ( N ( .g ` ( mulGrp ` ( Poly1 ` R ) ) ) ( var1 ` R ) ) ( -g ` ( Poly1 ` R ) ) ( ( algSc ` ( Poly1 ` R ) ) ` X ) ) ) e. NN0 )
64 5 3 8 4 deg1nn0clb 
 |-  ( ( R e. Ring /\ ( ( N ( .g ` ( mulGrp ` ( Poly1 ` R ) ) ) ( var1 ` R ) ) ( -g ` ( Poly1 ` R ) ) ( ( algSc ` ( Poly1 ` R ) ) ` X ) ) e. ( Base ` ( Poly1 ` R ) ) ) -> ( ( ( N ( .g ` ( mulGrp ` ( Poly1 ` R ) ) ) ( var1 ` R ) ) ( -g ` ( Poly1 ` R ) ) ( ( algSc ` ( Poly1 ` R ) ) ` X ) ) =/= ( 0g ` ( Poly1 ` R ) ) <-> ( ( deg1 ` R ) ` ( ( N ( .g ` ( mulGrp ` ( Poly1 ` R ) ) ) ( var1 ` R ) ) ( -g ` ( Poly1 ` R ) ) ( ( algSc ` ( Poly1 ` R ) ) ` X ) ) ) e. NN0 ) )
65 14 39 64 syl2anc 
 |-  ( ( R e. IDomn /\ X e. B /\ N e. NN ) -> ( ( ( N ( .g ` ( mulGrp ` ( Poly1 ` R ) ) ) ( var1 ` R ) ) ( -g ` ( Poly1 ` R ) ) ( ( algSc ` ( Poly1 ` R ) ) ` X ) ) =/= ( 0g ` ( Poly1 ` R ) ) <-> ( ( deg1 ` R ) ` ( ( N ( .g ` ( mulGrp ` ( Poly1 ` R ) ) ) ( var1 ` R ) ) ( -g ` ( Poly1 ` R ) ) ( ( algSc ` ( Poly1 ` R ) ) ` X ) ) ) e. NN0 ) )
66 63 65 mpbird 
 |-  ( ( R e. IDomn /\ X e. B /\ N e. NN ) -> ( ( N ( .g ` ( mulGrp ` ( Poly1 ` R ) ) ) ( var1 ` R ) ) ( -g ` ( Poly1 ` R ) ) ( ( algSc ` ( Poly1 ` R ) ) ` X ) ) =/= ( 0g ` ( Poly1 ` R ) ) )
67 3 4 5 6 7 8 9 39 66 fta1g 
 |-  ( ( R e. IDomn /\ X e. B /\ N e. NN ) -> ( # ` ( `' ( ( eval1 ` R ) ` ( ( N ( .g ` ( mulGrp ` ( Poly1 ` R ) ) ) ( var1 ` R ) ) ( -g ` ( Poly1 ` R ) ) ( ( algSc ` ( Poly1 ` R ) ) ` X ) ) ) " { ( 0g ` R ) } ) ) <_ ( ( deg1 ` R ) ` ( ( N ( .g ` ( mulGrp ` ( Poly1 ` R ) ) ) ( var1 ` R ) ) ( -g ` ( Poly1 ` R ) ) ( ( algSc ` ( Poly1 ` R ) ) ` X ) ) ) )
68 eqid 
 |-  ( R ^s B ) = ( R ^s B )
69 eqid 
 |-  ( Base ` ( R ^s B ) ) = ( Base ` ( R ^s B ) )
70 1 fvexi 
 |-  B e. _V
71 70 a1i 
 |-  ( ( R e. IDomn /\ X e. B /\ N e. NN ) -> B e. _V )
72 6 3 68 1 evl1rhm 
 |-  ( R e. CRing -> ( eval1 ` R ) e. ( ( Poly1 ` R ) RingHom ( R ^s B ) ) )
73 12 72 syl 
 |-  ( ( R e. IDomn /\ X e. B /\ N e. NN ) -> ( eval1 ` R ) e. ( ( Poly1 ` R ) RingHom ( R ^s B ) ) )
74 4 69 rhmf 
 |-  ( ( eval1 ` R ) e. ( ( Poly1 ` R ) RingHom ( R ^s B ) ) -> ( eval1 ` R ) : ( Base ` ( Poly1 ` R ) ) --> ( Base ` ( R ^s B ) ) )
75 73 74 syl 
 |-  ( ( R e. IDomn /\ X e. B /\ N e. NN ) -> ( eval1 ` R ) : ( Base ` ( Poly1 ` R ) ) --> ( Base ` ( R ^s B ) ) )
76 75 39 ffvelcdmd 
 |-  ( ( R e. IDomn /\ X e. B /\ N e. NN ) -> ( ( eval1 ` R ) ` ( ( N ( .g ` ( mulGrp ` ( Poly1 ` R ) ) ) ( var1 ` R ) ) ( -g ` ( Poly1 ` R ) ) ( ( algSc ` ( Poly1 ` R ) ) ` X ) ) ) e. ( Base ` ( R ^s B ) ) )
77 68 1 69 9 71 76 pwselbas 
 |-  ( ( R e. IDomn /\ X e. B /\ N e. NN ) -> ( ( eval1 ` R ) ` ( ( N ( .g ` ( mulGrp ` ( Poly1 ` R ) ) ) ( var1 ` R ) ) ( -g ` ( Poly1 ` R ) ) ( ( algSc ` ( Poly1 ` R ) ) ` X ) ) ) : B --> B )
78 77 ffnd 
 |-  ( ( R e. IDomn /\ X e. B /\ N e. NN ) -> ( ( eval1 ` R ) ` ( ( N ( .g ` ( mulGrp ` ( Poly1 ` R ) ) ) ( var1 ` R ) ) ( -g ` ( Poly1 ` R ) ) ( ( algSc ` ( Poly1 ` R ) ) ` X ) ) ) Fn B )
79 fniniseg2 
 |-  ( ( ( eval1 ` R ) ` ( ( N ( .g ` ( mulGrp ` ( Poly1 ` R ) ) ) ( var1 ` R ) ) ( -g ` ( Poly1 ` R ) ) ( ( algSc ` ( Poly1 ` R ) ) ` X ) ) ) Fn B -> ( `' ( ( eval1 ` R ) ` ( ( N ( .g ` ( mulGrp ` ( Poly1 ` R ) ) ) ( var1 ` R ) ) ( -g ` ( Poly1 ` R ) ) ( ( algSc ` ( Poly1 ` R ) ) ` X ) ) ) " { ( 0g ` R ) } ) = { y e. B | ( ( ( eval1 ` R ) ` ( ( N ( .g ` ( mulGrp ` ( Poly1 ` R ) ) ) ( var1 ` R ) ) ( -g ` ( Poly1 ` R ) ) ( ( algSc ` ( Poly1 ` R ) ) ` X ) ) ) ` y ) = ( 0g ` R ) } )
80 78 79 syl 
 |-  ( ( R e. IDomn /\ X e. B /\ N e. NN ) -> ( `' ( ( eval1 ` R ) ` ( ( N ( .g ` ( mulGrp ` ( Poly1 ` R ) ) ) ( var1 ` R ) ) ( -g ` ( Poly1 ` R ) ) ( ( algSc ` ( Poly1 ` R ) ) ` X ) ) ) " { ( 0g ` R ) } ) = { y e. B | ( ( ( eval1 ` R ) ` ( ( N ( .g ` ( mulGrp ` ( Poly1 ` R ) ) ) ( var1 ` R ) ) ( -g ` ( Poly1 ` R ) ) ( ( algSc ` ( Poly1 ` R ) ) ` X ) ) ) ` y ) = ( 0g ` R ) } )
81 12 adantr 
 |-  ( ( ( R e. IDomn /\ X e. B /\ N e. NN ) /\ y e. B ) -> R e. CRing )
82 simpr 
 |-  ( ( ( R e. IDomn /\ X e. B /\ N e. NN ) /\ y e. B ) -> y e. B )
83 6 25 1 3 4 81 82 evl1vard 
 |-  ( ( ( R e. IDomn /\ X e. B /\ N e. NN ) /\ y e. B ) -> ( ( var1 ` R ) e. ( Base ` ( Poly1 ` R ) ) /\ ( ( ( eval1 ` R ) ` ( var1 ` R ) ) ` y ) = y ) )
84 simpl3 
 |-  ( ( ( R e. IDomn /\ X e. B /\ N e. NN ) /\ y e. B ) -> N e. NN )
85 84 56 syl 
 |-  ( ( ( R e. IDomn /\ X e. B /\ N e. NN ) /\ y e. B ) -> N e. NN0 )
86 6 3 1 4 81 82 83 29 2 85 evl1expd 
 |-  ( ( ( R e. IDomn /\ X e. B /\ N e. NN ) /\ y e. B ) -> ( ( N ( .g ` ( mulGrp ` ( Poly1 ` R ) ) ) ( var1 ` R ) ) e. ( Base ` ( Poly1 ` R ) ) /\ ( ( ( eval1 ` R ) ` ( N ( .g ` ( mulGrp ` ( Poly1 ` R ) ) ) ( var1 ` R ) ) ) ` y ) = ( N .^ y ) ) )
87 simpl2 
 |-  ( ( ( R e. IDomn /\ X e. B /\ N e. NN ) /\ y e. B ) -> X e. B )
88 6 3 1 32 4 81 87 82 evl1scad 
 |-  ( ( ( R e. IDomn /\ X e. B /\ N e. NN ) /\ y e. B ) -> ( ( ( algSc ` ( Poly1 ` R ) ) ` X ) e. ( Base ` ( Poly1 ` R ) ) /\ ( ( ( eval1 ` R ) ` ( ( algSc ` ( Poly1 ` R ) ) ` X ) ) ` y ) = X ) )
89 eqid 
 |-  ( -g ` R ) = ( -g ` R )
90 6 3 1 4 81 82 86 88 37 89 evl1subd 
 |-  ( ( ( R e. IDomn /\ X e. B /\ N e. NN ) /\ y e. B ) -> ( ( ( N ( .g ` ( mulGrp ` ( Poly1 ` R ) ) ) ( var1 ` R ) ) ( -g ` ( Poly1 ` R ) ) ( ( algSc ` ( Poly1 ` R ) ) ` X ) ) e. ( Base ` ( Poly1 ` R ) ) /\ ( ( ( eval1 ` R ) ` ( ( N ( .g ` ( mulGrp ` ( Poly1 ` R ) ) ) ( var1 ` R ) ) ( -g ` ( Poly1 ` R ) ) ( ( algSc ` ( Poly1 ` R ) ) ` X ) ) ) ` y ) = ( ( N .^ y ) ( -g ` R ) X ) ) )
91 90 simprd 
 |-  ( ( ( R e. IDomn /\ X e. B /\ N e. NN ) /\ y e. B ) -> ( ( ( eval1 ` R ) ` ( ( N ( .g ` ( mulGrp ` ( Poly1 ` R ) ) ) ( var1 ` R ) ) ( -g ` ( Poly1 ` R ) ) ( ( algSc ` ( Poly1 ` R ) ) ` X ) ) ) ` y ) = ( ( N .^ y ) ( -g ` R ) X ) )
92 91 eqeq1d 
 |-  ( ( ( R e. IDomn /\ X e. B /\ N e. NN ) /\ y e. B ) -> ( ( ( ( eval1 ` R ) ` ( ( N ( .g ` ( mulGrp ` ( Poly1 ` R ) ) ) ( var1 ` R ) ) ( -g ` ( Poly1 ` R ) ) ( ( algSc ` ( Poly1 ` R ) ) ` X ) ) ) ` y ) = ( 0g ` R ) <-> ( ( N .^ y ) ( -g ` R ) X ) = ( 0g ` R ) ) )
93 ringgrp 
 |-  ( R e. Ring -> R e. Grp )
94 14 93 syl 
 |-  ( ( R e. IDomn /\ X e. B /\ N e. NN ) -> R e. Grp )
95 94 adantr 
 |-  ( ( ( R e. IDomn /\ X e. B /\ N e. NN ) /\ y e. B ) -> R e. Grp )
96 eqid 
 |-  ( mulGrp ` R ) = ( mulGrp ` R )
97 96 ringmgp 
 |-  ( R e. Ring -> ( mulGrp ` R ) e. Mnd )
98 14 97 syl 
 |-  ( ( R e. IDomn /\ X e. B /\ N e. NN ) -> ( mulGrp ` R ) e. Mnd )
99 98 adantr 
 |-  ( ( ( R e. IDomn /\ X e. B /\ N e. NN ) /\ y e. B ) -> ( mulGrp ` R ) e. Mnd )
100 mndmgm 
 |-  ( ( mulGrp ` R ) e. Mnd -> ( mulGrp ` R ) e. Mgm )
101 99 100 syl 
 |-  ( ( ( R e. IDomn /\ X e. B /\ N e. NN ) /\ y e. B ) -> ( mulGrp ` R ) e. Mgm )
102 96 1 mgpbas 
 |-  B = ( Base ` ( mulGrp ` R ) )
103 102 2 mulgnncl 
 |-  ( ( ( mulGrp ` R ) e. Mgm /\ N e. NN /\ y e. B ) -> ( N .^ y ) e. B )
104 101 84 82 103 syl3anc 
 |-  ( ( ( R e. IDomn /\ X e. B /\ N e. NN ) /\ y e. B ) -> ( N .^ y ) e. B )
105 1 7 89 grpsubeq0 
 |-  ( ( R e. Grp /\ ( N .^ y ) e. B /\ X e. B ) -> ( ( ( N .^ y ) ( -g ` R ) X ) = ( 0g ` R ) <-> ( N .^ y ) = X ) )
106 95 104 87 105 syl3anc 
 |-  ( ( ( R e. IDomn /\ X e. B /\ N e. NN ) /\ y e. B ) -> ( ( ( N .^ y ) ( -g ` R ) X ) = ( 0g ` R ) <-> ( N .^ y ) = X ) )
107 92 106 bitrd 
 |-  ( ( ( R e. IDomn /\ X e. B /\ N e. NN ) /\ y e. B ) -> ( ( ( ( eval1 ` R ) ` ( ( N ( .g ` ( mulGrp ` ( Poly1 ` R ) ) ) ( var1 ` R ) ) ( -g ` ( Poly1 ` R ) ) ( ( algSc ` ( Poly1 ` R ) ) ` X ) ) ) ` y ) = ( 0g ` R ) <-> ( N .^ y ) = X ) )
108 107 rabbidva 
 |-  ( ( R e. IDomn /\ X e. B /\ N e. NN ) -> { y e. B | ( ( ( eval1 ` R ) ` ( ( N ( .g ` ( mulGrp ` ( Poly1 ` R ) ) ) ( var1 ` R ) ) ( -g ` ( Poly1 ` R ) ) ( ( algSc ` ( Poly1 ` R ) ) ` X ) ) ) ` y ) = ( 0g ` R ) } = { y e. B | ( N .^ y ) = X } )
109 80 108 eqtrd 
 |-  ( ( R e. IDomn /\ X e. B /\ N e. NN ) -> ( `' ( ( eval1 ` R ) ` ( ( N ( .g ` ( mulGrp ` ( Poly1 ` R ) ) ) ( var1 ` R ) ) ( -g ` ( Poly1 ` R ) ) ( ( algSc ` ( Poly1 ` R ) ) ` X ) ) ) " { ( 0g ` R ) } ) = { y e. B | ( N .^ y ) = X } )
110 109 fveq2d 
 |-  ( ( R e. IDomn /\ X e. B /\ N e. NN ) -> ( # ` ( `' ( ( eval1 ` R ) ` ( ( N ( .g ` ( mulGrp ` ( Poly1 ` R ) ) ) ( var1 ` R ) ) ( -g ` ( Poly1 ` R ) ) ( ( algSc ` ( Poly1 ` R ) ) ` X ) ) ) " { ( 0g ` R ) } ) ) = ( # ` { y e. B | ( N .^ y ) = X } ) )
111 67 110 62 3brtr3d 
 |-  ( ( R e. IDomn /\ X e. B /\ N e. NN ) -> ( # ` { y e. B | ( N .^ y ) = X } ) <_ N )