Metamath Proof Explorer


Theorem imasmulfn

Description: The image structure's ring multiplication is a function. (Contributed by Mario Carneiro, 23-Feb-2015)

Ref Expression
Hypotheses imasaddf.f φF:VontoB
imasaddf.e φaVbVpVqVFa=FpFb=FqFa·˙b=Fp·˙q
imasaddf.u φU=F𝑠R
imasaddf.v φV=BaseR
imasaddf.r φRZ
imasmulf.p ·˙=R
imasmulf.a ˙=U
Assertion imasmulfn φ˙FnB×B

Proof

Step Hyp Ref Expression
1 imasaddf.f φF:VontoB
2 imasaddf.e φaVbVpVqVFa=FpFb=FqFa·˙b=Fp·˙q
3 imasaddf.u φU=F𝑠R
4 imasaddf.v φV=BaseR
5 imasaddf.r φRZ
6 imasmulf.p ·˙=R
7 imasmulf.a ˙=U
8 3 4 1 5 6 7 imasmulr φ˙=pVqVFpFqFp·˙q
9 1 2 8 imasaddfnlem φ˙FnB×B