Metamath Proof Explorer


Theorem imasmulval

Description: The value of an image structure's ring multiplication. (Contributed by Mario Carneiro, 23-Feb-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
imasmulf.p · ˙ = R
imasmulf.a ˙ = U
Assertion imasmulval φ X V Y V F X ˙ F Y = F X · ˙ Y

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 imasmulf.p · ˙ = R
7 imasmulf.a ˙ = U
8 3 4 1 5 6 7 imasmulr φ ˙ = p V q V F p F q F p · ˙ q
9 1 2 8 imasaddvallem φ X V Y V F X ˙ F Y = F X · ˙ Y