ig1pdvds

Description: The monic generator of an ideal divides all elements of the ideal. (Contributed by Stefan O'Rear, 29-Mar-2015) (Proof shortened by AV, 25-Sep-2020)

	Ref	Expression
Hypotheses	ig1pval.p	$⊢ P = {Poly}_{1} (R)$
	ig1pval.g	$⊢ G = {idlGen}_{1p} (R)$
	ig1pcl.u	$⊢ U = LIdeal (P)$
	ig1pdvds.d	$⊢ \underset{˙}{∥} = ∥_{r} (P)$
Assertion	ig1pdvds	$⊢ (R \in DivRing \land I \in U \land X \in I) \to G (I) \underset{˙}{∥} X$

Proof

Step	Hyp	Ref	Expression
1		ig1pval.p	$⊢ P = {Poly}_{1} (R)$
2		ig1pval.g	$⊢ G = {idlGen}_{1p} (R)$
3		ig1pcl.u	$⊢ U = LIdeal (P)$
4		ig1pdvds.d	$⊢ \underset{˙}{∥} = ∥_{r} (P)$
5		drngring	$⊢ R \in DivRing \to R \in Ring$
6	1	ply1ring	$⊢ R \in Ring \to P \in Ring$
7	5 6	syl	$⊢ R \in DivRing \to P \in Ring$
8	7	3ad2ant1	$⊢ (R \in DivRing \land I \in U \land X \in I) \to P \in Ring$
9		eqid	$⊢ {Base}_{P} = {Base}_{P}$
10	9 3	lidlss	$⊢ I \in U \to I \subseteq {Base}_{P}$
11	10	3ad2ant2	$⊢ (R \in DivRing \land I \in U \land X \in I) \to I \subseteq {Base}_{P}$
12	1 2 3	ig1pcl	$⊢ (R \in DivRing \land I \in U) \to G (I) \in I$
13	12	3adant3	$⊢ (R \in DivRing \land I \in U \land X \in I) \to G (I) \in I$
14	11 13	sseldd	$⊢ (R \in DivRing \land I \in U \land X \in I) \to G (I) \in {Base}_{P}$
15		eqid	$⊢ 0_{P} = 0_{P}$
16	9 4 15	dvdsr01	$⊢ (P \in Ring \land G (I) \in {Base}_{P}) \to G (I) \underset{˙}{∥} 0_{P}$
17	8 14 16	syl2anc	$⊢ (R \in DivRing \land I \in U \land X \in I) \to G (I) \underset{˙}{∥} 0_{P}$
18	17	adantr	$⊢ ((R \in DivRing \land I \in U \land X \in I) \land I = \{0_{P}\}) \to G (I) \underset{˙}{∥} 0_{P}$
19		eleq2	$⊢ I = \{0_{P}\} \to (X \in I \leftrightarrow X \in \{0_{P}\})$
20	19	biimpac	$⊢ (X \in I \land I = \{0_{P}\}) \to X \in \{0_{P}\}$
21	20	3ad2antl3	$⊢ ((R \in DivRing \land I \in U \land X \in I) \land I = \{0_{P}\}) \to X \in \{0_{P}\}$
22		elsni	$⊢ X \in \{0_{P}\} \to X = 0_{P}$
23	21 22	syl	$⊢ ((R \in DivRing \land I \in U \land X \in I) \land I = \{0_{P}\}) \to X = 0_{P}$
24	18 23	breqtrrd	$⊢ ((R \in DivRing \land I \in U \land X \in I) \land I = \{0_{P}\}) \to G (I) \underset{˙}{∥} X$
25		simpl1	$⊢ ((R \in DivRing \land I \in U \land X \in I) \land I \neq \{0_{P}\}) \to R \in DivRing$
26	25 5	syl	$⊢ ((R \in DivRing \land I \in U \land X \in I) \land I \neq \{0_{P}\}) \to R \in Ring$
27		simpl2	$⊢ ((R \in DivRing \land I \in U \land X \in I) \land I \neq \{0_{P}\}) \to I \in U$
28	27 10	syl	$⊢ ((R \in DivRing \land I \in U \land X \in I) \land I \neq \{0_{P}\}) \to I \subseteq {Base}_{P}$
29		simpl3	$⊢ ((R \in DivRing \land I \in U \land X \in I) \land I \neq \{0_{P}\}) \to X \in I$
30	28 29	sseldd	$⊢ ((R \in DivRing \land I \in U \land X \in I) \land I \neq \{0_{P}\}) \to X \in {Base}_{P}$
31		simpr	$⊢ ((R \in DivRing \land I \in U \land X \in I) \land I \neq \{0_{P}\}) \to I \neq \{0_{P}\}$
32		eqid	$⊢ \deg_{1} (R) = \deg_{1} (R)$
33		eqid	$⊢ {Monic}_{1p} (R) = {Monic}_{1p} (R)$
34	1 2 15 3 32 33	ig1pval3	$⊢ (R \in DivRing \land I \in U \land I \neq \{0_{P}\}) \to (G (I) \in I \land G (I) \in {Monic}_{1p} (R) \land \deg_{1} (R) (G (I)) = inf (\deg_{1} (R) [I ∖ \{0_{P}\}] ℝ <))$
35	25 27 31 34	syl3anc	$⊢ ((R \in DivRing \land I \in U \land X \in I) \land I \neq \{0_{P}\}) \to (G (I) \in I \land G (I) \in {Monic}_{1p} (R) \land \deg_{1} (R) (G (I)) = inf (\deg_{1} (R) [I ∖ \{0_{P}\}] ℝ <))$
36	35	simp2d	$⊢ ((R \in DivRing \land I \in U \land X \in I) \land I \neq \{0_{P}\}) \to G (I) \in {Monic}_{1p} (R)$
37		eqid	$⊢ {Unic}_{1p} (R) = {Unic}_{1p} (R)$
38	37 33	mon1puc1p	$⊢ (R \in Ring \land G (I) \in {Monic}_{1p} (R)) \to G (I) \in {Unic}_{1p} (R)$
39	26 36 38	syl2anc	$⊢ ((R \in DivRing \land I \in U \land X \in I) \land I \neq \{0_{P}\}) \to G (I) \in {Unic}_{1p} (R)$
40		eqid	$⊢ {rem}_{1p} (R) = {rem}_{1p} (R)$
41	40 1 9 37 32	r1pdeglt	$⊢ (R \in Ring \land X \in {Base}_{P} \land G (I) \in {Unic}_{1p} (R)) \to \deg_{1} (R) (X {rem}_{1p} (R) G (I)) < \deg_{1} (R) (G (I))$
42	26 30 39 41	syl3anc	$⊢ ((R \in DivRing \land I \in U \land X \in I) \land I \neq \{0_{P}\}) \to \deg_{1} (R) (X {rem}_{1p} (R) G (I)) < \deg_{1} (R) (G (I))$
43	35	simp3d	$⊢ ((R \in DivRing \land I \in U \land X \in I) \land I \neq \{0_{P}\}) \to \deg_{1} (R) (G (I)) = inf (\deg_{1} (R) [I ∖ \{0_{P}\}] ℝ <)$
44	42 43	breqtrd	$⊢ ((R \in DivRing \land I \in U \land X \in I) \land I \neq \{0_{P}\}) \to \deg_{1} (R) (X {rem}_{1p} (R) G (I)) < inf (\deg_{1} (R) [I ∖ \{0_{P}\}] ℝ <)$
45	32 1 9	deg1xrf	$⊢ \deg_{1} (R) : {Base}_{P} ⟶ ℝ^{*}$
46	35	simp1d	$⊢ ((R \in DivRing \land I \in U \land X \in I) \land I \neq \{0_{P}\}) \to G (I) \in I$
47	28 46	sseldd	$⊢ ((R \in DivRing \land I \in U \land X \in I) \land I \neq \{0_{P}\}) \to G (I) \in {Base}_{P}$
48		eqid	$⊢ {quot}_{1p} (R) = {quot}_{1p} (R)$
49		eqid	$⊢ \cdot_{P} = \cdot_{P}$
50		eqid	$⊢ -_{P} = -_{P}$
51	40 1 9 48 49 50	r1pval	$⊢ (X \in {Base}_{P} \land G (I) \in {Base}_{P}) \to X {rem}_{1p} (R) G (I) = X -_{P} ((X {quot}_{1p} (R) G (I)) \cdot_{P} G (I))$
52	30 47 51	syl2anc	$⊢ ((R \in DivRing \land I \in U \land X \in I) \land I \neq \{0_{P}\}) \to X {rem}_{1p} (R) G (I) = X -_{P} ((X {quot}_{1p} (R) G (I)) \cdot_{P} G (I))$
53	26 6	syl	$⊢ ((R \in DivRing \land I \in U \land X \in I) \land I \neq \{0_{P}\}) \to P \in Ring$
54	48 1 9 37	q1pcl	$⊢ (R \in Ring \land X \in {Base}_{P} \land G (I) \in {Unic}_{1p} (R)) \to X {quot}_{1p} (R) G (I) \in {Base}_{P}$
55	26 30 39 54	syl3anc	$⊢ ((R \in DivRing \land I \in U \land X \in I) \land I \neq \{0_{P}\}) \to X {quot}_{1p} (R) G (I) \in {Base}_{P}$
56	3 9 49	lidlmcl	$⊢ ((P \in Ring \land I \in U) \land (X {quot}_{1p} (R) G (I) \in {Base}_{P} \land G (I) \in I)) \to (X {quot}_{1p} (R) G (I)) \cdot_{P} G (I) \in I$
57	53 27 55 46 56	syl22anc	$⊢ ((R \in DivRing \land I \in U \land X \in I) \land I \neq \{0_{P}\}) \to (X {quot}_{1p} (R) G (I)) \cdot_{P} G (I) \in I$
58	3 50	lidlsubcl	$⊢ ((P \in Ring \land I \in U) \land (X \in I \land (X {quot}_{1p} (R) G (I)) \cdot_{P} G (I) \in I)) \to X -_{P} ((X {quot}_{1p} (R) G (I)) \cdot_{P} G (I)) \in I$
59	53 27 29 57 58	syl22anc	$⊢ ((R \in DivRing \land I \in U \land X \in I) \land I \neq \{0_{P}\}) \to X -_{P} ((X {quot}_{1p} (R) G (I)) \cdot_{P} G (I)) \in I$
60	52 59	eqeltrd	$⊢ ((R \in DivRing \land I \in U \land X \in I) \land I \neq \{0_{P}\}) \to X {rem}_{1p} (R) G (I) \in I$
61	28 60	sseldd	$⊢ ((R \in DivRing \land I \in U \land X \in I) \land I \neq \{0_{P}\}) \to X {rem}_{1p} (R) G (I) \in {Base}_{P}$
62		ffvelcdm	$⊢ (\deg_{1} (R) : {Base}_{P} ⟶ ℝ^{} \land X {rem}_{1p} (R) G (I) \in {Base}_{P}) \to \deg_{1} (R) (X {rem}_{1p} (R) G (I)) \in ℝ^{}$
63	45 61 62	sylancr	$⊢ ((R \in DivRing \land I \in U \land X \in I) \land I \neq \{0_{P}\}) \to \deg_{1} (R) (X {rem}_{1p} (R) G (I)) \in ℝ^{*}$
64	28	ssdifd	$⊢ ((R \in DivRing \land I \in U \land X \in I) \land I \neq \{0_{P}\}) \to I ∖ \{0_{P}\} \subseteq {Base}_{P} ∖ \{0_{P}\}$
65		imass2	$⊢ I ∖ \{0_{P}\} \subseteq {Base}_{P} ∖ \{0_{P}\} \to \deg_{1} (R) [I ∖ \{0_{P}\}] \subseteq \deg_{1} (R) [{Base}_{P} ∖ \{0_{P}\}]$
66	64 65	syl	$⊢ ((R \in DivRing \land I \in U \land X \in I) \land I \neq \{0_{P}\}) \to \deg_{1} (R) [I ∖ \{0_{P}\}] \subseteq \deg_{1} (R) [{Base}_{P} ∖ \{0_{P}\}]$
67	32 1 15 9	deg1n0ima	$⊢ R \in Ring \to \deg_{1} (R) [{Base}_{P} ∖ \{0_{P}\}] \subseteq ℕ_{0}$
68	26 67	syl	$⊢ ((R \in DivRing \land I \in U \land X \in I) \land I \neq \{0_{P}\}) \to \deg_{1} (R) [{Base}_{P} ∖ \{0_{P}\}] \subseteq ℕ_{0}$
69		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
70	68 69	sseqtrdi	$⊢ ((R \in DivRing \land I \in U \land X \in I) \land I \neq \{0_{P}\}) \to \deg_{1} (R) [{Base}_{P} ∖ \{0_{P}\}] \subseteq ℤ_{\geq 0}$
71	66 70	sstrd	$⊢ ((R \in DivRing \land I \in U \land X \in I) \land I \neq \{0_{P}\}) \to \deg_{1} (R) [I ∖ \{0_{P}\}] \subseteq ℤ_{\geq 0}$
72		uzssz	$⊢ ℤ_{\geq 0} \subseteq ℤ$
73		zssre	$⊢ ℤ \subseteq ℝ$
74		ressxr	$⊢ ℝ \subseteq ℝ^{*}$
75	73 74	sstri	$⊢ ℤ \subseteq ℝ^{*}$
76	72 75	sstri	$⊢ ℤ_{\geq 0} \subseteq ℝ^{*}$
77	71 76	sstrdi	$⊢ ((R \in DivRing \land I \in U \land X \in I) \land I \neq \{0_{P}\}) \to \deg_{1} (R) [I ∖ \{0_{P}\}] \subseteq ℝ^{*}$
78	3 15	lidl0cl	$⊢ (P \in Ring \land I \in U) \to 0_{P} \in I$
79	53 27 78	syl2anc	$⊢ ((R \in DivRing \land I \in U \land X \in I) \land I \neq \{0_{P}\}) \to 0_{P} \in I$
80	79	snssd	$⊢ ((R \in DivRing \land I \in U \land X \in I) \land I \neq \{0_{P}\}) \to \{0_{P}\} \subseteq I$
81	31	necomd	$⊢ ((R \in DivRing \land I \in U \land X \in I) \land I \neq \{0_{P}\}) \to \{0_{P}\} \neq I$
82		pssdifn0	$⊢ (\{0_{P}\} \subseteq I \land \{0_{P}\} \neq I) \to I ∖ \{0_{P}\} \neq \emptyset$
83	80 81 82	syl2anc	$⊢ ((R \in DivRing \land I \in U \land X \in I) \land I \neq \{0_{P}\}) \to I ∖ \{0_{P}\} \neq \emptyset$
84		ffn	$⊢ \deg_{1} (R) : {Base}_{P} ⟶ ℝ^{*} \to \deg_{1} (R) Fn {Base}_{P}$
85	45 84	ax-mp	$⊢ \deg_{1} (R) Fn {Base}_{P}$
86	28	ssdifssd	$⊢ ((R \in DivRing \land I \in U \land X \in I) \land I \neq \{0_{P}\}) \to I ∖ \{0_{P}\} \subseteq {Base}_{P}$
87		fnimaeq0	$⊢ (\deg_{1} (R) Fn {Base}_{P} \land I ∖ \{0_{P}\} \subseteq {Base}_{P}) \to (\deg_{1} (R) [I ∖ \{0_{P}\}] = \emptyset \leftrightarrow I ∖ \{0_{P}\} = \emptyset)$
88	85 86 87	sylancr	$⊢ ((R \in DivRing \land I \in U \land X \in I) \land I \neq \{0_{P}\}) \to (\deg_{1} (R) [I ∖ \{0_{P}\}] = \emptyset \leftrightarrow I ∖ \{0_{P}\} = \emptyset)$
89	88	necon3bid	$⊢ ((R \in DivRing \land I \in U \land X \in I) \land I \neq \{0_{P}\}) \to (\deg_{1} (R) [I ∖ \{0_{P}\}] \neq \emptyset \leftrightarrow I ∖ \{0_{P}\} \neq \emptyset)$
90	83 89	mpbird	$⊢ ((R \in DivRing \land I \in U \land X \in I) \land I \neq \{0_{P}\}) \to \deg_{1} (R) [I ∖ \{0_{P}\}] \neq \emptyset$
91		infssuzcl	$⊢ (\deg_{1} (R) [I ∖ \{0_{P}\}] \subseteq ℤ_{\geq 0} \land \deg_{1} (R) [I ∖ \{0_{P}\}] \neq \emptyset) \to inf (\deg_{1} (R) [I ∖ \{0_{P}\}] ℝ <) \in \deg_{1} (R) [I ∖ \{0_{P}\}]$
92	71 90 91	syl2anc	$⊢ ((R \in DivRing \land I \in U \land X \in I) \land I \neq \{0_{P}\}) \to inf (\deg_{1} (R) [I ∖ \{0_{P}\}] ℝ <) \in \deg_{1} (R) [I ∖ \{0_{P}\}]$
93	77 92	sseldd	$⊢ ((R \in DivRing \land I \in U \land X \in I) \land I \neq \{0_{P}\}) \to inf (\deg_{1} (R) [I ∖ \{0_{P}\}] ℝ <) \in ℝ^{*}$
94		xrltnle	$⊢ (\deg_{1} (R) (X {rem}_{1p} (R) G (I)) \in ℝ^{} \land inf (\deg_{1} (R) [I ∖ \{0_{P}\}] ℝ <) \in ℝ^{}) \to (\deg_{1} (R) (X {rem}_{1p} (R) G (I)) < inf (\deg_{1} (R) [I ∖ \{0_{P}\}] ℝ <) \leftrightarrow \neg inf (\deg_{1} (R) [I ∖ \{0_{P}\}] ℝ <) \leq \deg_{1} (R) (X {rem}_{1p} (R) G (I)))$
95	63 93 94	syl2anc	$⊢ ((R \in DivRing \land I \in U \land X \in I) \land I \neq \{0_{P}\}) \to (\deg_{1} (R) (X {rem}_{1p} (R) G (I)) < inf (\deg_{1} (R) [I ∖ \{0_{P}\}] ℝ <) \leftrightarrow \neg inf (\deg_{1} (R) [I ∖ \{0_{P}\}] ℝ <) \leq \deg_{1} (R) (X {rem}_{1p} (R) G (I)))$
96	44 95	mpbid	$⊢ ((R \in DivRing \land I \in U \land X \in I) \land I \neq \{0_{P}\}) \to \neg inf (\deg_{1} (R) [I ∖ \{0_{P}\}] ℝ <) \leq \deg_{1} (R) (X {rem}_{1p} (R) G (I))$
97	71	adantr	$⊢ (((R \in DivRing \land I \in U \land X \in I) \land I \neq \{0_{P}\}) \land X {rem}_{1p} (R) G (I) \neq 0_{P}) \to \deg_{1} (R) [I ∖ \{0_{P}\}] \subseteq ℤ_{\geq 0}$
98	60	adantr	$⊢ (((R \in DivRing \land I \in U \land X \in I) \land I \neq \{0_{P}\}) \land X {rem}_{1p} (R) G (I) \neq 0_{P}) \to X {rem}_{1p} (R) G (I) \in I$
99		simpr	$⊢ (((R \in DivRing \land I \in U \land X \in I) \land I \neq \{0_{P}\}) \land X {rem}_{1p} (R) G (I) \neq 0_{P}) \to X {rem}_{1p} (R) G (I) \neq 0_{P}$
100		eldifsn	$⊢ X {rem}_{1p} (R) G (I) \in (I ∖ \{0_{P}\}) \leftrightarrow (X {rem}_{1p} (R) G (I) \in I \land X {rem}_{1p} (R) G (I) \neq 0_{P})$
101	98 99 100	sylanbrc	$⊢ (((R \in DivRing \land I \in U \land X \in I) \land I \neq \{0_{P}\}) \land X {rem}_{1p} (R) G (I) \neq 0_{P}) \to X {rem}_{1p} (R) G (I) \in (I ∖ \{0_{P}\})$
102		fnfvima	$⊢ (\deg_{1} (R) Fn {Base}_{P} \land I ∖ \{0_{P}\} \subseteq {Base}_{P} \land X {rem}_{1p} (R) G (I) \in (I ∖ \{0_{P}\})) \to \deg_{1} (R) (X {rem}_{1p} (R) G (I)) \in \deg_{1} (R) [I ∖ \{0_{P}\}]$
103	85 86 101 102	mp3an2ani	$⊢ (((R \in DivRing \land I \in U \land X \in I) \land I \neq \{0_{P}\}) \land X {rem}_{1p} (R) G (I) \neq 0_{P}) \to \deg_{1} (R) (X {rem}_{1p} (R) G (I)) \in \deg_{1} (R) [I ∖ \{0_{P}\}]$
104		infssuzle	$⊢ (\deg_{1} (R) [I ∖ \{0_{P}\}] \subseteq ℤ_{\geq 0} \land \deg_{1} (R) (X {rem}_{1p} (R) G (I)) \in \deg_{1} (R) [I ∖ \{0_{P}\}]) \to inf (\deg_{1} (R) [I ∖ \{0_{P}\}] ℝ <) \leq \deg_{1} (R) (X {rem}_{1p} (R) G (I))$
105	97 103 104	syl2anc	$⊢ (((R \in DivRing \land I \in U \land X \in I) \land I \neq \{0_{P}\}) \land X {rem}_{1p} (R) G (I) \neq 0_{P}) \to inf (\deg_{1} (R) [I ∖ \{0_{P}\}] ℝ <) \leq \deg_{1} (R) (X {rem}_{1p} (R) G (I))$
106	105	ex	$⊢ ((R \in DivRing \land I \in U \land X \in I) \land I \neq \{0_{P}\}) \to (X {rem}_{1p} (R) G (I) \neq 0_{P} \to inf (\deg_{1} (R) [I ∖ \{0_{P}\}] ℝ <) \leq \deg_{1} (R) (X {rem}_{1p} (R) G (I)))$
107	106	necon1bd	$⊢ ((R \in DivRing \land I \in U \land X \in I) \land I \neq \{0_{P}\}) \to (\neg inf (\deg_{1} (R) [I ∖ \{0_{P}\}] ℝ <) \leq \deg_{1} (R) (X {rem}_{1p} (R) G (I)) \to X {rem}_{1p} (R) G (I) = 0_{P})$
108	96 107	mpd	$⊢ ((R \in DivRing \land I \in U \land X \in I) \land I \neq \{0_{P}\}) \to X {rem}_{1p} (R) G (I) = 0_{P}$
109	1 4 9 37 15 40	dvdsr1p	$⊢ (R \in Ring \land X \in {Base}_{P} \land G (I) \in {Unic}_{1p} (R)) \to (G (I) \underset{˙}{∥} X \leftrightarrow X {rem}_{1p} (R) G (I) = 0_{P})$
110	26 30 39 109	syl3anc	$⊢ ((R \in DivRing \land I \in U \land X \in I) \land I \neq \{0_{P}\}) \to (G (I) \underset{˙}{∥} X \leftrightarrow X {rem}_{1p} (R) G (I) = 0_{P})$
111	108 110	mpbird	$⊢ ((R \in DivRing \land I \in U \land X \in I) \land I \neq \{0_{P}\}) \to G (I) \underset{˙}{∥} X$
112	24 111	pm2.61dane	$⊢ (R \in DivRing \land I \in U \land X \in I) \to G (I) \underset{˙}{∥} X$

Metamath Proof Explorer

Theorem ig1pdvds

Proof