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 
|- .X. = ( LSSum ` G )
lsmsnpridl.4 
|- K = ( RSpan ` R )
lsmsnpridl.5 
|- ( ph -> R e. Ring )
lsmsnpridl.6 
|- ( ph -> X e. B )
Assertion lsmsnpridl 
|- ( ph -> ( B .X. { X } ) = ( K ` { X } ) )

Proof

Step Hyp Ref Expression
1 lsmsnpridl.1 
 |-  B = ( Base ` R )
2 lsmsnpridl.2 
 |-  G = ( mulGrp ` R )
3 lsmsnpridl.3 
 |-  .X. = ( LSSum ` G )
4 lsmsnpridl.4 
 |-  K = ( RSpan ` R )
5 lsmsnpridl.5 
 |-  ( ph -> R e. Ring )
6 lsmsnpridl.6 
 |-  ( ph -> X e. B )
7 2 1 mgpbas 
 |-  B = ( Base ` G )
8 eqid 
 |-  ( .r ` R ) = ( .r ` R )
9 2 8 mgpplusg 
 |-  ( .r ` R ) = ( +g ` G )
10 2 fvexi 
 |-  G e. _V
11 10 a1i 
 |-  ( ph -> G e. _V )
12 ssidd 
 |-  ( ph -> B C_ B )
13 7 9 3 11 12 6 elgrplsmsn 
 |-  ( ph -> ( x e. ( B .X. { X } ) <-> E. y e. B x = ( y ( .r ` R ) X ) ) )
14 1 8 4 elrspsn 
 |-  ( ( R e. Ring /\ X e. B ) -> ( x e. ( K ` { X } ) <-> E. y e. B x = ( y ( .r ` R ) X ) ) )
15 5 6 14 syl2anc 
 |-  ( ph -> ( x e. ( K ` { X } ) <-> E. y e. B x = ( y ( .r ` R ) X ) ) )
16 13 15 bitr4d 
 |-  ( ph -> ( x e. ( B .X. { X } ) <-> x e. ( K ` { X } ) ) )
17 16 eqrdv 
 |-  ( ph -> ( B .X. { X } ) = ( K ` { X } ) )