Theorem imasmulfn

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

	Ref	Expression
Hypotheses	imasaddf.f	$$⊢\phi \to F:V\underset{onto}{⟶}B$$
	imasaddf.e	$$⊢\left(\phi \wedge \left(a\in V\wedge b\in V\right)\wedge \left(p\in V\wedge q\in V\right)\right)\to \left(\left(F\left(a\right)=F\left(p\right)\wedge F\left(b\right)=F\left(q\right)\right)\to F\left(a\underset{\dot{}}{·}b\right)=F\left(p\underset{\dot{}}{·}q\right)\right)$$
	imasaddf.u	$$⊢\phi \to U=F{“}_{𝑠}R$$
	imasaddf.v	$$⊢\phi \to V={\mathrm{Base}}_R$$
	imasaddf.r	$$⊢\phi \to R\in Z$$
	imasmulf.p	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
	imasmulf.a	$$⊢\underset{\dot{}}{\bullet }={\cdot }_U$$
Assertion	imasmulfn	$$⊢\phi \to \underset{\dot{}}{\bullet }Fn\left(B\times B\right)$$

Proof

Step	Hyp	Ref	Expression
1		imasaddf.f	$$⊢\phi \to F:V\underset{onto}{⟶}B$$
2		imasaddf.e	$$⊢\left(\phi \wedge \left(a\in V\wedge b\in V\right)\wedge \left(p\in V\wedge q\in V\right)\right)\to \left(\left(F\left(a\right)=F\left(p\right)\wedge F\left(b\right)=F\left(q\right)\right)\to F\left(a\underset{\dot{}}{·}b\right)=F\left(p\underset{\dot{}}{·}q\right)\right)$$
3		imasaddf.u	$$⊢\phi \to U=F{“}_{𝑠}R$$
4		imasaddf.v	$$⊢\phi \to V={\mathrm{Base}}_R$$
5		imasaddf.r	$$⊢\phi \to R\in Z$$
6		imasmulf.p	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
7		imasmulf.a	$$⊢\underset{\dot{}}{\bullet }={\cdot }_U$$
8	3 4 1 5 6 7	imasmulr	$$⊢\phi \to \underset{\dot{}}{\bullet }=\bigcup _{p\in V}\bigcup _{q\in V}\left\{⟨⟨F\left(p\right),F\left(q\right)⟩,F\left(p\underset{\dot{}}{·}q\right)⟩\right\}$$
9	1 2 8	imasaddfnlem	$$⊢\phi \to \underset{\dot{}}{\bullet }Fn\left(B\times B\right)$$