This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem lsmsnpridl

Description: The product of the ring with a single element is equal to the principal ideal generated by that element. (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	lsmsnpridl	$⊢ φ \to B \underset{˙}{\times} \{X\} = K (\{X\})$

Proof

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	2 1	mgpbas	$⊢ B = {Base}_{G}$
8		eqid	$⊢ \cdot_{R} = \cdot_{R}$
9	2 8	mgpplusg	$⊢ \cdot_{R} = +_{G}$
10	2	fvexi	$⊢ G \in V$
11	10	a1i	$⊢ φ \to G \in V$
12		ssidd	$⊢ φ \to B \subseteq B$
13	7 9 3 11 12 6	elgrplsmsn	$⊢ φ \to (x \in (B \underset{˙}{\times} \{X\}) \leftrightarrow \exists y \in B x = y \cdot_{R} X)$
14	1 8 4	elrspsn	$⊢ (R \in Ring \land X \in B) \to (x \in K (\{X\}) \leftrightarrow \exists y \in B x = y \cdot_{R} X)$
15	5 6 14	syl2anc	$⊢ φ \to (x \in K (\{X\}) \leftrightarrow \exists y \in B x = y \cdot_{R} X)$
16	13 15	bitr4d	$⊢ φ \to (x \in (B \underset{˙}{\times} \{X\}) \leftrightarrow x \in K (\{X\}))$
17	16	eqrdv	$⊢ φ \to B \underset{˙}{\times} \{X\} = K (\{X\})$