Metamath Proof Explorer


Theorem imasaddfn

Description: The image structure's group operation is a function. (Contributed by Mario Carneiro, 23-Feb-2015) (Revised by Mario Carneiro, 10-Jul-2015)

Ref Expression
Hypotheses imasaddf.f φ F : V onto B
imasaddf.e φ a V b V p V q V F a = F p F b = F q F a · ˙ b = F p · ˙ q
imasaddf.u φ U = F 𝑠 R
imasaddf.v φ V = Base R
imasaddf.r φ R Z
imasaddf.p · ˙ = + R
imasaddf.a ˙ = + U
Assertion imasaddfn φ ˙ Fn B × B

Proof

Step Hyp Ref Expression
1 imasaddf.f φ F : V onto B
2 imasaddf.e φ a V b V p V q V F a = F p F b = F q F a · ˙ b = F p · ˙ q
3 imasaddf.u φ U = F 𝑠 R
4 imasaddf.v φ V = Base R
5 imasaddf.r φ R Z
6 imasaddf.p · ˙ = + R
7 imasaddf.a ˙ = + U
8 3 4 1 5 6 7 imasplusg φ ˙ = p V q V F p F q F p · ˙ q
9 1 2 8 imasaddfnlem φ ˙ Fn B × B