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	⊢ 𝐵 = ( Base ‘ 𝑅 )
	lsmsnpridl.2	⊢ 𝐺 = ( mulGrp ‘ 𝑅 )
	lsmsnpridl.3	⊢ × = ( LSSum ‘ 𝐺 )
	lsmsnpridl.4	⊢ 𝐾 = ( RSpan ‘ 𝑅 )
	lsmsnpridl.5	⊢ ( 𝜑 → 𝑅 ∈ Ring )
	lsmsnpridl.6	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
Assertion	lsmsnpridl	⊢ ( 𝜑 → ( 𝐵 × { 𝑋 } ) = ( 𝐾 ‘ { 𝑋 } ) )

Proof

Step	Hyp	Ref	Expression
1		lsmsnpridl.1	⊢ 𝐵 = ( Base ‘ 𝑅 )
2		lsmsnpridl.2	⊢ 𝐺 = ( mulGrp ‘ 𝑅 )
3		lsmsnpridl.3	⊢ × = ( LSSum ‘ 𝐺 )
4		lsmsnpridl.4	⊢ 𝐾 = ( RSpan ‘ 𝑅 )
5		lsmsnpridl.5	⊢ ( 𝜑 → 𝑅 ∈ Ring )
6		lsmsnpridl.6	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
7	2 1	mgpbas	⊢ 𝐵 = ( Base ‘ 𝐺 )
8		eqid	⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
9	2 8	mgpplusg	⊢ ( .r ‘ 𝑅 ) = ( +g ‘ 𝐺 )
10	2	fvexi	⊢ 𝐺 ∈ V
11	10	a1i	⊢ ( 𝜑 → 𝐺 ∈ V )
12		ssidd	⊢ ( 𝜑 → 𝐵 ⊆ 𝐵 )
13	7 9 3 11 12 6	elgrplsmsn	⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐵 × { 𝑋 } ) ↔ ∃ 𝑦 ∈ 𝐵 𝑥 = ( 𝑦 ( .r ‘ 𝑅 ) 𝑋 ) ) )
14	1 8 4	rspsnel	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ) → ( 𝑥 ∈ ( 𝐾 ‘ { 𝑋 } ) ↔ ∃ 𝑦 ∈ 𝐵 𝑥 = ( 𝑦 ( .r ‘ 𝑅 ) 𝑋 ) ) )
15	5 6 14	syl2anc	⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐾 ‘ { 𝑋 } ) ↔ ∃ 𝑦 ∈ 𝐵 𝑥 = ( 𝑦 ( .r ‘ 𝑅 ) 𝑋 ) ) )
16	13 15	bitr4d	⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐵 × { 𝑋 } ) ↔ 𝑥 ∈ ( 𝐾 ‘ { 𝑋 } ) ) )
17	16	eqrdv	⊢ ( 𝜑 → ( 𝐵 × { 𝑋 } ) = ( 𝐾 ‘ { 𝑋 } ) )