Theorem idomrootle 26843

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 2256	. . 3 |- (Poly1 ` R ) = (Poly1 ` R )
2		eqid 2256	. . 3 |- ( Base ` (Poly1 ` R ) ) = ( Base ` (Poly1 ` R ) )
3		eqid 2256	. . 3 |- ( deg1 ` R ) = ( deg1 ` R )
4		eqid 2256	. . 3 |- (eval1 ` R ) = (eval1 ` R )
5		eqid 2256	. . 3 |- ( 0g ` R ) = ( 0g ` R )
6		eqid 2256	. . 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 15972	. . . . . . . . 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 15278	. . . . . . 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 16253	. . . . . 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 15273	. . . . 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 2256	. . . . . . 7 |- (mulGrp ` (Poly1 ` R ) ) = (mulGrp ` (Poly1 ` R ) )
18	17	rngmgp 15274	. . . . . 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 2256	. . . . . . 7 |- (var1 ` R ) = (var1 ` R )
22	21, 1, 2	vr1cl 16221	. . . . . 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 15258	. . . . . 6 |- ( Base ` (Poly1 ` R ) ) = ( Base ` (mulGrp ` (Poly1 ` R ) ) )
25		eqid 2256	. . . . . 6 |- (.g ` (mulGrp ` (Poly1 ` R ) ) ) = (.g ` (mulGrp ` (Poly1 ` R ) ) )
26	24, 25	mulgnncl 14509	. . . . 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 2256	. . . . . . 7 |- (algSc ` (Poly1 ` R ) ) = (algSc ` (Poly1 ` R ) )
29		idomrootle.b	. . . . . . 7 |- B = ( Base ` R )
30	1, 28, 29, 2	ply1sclf 16288	. . . . . 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 5562	. . . . 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 2256	. . . . 5 |- ( -g ` (Poly1 ` R ) ) = ( -g ` (Poly1 ` R ) )
36	2, 35	grpsubcl 14473	. . . 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 19395	. . . . . . . . . 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 8811	. . . . . . . . . 10 |- 0 e. RR*
41	40	a1i 12	. . . . . . . . 9 |- ( ( R e. IDomn /\ X e. B /\ N e. NN ) -> 0 e. RR* )
42		nnre 9686	. . . . . . . . . . 11 |- ( N e. NN -> N e. RR )
43	42	rexrd 8814	. . . . . . . . . 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 19425	. . . . . . . . . 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 9708	. . . . . . . . . 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 10423	. . . . . . . 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 15963	. . . . . . . . . . 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 9904	. . . . . . . . . 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 19433	. . . . . . . . 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 3989	. . . . . . 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 19421	. . . . . 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 2288	. . . . 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 2330	. . . 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 19403	. . . . 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 19480	. 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 2256	. . . . . . 7 |- ( R ^s B ) = ( R ^s B )
67		eqid 2256	. . . . . . 7 |- ( Base ` ( R ^s B ) ) = ( Base ` ( R ^s B ) )
68		fvex 5437	. . . . . . . . 9 |- ( Base ` R ) e. _V
69	29, 68	eqeltri 2326	. . . . . . . 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 19339	. . . . . . . . . 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 15431	. . . . . . . . 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 5562	. . . . . . . 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 13315	. . . . . 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 5292	. . . . . 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 5547	. . . . 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 19343	. . . . . . . . . 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 19348	. . . . . . . . 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 19341	. . . . . . . . 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 2256	. . . . . . . . 9 |- ( -g ` R ) = ( -g ` R )
92	4, 1, 29, 2, 82, 83, 88, 90, 35, 91	evl1subd 19345	. . . . . . . 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 2264	. . . . . 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 15273	. . . . . . . . 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 2256	. . . . . . . . . . 11 |- (mulGrp ` R ) = (mulGrp ` R )
99	98	rngmgp 15274	. . . . . . . . . 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 15258	. . . . . . . . 9 |- B = ( Base ` (mulGrp ` R ) )
103	102, 85	mulgnncl 14509	. . . . . . . 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 14479	. . . . . . 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 2731	. . . 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 2288	. . 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 5427	. 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 3992	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 2419   {crab 2519   _Vcvv 2740   {csn 3581   class class class wbr 3963   `'ccnv 4625   "cima 4629   Fn wfn 4633   -->wf 4634   ` cfv 4638  (class class class)co 5757   0cc0 8670   RR*cxr 8799   < clt 8800   <_ cle 8801   NNcn 9679   NN0cn0 9897   #chash 11268   Basecbs 13075   ^_s cpws 13274   0gc0g 13327   Mndcmnd 14288   Grpcgrp 14289   -gcsg 14292  ._gcmg 14293  mulGrpcmgp 15252   Ringcrg 15264   CRingccrg 15265   RingHom crh 15421  NzRingcnzr 15936  Domncdomn 15948  IDomncidom 15949  algSccascl 15979  var₁cv1 16178  Poly₁cpl1 16179  eval₁ce1 16181   deg₁ cdg1 19367

This theorem is referenced by:  idomodle  26844

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 2105  ax-ext 2237  ax-rep 4071  ax-sep 4081  ax-nul 4089  ax-pow 4126  ax-pr 4152  ax-un 4449  ax-inf2 7275  ax-cnex 8726  ax-resscn 8727  ax-1cn 8728  ax-icn 8729  ax-addcl 8730  ax-addrcl 8731  ax-mulcl 8732  ax-mulrcl 8733  ax-mulcom 8734  ax-addass 8735  ax-mulass 8736  ax-distr 8737  ax-i2m1 8738  ax-1ne0 8739  ax-1rid 8740  ax-rnegex 8741  ax-rrecex 8742  ax-cnre 8743  ax-pre-lttri 8744  ax-pre-lttrn 8745  ax-pre-ltadd 8746  ax-pre-mulgt0 8747  ax-pre-sup 8748  ax-addf 8749  ax-mulf 8750

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 2121  df-mo 2122  df-clab 2243  df-cleq 2249  df-clel 2252  df-nfc 2381  df-ne 2421  df-nel 2422  df-ral 2520  df-rex 2521  df-reu 2522  df-rab 2523  df-v 2742  df-sbc 2936  df-csb 3024  df-dif 3097  df-un 3099  df-in 3101  df-ss 3108  df-pss 3110  df-nul 3398  df-if 3507  df-pw 3568  df-sn 3587  df-pr 3588  df-tp 3589  df-op 3590  df-uni 3769  df-int 3804  df-iun 3848  df-iin 3849  df-br 3964  df-opab 4018  df-mpt 4019  df-tr 4054  df-eprel 4242  df-id 4246  df-po 4251  df-so 4252  df-fr 4289  df-se 4290  df-we 4291  df-ord 4332  df-on 4333  df-lim 4334  df-suc 4335  df-om 4594  df-xp 4640  df-rel 4641  df-cnv 4642  df-co 4643  df-dm 4644  df-rn 4645  df-res 4646  df-ima 4647  df-fun 4648  df-fn 4649  df-f 4650  df-f1 4651  df-fo 4652  df-f1o 4653  df-fv 4654  df-isom 4655  df-ov 5760  df-oprab 5761  df-mpt2 5762  df-of 5977  df-ofr 5978  df-1st 6021  df-2nd 6022  df-tpos 6133  df-iota 6190  df-riota 6237  df-recs 6321  df-rdg 6356  df-1o 6412  df-2o 6413  df-oadd 6416  df-er 6593  df-map 6707  df-pm 6708  df-ixp 6751  df-en 6797  df-dom 6798  df-sdom 6799  df-fin 6800  df-sup 7127  df-oi 7158  df-card 7505  df-cda 7727  df-pnf 8802  df-mnf 8803  df-xr 8804  df-ltxr 8805  df-le 8806  df-sub 8972  df-neg 8973  df-n 9680  df-2 9737  df-3 9738  df-4 9739  df-5 9740  df-6 9741  df-7 9742  df-8 9743  df-9 9744  df-10 9745  df-n0 9898  df-z 9957  df-dec 10057  df-uz 10163  df-fz 10714  df-fzo 10802  df-seq 10978  df-hash 11269  df-struct 13077  df-ndx 13078  df-slot 13079  df-base 13080  df-sets 13081  df-ress 13082  df-plusg 13148  df-mulr 13149  df-starv 13150  df-sca 13151  df-vsca 13152  df-tset 13154  df-ple 13155  df-ds 13157  df-hom 13159  df-cco 13160  df-prds 13275  df-pws 13277  df-0g 13331  df-gsum 13332  df-mre 13415  df-mrc 13416  df-acs 13418  df-mnd 14294  df-mhm 14342  df-submnd 14343  df-grp 14416  df-minusg 14417  df-sbg 14418  df-mulg 14419  df-subg 14545  df-ghm 14608  df-cntz 14720  df-cmn 15018  df-abl 15019  df-mgp 15253  df-ring 15267  df-cring 15268  df-ur 15269  df-oppr 15332  df-dvdsr 15350  df-unit 15351  df-invr 15381  df-rnghom 15423  df-subrg 15470  df-lmod 15556  df-lss 15617  df-lsp 15656  df-nzr 15937  df-rlreg 15951  df-domn 15952  df-idom 15953  df-assa 15980  df-asp 15981  df-ascl 15982  df-psr 16025  df-mvr 16026  df-mpl 16027  df-evls 16028  df-evl 16029  df-opsr 16033  df-psr1 16184  df-vr1 16185  df-ply1 16186  df-evl1 16188  df-coe1 16189  df-cnfld 16305  df-mdeg 19368  df-deg1 19369  df-mon1 19443  df-uc1p 19444  df-q1p 19445  df-r1p 19446