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	$⊢ \underset{˙}{\times} = \cdot_{{mulGrp}_{R}}$
Assertion	idomrootle	$⊢ (R \in IDomn \land X \in B \land N \in ℕ) \to \|\{y \in B \| N \underset{˙}{\times} y = X\}\| \leq N$

Proof

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

Metamath Proof Explorer

Theorem idomrootle

Proof