This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem qusaddf

Description: The addition in a quotient structure as a function. (Contributed by Mario Carneiro, 24-Feb-2015)

Ref Expression
Hypotheses qusaddf.u ⊢ φ → U = R / 𝑠 ∼ ˙
qusaddf.v ⊢ φ → V = Base R
qusaddf.r ⊢ φ → ∼ ˙ Er V
qusaddf.z ⊢ φ → R ∈ Z
qusaddf.e ⊢ φ → a ∼ ˙ p ∧ b ∼ ˙ q → a · ˙ b ∼ ˙ p · ˙ q
qusaddf.c ⊢ φ ∧ p ∈ V ∧ q ∈ V → p · ˙ q ∈ V
qusaddf.p ⊢ · ˙ = + R
qusaddf.a ⊢ ∙ ˙ = + U
Assertion qusaddf ⊢ φ → ∙ ˙ : V / ∼ ˙ × V / ∼ ˙ ⟶ V / ∼ ˙

Proof

Step Hyp Ref Expression
1 qusaddf.u ⊢ φ → U = R / 𝑠 ∼ ˙
2 qusaddf.v ⊢ φ → V = Base R
3 qusaddf.r ⊢ φ → ∼ ˙ Er V
4 qusaddf.z ⊢ φ → R ∈ Z
5 qusaddf.e ⊢ φ → a ∼ ˙ p ∧ b ∼ ˙ q → a · ˙ b ∼ ˙ p · ˙ q
6 qusaddf.c ⊢ φ ∧ p ∈ V ∧ q ∈ V → p · ˙ q ∈ V
7 qusaddf.p ⊢ · ˙ = + R
8 qusaddf.a ⊢ ∙ ˙ = + U
9 eqid ⊢ x ∈ V ⟼ x ∼ ˙ = x ∈ V ⟼ x ∼ ˙
10 fvex ⊢ Base R ∈ V
11 2 10 eqeltrdi ⊢ φ → V ∈ V
12 erex ⊢ ∼ ˙ Er V → V ∈ V → ∼ ˙ ∈ V
13 3 11 12 sylc ⊢ φ → ∼ ˙ ∈ V
14 1 2 9 13 4 qusval ⊢ φ → U = x ∈ V ⟼ x ∼ ˙ “ 𝑠 R
15 1 2 9 13 4 quslem ⊢ φ → x ∈ V ⟼ x ∼ ˙ : V ⟶ onto V / ∼ ˙
16 14 2 15 4 7 8 imasplusg ⊢ φ → ∙ ˙ = ⋃ p ∈ V ⋃ q ∈ V x ∈ V ⟼ x ∼ ˙ ⁡ p x ∈ V ⟼ x ∼ ˙ ⁡ q x ∈ V ⟼ x ∼ ˙ ⁡ p · ˙ q
17 1 2 3 4 5 6 9 16 qusaddflem ⊢ φ → ∙ ˙ : V / ∼ ˙ × V / ∼ ˙ ⟶ V / ∼ ˙