grpplusgx

Description: The operation of an explicitly given group. Note: This theorem has hard-coded structure indices for demonstration purposes. It is not intended for general use; use grpplusg instead. (New usage is discouraged.) (Contributed by NM, 17-Oct-2012)

	Ref	Expression
Hypotheses	grpstrx.b	$⊢ B \in V$
	grpstrx.p	$⊢ \underset{˙}{+} \in V$
	grpstrx.g	$⊢ G = \{⟨1, B⟩, ⟨2, \underset{˙}{+}⟩\}$
Assertion	grpplusgx	$⊢ \underset{˙}{+} = +_{G}$

Proof

Step	Hyp	Ref	Expression
1		grpstrx.b	$⊢ B \in V$
2		grpstrx.p	$⊢ \underset{˙}{+} \in V$
3		grpstrx.g	$⊢ G = \{⟨1, B⟩, ⟨2, \underset{˙}{+}⟩\}$
4		basendx	$⊢ {Base}_{ndx} = 1$
5	4	opeq1i	$⊢ ⟨{Base}_{ndx}, B⟩ = ⟨1, B⟩$
6		plusgndx	$⊢ +_{ndx} = 2$
7	6	opeq1i	$⊢ ⟨+_{ndx}, \underset{˙}{+}⟩ = ⟨2, \underset{˙}{+}⟩$
8	5 7	preq12i	$⊢ \{⟨{Base}_{ndx}, B⟩, ⟨+_{ndx}, \underset{˙}{+}⟩\} = \{⟨1, B⟩, ⟨2, \underset{˙}{+}⟩\}$
9	3 8	eqtr4i	$⊢ G = \{⟨{Base}_{ndx}, B⟩, ⟨+_{ndx}, \underset{˙}{+}⟩\}$
10	9	grpplusg	$⊢ \underset{˙}{+} \in V \to \underset{˙}{+} = +_{G}$
11	2 10	ax-mp	$⊢ \underset{˙}{+} = +_{G}$

Metamath Proof Explorer

Theorem grpplusgx

Proof