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 ⊢ φ → I ∈ NrmSGrp ⁡ R
ecqusaddd.b ⊢ B = Base R
ecqusaddd.g ⊢ ∼ ˙ = R ~ QG I
ecqusaddd.q ⊢ Q = R / 𝑠 ∼ ˙
Assertion ecqusaddcl ⊢ φ ∧ A ∈ B ∧ C ∈ B → A ∼ ˙ + Q C ∼ ˙ ∈ Base Q

Proof

Step Hyp Ref Expression
1 ecqusaddd.i ⊢ φ → I ∈ NrmSGrp ⁡ R
2 ecqusaddd.b ⊢ B = Base R
3 ecqusaddd.g ⊢ ∼ ˙ = R ~ QG I
4 ecqusaddd.q ⊢ Q = R / 𝑠 ∼ ˙
5 1 2 3 4 ecqusaddd ⊢ φ ∧ A ∈ B ∧ C ∈ B → A + R C ∼ ˙ = A ∼ ˙ + Q C ∼ ˙
6 1 elfvexd ⊢ φ → R ∈ V
7 nsgsubg ⊢ I ∈ NrmSGrp ⁡ R → I ∈ SubGrp ⁡ R
8 subgrcl ⊢ I ∈ SubGrp ⁡ R → R ∈ Grp
9 1 7 8 3syl ⊢ φ → R ∈ Grp
10 9 anim1i ⊢ φ ∧ A ∈ B ∧ C ∈ B → R ∈ Grp ∧ A ∈ B ∧ C ∈ B
11 3anass ⊢ R ∈ Grp ∧ A ∈ B ∧ C ∈ B ↔ R ∈ Grp ∧ A ∈ B ∧ C ∈ B
12 10 11 sylibr ⊢ φ ∧ A ∈ B ∧ C ∈ B → R ∈ Grp ∧ A ∈ B ∧ C ∈ B
13 eqid ⊢ + R = + R
14 2 13 grpcl ⊢ R ∈ Grp ∧ A ∈ B ∧ C ∈ B → A + R C ∈ B
15 12 14 syl ⊢ φ ∧ A ∈ B ∧ C ∈ B → A + R C ∈ B
16 eqid ⊢ Base Q = Base Q
17 3 4 2 16 quseccl0 ⊢ R ∈ V ∧ A + R C ∈ B → A + R C ∼ ˙ ∈ Base Q
18 6 15 17 syl2an2r ⊢ φ ∧ A ∈ B ∧ C ∈ B → A + R C ∼ ˙ ∈ Base Q
19 5 18 eqeltrrd ⊢ φ ∧ A ∈ B ∧ C ∈ B → A ∼ ˙ + Q C ∼ ˙ ∈ Base Q