lsmsnidl

Description: The product of the ring with a single element is a principal ideal. (Contributed by Thierry Arnoux, 21-Jan-2024)

	Ref	Expression
Hypotheses	lsmsnpridl.1	$⊢ B = {Base}_{R}$
	lsmsnpridl.2	$⊢ G = {mulGrp}_{R}$
	lsmsnpridl.3	$⊢ \underset{˙}{\times} = LSSum (G)$
	lsmsnpridl.4	$⊢ K = RSpan (R)$
	lsmsnpridl.5	$⊢ φ \to R \in Ring$
	lsmsnpridl.6	$⊢ φ \to X \in B$
Assertion	lsmsnidl	$⊢ φ \to B \underset{˙}{\times} \{X\} \in LPIdeal (R)$

Step	Hyp	Ref	Expression
1		lsmsnpridl.1	$⊢ B = {Base}_{R}$
2		lsmsnpridl.2	$⊢ G = {mulGrp}_{R}$
3		lsmsnpridl.3	$⊢ \underset{˙}{\times} = LSSum (G)$
4		lsmsnpridl.4	$⊢ K = RSpan (R)$
5		lsmsnpridl.5	$⊢ φ \to R \in Ring$
6		lsmsnpridl.6	$⊢ φ \to X \in B$
7		sneq	$⊢ y = X \to \{y\} = \{X\}$
8	7	fveq2d	$⊢ y = X \to K (\{y\}) = K (\{X\})$
9	8	eqeq2d	$⊢ y = X \to (B \underset{˙}{\times} \{X\} = K (\{y\}) \leftrightarrow B \underset{˙}{\times} \{X\} = K (\{X\}))$
10	9	adantl	$⊢ (φ \land y = X) \to (B \underset{˙}{\times} \{X\} = K (\{y\}) \leftrightarrow B \underset{˙}{\times} \{X\} = K (\{X\}))$
11	1 2 3 4 5 6	lsmsnpridl	$⊢ φ \to B \underset{˙}{\times} \{X\} = K (\{X\})$
12	6 10 11	rspcedvd	$⊢ φ \to \exists y \in B B \underset{˙}{\times} \{X\} = K (\{y\})$
13		eqid	$⊢ LPIdeal (R) = LPIdeal (R)$
14	13 4 1	islpidl	$⊢ R \in Ring \to (B \underset{˙}{\times} \{X\} \in LPIdeal (R) \leftrightarrow \exists y \in B B \underset{˙}{\times} \{X\} = K (\{y\}))$
15	5 14	syl	$⊢ φ \to (B \underset{˙}{\times} \{X\} \in LPIdeal (R) \leftrightarrow \exists y \in B B \underset{˙}{\times} \{X\} = K (\{y\}))$
16	12 15	mpbird	$⊢ φ \to B \underset{˙}{\times} \{X\} \in LPIdeal (R)$

Metamath Proof Explorer