ecqusaddcl

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

	Ref	Expression
Hypotheses	ecqusadd.i	$⊢ φ \to I \in NrmSGrp (R)$
	ecqusadd.b	$⊢ B = {Base}_{R}$
	ecqusadd.g	$⊢ \underset{˙}{\sim} = R ~_{QG} I$
	ecqusadd.q	$⊢ Q = R /_{𝑠} \underset{˙}{\sim}$
Assertion	ecqusaddcl	$⊢ (φ \land (A \in B \land C \in B)) \to [A] \underset{˙}{\sim} +_{Q} [C] \underset{˙}{\sim} \in {Base}_{Q}$

Step	Hyp	Ref	Expression
1		ecqusadd.i	$⊢ φ \to I \in NrmSGrp (R)$
2		ecqusadd.b	$⊢ B = {Base}_{R}$
3		ecqusadd.g	$⊢ \underset{˙}{\sim} = R ~_{QG} I$
4		ecqusadd.q	$⊢ Q = R /_{𝑠} \underset{˙}{\sim}$
5	1 2 3 4	ecqusadd	$⊢ (φ \land (A \in B \land C \in B)) \to [(A +_{R} C)] \underset{˙}{\sim} = [A] \underset{˙}{\sim} +_{Q} [C] \underset{˙}{\sim}$
6	1	elfvexd	$⊢ φ \to R \in V$
7		nsgsubg	$⊢ I \in NrmSGrp (R) \to I \in SubGrp (R)$
8		subgrcl	$⊢ I \in SubGrp (R) \to R \in Grp$
9	1 7 8	3syl	$⊢ φ \to R \in Grp$
10	9	anim1i	$⊢ (φ \land (A \in B \land C \in B)) \to (R \in Grp \land (A \in B \land C \in B))$
11		3anass	$⊢ (R \in Grp \land A \in B \land C \in B) \leftrightarrow (R \in Grp \land (A \in B \land C \in B))$
12	10 11	sylibr	$⊢ (φ \land (A \in B \land C \in B)) \to (R \in Grp \land A \in B \land C \in B)$
13		eqid	$⊢ +_{R} = +_{R}$
14	2 13	grpcl	$⊢ (R \in Grp \land A \in B \land C \in B) \to A +_{R} C \in B$
15	12 14	syl	$⊢ (φ \land (A \in B \land C \in B)) \to A +_{R} C \in B$
16		eqid	$⊢ {Base}_{Q} = {Base}_{Q}$
17	3 4 2 16	quseccl0	$⊢ (R \in V \land A +_{R} C \in B) \to [(A +_{R} C)] \underset{˙}{\sim} \in {Base}_{Q}$
18	6 15 17	syl2an2r	$⊢ (φ \land (A \in B \land C \in B)) \to [(A +_{R} C)] \underset{˙}{\sim} \in {Base}_{Q}$
19	5 18	eqeltrrd	$⊢ (φ \land (A \in B \land C \in B)) \to [A] \underset{˙}{\sim} +_{Q} [C] \underset{˙}{\sim} \in {Base}_{Q}$

Metamath Proof Explorer