Metamath Proof Explorer


Theorem imasaddval

Description: The value of an image structure's group operation. (Contributed by Mario Carneiro, 23-Feb-2015)

Ref Expression
Hypotheses imasaddf.f ( 𝜑𝐹 : 𝑉onto𝐵 )
imasaddf.e ( ( 𝜑 ∧ ( 𝑎𝑉𝑏𝑉 ) ∧ ( 𝑝𝑉𝑞𝑉 ) ) → ( ( ( 𝐹𝑎 ) = ( 𝐹𝑝 ) ∧ ( 𝐹𝑏 ) = ( 𝐹𝑞 ) ) → ( 𝐹 ‘ ( 𝑎 · 𝑏 ) ) = ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ) )
imasaddf.u ( 𝜑𝑈 = ( 𝐹s 𝑅 ) )
imasaddf.v ( 𝜑𝑉 = ( Base ‘ 𝑅 ) )
imasaddf.r ( 𝜑𝑅𝑍 )
imasaddf.p · = ( +g𝑅 )
imasaddf.a = ( +g𝑈 )
Assertion imasaddval ( ( 𝜑𝑋𝑉𝑌𝑉 ) → ( ( 𝐹𝑋 ) ( 𝐹𝑌 ) ) = ( 𝐹 ‘ ( 𝑋 · 𝑌 ) ) )

Proof

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