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 / ˙