Theorem ecqusaddcl

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

	Ref	Expression
Hypotheses	ecqusaddd.i	⊢ ( 𝜑 → 𝐼 ∈ ( NrmSGrp ‘ 𝑅 ) )
	ecqusaddd.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
	ecqusaddd.g	⊢ ∼ = ( 𝑅 ~QG 𝐼 )
	ecqusaddd.q	⊢ 𝑄 = ( 𝑅 /s ∼ )
Assertion	ecqusaddcl	⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝐵 ∧ 𝐶 ∈ 𝐵 ) ) → ( [ 𝐴 ] ∼ ( +g ‘ 𝑄 ) [ 𝐶 ] ∼ ) ∈ ( Base ‘ 𝑄 ) )

Proof

Step	Hyp	Ref	Expression
1		ecqusaddd.i	⊢ ( 𝜑 → 𝐼 ∈ ( NrmSGrp ‘ 𝑅 ) )
2		ecqusaddd.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
3		ecqusaddd.g	⊢ ∼ = ( 𝑅 ~QG 𝐼 )
4		ecqusaddd.q	⊢ 𝑄 = ( 𝑅 /s ∼ )
5	1 2 3 4	ecqusaddd	⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝐵 ∧ 𝐶 ∈ 𝐵 ) ) → [ ( 𝐴 ( +g ‘ 𝑅 ) 𝐶 ) ] ∼ = ( [ 𝐴 ] ∼ ( +g ‘ 𝑄 ) [ 𝐶 ] ∼ ) )
6	1	elfvexd	⊢ ( 𝜑 → 𝑅 ∈ V )
7		nsgsubg	⊢ ( 𝐼 ∈ ( NrmSGrp ‘ 𝑅 ) → 𝐼 ∈ ( SubGrp ‘ 𝑅 ) )
8		subgrcl	⊢ ( 𝐼 ∈ ( SubGrp ‘ 𝑅 ) → 𝑅 ∈ Grp )
9	1 7 8	3syl	⊢ ( 𝜑 → 𝑅 ∈ Grp )
10	9	anim1i	⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝐵 ∧ 𝐶 ∈ 𝐵 ) ) → ( 𝑅 ∈ Grp ∧ ( 𝐴 ∈ 𝐵 ∧ 𝐶 ∈ 𝐵 ) ) )
11		3anass	⊢ ( ( 𝑅 ∈ Grp ∧ 𝐴 ∈ 𝐵 ∧ 𝐶 ∈ 𝐵 ) ↔ ( 𝑅 ∈ Grp ∧ ( 𝐴 ∈ 𝐵 ∧ 𝐶 ∈ 𝐵 ) ) )
12	10 11	sylibr	⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝐵 ∧ 𝐶 ∈ 𝐵 ) ) → ( 𝑅 ∈ Grp ∧ 𝐴 ∈ 𝐵 ∧ 𝐶 ∈ 𝐵 ) )
13		eqid	⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 )
14	2 13	grpcl	⊢ ( ( 𝑅 ∈ Grp ∧ 𝐴 ∈ 𝐵 ∧ 𝐶 ∈ 𝐵 ) → ( 𝐴 ( +g ‘ 𝑅 ) 𝐶 ) ∈ 𝐵 )
15	12 14	syl	⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝐵 ∧ 𝐶 ∈ 𝐵 ) ) → ( 𝐴 ( +g ‘ 𝑅 ) 𝐶 ) ∈ 𝐵 )
16		eqid	⊢ ( Base ‘ 𝑄 ) = ( Base ‘ 𝑄 )
17	3 4 2 16	quseccl0	⊢ ( ( 𝑅 ∈ V ∧ ( 𝐴 ( +g ‘ 𝑅 ) 𝐶 ) ∈ 𝐵 ) → [ ( 𝐴 ( +g ‘ 𝑅 ) 𝐶 ) ] ∼ ∈ ( Base ‘ 𝑄 ) )
18	6 15 17	syl2an2r	⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝐵 ∧ 𝐶 ∈ 𝐵 ) ) → [ ( 𝐴 ( +g ‘ 𝑅 ) 𝐶 ) ] ∼ ∈ ( Base ‘ 𝑄 ) )
19	5 18	eqeltrrd	⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝐵 ∧ 𝐶 ∈ 𝐵 ) ) → ( [ 𝐴 ] ∼ ( +g ‘ 𝑄 ) [ 𝐶 ] ∼ ) ∈ ( Base ‘ 𝑄 ) )