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	⊢ 𝐵 ∈ V
	grpstrx.p	⊢ + ∈ V
	grpstrx.g	⊢ 𝐺 = { ⟨ 1 , 𝐵 ⟩ , ⟨ 2 , + ⟩ }
Assertion	grpbasex	⊢ 𝐵 = ( Base ‘ 𝐺 )

Proof

Step	Hyp	Ref	Expression
1		grpstrx.b	⊢ 𝐵 ∈ V
2		grpstrx.p	⊢ + ∈ V
3		grpstrx.g	⊢ 𝐺 = { ⟨ 1 , 𝐵 ⟩ , ⟨ 2 , + ⟩ }
4		basendx	⊢ ( Base ‘ ndx ) = 1
5	4	opeq1i	⊢ ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ = ⟨ 1 , 𝐵 ⟩
6		plusgndx	⊢ ( +_g ‘ ndx ) = 2
7	6	opeq1i	⊢ ⟨ ( +_g ‘ ndx ) , + ⟩ = ⟨ 2 , + ⟩
8	5 7	preq12i	⊢ { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +_g ‘ ndx ) , + ⟩ } = { ⟨ 1 , 𝐵 ⟩ , ⟨ 2 , + ⟩ }
9	3 8	eqtr4i	⊢ 𝐺 = { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +_g ‘ ndx ) , + ⟩ }
10	9	grpbase	⊢ ( 𝐵 ∈ V → 𝐵 = ( Base ‘ 𝐺 ) )
11	1 10	ax-mp	⊢ 𝐵 = ( Base ‘ 𝐺 )

Metamath Proof Explorer

Theorem grpbasex

Proof