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

Metamath Proof Explorer

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 ‘ 𝑅 ) )