grpbasex

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

	Ref	Expression
Hypotheses	grpstrx.b	\|- B e. _V
	grpstrx.p	\|- .+ e. _V
	grpstrx.g	\|- G = { <. 1 , B >. , <. 2 , .+ >. }
Assertion	grpbasex	\|- B = ( Base ` G )

Proof

Step	Hyp	Ref	Expression
1		grpstrx.b	\|- B e. _V
2		grpstrx.p	\|- .+ e. _V
3		grpstrx.g	\|- G = { <. 1 , B >. , <. 2 , .+ >. }
4		basendx	\|- ( Base ` ndx ) = 1
5	4	opeq1i	\|- <. ( Base ` ndx ) , B >. = <. 1 , B >.
6		plusgndx	\|- ( +g ` ndx ) = 2
7	6	opeq1i	\|- <. ( +g ` ndx ) , .+ >. = <. 2 , .+ >.
8	5 7	preq12i	\|- { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. } = { <. 1 , B >. , <. 2 , .+ >. }
9	3 8	eqtr4i	\|- G = { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. }
10	9	grpbase	\|- ( B e. _V -> B = ( Base ` G ) )
11	1 10	ax-mp	\|- B = ( Base ` G )

Metamath Proof Explorer

Theorem grpbasex

Proof