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

Metamath Proof Explorer

Theorem ecqusaddcl

Description: Closure of the addition in a quotient group. (Contributed by AV, 24-Feb-2025)

Ref Expression
Hypotheses ecqusaddd.i 
|- ( ph -> I e. ( NrmSGrp ` R ) )
ecqusaddd.b 
|- B = ( Base ` R )
ecqusaddd.g 
|- .~ = ( R ~QG I )
ecqusaddd.q 
|- Q = ( R /s .~ )
Assertion ecqusaddcl 
|- ( ( ph /\ ( A e. B /\ C e. B ) ) -> ( [ A ] .~ ( +g ` Q ) [ C ] .~ ) e. ( Base ` Q ) )

Proof

Step Hyp Ref Expression
1 ecqusaddd.i 
 |-  ( ph -> I e. ( NrmSGrp ` R ) )
2 ecqusaddd.b 
 |-  B = ( Base ` R )
3 ecqusaddd.g 
 |-  .~ = ( R ~QG I )
4 ecqusaddd.q 
 |-  Q = ( R /s .~ )
5 1 2 3 4 ecqusaddd 
 |-  ( ( ph /\ ( A e. B /\ C e. B ) ) -> [ ( A ( +g ` R ) C ) ] .~ = ( [ A ] .~ ( +g ` Q ) [ C ] .~ ) )
6 1 elfvexd 
 |-  ( ph -> R e. _V )
7 nsgsubg 
 |-  ( I e. ( NrmSGrp ` R ) -> I e. ( SubGrp ` R ) )
8 subgrcl 
 |-  ( I e. ( SubGrp ` R ) -> R e. Grp )
9 1 7 8 3syl 
 |-  ( ph -> R e. Grp )
10 9 anim1i 
 |-  ( ( ph /\ ( A e. B /\ C e. B ) ) -> ( R e. Grp /\ ( A e. B /\ C e. B ) ) )
11 3anass 
 |-  ( ( R e. Grp /\ A e. B /\ C e. B ) <-> ( R e. Grp /\ ( A e. B /\ C e. B ) ) )
12 10 11 sylibr 
 |-  ( ( ph /\ ( A e. B /\ C e. B ) ) -> ( R e. Grp /\ A e. B /\ C e. B ) )
13 eqid 
 |-  ( +g ` R ) = ( +g ` R )
14 2 13 grpcl 
 |-  ( ( R e. Grp /\ A e. B /\ C e. B ) -> ( A ( +g ` R ) C ) e. B )
15 12 14 syl 
 |-  ( ( ph /\ ( A e. B /\ C e. B ) ) -> ( A ( +g ` R ) C ) e. B )
16 eqid 
 |-  ( Base ` Q ) = ( Base ` Q )
17 3 4 2 16 quseccl0 
 |-  ( ( R e. _V /\ ( A ( +g ` R ) C ) e. B ) -> [ ( A ( +g ` R ) C ) ] .~ e. ( Base ` Q ) )
18 6 15 17 syl2an2r 
 |-  ( ( ph /\ ( A e. B /\ C e. B ) ) -> [ ( A ( +g ` R ) C ) ] .~ e. ( Base ` Q ) )
19 5 18 eqeltrrd 
 |-  ( ( ph /\ ( A e. B /\ C e. B ) ) -> ( [ A ] .~ ( +g ` Q ) [ C ] .~ ) e. ( Base ` Q ) )