Metamath Proof Explorer

Theorem ecqusaddd

Description: Addition of equivalence classes in a quotient group. (Contributed by AV, 25-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 ecqusaddd ⊢ φ ∧ A ∈ B ∧ C ∈ B → A + R C ∼ ˙ = A ∼ ˙ + Q C ∼ ˙

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 anim1i ⊢ φ ∧ A ∈ B ∧ C ∈ B → I ∈ NrmSGrp ⁡ R ∧ A ∈ B ∧ C ∈ B
6 3anass ⊢ I ∈ NrmSGrp ⁡ R ∧ A ∈ B ∧ C ∈ B ↔ I ∈ NrmSGrp ⁡ R ∧ A ∈ B ∧ C ∈ B
7 5 6 sylibr ⊢ φ ∧ A ∈ B ∧ C ∈ B → I ∈ NrmSGrp ⁡ R ∧ A ∈ B ∧ C ∈ B
8 3 oveq2i ⊢ R / 𝑠 ∼ ˙ = 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 ∈ NrmSGrp ⁡ R ∧ A ∈ B ∧ C ∈ B → A R ~ QG I + Q C R ~ QG I = A + R C R ~ QG I
13 7 12 syl ⊢ φ ∧ A ∈ B ∧ C ∈ B → A R ~ QG I + Q C R ~ QG I = A + R C R ~ QG I
14 3 eceq2i ⊢ A ∼ ˙ = A R ~ QG I
15 3 eceq2i ⊢ C ∼ ˙ = C R ~ QG I
16 14 15 oveq12i ⊢ A ∼ ˙ + Q C ∼ ˙ = A R ~ QG I + Q C R ~ QG I
17 3 eceq2i ⊢ A + R C ∼ ˙ = A + R C R ~ QG I
18 13 16 17 3eqtr4g ⊢ φ ∧ A ∈ B ∧ C ∈ B → A ∼ ˙ + Q C ∼ ˙ = A + R C ∼ ˙
19 18 eqcomd ⊢ φ ∧ A ∈ B ∧ C ∈ B → A + R C ∼ ˙ = A ∼ ˙ + Q C ∼ ˙