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 ( 𝜑𝐹 : 𝑉onto𝐵 )
imasaddf.e ( ( 𝜑 ∧ ( 𝑎𝑉𝑏𝑉 ) ∧ ( 𝑝𝑉𝑞𝑉 ) ) → ( ( ( 𝐹𝑎 ) = ( 𝐹𝑝 ) ∧ ( 𝐹𝑏 ) = ( 𝐹𝑞 ) ) → ( 𝐹 ‘ ( 𝑎 · 𝑏 ) ) = ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ) )
imasaddf.u ( 𝜑𝑈 = ( 𝐹s 𝑅 ) )
imasaddf.v ( 𝜑𝑉 = ( Base ‘ 𝑅 ) )
imasaddf.r ( 𝜑𝑅𝑍 )
imasmulf.p · = ( .r𝑅 )
imasmulf.a = ( .r𝑈 )
Assertion imasmulfn ( 𝜑 Fn ( 𝐵 × 𝐵 ) )

Proof

Step Hyp Ref Expression
1 imasaddf.f ( 𝜑𝐹 : 𝑉onto𝐵 )
2 imasaddf.e ( ( 𝜑 ∧ ( 𝑎𝑉𝑏𝑉 ) ∧ ( 𝑝𝑉𝑞𝑉 ) ) → ( ( ( 𝐹𝑎 ) = ( 𝐹𝑝 ) ∧ ( 𝐹𝑏 ) = ( 𝐹𝑞 ) ) → ( 𝐹 ‘ ( 𝑎 · 𝑏 ) ) = ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ) )
3 imasaddf.u ( 𝜑𝑈 = ( 𝐹s 𝑅 ) )
4 imasaddf.v ( 𝜑𝑉 = ( Base ‘ 𝑅 ) )
5 imasaddf.r ( 𝜑𝑅𝑍 )
6 imasmulf.p · = ( .r𝑅 )
7 imasmulf.a = ( .r𝑈 )
8 3 4 1 5 6 7 imasmulr ( 𝜑 = 𝑝𝑉 𝑞𝑉 { ⟨ ⟨ ( 𝐹𝑝 ) , ( 𝐹𝑞 ) ⟩ , ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ⟩ } )
9 1 2 8 imasaddfnlem ( 𝜑 Fn ( 𝐵 × 𝐵 ) )