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 ⊢ ( 𝜑 → 𝐼 ∈ ( 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 ‘ 𝑄 ) )