This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem plusffn

Description: The group addition operation is a function. (Contributed by Mario Carneiro, 20-Sep-2015)

Ref Expression
Hypotheses plusffn.1 ⊢ 𝐵 = ( Base ‘ 𝐺 )
plusffn.2 ⊢ ⨣ = ( +𝑓 ‘ 𝐺 )
Assertion plusffn ⨣ Fn ( 𝐵 × 𝐵 )

Proof

Step Hyp Ref Expression
1 plusffn.1 ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 plusffn.2 ⊢ ⨣ = ( +𝑓 ‘ 𝐺 )
3 eqid ⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
4 1 3 2 plusffval ⊢ ⨣ = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) )
5 ovex ⊢ ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ V
6 4 5 fnmpoi ⊢ ⨣ Fn ( 𝐵 × 𝐵 )