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=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨{+}_{\mathrm{ndx}},\underset{\dot{}}{+}⟩\right\}$$
Assertion	grpstr	$$⊢G\mathrm{Struct}⟨{\mathrm{Base}}_{\mathrm{ndx}},{+}_{\mathrm{ndx}}⟩$$

Proof

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