Metamath Proof Explorer

Theorem ecqusadd

Description: Addition of equivalence classes in a quotient group. (Contributed by AV, 25-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	ecqusadd	$⊢ (φ \land (A \in B \land C \in B)) \to [(A +_{R} C)] \underset{˙}{\sim} = [A] \underset{˙}{\sim} +_{Q} [C] \underset{˙}{\sim}$

Proof

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	anim1i	$⊢ (φ \land (A \in B \land C \in B)) \to (I \in NrmSGrp (R) \land (A \in B \land C \in B))$
6		3anass	$⊢ (I \in NrmSGrp (R) \land A \in B \land C \in B) \leftrightarrow (I \in NrmSGrp (R) \land (A \in B \land C \in B))$
7	5 6	sylibr	$⊢ (φ \land (A \in B \land C \in B)) \to (I \in NrmSGrp (R) \land A \in B \land C \in B)$
8	3	oveq2i	$⊢ R /_{𝑠} \underset{˙}{\sim} = R /_{𝑠} (R ~_{QG} I)$
9	4 8	eqtri	$⊢ Q = R /_{𝑠} (R ~_{QG} I)$
10		eqid	$⊢ +_{R} = +_{R}$
11		eqid	$⊢ +_{Q} = +_{Q}$
12	9 2 10 11	qusadd	$⊢ (I \in NrmSGrp (R) \land A \in B \land C \in B) \to [A] (R ~_{QG} I) +_{Q} [C] (R ~_{QG} I) = [(A +_{R} C)] (R ~_{QG} I)$
13	7 12	syl	$⊢ (φ \land (A \in B \land C \in B)) \to [A] (R ~_{QG} I) +_{Q} [C] (R ~_{QG} I) = [(A +_{R} C)] (R ~_{QG} I)$
14	3	eceq2i	$⊢ [A] \underset{˙}{\sim} = [A] (R ~_{QG} I)$
15	3	eceq2i	$⊢ [C] \underset{˙}{\sim} = [C] (R ~_{QG} I)$
16	14 15	oveq12i	$⊢ [A] \underset{˙}{\sim} +_{Q} [C] \underset{˙}{\sim} = [A] (R ~_{QG} I) +_{Q} [C] (R ~_{QG} I)$
17	3	eceq2i	$⊢ [(A +_{R} C)] \underset{˙}{\sim} = [(A +_{R} C)] (R ~_{QG} I)$
18	13 16 17	3eqtr4g	$⊢ (φ \land (A \in B \land C \in B)) \to [A] \underset{˙}{\sim} +_{Q} [C] \underset{˙}{\sim} = [(A +_{R} C)] \underset{˙}{\sim}$
19	18	eqcomd	$⊢ (φ \land (A \in B \land C \in B)) \to [(A +_{R} C)] \underset{˙}{\sim} = [A] \underset{˙}{\sim} +_{Q} [C] \underset{˙}{\sim}$