Theorem idomrootle 26879

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

Hypotheses

Ref	Expression
idomrootle.b	|- B = ( Base ` R )
idomrootle.e	|- .^ = (.g ` (mulGrp ` R ) )

Assertion

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

Distinct variable groups:   y, B   y, N   y, R   y, X

Allowed substitution hint:   .^ ( y)

Proof of Theorem idomrootle

Step	Hyp	Ref	Expression
1		eqid 2258	. . 3 |- (Poly1 ` R ) = (Poly1 ` R )
2		eqid 2258	. . 3 |- ( Base ` (Poly1 ` R ) ) = ( Base ` (Poly1 ` R ) )
3		eqid 2258	. . 3 |- ( deg1 ` R ) = ( deg1 ` R )
4		eqid 2258	. . 3 |- (eval1 ` R ) = (eval1 ` R )
5		eqid 2258	. . 3 |- ( 0g ` R ) = ( 0g ` R )
6		eqid 2258	. . 3 |- ( 0g ` (Poly1 ` R ) ) = ( 0g ` (Poly1 ` R ) )
7		simp1 960	. . 3 |- ( ( R e. IDomn /\ X e. B /\ N e. NN ) -> R e. IDomn )
8		isidom 16008	. . . . . . . . 9 |- ( R e. IDomn <-> ( R e. CRing /\ R e. Domn ) )
9	8	simplbi 448	. . . . . . . 8 |- ( R e. IDomn -> R e. CRing )
10	7, 9	syl 17	. . . . . . 7 |- ( ( R e. IDomn /\ X e. B /\ N e. NN ) -> R e. CRing )
11		crngrng 15314	. . . . . . 7 |- ( R e. CRing -> R e. Ring )
12	10, 11	syl 17	. . . . . 6 |- ( ( R e. IDomn /\ X e. B /\ N e. NN ) -> R e. Ring )
13	1	ply1rng 16289	. . . . . 6 |- ( R e. Ring -> (Poly1 ` R ) e. Ring )
14	12, 13	syl 17	. . . . 5 |- ( ( R e. IDomn /\ X e. B /\ N e. NN ) -> (Poly1 ` R ) e. Ring )
15		rnggrp 15309	. . . . 5 |- ( (Poly1 ` R ) e. Ring -> (Poly1 ` R ) e. Grp )
16	14, 15	syl 17	. . . 4 |- ( ( R e. IDomn /\ X e. B /\ N e. NN ) -> (Poly1 ` R ) e. Grp )
17		eqid 2258	. . . . . . 7 |- (mulGrp ` (Poly1 ` R ) ) = (mulGrp ` (Poly1 ` R ) )
18	17	rngmgp 15310	. . . . . 6 |- ( (Poly1 ` R ) e. Ring -> (mulGrp ` (Poly1 ` R ) ) e. Mnd )
19	14, 18	syl 17	. . . . 5 |- ( ( R e. IDomn /\ X e. B /\ N e. NN ) -> (mulGrp ` (Poly1 ` R ) ) e. Mnd )
20		simp3 962	. . . . 5 |- ( ( R e. IDomn /\ X e. B /\ N e. NN ) -> N e. NN )
21		eqid 2258	. . . . . . 7 |- (var1 ` R ) = (var1 ` R )
22	21, 1, 2	vr1cl 16257	. . . . . 6 |- ( R e. Ring -> (var1 ` R ) e. ( Base ` (Poly1 ` R ) ) )
23	12, 22	syl 17	. . . . 5 |- ( ( R e. IDomn /\ X e. B /\ N e. NN ) -> (var1 ` R ) e. ( Base ` (Poly1 ` R ) ) )
24	17, 2	mgpbas 15294	. . . . . 6 |- ( Base ` (Poly1 ` R ) ) = ( Base ` (mulGrp ` (Poly1 ` R ) ) )
25		eqid 2258	. . . . . 6 |- (.g ` (mulGrp ` (Poly1 ` R ) ) ) = (.g ` (mulGrp ` (Poly1 ` R ) ) )
26	24, 25	mulgnncl 14545	. . . . 5 |- ( ( (mulGrp ` (Poly1 ` R ) ) e. Mnd /\ N e. NN /\ (var1 ` R ) e. ( Base ` (Poly1 ` R ) ) ) -> ( N (.g ` (mulGrp ` (Poly1 ` R ) ) ) (var1 ` R ) ) e. ( Base ` (Poly1 ` R ) ) )
27	19, 20, 23, 26	syl3anc 1187	. . . 4 |- ( ( R e. IDomn /\ X e. B /\ N e. NN ) -> ( N (.g ` (mulGrp ` (Poly1 ` R ) ) ) (var1 ` R ) ) e. ( Base ` (Poly1 ` R ) ) )
28		eqid 2258	. . . . . . 7 |- (algSc ` (Poly1 ` R ) ) = (algSc ` (Poly1 ` R ) )
29		idomrootle.b	. . . . . . 7 |- B = ( Base ` R )
30	1, 28, 29, 2	ply1sclf 16324	. . . . . 6 |- ( R e. Ring -> (algSc ` (Poly1 ` R ) ) : B --> ( Base ` (Poly1 ` R ) ) )
31	12, 30	syl 17	. . . . 5 |- ( ( R e. IDomn /\ X e. B /\ N e. NN ) -> (algSc ` (Poly1 ` R ) ) : B --> ( Base ` (Poly1 ` R ) ) )
32		simp2 961	. . . . 5 |- ( ( R e. IDomn /\ X e. B /\ N e. NN ) -> X e. B )
33		ffvelrn 5597	. . . . 5 |- ( ( (algSc ` (Poly1 ` R ) ) : B --> ( Base ` (Poly1 ` R ) ) /\ X e. B ) -> ( (algSc ` (Poly1 ` R ) ) ` X ) e. ( Base ` (Poly1 ` R ) ) )
34	31, 32, 33	syl2anc 645	. . . 4 |- ( ( R e. IDomn /\ X e. B /\ N e. NN ) -> ( (algSc ` (Poly1 ` R ) ) ` X ) e. ( Base ` (Poly1 ` R ) ) )
35		eqid 2258	. . . . 5 |- ( -g ` (Poly1 ` R ) ) = ( -g ` (Poly1 ` R ) )
36	2, 35	grpsubcl 14509	. . . 4 |- ( ( (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 ) ) )
37	16, 27, 34, 36	syl3anc 1187	. . 3 |- ( ( 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 ) ) )
38	3, 1, 2	deg1xrcl 19431	. . . . . . . . . 10 |- ( ( (algSc ` (Poly1 ` R ) ) ` X ) e. ( Base ` (Poly1 ` R ) ) -> ( ( deg1 ` R ) ` ( (algSc ` (Poly1 ` R ) ) ` X ) ) e. RR* )
39	34, 38	syl 17	. . . . . . . . 9 |- ( ( R e. IDomn /\ X e. B /\ N e. NN ) -> ( ( deg1 ` R ) ` ( (algSc ` (Poly1 ` R ) ) ` X ) ) e. RR* )
40		0xr 8846	. . . . . . . . . 10 |- 0 e. RR*
41	40	a1i 12	. . . . . . . . 9 |- ( ( R e. IDomn /\ X e. B /\ N e. NN ) -> 0 e. RR* )
42		nnre 9721	. . . . . . . . . . 11 |- ( N e. NN -> N e. RR )
43	42	rexrd 8849	. . . . . . . . . 10 |- ( N e. NN -> N e. RR* )
44	43	3ad2ant3 983	. . . . . . . . 9 |- ( ( R e. IDomn /\ X e. B /\ N e. NN ) -> N e. RR* )
45	3, 1, 29, 28	deg1sclle 19461	. . . . . . . . . 10 |- ( ( R e. Ring /\ X e. B ) -> ( ( deg1 ` R ) ` ( (algSc ` (Poly1 ` R ) ) ` X ) ) <_ 0 )
46	12, 32, 45	syl2anc 645	. . . . . . . . 9 |- ( ( R e. IDomn /\ X e. B /\ N e. NN ) -> ( ( deg1 ` R ) ` ( (algSc ` (Poly1 ` R ) ) ` X ) ) <_ 0 )
47		nngt0 9743	. . . . . . . . . 10 |- ( N e. NN -> 0 < N )
48	47	3ad2ant3 983	. . . . . . . . 9 |- ( ( R e. IDomn /\ X e. B /\ N e. NN ) -> 0 < N )
49	39, 41, 44, 46, 48	xrlelttrd 10459	. . . . . . . 8 |- ( ( R e. IDomn /\ X e. B /\ N e. NN ) -> ( ( deg1 ` R ) ` ( (algSc ` (Poly1 ` R ) ) ` X ) ) < N )
50	8	simprbi 452	. . . . . . . . . . 11 |- ( R e. IDomn -> R e. Domn )
51		domnnzr 15999	. . . . . . . . . . 11 |- ( R e. Domn -> R e. NzRing )
52	50, 51	syl 17	. . . . . . . . . 10 |- ( R e. IDomn -> R e. NzRing )
53	7, 52	syl 17	. . . . . . . . 9 |- ( ( R e. IDomn /\ X e. B /\ N e. NN ) -> R e. NzRing )
54		nnnn0 9940	. . . . . . . . . 10 |- ( N e. NN -> N e. NN0 )
55	54	3ad2ant3 983	. . . . . . . . 9 |- ( ( R e. IDomn /\ X e. B /\ N e. NN ) -> N e. NN0 )
56	3, 1, 21, 17, 25	deg1pw 19469	. . . . . . . . 9 |- ( ( R e. NzRing /\ N e. NN0 ) -> ( ( deg1 ` R ) ` ( N (.g ` (mulGrp ` (Poly1 ` R ) ) ) (var1 ` R ) ) ) = N )
57	53, 55, 56	syl2anc 645	. . . . . . . 8 |- ( ( R e. IDomn /\ X e. B /\ N e. NN ) -> ( ( deg1 ` R ) ` ( N (.g ` (mulGrp ` (Poly1 ` R ) ) ) (var1 ` R ) ) ) = N )
58	49, 57	breqtrrd 4023	. . . . . . 7 |- ( ( R e. IDomn /\ X e. B /\ N e. NN ) -> ( ( deg1 ` R ) ` ( (algSc ` (Poly1 ` R ) ) ` X ) ) < ( ( deg1 ` R ) ` ( N (.g ` (mulGrp ` (Poly1 ` R ) ) ) (var1 ` R ) ) ) )
59	1, 3, 12, 2, 35, 27, 34, 58	deg1sub 19457	. . . . . 6 |- ( ( 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 ) ) ) )
60	59, 57	eqtrd 2290	. . . . 5 |- ( ( 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 )
61	60, 55	eqeltrd 2332	. . . 4 |- ( ( 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 )
62	3, 1, 6, 2	deg1nn0clb 19439	. . . . 5 |- ( ( 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 ) )
63	12, 37, 62	syl2anc 645	. . . 4 |- ( ( 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 ) )
64	61, 63	mpbird 225	. . 3 |- ( ( 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 ) ) )
65	1, 2, 3, 4, 5, 6, 7, 37, 64	fta1g 19516	. 2 |- ( ( 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 ) ) ) )
66		eqid 2258	. . . . . . 7 |- ( R ^s B ) = ( R ^s B )
67		eqid 2258	. . . . . . 7 |- ( Base ` ( R ^s B ) ) = ( Base ` ( R ^s B ) )
68		fvex 5472	. . . . . . . . 9 |- ( Base ` R ) e. _V
69	29, 68	eqeltri 2328	. . . . . . . 8 |- B e. _V
70	69	a1i 12	. . . . . . 7 |- ( ( R e. IDomn /\ X e. B /\ N e. NN ) -> B e. _V )
71	4, 1, 66, 29	evl1rhm 19375	. . . . . . . . . 10 |- ( R e. CRing -> (eval1 ` R ) e. ( (Poly1 ` R ) RingHom ( R ^s B ) ) )
72	10, 71	syl 17	. . . . . . . . 9 |- ( ( R e. IDomn /\ X e. B /\ N e. NN ) -> (eval1 ` R ) e. ( (Poly1 ` R ) RingHom ( R ^s B ) ) )
73	2, 67	rhmf 15467	. . . . . . . . 9 |- ( (eval1 ` R ) e. ( (Poly1 ` R ) RingHom ( R ^s B ) ) -> (eval1 ` R ) : ( Base ` (Poly1 ` R ) ) --> ( Base ` ( R ^s B ) ) )
74	72, 73	syl 17	. . . . . . . 8 |- ( ( R e. IDomn /\ X e. B /\ N e. NN ) -> (eval1 ` R ) : ( Base ` (Poly1 ` R ) ) --> ( Base ` ( R ^s B ) ) )
75		ffvelrn 5597	. . . . . . . 8 |- ( ( (eval1 ` R ) : ( Base ` (Poly1 ` R ) ) --> ( Base ` ( R ^s 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 ) ) ) e. ( Base ` ( R ^s B ) ) )
76	74, 37, 75	syl2anc 645	. . . . . . 7 |- ( ( 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	66, 29, 67, 7, 70, 76	pwselbas 13351	. . . . . 6 |- ( ( 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		ffn 5327	. . . . . 6 |- ( ( (eval1 ` R ) ` ( ( N (.g ` (mulGrp ` (Poly1 ` R ) ) ) (var1 ` R ) ) ( -g ` (Poly1 ` R ) ) ( (algSc ` (Poly1 ` R ) ) ` X ) ) ) : B --> B -> ( (eval1 ` R ) ` ( ( N (.g ` (mulGrp ` (Poly1 ` R ) ) ) (var1 ` R ) ) ( -g ` (Poly1 ` R ) ) ( (algSc ` (Poly1 ` R ) ) ` X ) ) ) Fn B )
79	77, 78	syl 17	. . . . 5 |- ( ( 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 )
80		fniniseg2 5582	. . . . 5 |- ( ( (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 ) } )
81	79, 80	syl 17	. . . 4 |- ( ( 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 ) } )
82	10	adantr 453	. . . . . . . . 9 |- ( ( ( R e. IDomn /\ X e. B /\ N e. NN ) /\ y e. B ) -> R e. CRing )
83		simpr 449	. . . . . . . . 9 |- ( ( ( R e. IDomn /\ X e. B /\ N e. NN ) /\ y e. B ) -> y e. B )
84	4, 21, 29, 1, 2, 82, 83	evl1vard 19379	. . . . . . . . . 10 |- ( ( ( R e. IDomn /\ X e. B /\ N e. NN ) /\ y e. B ) -> ( (var1 ` R ) e. ( Base ` (Poly1 ` R ) ) /\ ( ( (eval1 ` R ) ` (var1 ` R ) ) ` y ) = y ) )
85		idomrootle.e	. . . . . . . . . 10 |- .^ = (.g ` (mulGrp ` R ) )
86		simpl3 965	. . . . . . . . . . 11 |- ( ( ( R e. IDomn /\ X e. B /\ N e. NN ) /\ y e. B ) -> N e. NN )
87	86, 54	syl 17	. . . . . . . . . 10 |- ( ( ( R e. IDomn /\ X e. B /\ N e. NN ) /\ y e. B ) -> N e. NN0 )
88	4, 1, 29, 2, 82, 83, 84, 25, 85, 87	evl1expd 19384	. . . . . . . . 9 |- ( ( ( 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 ) ) )
89		simpl2 964	. . . . . . . . . 10 |- ( ( ( R e. IDomn /\ X e. B /\ N e. NN ) /\ y e. B ) -> X e. B )
90	4, 1, 29, 28, 2, 82, 89, 83	evl1scad 19377	. . . . . . . . 9 |- ( ( ( 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 ) )
91		eqid 2258	. . . . . . . . 9 |- ( -g ` R ) = ( -g ` R )
92	4, 1, 29, 2, 82, 83, 88, 90, 35, 91	evl1subd 19381	. . . . . . . 8 |- ( ( ( 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 ) ) )
93	92	simprd 451	. . . . . . 7 |- ( ( ( 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 ) )
94	93	eqeq1d 2266	. . . . . 6 |- ( ( ( 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 ) ) )
95		rnggrp 15309	. . . . . . . . 9 |- ( R e. Ring -> R e. Grp )
96	12, 95	syl 17	. . . . . . . 8 |- ( ( R e. IDomn /\ X e. B /\ N e. NN ) -> R e. Grp )
97	96	adantr 453	. . . . . . 7 |- ( ( ( R e. IDomn /\ X e. B /\ N e. NN ) /\ y e. B ) -> R e. Grp )
98		eqid 2258	. . . . . . . . . . 11 |- (mulGrp ` R ) = (mulGrp ` R )
99	98	rngmgp 15310	. . . . . . . . . 10 |- ( R e. Ring -> (mulGrp ` R ) e. Mnd )
100	12, 99	syl 17	. . . . . . . . 9 |- ( ( R e. IDomn /\ X e. B /\ N e. NN ) -> (mulGrp ` R ) e. Mnd )
101	100	adantr 453	. . . . . . . 8 |- ( ( ( R e. IDomn /\ X e. B /\ N e. NN ) /\ y e. B ) -> (mulGrp ` R ) e. Mnd )
102	98, 29	mgpbas 15294	. . . . . . . . 9 |- B = ( Base ` (mulGrp ` R ) )
103	102, 85	mulgnncl 14545	. . . . . . . 8 |- ( ( (mulGrp ` R ) e. Mnd /\ N e. NN /\ y e. B ) -> ( N .^ y ) e. B )
104	101, 86, 83, 103	syl3anc 1187	. . . . . . 7 |- ( ( ( R e. IDomn /\ X e. B /\ N e. NN ) /\ y e. B ) -> ( N .^ y ) e. B )
105	29, 5, 91	grpsubeq0 14515	. . . . . . 7 |- ( ( R e. Grp /\ ( N .^ y ) e. B /\ X e. B ) -> ( ( ( N .^ y ) ( -g ` R ) X ) = ( 0g ` R ) <-> ( N .^ y ) = X ) )
106	97, 104, 89, 105	syl3anc 1187	. . . . . 6 |- ( ( ( R e. IDomn /\ X e. B /\ N e. NN ) /\ y e. B ) -> ( ( ( N .^ y ) ( -g ` R ) X ) = ( 0g ` R ) <-> ( N .^ y ) = X ) )
107	94, 106	bitrd 246	. . . . 5 |- ( ( ( 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 2754	. . . 4 |- ( ( 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	81, 108	eqtrd 2290	. . 3 |- ( ( 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 5462	. 2 |- ( ( 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	65, 110, 60	3brtr3d 4026	1 |- ( ( R e. IDomn /\ X e. B /\ N e. NN ) -> ( # ` { y e. B | ( N .^ y ) = X } ) <_ N )

Syntax hints:   -> wi 6   <-> wb 178   /\ wa 360   /\ w3a 939   = wceq 1619   e. wcel 1621   =/= wne 2421   {crab 2522   _Vcvv 2763   {csn 3614   class class class wbr 3997   `'ccnv 4660   "cima 4664   Fn wfn 4668   -->wf 4669   ` cfv 4673  (class class class)co 5792   0cc0 8705   RR*cxr 8834   < clt 8835   <_ cle 8836   NNcn 9714   NN0cn0 9933   #chash 11304   Basecbs 13111   ^_s cpws 13310   0gc0g 13363   Mndcmnd 14324   Grpcgrp 14325   -gcsg 14328  ._gcmg 14329  mulGrpcmgp 15288   Ringcrg 15300   CRingccrg 15301   RingHom crh 15457  NzRingcnzr 15972  Domncdomn 15984  IDomncidom 15985  algSccascl 16015  var₁cv1 16214  Poly₁cpl1 16215  eval₁ce1 16217   deg₁ cdg1 19403

This theorem is referenced by:  idomodle  26880

This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-13 1625  ax-14 1626  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1927  ax-15 2106  ax-ext 2239  ax-rep 4105  ax-sep 4115  ax-nul 4123  ax-pow 4160  ax-pr 4186  ax-un 4484  ax-inf2 7310  ax-cnex 8761  ax-resscn 8762  ax-1cn 8763  ax-icn 8764  ax-addcl 8765  ax-addrcl 8766  ax-mulcl 8767  ax-mulrcl 8768  ax-mulcom 8769  ax-addass 8770  ax-mulass 8771  ax-distr 8772  ax-i2m1 8773  ax-1ne0 8774  ax-1rid 8775  ax-rnegex 8776  ax-rrecex 8777  ax-cnre 8778  ax-pre-lttri 8779  ax-pre-lttrn 8780  ax-pre-ltadd 8781  ax-pre-mulgt0 8782  ax-pre-sup 8783  ax-addf 8784  ax-mulf 8785

This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 940  df-3an 941  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1884  df-eu 2122  df-mo 2123  df-clab 2245  df-cleq 2251  df-clel 2254  df-nfc 2383  df-ne 2423  df-nel 2424  df-ral 2523  df-rex 2524  df-reu 2525  df-rmo 2526  df-rab 2527  df-v 2765  df-sbc 2967  df-csb 3057  df-dif 3130  df-un 3132  df-in 3134  df-ss 3141  df-pss 3143  df-nul 3431  df-if 3540  df-pw 3601  df-sn 3620  df-pr 3621  df-tp 3622  df-op 3623  df-uni 3802  df-int 3837  df-iun 3881  df-iin 3882  df-br 3998  df-opab 4052  df-mpt 4053  df-tr 4088  df-eprel 4277  df-id 4281  df-po 4286  df-so 4287  df-fr 4324  df-se 4325  df-we 4326  df-ord 4367  df-on 4368  df-lim 4369  df-suc 4370  df-om 4629  df-xp 4675  df-rel 4676  df-cnv 4677  df-co 4678  df-dm 4679  df-rn 4680  df-res 4681  df-ima 4682  df-fun 4683  df-fn 4684  df-f 4685  df-f1 4686  df-fo 4687  df-f1o 4688  df-fv 4689  df-isom 4690  df-ov 5795  df-oprab 5796  df-mpt2 5797  df-of 6012  df-ofr 6013  df-1st 6056  df-2nd 6057  df-tpos 6168  df-iota 6225  df-riota 6272  df-recs 6356  df-rdg 6391  df-1o 6447  df-2o 6448  df-oadd 6451  df-er 6628  df-map 6742  df-pm 6743  df-ixp 6786  df-en 6832  df-dom 6833  df-sdom 6834  df-fin 6835  df-sup 7162  df-oi 7193  df-card 7540  df-cda 7762  df-pnf 8837  df-mnf 8838  df-xr 8839  df-ltxr 8840  df-le 8841  df-sub 9007  df-neg 9008  df-n 9715  df-2 9772  df-3 9773  df-4 9774  df-5 9775  df-6 9776  df-7 9777  df-8 9778  df-9 9779  df-10 9780  df-n0 9934  df-z 9993  df-dec 10093  df-uz 10199  df-fz 10750  df-fzo 10838  df-seq 11014  df-hash 11305  df-struct 13113  df-ndx 13114  df-slot 13115  df-base 13116  df-sets 13117  df-ress 13118  df-plusg 13184  df-mulr 13185  df-starv 13186  df-sca 13187  df-vsca 13188  df-tset 13190  df-ple 13191  df-ds 13193  df-hom 13195  df-cco 13196  df-prds 13311  df-pws 13313  df-0g 13367  df-gsum 13368  df-mre 13451  df-mrc 13452  df-acs 13454  df-mnd 14330  df-mhm 14378  df-submnd 14379  df-grp 14452  df-minusg 14453  df-sbg 14454  df-mulg 14455  df-subg 14581  df-ghm 14644  df-cntz 14756  df-cmn 15054  df-abl 15055  df-mgp 15289  df-ring 15303  df-cring 15304  df-ur 15305  df-oppr 15368  df-dvdsr 15386  df-unit 15387  df-invr 15417  df-rnghom 15459  df-subrg 15506  df-lmod 15592  df-lss 15653  df-lsp 15692  df-nzr 15973  df-rlreg 15987  df-domn 15988  df-idom 15989  df-assa 16016  df-asp 16017  df-ascl 16018  df-psr 16061  df-mvr 16062  df-mpl 16063  df-evls 16064  df-evl 16065  df-opsr 16069  df-psr1 16220  df-vr1 16221  df-ply1 16222  df-evl1 16224  df-coe1 16225  df-cnfld 16341  df-mdeg 19404  df-deg1 19405  df-mon1 19479  df-uc1p 19480  df-q1p 19481  df-r1p 19482