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	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ( ( 𝐹 ‘ 𝑋 ) ∙ ( 𝐹 ‘ 𝑌 ) ) = ( 𝐹 ‘ ( 𝑋 · 𝑌 ) ) )