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 ⊢ 𝐵 = ( 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 elrspsn ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ) → ( 𝑥 ∈ ( 𝐾 ‘ { 𝑋 } ) ↔ ∃ 𝑦 ∈ 𝐵 𝑥 = ( 𝑦 ( .r ‘ 𝑅 ) 𝑋 ) ) )
15 5 6 14 syl2anc ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐾 ‘ { 𝑋 } ) ↔ ∃ 𝑦 ∈ 𝐵 𝑥 = ( 𝑦 ( .r ‘ 𝑅 ) 𝑋 ) ) )
16 13 15 bitr4d ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐵 × { 𝑋 } ) ↔ 𝑥 ∈ ( 𝐾 ‘ { 𝑋 } ) ) )
17 16 eqrdv ⊢ ( 𝜑 → ( 𝐵 × { 𝑋 } ) = ( 𝐾 ‘ { 𝑋 } ) )