Metamath Proof Explorer


Theorem 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 ‘ 𝐺 )