Metamath Proof Explorer


Theorem qusaddvallem

Description: Value of an operation defined on a quotient structure. (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 qusaddvallem φ X V Y V X ˙ ˙ Y ˙ = X · ˙ Y ˙

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 imasaddvallem φ X V Y V F X ˙ F Y = F X · ˙ Y
16 3 3ad2ant1 φ X V Y V ˙ Er V
17 10 3ad2ant1 φ X V Y V V V
18 16 17 7 divsfval φ X V Y V F X = X ˙
19 16 17 7 divsfval φ X V Y V F Y = Y ˙
20 18 19 oveq12d φ X V Y V F X ˙ F Y = X ˙ ˙ Y ˙
21 16 17 7 divsfval φ X V Y V F X · ˙ Y = X · ˙ Y ˙
22 15 20 21 3eqtr3d φ X V Y V X ˙ ˙ Y ˙ = X · ˙ Y ˙