Metamath Proof Explorer

Theorem ellcsrspsn

Description: Membership in a left coset in a quotient of a ring by the span of a singleton (that is, by the ideal generated by an element). This characterization comes from eqglact and elrspsn . (Contributed by SN, 19-Jun-2025)

Ref Expression
Hypotheses ellcsrspsn.b 
|- B = ( Base ` R )
ellcsrspsn.p 
|- .+ = ( +g ` R )
ellcsrspsn.t 
|- .x. = ( .r ` R )
ellcsrspsn.e 
|- .~ = ( R ~QG I )
ellcsrspsn.u 
|- U = ( R /s .~ )
ellcsrspsn.i 
|- I = ( ( RSpan ` R ) ` { M } )
ellcsrspsn.r 
|- ( ph -> R e. Ring )
ellcsrspsn.m 
|- ( ph -> M e. B )
ellcsrspsn.x 
|- ( ph -> X e. ( Base ` U ) )
Assertion ellcsrspsn 
|- ( ph -> E. x e. B ( X = [ x ] .~ /\ X = { z | E. y e. B z = ( x .+ ( y .x. M ) ) } ) )

Proof

Step Hyp Ref Expression
1 ellcsrspsn.b 
 |-  B = ( Base ` R )
2 ellcsrspsn.p 
 |-  .+ = ( +g ` R )
3 ellcsrspsn.t 
 |-  .x. = ( .r ` R )
4 ellcsrspsn.e 
 |-  .~ = ( R ~QG I )
5 ellcsrspsn.u 
 |-  U = ( R /s .~ )
6 ellcsrspsn.i 
 |-  I = ( ( RSpan ` R ) ` { M } )
7 ellcsrspsn.r 
 |-  ( ph -> R e. Ring )
8 ellcsrspsn.m 
 |-  ( ph -> M e. B )
9 ellcsrspsn.x 
 |-  ( ph -> X e. ( Base ` U ) )
10 4 5 1 quselbas 
 |-  ( ( R e. Ring /\ X e. ( Base ` U ) ) -> ( X e. ( Base ` U ) <-> E. x e. B X = [ x ] .~ ) )
11 7 9 10 syl2anc 
 |-  ( ph -> ( X e. ( Base ` U ) <-> E. x e. B X = [ x ] .~ ) )
12 9 11 mpbid 
 |-  ( ph -> E. x e. B X = [ x ] .~ )
13 7 ringgrpd 
 |-  ( ph -> R e. Grp )
14 13 adantr 
 |-  ( ( ph /\ x e. B ) -> R e. Grp )
15 eqid 
 |-  ( RSpan ` R ) = ( RSpan ` R )
16 8 snssd 
 |-  ( ph -> { M } C_ B )
17 15 1 7 16 rspssbasd 
 |-  ( ph -> ( ( RSpan ` R ) ` { M } ) C_ B )
18 6 17 eqsstrid 
 |-  ( ph -> I C_ B )
19 18 adantr 
 |-  ( ( ph /\ x e. B ) -> I C_ B )
20 simpr 
 |-  ( ( ph /\ x e. B ) -> x e. B )
21 1 4 2 eqglact 
 |-  ( ( R e. Grp /\ I C_ B /\ x e. B ) -> [ x ] .~ = ( ( i e. B |-> ( x .+ i ) ) " I ) )
22 14 19 20 21 syl3anc 
 |-  ( ( ph /\ x e. B ) -> [ x ] .~ = ( ( i e. B |-> ( x .+ i ) ) " I ) )
23 eqid 
 |-  ( i e. B |-> ( x .+ i ) ) = ( i e. B |-> ( x .+ i ) )
24 vex 
 |-  z e. _V
25 24 a1i 
 |-  ( ( ph /\ x e. B ) -> z e. _V )
26 23 25 19 elimampt 
 |-  ( ( ph /\ x e. B ) -> ( z e. ( ( i e. B |-> ( x .+ i ) ) " I ) <-> E. i e. I z = ( x .+ i ) ) )
27 oveq2 
 |-  ( i = ( y .x. M ) -> ( x .+ i ) = ( x .+ ( y .x. M ) ) )
28 27 eqeq2d 
 |-  ( i = ( y .x. M ) -> ( z = ( x .+ i ) <-> z = ( x .+ ( y .x. M ) ) ) )
29 6 eleq2i 
 |-  ( i e. I <-> i e. ( ( RSpan ` R ) ` { M } ) )
30 1 3 15 elrspsn 
 |-  ( ( R e. Ring /\ M e. B ) -> ( i e. ( ( RSpan ` R ) ` { M } ) <-> E. y e. B i = ( y .x. M ) ) )
31 7 8 30 syl2anc 
 |-  ( ph -> ( i e. ( ( RSpan ` R ) ` { M } ) <-> E. y e. B i = ( y .x. M ) ) )
32 29 31 bitrid 
 |-  ( ph -> ( i e. I <-> E. y e. B i = ( y .x. M ) ) )
33 32 adantr 
 |-  ( ( ph /\ x e. B ) -> ( i e. I <-> E. y e. B i = ( y .x. M ) ) )
34 ovexd 
 |-  ( ( ph /\ x e. B ) -> ( y .x. M ) e. _V )
35 28 33 34 rexxfr3d 
 |-  ( ( ph /\ x e. B ) -> ( E. i e. I z = ( x .+ i ) <-> E. y e. B z = ( x .+ ( y .x. M ) ) ) )
36 26 35 bitrd 
 |-  ( ( ph /\ x e. B ) -> ( z e. ( ( i e. B |-> ( x .+ i ) ) " I ) <-> E. y e. B z = ( x .+ ( y .x. M ) ) ) )
37 36 eqabdv 
 |-  ( ( ph /\ x e. B ) -> ( ( i e. B |-> ( x .+ i ) ) " I ) = { z | E. y e. B z = ( x .+ ( y .x. M ) ) } )
38 22 37 eqtrd 
 |-  ( ( ph /\ x e. B ) -> [ x ] .~ = { z | E. y e. B z = ( x .+ ( y .x. M ) ) } )
39 eqeq1 
 |-  ( X = [ x ] .~ -> ( X = { z | E. y e. B z = ( x .+ ( y .x. M ) ) } <-> [ x ] .~ = { z | E. y e. B z = ( x .+ ( y .x. M ) ) } ) )
40 38 39 syl5ibrcom 
 |-  ( ( ph /\ x e. B ) -> ( X = [ x ] .~ -> X = { z | E. y e. B z = ( x .+ ( y .x. M ) ) } ) )
41 40 ancld 
 |-  ( ( ph /\ x e. B ) -> ( X = [ x ] .~ -> ( X = [ x ] .~ /\ X = { z | E. y e. B z = ( x .+ ( y .x. M ) ) } ) ) )
42 41 reximdva 
 |-  ( ph -> ( E. x e. B X = [ x ] .~ -> E. x e. B ( X = [ x ] .~ /\ X = { z | E. y e. B z = ( x .+ ( y .x. M ) ) } ) ) )
43 12 42 mpd 
 |-  ( ph -> E. x e. B ( X = [ x ] .~ /\ X = { z | E. y e. B z = ( x .+ ( y .x. M ) ) } ) )