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

Metamath Proof Explorer

Theorem plusfeq

Description: If the addition operation is already a function, the functionalization of it is equal to the original operation. (Contributed by Mario Carneiro, 14-Aug-2015)

		Ref	Expression
	Hypotheses	plusffval.1	$⊢ B = {Base}_{G}$
		plusffval.2	$⊢ \underset{˙}{+} = +_{G}$
		plusffval.3	$⊢ \underset{˙}{⨣} = +_{𝑓} (G)$
	Assertion	plusfeq	$⊢ \underset{˙}{+} Fn (B \times B) \to \underset{˙}{⨣} = \underset{˙}{+}$

Proof

Step	Hyp	Ref	Expression
1		plusffval.1	$⊢ B = {Base}_{G}$
2		plusffval.2	$⊢ \underset{˙}{+} = +_{G}$
3		plusffval.3	$⊢ \underset{˙}{⨣} = +_{𝑓} (G)$
4	1 2 3	plusffval	$⊢ \underset{˙}{⨣} = (x \in B, y \in B ⟼ x \underset{˙}{+} y)$
5		fnov	$⊢ \underset{˙}{+} Fn (B \times B) \leftrightarrow \underset{˙}{+} = (x \in B, y \in B ⟼ x \underset{˙}{+} y)$
6	5	biimpi	$⊢ \underset{˙}{+} Fn (B \times B) \to \underset{˙}{+} = (x \in B, y \in B ⟼ x \underset{˙}{+} y)$
7	4 6	eqtr4id	$⊢ \underset{˙}{+} Fn (B \times B) \to \underset{˙}{⨣} = \underset{˙}{+}$