ig1peu

Description: There is a unique monic polynomial of minimal degree in any nonzero ideal. (Contributed by Stefan O'Rear, 29-Mar-2015) (Revised by AV, 25-Sep-2020)

	Ref	Expression
Hypotheses	ig1peu.p	$⊢ P = {Poly}_{1} (R)$
	ig1peu.u	$⊢ U = LIdeal (P)$
	ig1peu.z	$⊢ \underset{˙}{0} = 0_{P}$
	ig1peu.m	$⊢ M = {Monic}_{1p} (R)$
	ig1peu.d	$⊢ D = \deg_{1} (R)$
Assertion	ig1peu	$⊢ (R \in DivRing \land I \in U \land I \neq \{\underset{˙}{0}\}) \to \exists! g \in (I \cap M) D (g) = inf (D [I ∖ \{\underset{˙}{0}\}] ℝ <)$

Proof

Step	Hyp	Ref	Expression
1		ig1peu.p	$⊢ P = {Poly}_{1} (R)$
2		ig1peu.u	$⊢ U = LIdeal (P)$
3		ig1peu.z	$⊢ \underset{˙}{0} = 0_{P}$
4		ig1peu.m	$⊢ M = {Monic}_{1p} (R)$
5		ig1peu.d	$⊢ D = \deg_{1} (R)$
6		eqid	$⊢ {Base}_{P} = {Base}_{P}$
7	6 2	lidlss	$⊢ I \in U \to I \subseteq {Base}_{P}$
8	7	3ad2ant2	$⊢ (R \in DivRing \land I \in U \land I \neq \{\underset{˙}{0}\}) \to I \subseteq {Base}_{P}$
9	8	ssdifd	$⊢ (R \in DivRing \land I \in U \land I \neq \{\underset{˙}{0}\}) \to I ∖ \{\underset{˙}{0}\} \subseteq {Base}_{P} ∖ \{\underset{˙}{0}\}$
10		imass2	$⊢ I ∖ \{\underset{˙}{0}\} \subseteq {Base}_{P} ∖ \{\underset{˙}{0}\} \to D [I ∖ \{\underset{˙}{0}\}] \subseteq D [{Base}_{P} ∖ \{\underset{˙}{0}\}]$
11	9 10	syl	$⊢ (R \in DivRing \land I \in U \land I \neq \{\underset{˙}{0}\}) \to D [I ∖ \{\underset{˙}{0}\}] \subseteq D [{Base}_{P} ∖ \{\underset{˙}{0}\}]$
12		drngring	$⊢ R \in DivRing \to R \in Ring$
13	12	3ad2ant1	$⊢ (R \in DivRing \land I \in U \land I \neq \{\underset{˙}{0}\}) \to R \in Ring$
14	5 1 3 6	deg1n0ima	$⊢ R \in Ring \to D [{Base}_{P} ∖ \{\underset{˙}{0}\}] \subseteq ℕ_{0}$
15	13 14	syl	$⊢ (R \in DivRing \land I \in U \land I \neq \{\underset{˙}{0}\}) \to D [{Base}_{P} ∖ \{\underset{˙}{0}\}] \subseteq ℕ_{0}$
16	11 15	sstrd	$⊢ (R \in DivRing \land I \in U \land I \neq \{\underset{˙}{0}\}) \to D [I ∖ \{\underset{˙}{0}\}] \subseteq ℕ_{0}$
17		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
18	16 17	sseqtrdi	$⊢ (R \in DivRing \land I \in U \land I \neq \{\underset{˙}{0}\}) \to D [I ∖ \{\underset{˙}{0}\}] \subseteq ℤ_{\geq 0}$
19	1	ply1ring	$⊢ R \in Ring \to P \in Ring$
20	13 19	syl	$⊢ (R \in DivRing \land I \in U \land I \neq \{\underset{˙}{0}\}) \to P \in Ring$
21		simp2	$⊢ (R \in DivRing \land I \in U \land I \neq \{\underset{˙}{0}\}) \to I \in U$
22	2 3	lidl0cl	$⊢ (P \in Ring \land I \in U) \to \underset{˙}{0} \in I$
23	20 21 22	syl2anc	$⊢ (R \in DivRing \land I \in U \land I \neq \{\underset{˙}{0}\}) \to \underset{˙}{0} \in I$
24	23	snssd	$⊢ (R \in DivRing \land I \in U \land I \neq \{\underset{˙}{0}\}) \to \{\underset{˙}{0}\} \subseteq I$
25		simp3	$⊢ (R \in DivRing \land I \in U \land I \neq \{\underset{˙}{0}\}) \to I \neq \{\underset{˙}{0}\}$
26	25	necomd	$⊢ (R \in DivRing \land I \in U \land I \neq \{\underset{˙}{0}\}) \to \{\underset{˙}{0}\} \neq I$
27		pssdifn0	$⊢ (\{\underset{˙}{0}\} \subseteq I \land \{\underset{˙}{0}\} \neq I) \to I ∖ \{\underset{˙}{0}\} \neq \emptyset$
28	24 26 27	syl2anc	$⊢ (R \in DivRing \land I \in U \land I \neq \{\underset{˙}{0}\}) \to I ∖ \{\underset{˙}{0}\} \neq \emptyset$
29	5 1 6	deg1xrf	$⊢ D : {Base}_{P} ⟶ ℝ^{*}$
30		ffn	$⊢ D : {Base}_{P} ⟶ ℝ^{*} \to D Fn {Base}_{P}$
31	29 30	ax-mp	$⊢ D Fn {Base}_{P}$
32	31	a1i	$⊢ (R \in DivRing \land I \in U \land I \neq \{\underset{˙}{0}\}) \to D Fn {Base}_{P}$
33	8	ssdifssd	$⊢ (R \in DivRing \land I \in U \land I \neq \{\underset{˙}{0}\}) \to I ∖ \{\underset{˙}{0}\} \subseteq {Base}_{P}$
34		fnimaeq0	$⊢ (D Fn {Base}_{P} \land I ∖ \{\underset{˙}{0}\} \subseteq {Base}_{P}) \to (D [I ∖ \{\underset{˙}{0}\}] = \emptyset \leftrightarrow I ∖ \{\underset{˙}{0}\} = \emptyset)$
35	32 33 34	syl2anc	$⊢ (R \in DivRing \land I \in U \land I \neq \{\underset{˙}{0}\}) \to (D [I ∖ \{\underset{˙}{0}\}] = \emptyset \leftrightarrow I ∖ \{\underset{˙}{0}\} = \emptyset)$
36	35	necon3bid	$⊢ (R \in DivRing \land I \in U \land I \neq \{\underset{˙}{0}\}) \to (D [I ∖ \{\underset{˙}{0}\}] \neq \emptyset \leftrightarrow I ∖ \{\underset{˙}{0}\} \neq \emptyset)$
37	28 36	mpbird	$⊢ (R \in DivRing \land I \in U \land I \neq \{\underset{˙}{0}\}) \to D [I ∖ \{\underset{˙}{0}\}] \neq \emptyset$
38		infssuzcl	$⊢ (D [I ∖ \{\underset{˙}{0}\}] \subseteq ℤ_{\geq 0} \land D [I ∖ \{\underset{˙}{0}\}] \neq \emptyset) \to inf (D [I ∖ \{\underset{˙}{0}\}] ℝ <) \in D [I ∖ \{\underset{˙}{0}\}]$
39	18 37 38	syl2anc	$⊢ (R \in DivRing \land I \in U \land I \neq \{\underset{˙}{0}\}) \to inf (D [I ∖ \{\underset{˙}{0}\}] ℝ <) \in D [I ∖ \{\underset{˙}{0}\}]$
40	32 33	fvelimabd	$⊢ (R \in DivRing \land I \in U \land I \neq \{\underset{˙}{0}\}) \to (inf (D [I ∖ \{\underset{˙}{0}\}] ℝ <) \in D [I ∖ \{\underset{˙}{0}\}] \leftrightarrow \exists h \in (I ∖ \{\underset{˙}{0}\}) D (h) = inf (D [I ∖ \{\underset{˙}{0}\}] ℝ <))$
41	39 40	mpbid	$⊢ (R \in DivRing \land I \in U \land I \neq \{\underset{˙}{0}\}) \to \exists h \in (I ∖ \{\underset{˙}{0}\}) D (h) = inf (D [I ∖ \{\underset{˙}{0}\}] ℝ <)$
42	20	adantr	$⊢ ((R \in DivRing \land I \in U \land I \neq \{\underset{˙}{0}\}) \land h \in (I ∖ \{\underset{˙}{0}\})) \to P \in Ring$
43		simpl2	$⊢ ((R \in DivRing \land I \in U \land I \neq \{\underset{˙}{0}\}) \land h \in (I ∖ \{\underset{˙}{0}\})) \to I \in U$
44	13	adantr	$⊢ ((R \in DivRing \land I \in U \land I \neq \{\underset{˙}{0}\}) \land h \in (I ∖ \{\underset{˙}{0}\})) \to R \in Ring$
45		eqid	$⊢ algSc (P) = algSc (P)$
46		eqid	$⊢ {Base}_{R} = {Base}_{R}$
47	1 45 46 6	ply1sclf	$⊢ R \in Ring \to algSc (P) : {Base}_{R} ⟶ {Base}_{P}$
48	44 47	syl	$⊢ ((R \in DivRing \land I \in U \land I \neq \{\underset{˙}{0}\}) \land h \in (I ∖ \{\underset{˙}{0}\})) \to algSc (P) : {Base}_{R} ⟶ {Base}_{P}$
49		simpl1	$⊢ ((R \in DivRing \land I \in U \land I \neq \{\underset{˙}{0}\}) \land h \in (I ∖ \{\underset{˙}{0}\})) \to R \in DivRing$
50	33	sselda	$⊢ ((R \in DivRing \land I \in U \land I \neq \{\underset{˙}{0}\}) \land h \in (I ∖ \{\underset{˙}{0}\})) \to h \in {Base}_{P}$
51		eldifsni	$⊢ h \in (I ∖ \{\underset{˙}{0}\}) \to h \neq \underset{˙}{0}$
52	51	adantl	$⊢ ((R \in DivRing \land I \in U \land I \neq \{\underset{˙}{0}\}) \land h \in (I ∖ \{\underset{˙}{0}\})) \to h \neq \underset{˙}{0}$
53		eqid	$⊢ {Unic}_{1p} (R) = {Unic}_{1p} (R)$
54	1 6 3 53	drnguc1p	$⊢ (R \in DivRing \land h \in {Base}_{P} \land h \neq \underset{˙}{0}) \to h \in {Unic}_{1p} (R)$
55	49 50 52 54	syl3anc	$⊢ ((R \in DivRing \land I \in U \land I \neq \{\underset{˙}{0}\}) \land h \in (I ∖ \{\underset{˙}{0}\})) \to h \in {Unic}_{1p} (R)$
56		eqid	$⊢ Unit (R) = Unit (R)$
57	5 56 53	uc1pldg	$⊢ h \in {Unic}_{1p} (R) \to {coe}_{1} (h) (D (h)) \in Unit (R)$
58	55 57	syl	$⊢ ((R \in DivRing \land I \in U \land I \neq \{\underset{˙}{0}\}) \land h \in (I ∖ \{\underset{˙}{0}\})) \to {coe}_{1} (h) (D (h)) \in Unit (R)$
59		eqid	$⊢ {inv}_{r} (R) = {inv}_{r} (R)$
60	56 59	unitinvcl	$⊢ (R \in Ring \land {coe}_{1} (h) (D (h)) \in Unit (R)) \to {inv}_{r} (R) ({coe}_{1} (h) (D (h))) \in Unit (R)$
61	44 58 60	syl2anc	$⊢ ((R \in DivRing \land I \in U \land I \neq \{\underset{˙}{0}\}) \land h \in (I ∖ \{\underset{˙}{0}\})) \to {inv}_{r} (R) ({coe}_{1} (h) (D (h))) \in Unit (R)$
62	46 56	unitcl	$⊢ {inv}_{r} (R) ({coe}_{1} (h) (D (h))) \in Unit (R) \to {inv}_{r} (R) ({coe}_{1} (h) (D (h))) \in {Base}_{R}$
63	61 62	syl	$⊢ ((R \in DivRing \land I \in U \land I \neq \{\underset{˙}{0}\}) \land h \in (I ∖ \{\underset{˙}{0}\})) \to {inv}_{r} (R) ({coe}_{1} (h) (D (h))) \in {Base}_{R}$
64	48 63	ffvelcdmd	$⊢ ((R \in DivRing \land I \in U \land I \neq \{\underset{˙}{0}\}) \land h \in (I ∖ \{\underset{˙}{0}\})) \to algSc (P) ({inv}_{r} (R) ({coe}_{1} (h) (D (h)))) \in {Base}_{P}$
65		eldifi	$⊢ h \in (I ∖ \{\underset{˙}{0}\}) \to h \in I$
66	65	adantl	$⊢ ((R \in DivRing \land I \in U \land I \neq \{\underset{˙}{0}\}) \land h \in (I ∖ \{\underset{˙}{0}\})) \to h \in I$
67		eqid	$⊢ \cdot_{P} = \cdot_{P}$
68	2 6 67	lidlmcl	$⊢ ((P \in Ring \land I \in U) \land (algSc (P) ({inv}_{r} (R) ({coe}_{1} (h) (D (h)))) \in {Base}_{P} \land h \in I)) \to algSc (P) ({inv}_{r} (R) ({coe}_{1} (h) (D (h)))) \cdot_{P} h \in I$
69	42 43 64 66 68	syl22anc	$⊢ ((R \in DivRing \land I \in U \land I \neq \{\underset{˙}{0}\}) \land h \in (I ∖ \{\underset{˙}{0}\})) \to algSc (P) ({inv}_{r} (R) ({coe}_{1} (h) (D (h)))) \cdot_{P} h \in I$
70	53 4 1 67 45 5 59	uc1pmon1p	$⊢ (R \in Ring \land h \in {Unic}_{1p} (R)) \to algSc (P) ({inv}_{r} (R) ({coe}_{1} (h) (D (h)))) \cdot_{P} h \in M$
71	44 55 70	syl2anc	$⊢ ((R \in DivRing \land I \in U \land I \neq \{\underset{˙}{0}\}) \land h \in (I ∖ \{\underset{˙}{0}\})) \to algSc (P) ({inv}_{r} (R) ({coe}_{1} (h) (D (h)))) \cdot_{P} h \in M$
72	69 71	elind	$⊢ ((R \in DivRing \land I \in U \land I \neq \{\underset{˙}{0}\}) \land h \in (I ∖ \{\underset{˙}{0}\})) \to algSc (P) ({inv}_{r} (R) ({coe}_{1} (h) (D (h)))) \cdot_{P} h \in (I \cap M)$
73		eqid	$⊢ RLReg (R) = RLReg (R)$
74	73 56	unitrrg	$⊢ R \in Ring \to Unit (R) \subseteq RLReg (R)$
75	44 74	syl	$⊢ ((R \in DivRing \land I \in U \land I \neq \{\underset{˙}{0}\}) \land h \in (I ∖ \{\underset{˙}{0}\})) \to Unit (R) \subseteq RLReg (R)$
76	75 61	sseldd	$⊢ ((R \in DivRing \land I \in U \land I \neq \{\underset{˙}{0}\}) \land h \in (I ∖ \{\underset{˙}{0}\})) \to {inv}_{r} (R) ({coe}_{1} (h) (D (h))) \in RLReg (R)$
77	5 1 73 6 67 45	deg1mul3	$⊢ (R \in Ring \land {inv}_{r} (R) ({coe}_{1} (h) (D (h))) \in RLReg (R) \land h \in {Base}_{P}) \to D (algSc (P) ({inv}_{r} (R) ({coe}_{1} (h) (D (h)))) \cdot_{P} h) = D (h)$
78	44 76 50 77	syl3anc	$⊢ ((R \in DivRing \land I \in U \land I \neq \{\underset{˙}{0}\}) \land h \in (I ∖ \{\underset{˙}{0}\})) \to D (algSc (P) ({inv}_{r} (R) ({coe}_{1} (h) (D (h)))) \cdot_{P} h) = D (h)$
79		fveqeq2	$⊢ g = algSc (P) ({inv}_{r} (R) ({coe}_{1} (h) (D (h)))) \cdot_{P} h \to (D (g) = D (h) \leftrightarrow D (algSc (P) ({inv}_{r} (R) ({coe}_{1} (h) (D (h)))) \cdot_{P} h) = D (h))$
80	79	rspcev	$⊢ (algSc (P) ({inv}_{r} (R) ({coe}_{1} (h) (D (h)))) \cdot_{P} h \in (I \cap M) \land D (algSc (P) ({inv}_{r} (R) ({coe}_{1} (h) (D (h)))) \cdot_{P} h) = D (h)) \to \exists g \in (I \cap M) D (g) = D (h)$
81	72 78 80	syl2anc	$⊢ ((R \in DivRing \land I \in U \land I \neq \{\underset{˙}{0}\}) \land h \in (I ∖ \{\underset{˙}{0}\})) \to \exists g \in (I \cap M) D (g) = D (h)$
82		eqeq2	$⊢ D (h) = inf (D [I ∖ \{\underset{˙}{0}\}] ℝ <) \to (D (g) = D (h) \leftrightarrow D (g) = inf (D [I ∖ \{\underset{˙}{0}\}] ℝ <))$
83	82	rexbidv	$⊢ D (h) = inf (D [I ∖ \{\underset{˙}{0}\}] ℝ <) \to (\exists g \in (I \cap M) D (g) = D (h) \leftrightarrow \exists g \in (I \cap M) D (g) = inf (D [I ∖ \{\underset{˙}{0}\}] ℝ <))$
84	81 83	syl5ibcom	$⊢ ((R \in DivRing \land I \in U \land I \neq \{\underset{˙}{0}\}) \land h \in (I ∖ \{\underset{˙}{0}\})) \to (D (h) = inf (D [I ∖ \{\underset{˙}{0}\}] ℝ <) \to \exists g \in (I \cap M) D (g) = inf (D [I ∖ \{\underset{˙}{0}\}] ℝ <))$
85	84	rexlimdva	$⊢ (R \in DivRing \land I \in U \land I \neq \{\underset{˙}{0}\}) \to (\exists h \in (I ∖ \{\underset{˙}{0}\}) D (h) = inf (D [I ∖ \{\underset{˙}{0}\}] ℝ <) \to \exists g \in (I \cap M) D (g) = inf (D [I ∖ \{\underset{˙}{0}\}] ℝ <))$
86	41 85	mpd	$⊢ (R \in DivRing \land I \in U \land I \neq \{\underset{˙}{0}\}) \to \exists g \in (I \cap M) D (g) = inf (D [I ∖ \{\underset{˙}{0}\}] ℝ <)$
87		eqid	$⊢ -_{P} = -_{P}$
88	13	ad2antrr	$⊢ (((R \in DivRing \land I \in U \land I \neq \{\underset{˙}{0}\}) \land (g \in (I \cap M) \land h \in (I \cap M))) \land (D (g) = inf (D [I ∖ \{\underset{˙}{0}\}] ℝ <) \land D (h) = inf (D [I ∖ \{\underset{˙}{0}\}] ℝ <))) \to R \in Ring$
89		simprl	$⊢ ((R \in DivRing \land I \in U \land I \neq \{\underset{˙}{0}\}) \land (g \in (I \cap M) \land h \in (I \cap M))) \to g \in (I \cap M)$
90	89	elin2d	$⊢ ((R \in DivRing \land I \in U \land I \neq \{\underset{˙}{0}\}) \land (g \in (I \cap M) \land h \in (I \cap M))) \to g \in M$
91	90	adantr	$⊢ (((R \in DivRing \land I \in U \land I \neq \{\underset{˙}{0}\}) \land (g \in (I \cap M) \land h \in (I \cap M))) \land (D (g) = inf (D [I ∖ \{\underset{˙}{0}\}] ℝ <) \land D (h) = inf (D [I ∖ \{\underset{˙}{0}\}] ℝ <))) \to g \in M$
92		simprl	$⊢ (((R \in DivRing \land I \in U \land I \neq \{\underset{˙}{0}\}) \land (g \in (I \cap M) \land h \in (I \cap M))) \land (D (g) = inf (D [I ∖ \{\underset{˙}{0}\}] ℝ <) \land D (h) = inf (D [I ∖ \{\underset{˙}{0}\}] ℝ <))) \to D (g) = inf (D [I ∖ \{\underset{˙}{0}\}] ℝ <)$
93		simprr	$⊢ ((R \in DivRing \land I \in U \land I \neq \{\underset{˙}{0}\}) \land (g \in (I \cap M) \land h \in (I \cap M))) \to h \in (I \cap M)$
94	93	elin2d	$⊢ ((R \in DivRing \land I \in U \land I \neq \{\underset{˙}{0}\}) \land (g \in (I \cap M) \land h \in (I \cap M))) \to h \in M$
95	94	adantr	$⊢ (((R \in DivRing \land I \in U \land I \neq \{\underset{˙}{0}\}) \land (g \in (I \cap M) \land h \in (I \cap M))) \land (D (g) = inf (D [I ∖ \{\underset{˙}{0}\}] ℝ <) \land D (h) = inf (D [I ∖ \{\underset{˙}{0}\}] ℝ <))) \to h \in M$
96		simprr	$⊢ (((R \in DivRing \land I \in U \land I \neq \{\underset{˙}{0}\}) \land (g \in (I \cap M) \land h \in (I \cap M))) \land (D (g) = inf (D [I ∖ \{\underset{˙}{0}\}] ℝ <) \land D (h) = inf (D [I ∖ \{\underset{˙}{0}\}] ℝ <))) \to D (h) = inf (D [I ∖ \{\underset{˙}{0}\}] ℝ <)$
97	5 4 1 87 88 91 92 95 96	deg1submon1p	$⊢ (((R \in DivRing \land I \in U \land I \neq \{\underset{˙}{0}\}) \land (g \in (I \cap M) \land h \in (I \cap M))) \land (D (g) = inf (D [I ∖ \{\underset{˙}{0}\}] ℝ <) \land D (h) = inf (D [I ∖ \{\underset{˙}{0}\}] ℝ <))) \to D (g -_{P} h) < inf (D [I ∖ \{\underset{˙}{0}\}] ℝ <)$
98	97	ex	$⊢ ((R \in DivRing \land I \in U \land I \neq \{\underset{˙}{0}\}) \land (g \in (I \cap M) \land h \in (I \cap M))) \to ((D (g) = inf (D [I ∖ \{\underset{˙}{0}\}] ℝ <) \land D (h) = inf (D [I ∖ \{\underset{˙}{0}\}] ℝ <)) \to D (g -_{P} h) < inf (D [I ∖ \{\underset{˙}{0}\}] ℝ <))$
99	18	ad2antrr	$⊢ (((R \in DivRing \land I \in U \land I \neq \{\underset{˙}{0}\}) \land (g \in (I \cap M) \land h \in (I \cap M))) \land g -_{P} h \neq \underset{˙}{0}) \to D [I ∖ \{\underset{˙}{0}\}] \subseteq ℤ_{\geq 0}$
100	31	a1i	$⊢ (((R \in DivRing \land I \in U \land I \neq \{\underset{˙}{0}\}) \land (g \in (I \cap M) \land h \in (I \cap M))) \land g -_{P} h \neq \underset{˙}{0}) \to D Fn {Base}_{P}$
101	33	ad2antrr	$⊢ (((R \in DivRing \land I \in U \land I \neq \{\underset{˙}{0}\}) \land (g \in (I \cap M) \land h \in (I \cap M))) \land g -_{P} h \neq \underset{˙}{0}) \to I ∖ \{\underset{˙}{0}\} \subseteq {Base}_{P}$
102	20	adantr	$⊢ ((R \in DivRing \land I \in U \land I \neq \{\underset{˙}{0}\}) \land (g \in (I \cap M) \land h \in (I \cap M))) \to P \in Ring$
103		simpl2	$⊢ ((R \in DivRing \land I \in U \land I \neq \{\underset{˙}{0}\}) \land (g \in (I \cap M) \land h \in (I \cap M))) \to I \in U$
104	89	elin1d	$⊢ ((R \in DivRing \land I \in U \land I \neq \{\underset{˙}{0}\}) \land (g \in (I \cap M) \land h \in (I \cap M))) \to g \in I$
105	93	elin1d	$⊢ ((R \in DivRing \land I \in U \land I \neq \{\underset{˙}{0}\}) \land (g \in (I \cap M) \land h \in (I \cap M))) \to h \in I$
106	2 87	lidlsubcl	$⊢ ((P \in Ring \land I \in U) \land (g \in I \land h \in I)) \to g -_{P} h \in I$
107	102 103 104 105 106	syl22anc	$⊢ ((R \in DivRing \land I \in U \land I \neq \{\underset{˙}{0}\}) \land (g \in (I \cap M) \land h \in (I \cap M))) \to g -_{P} h \in I$
108	107	adantr	$⊢ (((R \in DivRing \land I \in U \land I \neq \{\underset{˙}{0}\}) \land (g \in (I \cap M) \land h \in (I \cap M))) \land g -_{P} h \neq \underset{˙}{0}) \to g -_{P} h \in I$
109		simpr	$⊢ (((R \in DivRing \land I \in U \land I \neq \{\underset{˙}{0}\}) \land (g \in (I \cap M) \land h \in (I \cap M))) \land g -_{P} h \neq \underset{˙}{0}) \to g -_{P} h \neq \underset{˙}{0}$
110		eldifsn	$⊢ g -_{P} h \in (I ∖ \{\underset{˙}{0}\}) \leftrightarrow (g -_{P} h \in I \land g -_{P} h \neq \underset{˙}{0})$
111	108 109 110	sylanbrc	$⊢ (((R \in DivRing \land I \in U \land I \neq \{\underset{˙}{0}\}) \land (g \in (I \cap M) \land h \in (I \cap M))) \land g -_{P} h \neq \underset{˙}{0}) \to g -_{P} h \in (I ∖ \{\underset{˙}{0}\})$
112		fnfvima	$⊢ (D Fn {Base}_{P} \land I ∖ \{\underset{˙}{0}\} \subseteq {Base}_{P} \land g -_{P} h \in (I ∖ \{\underset{˙}{0}\})) \to D (g -_{P} h) \in D [I ∖ \{\underset{˙}{0}\}]$
113	100 101 111 112	syl3anc	$⊢ (((R \in DivRing \land I \in U \land I \neq \{\underset{˙}{0}\}) \land (g \in (I \cap M) \land h \in (I \cap M))) \land g -_{P} h \neq \underset{˙}{0}) \to D (g -_{P} h) \in D [I ∖ \{\underset{˙}{0}\}]$
114		infssuzle	$⊢ (D [I ∖ \{\underset{˙}{0}\}] \subseteq ℤ_{\geq 0} \land D (g -_{P} h) \in D [I ∖ \{\underset{˙}{0}\}]) \to inf (D [I ∖ \{\underset{˙}{0}\}] ℝ <) \leq D (g -_{P} h)$
115	99 113 114	syl2anc	$⊢ (((R \in DivRing \land I \in U \land I \neq \{\underset{˙}{0}\}) \land (g \in (I \cap M) \land h \in (I \cap M))) \land g -_{P} h \neq \underset{˙}{0}) \to inf (D [I ∖ \{\underset{˙}{0}\}] ℝ <) \leq D (g -_{P} h)$
116	115	ex	$⊢ ((R \in DivRing \land I \in U \land I \neq \{\underset{˙}{0}\}) \land (g \in (I \cap M) \land h \in (I \cap M))) \to (g -_{P} h \neq \underset{˙}{0} \to inf (D [I ∖ \{\underset{˙}{0}\}] ℝ <) \leq D (g -_{P} h))$
117		imassrn	$⊢ D [I ∖ \{\underset{˙}{0}\}] \subseteq ran D$
118		frn	$⊢ D : {Base}_{P} ⟶ ℝ^{} \to ran D \subseteq ℝ^{}$
119	29 118	ax-mp	$⊢ ran D \subseteq ℝ^{*}$
120	117 119	sstri	$⊢ D [I ∖ \{\underset{˙}{0}\}] \subseteq ℝ^{*}$
121	120 39	sselid	$⊢ (R \in DivRing \land I \in U \land I \neq \{\underset{˙}{0}\}) \to inf (D [I ∖ \{\underset{˙}{0}\}] ℝ <) \in ℝ^{*}$
122	121	adantr	$⊢ ((R \in DivRing \land I \in U \land I \neq \{\underset{˙}{0}\}) \land (g \in (I \cap M) \land h \in (I \cap M))) \to inf (D [I ∖ \{\underset{˙}{0}\}] ℝ <) \in ℝ^{*}$
123		ringgrp	$⊢ P \in Ring \to P \in Grp$
124	20 123	syl	$⊢ (R \in DivRing \land I \in U \land I \neq \{\underset{˙}{0}\}) \to P \in Grp$
125	124	adantr	$⊢ ((R \in DivRing \land I \in U \land I \neq \{\underset{˙}{0}\}) \land (g \in (I \cap M) \land h \in (I \cap M))) \to P \in Grp$
126		inss1	$⊢ I \cap M \subseteq I$
127	126 8	sstrid	$⊢ (R \in DivRing \land I \in U \land I \neq \{\underset{˙}{0}\}) \to I \cap M \subseteq {Base}_{P}$
128	127	adantr	$⊢ ((R \in DivRing \land I \in U \land I \neq \{\underset{˙}{0}\}) \land (g \in (I \cap M) \land h \in (I \cap M))) \to I \cap M \subseteq {Base}_{P}$
129	128 89	sseldd	$⊢ ((R \in DivRing \land I \in U \land I \neq \{\underset{˙}{0}\}) \land (g \in (I \cap M) \land h \in (I \cap M))) \to g \in {Base}_{P}$
130	128 93	sseldd	$⊢ ((R \in DivRing \land I \in U \land I \neq \{\underset{˙}{0}\}) \land (g \in (I \cap M) \land h \in (I \cap M))) \to h \in {Base}_{P}$
131	6 87	grpsubcl	$⊢ (P \in Grp \land g \in {Base}_{P} \land h \in {Base}_{P}) \to g -_{P} h \in {Base}_{P}$
132	125 129 130 131	syl3anc	$⊢ ((R \in DivRing \land I \in U \land I \neq \{\underset{˙}{0}\}) \land (g \in (I \cap M) \land h \in (I \cap M))) \to g -_{P} h \in {Base}_{P}$
133	5 1 6	deg1xrcl	$⊢ g -_{P} h \in {Base}_{P} \to D (g -_{P} h) \in ℝ^{*}$
134	132 133	syl	$⊢ ((R \in DivRing \land I \in U \land I \neq \{\underset{˙}{0}\}) \land (g \in (I \cap M) \land h \in (I \cap M))) \to D (g -_{P} h) \in ℝ^{*}$
135	122 134	xrlenltd	$⊢ ((R \in DivRing \land I \in U \land I \neq \{\underset{˙}{0}\}) \land (g \in (I \cap M) \land h \in (I \cap M))) \to (inf (D [I ∖ \{\underset{˙}{0}\}] ℝ <) \leq D (g -_{P} h) \leftrightarrow \neg D (g -_{P} h) < inf (D [I ∖ \{\underset{˙}{0}\}] ℝ <))$
136	116 135	sylibd	$⊢ ((R \in DivRing \land I \in U \land I \neq \{\underset{˙}{0}\}) \land (g \in (I \cap M) \land h \in (I \cap M))) \to (g -_{P} h \neq \underset{˙}{0} \to \neg D (g -_{P} h) < inf (D [I ∖ \{\underset{˙}{0}\}] ℝ <))$
137	136	necon4ad	$⊢ ((R \in DivRing \land I \in U \land I \neq \{\underset{˙}{0}\}) \land (g \in (I \cap M) \land h \in (I \cap M))) \to (D (g -_{P} h) < inf (D [I ∖ \{\underset{˙}{0}\}] ℝ <) \to g -_{P} h = \underset{˙}{0})$
138	98 137	syld	$⊢ ((R \in DivRing \land I \in U \land I \neq \{\underset{˙}{0}\}) \land (g \in (I \cap M) \land h \in (I \cap M))) \to ((D (g) = inf (D [I ∖ \{\underset{˙}{0}\}] ℝ <) \land D (h) = inf (D [I ∖ \{\underset{˙}{0}\}] ℝ <)) \to g -_{P} h = \underset{˙}{0})$
139	6 3 87	grpsubeq0	$⊢ (P \in Grp \land g \in {Base}_{P} \land h \in {Base}_{P}) \to (g -_{P} h = \underset{˙}{0} \leftrightarrow g = h)$
140	125 129 130 139	syl3anc	$⊢ ((R \in DivRing \land I \in U \land I \neq \{\underset{˙}{0}\}) \land (g \in (I \cap M) \land h \in (I \cap M))) \to (g -_{P} h = \underset{˙}{0} \leftrightarrow g = h)$
141	138 140	sylibd	$⊢ ((R \in DivRing \land I \in U \land I \neq \{\underset{˙}{0}\}) \land (g \in (I \cap M) \land h \in (I \cap M))) \to ((D (g) = inf (D [I ∖ \{\underset{˙}{0}\}] ℝ <) \land D (h) = inf (D [I ∖ \{\underset{˙}{0}\}] ℝ <)) \to g = h)$
142	141	ralrimivva	$⊢ (R \in DivRing \land I \in U \land I \neq \{\underset{˙}{0}\}) \to \forall g \in (I \cap M) \forall h \in (I \cap M) ((D (g) = inf (D [I ∖ \{\underset{˙}{0}\}] ℝ <) \land D (h) = inf (D [I ∖ \{\underset{˙}{0}\}] ℝ <)) \to g = h)$
143		fveqeq2	$⊢ g = h \to (D (g) = inf (D [I ∖ \{\underset{˙}{0}\}] ℝ <) \leftrightarrow D (h) = inf (D [I ∖ \{\underset{˙}{0}\}] ℝ <))$
144	143	reu4	$⊢ \exists! g \in (I \cap M) D (g) = inf (D [I ∖ \{\underset{˙}{0}\}] ℝ <) \leftrightarrow (\exists g \in (I \cap M) D (g) = inf (D [I ∖ \{\underset{˙}{0}\}] ℝ <) \land \forall g \in (I \cap M) \forall h \in (I \cap M) ((D (g) = inf (D [I ∖ \{\underset{˙}{0}\}] ℝ <) \land D (h) = inf (D [I ∖ \{\underset{˙}{0}\}] ℝ <)) \to g = h))$
145	86 142 144	sylanbrc	$⊢ (R \in DivRing \land I \in U \land I \neq \{\underset{˙}{0}\}) \to \exists! g \in (I \cap M) D (g) = inf (D [I ∖ \{\underset{˙}{0}\}] ℝ <)$

Metamath Proof Explorer

Theorem ig1peu

Proof