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