This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem grppropstr

Description: Generalize a specific 2-element group L to show that any set K with the same (relevant) properties is also a group. (Contributed by NM, 28-Oct-2012) (Revised by Mario Carneiro, 6-Jan-2015)

Ref Expression
Hypotheses grppropstr.b ⊢ ( Base ‘ 𝐾 ) = 𝐵
grppropstr.p ⊢ ( +g ‘ 𝐾 ) = +
grppropstr.l ⊢ 𝐿 = { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ }
Assertion grppropstr ( 𝐾 ∈ Grp ↔ 𝐿 ∈ Grp )

Proof

Step Hyp Ref Expression
1 grppropstr.b ⊢ ( Base ‘ 𝐾 ) = 𝐵
2 grppropstr.p ⊢ ( +g ‘ 𝐾 ) = +
3 grppropstr.l ⊢ 𝐿 = { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ }
4 fvex ⊢ ( Base ‘ 𝐾 ) ∈ V
5 1 4 eqeltrri ⊢ 𝐵 ∈ V
6 3 grpbase ⊢ ( 𝐵 ∈ V → 𝐵 = ( Base ‘ 𝐿 ) )
7 5 6 ax-mp ⊢ 𝐵 = ( Base ‘ 𝐿 )
8 1 7 eqtri ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐿 )
9 fvex ⊢ ( +g ‘ 𝐾 ) ∈ V
10 2 9 eqeltrri ⊢ + ∈ V
11 3 grpplusg ⊢ ( + ∈ V → + = ( +g ‘ 𝐿 ) )
12 10 11 ax-mp ⊢ + = ( +g ‘ 𝐿 )
13 2 12 eqtri ⊢ ( +g ‘ 𝐾 ) = ( +g ‘ 𝐿 )
14 8 13 grpprop ⊢ ( 𝐾 ∈ Grp ↔ 𝐿 ∈ Grp )