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

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		sneq	⊢ ( 𝑦 = 𝑋 → { 𝑦 } = { 𝑋 } )
8	7	fveq2d	⊢ ( 𝑦 = 𝑋 → ( 𝐾 ‘ { 𝑦 } ) = ( 𝐾 ‘ { 𝑋 } ) )
9	8	eqeq2d	⊢ ( 𝑦 = 𝑋 → ( ( 𝐵 × { 𝑋 } ) = ( 𝐾 ‘ { 𝑦 } ) ↔ ( 𝐵 × { 𝑋 } ) = ( 𝐾 ‘ { 𝑋 } ) ) )
10	9	adantl	⊢ ( ( 𝜑 ∧ 𝑦 = 𝑋 ) → ( ( 𝐵 × { 𝑋 } ) = ( 𝐾 ‘ { 𝑦 } ) ↔ ( 𝐵 × { 𝑋 } ) = ( 𝐾 ‘ { 𝑋 } ) ) )
11	1 2 3 4 5 6	lsmsnpridl	⊢ ( 𝜑 → ( 𝐵 × { 𝑋 } ) = ( 𝐾 ‘ { 𝑋 } ) )
12	6 10 11	rspcedvd	⊢ ( 𝜑 → ∃ 𝑦 ∈ 𝐵 ( 𝐵 × { 𝑋 } ) = ( 𝐾 ‘ { 𝑦 } ) )
13		eqid	⊢ ( LPIdeal ‘ 𝑅 ) = ( LPIdeal ‘ 𝑅 )
14	13 4 1	islpidl	⊢ ( 𝑅 ∈ Ring → ( ( 𝐵 × { 𝑋 } ) ∈ ( LPIdeal ‘ 𝑅 ) ↔ ∃ 𝑦 ∈ 𝐵 ( 𝐵 × { 𝑋 } ) = ( 𝐾 ‘ { 𝑦 } ) ) )
15	5 14	syl	⊢ ( 𝜑 → ( ( 𝐵 × { 𝑋 } ) ∈ ( LPIdeal ‘ 𝑅 ) ↔ ∃ 𝑦 ∈ 𝐵 ( 𝐵 × { 𝑋 } ) = ( 𝐾 ‘ { 𝑦 } ) ) )
16	12 15	mpbird	⊢ ( 𝜑 → ( 𝐵 × { 𝑋 } ) ∈ ( LPIdeal ‘ 𝑅 ) )