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

Metamath Proof Explorer

Theorem grpstr

Description: A constructed group is a structure. Version not depending on the implementation of the indices. (Contributed by AV, 27-Oct-2024)

		Ref	Expression
	Hypothesis	grpfn.g	$⊢ G = \{⟨{Base}_{ndx}, B⟩, ⟨+_{ndx}, \underset{˙}{+}⟩\}$
	Assertion	grpstr	$⊢ G Struct ⟨{Base}_{ndx}, +_{ndx}⟩$

Step	Hyp	Ref	Expression
1		grpfn.g	$⊢ G = \{⟨{Base}_{ndx}, B⟩, ⟨+_{ndx}, \underset{˙}{+}⟩\}$
2		basendxltplusgndx	$⊢ {Base}_{ndx} < +_{ndx}$
3		plusgndxnn	$⊢ +_{ndx} \in ℕ$
4	1 2 3	2strstr	$⊢ G Struct ⟨{Base}_{ndx}, +_{ndx}⟩$