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

Metamath Proof Explorer

Theorem qusaddflem

Description: The operation of a quotient structure is 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
qusaddflem.f ⊢ F = x ∈ V ⟼ x ∼ ˙
qusaddflem.g ⊢ φ → ∙ ˙ = ⋃ p ∈ V ⋃ q ∈ V F ⁡ p F ⁡ q F ⁡ p · ˙ q
Assertion qusaddflem ⊢ φ → ∙ ˙ : 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 qusaddflem.f ⊢ F = x ∈ V ⟼ x ∼ ˙
8 qusaddflem.g ⊢ φ → ∙ ˙ = ⋃ p ∈ V ⋃ q ∈ V F ⁡ p F ⁡ q F ⁡ p · ˙ q
9 fvex ⊢ Base R ∈ V
10 2 9 eqeltrdi ⊢ φ → V ∈ V
11 erex ⊢ ∼ ˙ Er V → V ∈ V → ∼ ˙ ∈ V
12 3 10 11 sylc ⊢ φ → ∼ ˙ ∈ V
13 1 2 7 12 4 quslem ⊢ φ → F : V ⟶ onto V / ∼ ˙
14 3 10 7 6 5 ercpbl ⊢ φ ∧ a ∈ V ∧ b ∈ V ∧ p ∈ V ∧ q ∈ V → F ⁡ a = F ⁡ p ∧ F ⁡ b = F ⁡ q → F ⁡ a · ˙ b = F ⁡ p · ˙ q
15 13 14 8 6 imasaddflem ⊢ φ → ∙ ˙ : V / ∼ ˙ × V / ∼ ˙ ⟶ V / ∼ ˙