Theorem 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 \mathrm{V}$$
	grpstrx.p	$$⊢\underset{\dot{}}{+}\in \mathrm{V}$$
	grpstrx.g	$$⊢G=\left\{⟨1,B⟩,⟨2,\underset{\dot{}}{+}⟩\right\}$$
Assertion	grpplusgx	$$⊢\underset{\dot{}}{+}={+}_G$$

Proof

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