Theorem idomrootle 26922

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 2284	. . 3 |- (Poly1 ` R ) = (Poly1 ` R )
2		eqid 2284	. . 3 |- ( Base ` (Poly1 ` R ) ) = ( Base ` (Poly1 ` R ) )
3		eqid 2284	. . 3 |- ( deg1 ` R ) = ( deg1 ` R )
4		eqid 2284	. . 3 |- (eval1 ` R ) = (eval1 ` R )
5		eqid 2284	. . 3 |- ( 0g ` R ) = ( 0g ` R )
6		eqid 2284	. . 3 |- ( 0g ` (Poly1 ` R ) ) = ( 0g ` (Poly1 ` R ) )
7		simp1 955	. . 3 |- ( ( R e. IDomn /\ X e. B /\ N e. NN ) -> R e. IDomn )
8		isidom 16041	. . . . . . . . 9 |- ( R e. IDomn <-> ( R e. CRing /\ R e. Domn ) )
9	8	simplbi 446	. . . . . . . 8 |- ( R e. IDomn -> R e. CRing )
10	7, 9	syl 15	. . . . . . 7 |- ( ( R e. IDomn /\ X e. B /\ N e. NN ) -> R e. CRing )
11		crngrng 15347	. . . . . . 7 |- ( R e. CRing -> R e. Ring )
12	10, 11	syl 15	. . . . . 6 |- ( ( R e. IDomn /\ X e. B /\ N e. NN ) -> R e. Ring )
13	1	ply1rng 16322	. . . . . 6 |- ( R e. Ring -> (Poly1 ` R ) e. Ring )
14	12, 13	syl 15	. . . . 5 |- ( ( R e. IDomn /\ X e. B /\ N e. NN ) -> (Poly1 ` R ) e. Ring )
15		rnggrp 15342	. . . . 5 |- ( (Poly1 ` R ) e. Ring -> (Poly1 ` R ) e. Grp )
16	14, 15	syl 15	. . . 4 |- ( ( R e. IDomn /\ X e. B /\ N e. NN ) -> (Poly1 ` R ) e. Grp )
17		eqid 2284	. . . . . . 7 |- (mulGrp ` (Poly1 ` R ) ) = (mulGrp ` (Poly1 ` R ) )
18	17	rngmgp 15343	. . . . . 6 |- ( (Poly1 ` R ) e. Ring -> (mulGrp ` (Poly1 ` R ) ) e. Mnd )
19	14, 18	syl 15	. . . . 5 |- ( ( R e. IDomn /\ X e. B /\ N e. NN ) -> (mulGrp ` (Poly1 ` R ) ) e. Mnd )
20		simp3 957	. . . . 5 |- ( ( R e. IDomn /\ X e. B /\ N e. NN ) -> N e. NN )
21		eqid 2284	. . . . . . 7 |- (var1 ` R ) = (var1 ` R )
22	21, 1, 2	vr1cl 16290	. . . . . 6 |- ( R e. Ring -> (var1 ` R ) e. ( Base ` (Poly1 ` R ) ) )
23	12, 22	syl 15	. . . . 5 |- ( ( R e. IDomn /\ X e. B /\ N e. NN ) -> (var1 ` R ) e. ( Base ` (Poly1 ` R ) ) )
24	17, 2	mgpbas 15327	. . . . . 6 |- ( Base ` (Poly1 ` R ) ) = ( Base ` (mulGrp ` (Poly1 ` R ) ) )
25		eqid 2284	. . . . . 6 |- (.g ` (mulGrp ` (Poly1 ` R ) ) ) = (.g ` (mulGrp ` (Poly1 ` R ) ) )
26	24, 25	mulgnncl 14578	. . . . 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 1182	. . . 4 |- ( ( R e. IDomn /\ X e. B /\ N e. NN ) -> ( N (.g ` (mulGrp ` (Poly1 ` R ) ) ) (var1 ` R ) ) e. ( Base ` (Poly1 ` R ) ) )
28		eqid 2284	. . . . . . 7 |- (algSc ` (Poly1 ` R ) ) = (algSc ` (Poly1 ` R ) )
29		idomrootle.b	. . . . . . 7 |- B = ( Base ` R )
30	1, 28, 29, 2	ply1sclf 16357	. . . . . 6 |- ( R e. Ring -> (algSc ` (Poly1 ` R ) ) : B --> ( Base ` (Poly1 ` R ) ) )
31	12, 30	syl 15	. . . . 5 |- ( ( R e. IDomn /\ X e. B /\ N e. NN ) -> (algSc ` (Poly1 ` R ) ) : B --> ( Base ` (Poly1 ` R ) ) )
32		simp2 956	. . . . 5 |- ( ( R e. IDomn /\ X e. B /\ N e. NN ) -> X e. B )
33		ffvelrn 5625	. . . . 5 |- ( ( (algSc ` (Poly1 ` R ) ) : B --> ( Base ` (Poly1 ` R ) ) /\ X e. B ) -> ( (algSc ` (Poly1 ` R ) ) ` X ) e. ( Base ` (Poly1 ` R ) ) )
34	31, 32, 33	syl2anc 642	. . . 4 |- ( ( R e. IDomn /\ X e. B /\ N e. NN ) -> ( (algSc ` (Poly1 ` R ) ) ` X ) e. ( Base ` (Poly1 ` R ) ) )
35		eqid 2284	. . . . 5 |- ( -g ` (Poly1 ` R ) ) = ( -g ` (Poly1 ` R ) )
36	2, 35	grpsubcl 14542	. . . 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 1182	. . 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 19464	. . . . . . . . . 10 |- ( ( (algSc ` (Poly1 ` R ) ) ` X ) e. ( Base ` (Poly1 ` R ) ) -> ( ( deg1 ` R ) ` ( (algSc ` (Poly1 ` R ) ) ` X ) ) e. RR* )
39	34, 38	syl 15	. . . . . . . . 9 |- ( ( R e. IDomn /\ X e. B /\ N e. NN ) -> ( ( deg1 ` R ) ` ( (algSc ` (Poly1 ` R ) ) ` X ) ) e. RR* )
40		0xr 8874	. . . . . . . . . 10 |- 0 e. RR*
41	40	a1i 10	. . . . . . . . 9 |- ( ( R e. IDomn /\ X e. B /\ N e. NN ) -> 0 e. RR* )
42		nnre 9749	. . . . . . . . . . 11 |- ( N e. NN -> N e. RR )
43	42	rexrd 8877	. . . . . . . . . 10 |- ( N e. NN -> N e. RR* )
44	43	3ad2ant3 978	. . . . . . . . 9 |- ( ( R e. IDomn /\ X e. B /\ N e. NN ) -> N e. RR* )
45	3, 1, 29, 28	deg1sclle 19494	. . . . . . . . . 10 |- ( ( R e. Ring /\ X e. B ) -> ( ( deg1 ` R ) ` ( (algSc ` (Poly1 ` R ) ) ` X ) ) <_ 0 )
46	12, 32, 45	syl2anc 642	. . . . . . . . 9 |- ( ( R e. IDomn /\ X e. B /\ N e. NN ) -> ( ( deg1 ` R ) ` ( (algSc ` (Poly1 ` R ) ) ` X ) ) <_ 0 )
47		nngt0 9771	. . . . . . . . . 10 |- ( N e. NN -> 0 < N )
48	47	3ad2ant3 978	. . . . . . . . 9 |- ( ( R e. IDomn /\ X e. B /\ N e. NN ) -> 0 < N )
49	39, 41, 44, 46, 48	xrlelttrd 10487	. . . . . . . 8 |- ( ( R e. IDomn /\ X e. B /\ N e. NN ) -> ( ( deg1 ` R ) ` ( (algSc ` (Poly1 ` R ) ) ` X ) ) < N )
50	8	simprbi 450	. . . . . . . . . . 11 |- ( R e. IDomn -> R e. Domn )
51		domnnzr 16032	. . . . . . . . . . 11 |- ( R e. Domn -> R e. NzRing )
52	50, 51	syl 15	. . . . . . . . . 10 |- ( R e. IDomn -> R e. NzRing )
53	7, 52	syl 15	. . . . . . . . 9 |- ( ( R e. IDomn /\ X e. B /\ N e. NN ) -> R e. NzRing )
54		nnnn0 9968	. . . . . . . . . 10 |- ( N e. NN -> N e. NN0 )
55	54	3ad2ant3 978	. . . . . . . . 9 |- ( ( R e. IDomn /\ X e. B /\ N e. NN ) -> N e. NN0 )
56	3, 1, 21, 17, 25	deg1pw 19502	. . . . . . . . 9 |- ( ( R e. NzRing /\ N e. NN0 ) -> ( ( deg1 ` R ) ` ( N (.g ` (mulGrp ` (Poly1 ` R ) ) ) (var1 ` R ) ) ) = N )
57	53, 55, 56	syl2anc 642	. . . . . . . 8 |- ( ( R e. IDomn /\ X e. B /\ N e. NN ) -> ( ( deg1 ` R ) ` ( N (.g ` (mulGrp ` (Poly1 ` R ) ) ) (var1 ` R ) ) ) = N )
58	49, 57	breqtrrd 4050	. . . . . . 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 19490	. . . . . 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 2316	. . . . 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 2358	. . . 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 19472	. . . . 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 642	. . . 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 223	. . 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 19549	. 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 2284	. . . . . . 7 |- ( R ^s B ) = ( R ^s B )
67		eqid 2284	. . . . . . 7 |- ( Base ` ( R ^s B ) ) = ( Base ` ( R ^s B ) )
68		fvex 5500	. . . . . . . . 9 |- ( Base ` R ) e. _V
69	29, 68	eqeltri 2354	. . . . . . . 8 |- B e. _V
70	69	a1i 10	. . . . . . 7 |- ( ( R e. IDomn /\ X e. B /\ N e. NN ) -> B e. _V )
71	4, 1, 66, 29	evl1rhm 19408	. . . . . . . . . 10 |- ( R e. CRing -> (eval1 ` R ) e. ( (Poly1 ` R ) RingHom ( R ^s B ) ) )
72	10, 71	syl 15	. . . . . . . . 9 |- ( ( R e. IDomn /\ X e. B /\ N e. NN ) -> (eval1 ` R ) e. ( (Poly1 ` R ) RingHom ( R ^s B ) ) )
73	2, 67	rhmf 15500	. . . . . . . . 9 |- ( (eval1 ` R ) e. ( (Poly1 ` R ) RingHom ( R ^s B ) ) -> (eval1 ` R ) : ( Base ` (Poly1 ` R ) ) --> ( Base ` ( R ^s B ) ) )
74	72, 73	syl 15	. . . . . . . 8 |- ( ( R e. IDomn /\ X e. B /\ N e. NN ) -> (eval1 ` R ) : ( Base ` (Poly1 ` R ) ) --> ( Base ` ( R ^s B ) ) )
75		ffvelrn 5625	. . . . . . . 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 642	. . . . . . 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 13384	. . . . . 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 5355	. . . . . 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 15	. . . . 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 5610	. . . . 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 15	. . . 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 451	. . . . . . . . 9 |- ( ( ( R e. IDomn /\ X e. B /\ N e. NN ) /\ y e. B ) -> R e. CRing )
83		simpr 447	. . . . . . . . 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 19412	. . . . . . . . . 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 960	. . . . . . . . . . 11 |- ( ( ( R e. IDomn /\ X e. B /\ N e. NN ) /\ y e. B ) -> N e. NN )
87	86, 54	syl 15	. . . . . . . . . 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 19417	. . . . . . . . 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 959	. . . . . . . . . 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 19410	. . . . . . . . 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 2284	. . . . . . . . 9 |- ( -g ` R ) = ( -g ` R )
92	4, 1, 29, 2, 82, 83, 88, 90, 35, 91	evl1subd 19414	. . . . . . . 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 449	. . . . . . 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 2292	. . . . . 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 15342	. . . . . . . . 9 |- ( R e. Ring -> R e. Grp )
96	12, 95	syl 15	. . . . . . . 8 |- ( ( R e. IDomn /\ X e. B /\ N e. NN ) -> R e. Grp )
97	96	adantr 451	. . . . . . 7 |- ( ( ( R e. IDomn /\ X e. B /\ N e. NN ) /\ y e. B ) -> R e. Grp )
98		eqid 2284	. . . . . . . . . . 11 |- (mulGrp ` R ) = (mulGrp ` R )
99	98	rngmgp 15343	. . . . . . . . . 10 |- ( R e. Ring -> (mulGrp ` R ) e. Mnd )
100	12, 99	syl 15	. . . . . . . . 9 |- ( ( R e. IDomn /\ X e. B /\ N e. NN ) -> (mulGrp ` R ) e. Mnd )
101	100	adantr 451	. . . . . . . 8 |- ( ( ( R e. IDomn /\ X e. B /\ N e. NN ) /\ y e. B ) -> (mulGrp ` R ) e. Mnd )
102	98, 29	mgpbas 15327	. . . . . . . . 9 |- B = ( Base ` (mulGrp ` R ) )
103	102, 85	mulgnncl 14578	. . . . . . . 8 |- ( ( (mulGrp ` R ) e. Mnd /\ N e. NN /\ y e. B ) -> ( N .^ y ) e. B )
104	101, 86, 83, 103	syl3anc 1182	. . . . . . 7 |- ( ( ( R e. IDomn /\ X e. B /\ N e. NN ) /\ y e. B ) -> ( N .^ y ) e. B )
105	29, 5, 91	grpsubeq0 14548	. . . . . . 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 1182	. . . . . 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 244	. . . . 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 2780	. . . 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 2316	. . 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 5490	. 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 4053	1 |- ( ( R e. IDomn /\ X e. B /\ N e. NN ) -> ( # ` { y e. B | ( N .^ y ) = X } ) <_ N )

Syntax hints:   -> wi 4   <-> wb 176   /\ wa 358   /\ w3a 934   = wceq 1623   e. wcel 1685   =/= wne 2447   {crab 2548   _Vcvv 2789   {csn 3641   class class class wbr 4024   `'ccnv 4687   "cima 4691   Fn wfn 5216   -->wf 5217   ` cfv 5221  (class class class)co 5820   0cc0 8733   RR*cxr 8862   < clt 8863   <_ cle 8864   NNcn 9742   NN0cn0 9961   #chash 11333   Basecbs 13144   ^_s cpws 13343   0gc0g 13396   Mndcmnd 14357   Grpcgrp 14358   -gcsg 14361  ._gcmg 14362  mulGrpcmgp 15321   Ringcrg 15333   CRingccrg 15334   RingHom crh 15490  NzRingcnzr 16005  Domncdomn 16017  IDomncidom 16018  algSccascl 16048  var₁cv1 16247  Poly₁cpl1 16248  eval₁ce1 16250   deg₁ cdg1 19436

This theorem is referenced by:  idomodle  26923

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1636  ax-8 1644  ax-13 1687  ax-14 1689  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1868  ax-ext 2265  ax-rep 4132  ax-sep 4142  ax-nul 4150  ax-pow 4187  ax-pr 4213  ax-un 4511  ax-inf2 7338  ax-cnex 8789  ax-resscn 8790  ax-1cn 8791  ax-icn 8792  ax-addcl 8793  ax-addrcl 8794  ax-mulcl 8795  ax-mulrcl 8796  ax-mulcom 8797  ax-addass 8798  ax-mulass 8799  ax-distr 8800  ax-i2m1 8801  ax-1ne0 8802  ax-1rid 8803  ax-rnegex 8804  ax-rrecex 8805  ax-cnre 8806  ax-pre-lttri 8807  ax-pre-lttrn 8808  ax-pre-ltadd 8809  ax-pre-mulgt0 8810  ax-pre-sup 8811  ax-addf 8812  ax-mulf 8813

This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1631  df-eu 2148  df-mo 2149  df-clab 2271  df-cleq 2277  df-clel 2280  df-nfc 2409  df-ne 2449  df-nel 2450  df-ral 2549  df-rex 2550  df-reu 2551  df-rmo 2552  df-rab 2553  df-v 2791  df-sbc 2993  df-csb 3083  df-dif 3156  df-un 3158  df-in 3160  df-ss 3167  df-pss 3169  df-nul 3457  df-if 3567  df-pw 3628  df-sn 3647  df-pr 3648  df-tp 3649  df-op 3650  df-uni 3829  df-int 3864  df-iun 3908  df-iin 3909  df-br 4025  df-opab 4079  df-mpt 4080  df-tr 4115  df-eprel 4304  df-id 4308  df-po 4313  df-so 4314  df-fr 4351  df-se 4352  df-we 4353  df-ord 4394  df-on 4395  df-lim 4396  df-suc 4397  df-om 4656  df-xp 4694  df-rel 4695  df-cnv 4696  df-co 4697  df-dm 4698  df-rn 4699  df-res 4700  df-ima 4701  df-fun 5223  df-fn 5224  df-f 5225  df-f1 5226  df-fo 5227  df-f1o 5228  df-fv 5229  df-isom 5230  df-ov 5823  df-oprab 5824  df-mpt2 5825  df-of 6040  df-ofr 6041  df-1st 6084  df-2nd 6085  df-tpos 6196  df-iota 6253  df-riota 6300  df-recs 6384  df-rdg 6419  df-1o 6475  df-2o 6476  df-oadd 6479  df-er 6656  df-map 6770  df-pm 6771  df-ixp 6814  df-en 6860  df-dom 6861  df-sdom 6862  df-fin 6863  df-sup 7190  df-oi 7221  df-card 7568  df-cda 7790  df-pnf 8865  df-mnf 8866  df-xr 8867  df-ltxr 8868  df-le 8869  df-sub 9035  df-neg 9036  df-nn 9743  df-2 9800  df-3 9801  df-4 9802  df-5 9803  df-6 9804  df-7 9805  df-8 9806  df-9 9807  df-10 9808  df-n0 9962  df-z 10021  df-dec 10121  df-uz 10227  df-fz 10779  df-fzo 10867  df-seq 11043  df-hash 11334  df-struct 13146  df-ndx 13147  df-slot 13148  df-base 13149  df-sets 13150  df-ress 13151  df-plusg 13217  df-mulr 13218  df-starv 13219  df-sca 13220  df-vsca 13221  df-tset 13223  df-ple 13224  df-ds 13226  df-hom 13228  df-cco 13229  df-prds 13344  df-pws 13346  df-0g 13400  df-gsum 13401  df-mre 13484  df-mrc 13485  df-acs 13487  df-mnd 14363  df-mhm 14411  df-submnd 14412  df-grp 14485  df-minusg 14486  df-sbg 14487  df-mulg 14488  df-subg 14614  df-ghm 14677  df-cntz 14789  df-cmn 15087  df-abl 15088  df-mgp 15322  df-rng 15336  df-cring 15337  df-ur 15338  df-oppr 15401  df-dvdsr 15419  df-unit 15420  df-invr 15450  df-rnghom 15492  df-subrg 15539  df-lmod 15625  df-lss 15686  df-lsp 15725  df-nzr 16006  df-rlreg 16020  df-domn 16021  df-idom 16022  df-assa 16049  df-asp 16050  df-ascl 16051  df-psr 16094  df-mvr 16095  df-mpl 16096  df-evls 16097  df-evl 16098  df-opsr 16102  df-psr1 16253  df-vr1 16254  df-ply1 16255  df-evl1 16257  df-coe1 16258  df-cnfld 16374  df-mdeg 19437  df-deg1 19438  df-mon1 19512  df-uc1p 19513  df-q1p 19514  df-r1p 19515