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

Metamath Proof Explorer

Theorem plusfval

Description: The group addition operation as a function. (Contributed by Mario Carneiro, 14-Aug-2015)

	Ref	Expression
Hypotheses	plusffval.1	$⊢ B = {Base}_{G}$
	plusffval.2	$⊢ \underset{˙}{+} = +_{G}$
	plusffval.3	$⊢ \underset{˙}{⨣} = +_{𝑓} (G)$
Assertion	plusfval	$⊢ (X \in B \land Y \in B) \to X \underset{˙}{⨣} Y = X \underset{˙}{+} Y$

Step	Hyp	Ref	Expression
1		plusffval.1	$⊢ B = {Base}_{G}$
2		plusffval.2	$⊢ \underset{˙}{+} = +_{G}$
3		plusffval.3	$⊢ \underset{˙}{⨣} = +_{𝑓} (G)$
4		oveq12	$⊢ (x = X \land y = Y) \to x \underset{˙}{+} y = X \underset{˙}{+} Y$
5	1 2 3	plusffval	$⊢ \underset{˙}{⨣} = (x \in B, y \in B ⟼ x \underset{˙}{+} y)$
6		ovex	$⊢ X \underset{˙}{+} Y \in V$
7	4 5 6	ovmpoa	$⊢ (X \in B \land Y \in B) \to X \underset{˙}{⨣} Y = X \underset{˙}{+} Y$