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 )