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 | ⊢ 𝐵 ∈ V | |
grpstrx.p | ⊢ + ∈ V | ||
grpstrx.g | ⊢ 𝐺 = { ⟨ 1 , 𝐵 ⟩ , ⟨ 2 , + ⟩ } | ||
Assertion | grpplusgx | ⊢ + = ( +g ‘ 𝐺 ) |
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 | grpplusg | ⊢ ( + ∈ V → + = ( +g ‘ 𝐺 ) ) |
11 | 2 10 | ax-mp | ⊢ + = ( +g ‘ 𝐺 ) |