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	⊢ 𝐵 = ( Base ‘ 𝑅 )
	idomrootle.e	⊢ ↑ = ( ._g ‘ ( mulGrp ‘ 𝑅 ) )
Assertion	idomrootle	⊢ ( ( 𝑅 ∈ IDomn ∧ 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ℕ ) → ( ♯ ‘ { 𝑦 ∈ 𝐵 ∣ ( 𝑁 ↑ 𝑦 ) = 𝑋 } ) ≤ 𝑁 )

Proof

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

Metamath Proof Explorer

Theorem idomrootle

Proof