Metamath Proof Explorer

Theorem lpigen

Description: An ideal is principal iff it contains an element which right-divides all elements. (Contributed by Stefan O'Rear, 3-Jan-2015) (Revised by Wolf Lammen, 6-Sep-2020)

		Ref	Expression
	Hypotheses	lpigen.u	$⊢ U = LIdeal (R)$
		lpigen.p	$⊢ P = LPIdeal (R)$
		lpigen.d	$⊢ \underset{˙}{∥} = ∥_{r} (R)$
	Assertion	lpigen	$⊢ (R \in Ring \land I \in U) \to (I \in P \leftrightarrow \exists x \in I \forall y \in I x \underset{˙}{∥} y)$

Proof

Step	Hyp	Ref	Expression
1		lpigen.u	$⊢ U = LIdeal (R)$
2		lpigen.p	$⊢ P = LPIdeal (R)$
3		lpigen.d	$⊢ \underset{˙}{∥} = ∥_{r} (R)$
4		eqid	$⊢ RSpan (R) = RSpan (R)$
5		eqid	$⊢ {Base}_{R} = {Base}_{R}$
6	2 4 5	islpidl	$⊢ R \in Ring \to (I \in P \leftrightarrow \exists x \in {Base}_{R} I = RSpan (R) (\{x\}))$
7	6	adantr	$⊢ (R \in Ring \land I \in U) \to (I \in P \leftrightarrow \exists x \in {Base}_{R} I = RSpan (R) (\{x\}))$
8	5 1 4 3	lidldvgen	$⊢ (R \in Ring \land I \in U \land x \in {Base}_{R}) \to (I = RSpan (R) (\{x\}) \leftrightarrow (x \in I \land \forall y \in I x \underset{˙}{∥} y))$
9	8	3expa	$⊢ ((R \in Ring \land I \in U) \land x \in {Base}_{R}) \to (I = RSpan (R) (\{x\}) \leftrightarrow (x \in I \land \forall y \in I x \underset{˙}{∥} y))$
10	9	rexbidva	$⊢ (R \in Ring \land I \in U) \to (\exists x \in {Base}_{R} I = RSpan (R) (\{x\}) \leftrightarrow \exists x \in {Base}_{R} (x \in I \land \forall y \in I x \underset{˙}{∥} y))$
11		simpr	$⊢ (x \in {Base}_{R} \land (x \in I \land \forall y \in I x \underset{˙}{∥} y)) \to (x \in I \land \forall y \in I x \underset{˙}{∥} y)$
12	5 1	lidlss	$⊢ I \in U \to I \subseteq {Base}_{R}$
13	12	adantl	$⊢ (R \in Ring \land I \in U) \to I \subseteq {Base}_{R}$
14	13	sseld	$⊢ (R \in Ring \land I \in U) \to (x \in I \to x \in {Base}_{R})$
15	14	adantrd	$⊢ (R \in Ring \land I \in U) \to ((x \in I \land \forall y \in I x \underset{˙}{∥} y) \to x \in {Base}_{R})$
16	15	ancrd	$⊢ (R \in Ring \land I \in U) \to ((x \in I \land \forall y \in I x \underset{˙}{∥} y) \to (x \in {Base}_{R} \land (x \in I \land \forall y \in I x \underset{˙}{∥} y)))$
17	11 16	impbid2	$⊢ (R \in Ring \land I \in U) \to ((x \in {Base}_{R} \land (x \in I \land \forall y \in I x \underset{˙}{∥} y)) \leftrightarrow (x \in I \land \forall y \in I x \underset{˙}{∥} y))$
18	17	rexbidv2	$⊢ (R \in Ring \land I \in U) \to (\exists x \in {Base}_{R} (x \in I \land \forall y \in I x \underset{˙}{∥} y) \leftrightarrow \exists x \in I \forall y \in I x \underset{˙}{∥} y)$
19	7 10 18	3bitrd	$⊢ (R \in Ring \land I \in U) \to (I \in P \leftrightarrow \exists x \in I \forall y \in I x \underset{˙}{∥} y)$