Theorem sgrp1

Description: The structure with one element and the only closed internal operation for a singleton is a semigroup. (Contributed by AV, 10-Feb-2020)

	Ref	Expression
Hypothesis	sgrp1.m	$$⊢M=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\left\{I\right\}⟩,⟨{+}_{\mathrm{ndx}},\left\{⟨⟨I,I⟩,I⟩\right\}⟩\right\}$$
Assertion	sgrp1	Could not format assertion : No typesetting found for |- ( I e. V -> M e. Smgrp ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		sgrp1.m	$$⊢M=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\left\{I\right\}⟩,⟨{+}_{\mathrm{ndx}},\left\{⟨⟨I,I⟩,I⟩\right\}⟩\right\}$$
2	1	mgm1	$$⊢I\in V\to M\in \mathrm{Mgm}$$
3		df-ov	$$⊢I\left\{⟨⟨I,I⟩,I⟩\right\}I=\left\{⟨⟨I,I⟩,I⟩\right\}\left(⟨I,I⟩\right)$$
4		opex	$$⊢⟨I,I⟩\in \mathrm{V}$$
5		fvsng	$$⊢\left(⟨I,I⟩\in \mathrm{V}\wedge I\in V\right)\to \left\{⟨⟨I,I⟩,I⟩\right\}\left(⟨I,I⟩\right)=I$$
6	4 5	mpan	$$⊢I\in V\to \left\{⟨⟨I,I⟩,I⟩\right\}\left(⟨I,I⟩\right)=I$$
7	3 6	eqtrid	$$⊢I\in V\to I\left\{⟨⟨I,I⟩,I⟩\right\}I=I$$
8	7	oveq1d	$$⊢I\in V\to \left(I\left\{⟨⟨I,I⟩,I⟩\right\}I\right)\left\{⟨⟨I,I⟩,I⟩\right\}I=I\left\{⟨⟨I,I⟩,I⟩\right\}I$$
9	7	oveq2d	$$⊢I\in V\to I\left\{⟨⟨I,I⟩,I⟩\right\}\left(I\left\{⟨⟨I,I⟩,I⟩\right\}I\right)=I\left\{⟨⟨I,I⟩,I⟩\right\}I$$
10	8 9	eqtr4d	$$⊢I\in V\to \left(I\left\{⟨⟨I,I⟩,I⟩\right\}I\right)\left\{⟨⟨I,I⟩,I⟩\right\}I=I\left\{⟨⟨I,I⟩,I⟩\right\}\left(I\left\{⟨⟨I,I⟩,I⟩\right\}I\right)$$
11		oveq1	$$⊢x=I\to x\left\{⟨⟨I,I⟩,I⟩\right\}y=I\left\{⟨⟨I,I⟩,I⟩\right\}y$$
12	11	oveq1d	$$⊢x=I\to \left(x\left\{⟨⟨I,I⟩,I⟩\right\}y\right)\left\{⟨⟨I,I⟩,I⟩\right\}z=\left(I\left\{⟨⟨I,I⟩,I⟩\right\}y\right)\left\{⟨⟨I,I⟩,I⟩\right\}z$$
13		oveq1	$$⊢x=I\to x\left\{⟨⟨I,I⟩,I⟩\right\}\left(y\left\{⟨⟨I,I⟩,I⟩\right\}z\right)=I\left\{⟨⟨I,I⟩,I⟩\right\}\left(y\left\{⟨⟨I,I⟩,I⟩\right\}z\right)$$
14	12 13	eqeq12d	$$⊢x=I\to \left(\left(x\left\{⟨⟨I,I⟩,I⟩\right\}y\right)\left\{⟨⟨I,I⟩,I⟩\right\}z=x\left\{⟨⟨I,I⟩,I⟩\right\}\left(y\left\{⟨⟨I,I⟩,I⟩\right\}z\right)\leftrightarrow \left(I\left\{⟨⟨I,I⟩,I⟩\right\}y\right)\left\{⟨⟨I,I⟩,I⟩\right\}z=I\left\{⟨⟨I,I⟩,I⟩\right\}\left(y\left\{⟨⟨I,I⟩,I⟩\right\}z\right)\right)$$
15	14	2ralbidv	$$⊢x=I\to \left(\forall y\in \left\{I\right\}\forall z\in \left\{I\right\}\left(x\left\{⟨⟨I,I⟩,I⟩\right\}y\right)\left\{⟨⟨I,I⟩,I⟩\right\}z=x\left\{⟨⟨I,I⟩,I⟩\right\}\left(y\left\{⟨⟨I,I⟩,I⟩\right\}z\right)\leftrightarrow \forall y\in \left\{I\right\}\forall z\in \left\{I\right\}\left(I\left\{⟨⟨I,I⟩,I⟩\right\}y\right)\left\{⟨⟨I,I⟩,I⟩\right\}z=I\left\{⟨⟨I,I⟩,I⟩\right\}\left(y\left\{⟨⟨I,I⟩,I⟩\right\}z\right)\right)$$
16	15	ralsng	$$⊢I\in V\to \left(\forall x\in \left\{I\right\}\forall y\in \left\{I\right\}\forall z\in \left\{I\right\}\left(x\left\{⟨⟨I,I⟩,I⟩\right\}y\right)\left\{⟨⟨I,I⟩,I⟩\right\}z=x\left\{⟨⟨I,I⟩,I⟩\right\}\left(y\left\{⟨⟨I,I⟩,I⟩\right\}z\right)\leftrightarrow \forall y\in \left\{I\right\}\forall z\in \left\{I\right\}\left(I\left\{⟨⟨I,I⟩,I⟩\right\}y\right)\left\{⟨⟨I,I⟩,I⟩\right\}z=I\left\{⟨⟨I,I⟩,I⟩\right\}\left(y\left\{⟨⟨I,I⟩,I⟩\right\}z\right)\right)$$
17		oveq2	$$⊢y=I\to I\left\{⟨⟨I,I⟩,I⟩\right\}y=I\left\{⟨⟨I,I⟩,I⟩\right\}I$$
18	17	oveq1d	$$⊢y=I\to \left(I\left\{⟨⟨I,I⟩,I⟩\right\}y\right)\left\{⟨⟨I,I⟩,I⟩\right\}z=\left(I\left\{⟨⟨I,I⟩,I⟩\right\}I\right)\left\{⟨⟨I,I⟩,I⟩\right\}z$$
19		oveq1	$$⊢y=I\to y\left\{⟨⟨I,I⟩,I⟩\right\}z=I\left\{⟨⟨I,I⟩,I⟩\right\}z$$
20	19	oveq2d	$$⊢y=I\to I\left\{⟨⟨I,I⟩,I⟩\right\}\left(y\left\{⟨⟨I,I⟩,I⟩\right\}z\right)=I\left\{⟨⟨I,I⟩,I⟩\right\}\left(I\left\{⟨⟨I,I⟩,I⟩\right\}z\right)$$
21	18 20	eqeq12d	$$⊢y=I\to \left(\left(I\left\{⟨⟨I,I⟩,I⟩\right\}y\right)\left\{⟨⟨I,I⟩,I⟩\right\}z=I\left\{⟨⟨I,I⟩,I⟩\right\}\left(y\left\{⟨⟨I,I⟩,I⟩\right\}z\right)\leftrightarrow \left(I\left\{⟨⟨I,I⟩,I⟩\right\}I\right)\left\{⟨⟨I,I⟩,I⟩\right\}z=I\left\{⟨⟨I,I⟩,I⟩\right\}\left(I\left\{⟨⟨I,I⟩,I⟩\right\}z\right)\right)$$
22	21	ralbidv	$$⊢y=I\to \left(\forall z\in \left\{I\right\}\left(I\left\{⟨⟨I,I⟩,I⟩\right\}y\right)\left\{⟨⟨I,I⟩,I⟩\right\}z=I\left\{⟨⟨I,I⟩,I⟩\right\}\left(y\left\{⟨⟨I,I⟩,I⟩\right\}z\right)\leftrightarrow \forall z\in \left\{I\right\}\left(I\left\{⟨⟨I,I⟩,I⟩\right\}I\right)\left\{⟨⟨I,I⟩,I⟩\right\}z=I\left\{⟨⟨I,I⟩,I⟩\right\}\left(I\left\{⟨⟨I,I⟩,I⟩\right\}z\right)\right)$$
23	22	ralsng	$$⊢I\in V\to \left(\forall y\in \left\{I\right\}\forall z\in \left\{I\right\}\left(I\left\{⟨⟨I,I⟩,I⟩\right\}y\right)\left\{⟨⟨I,I⟩,I⟩\right\}z=I\left\{⟨⟨I,I⟩,I⟩\right\}\left(y\left\{⟨⟨I,I⟩,I⟩\right\}z\right)\leftrightarrow \forall z\in \left\{I\right\}\left(I\left\{⟨⟨I,I⟩,I⟩\right\}I\right)\left\{⟨⟨I,I⟩,I⟩\right\}z=I\left\{⟨⟨I,I⟩,I⟩\right\}\left(I\left\{⟨⟨I,I⟩,I⟩\right\}z\right)\right)$$
24		oveq2	$$⊢z=I\to \left(I\left\{⟨⟨I,I⟩,I⟩\right\}I\right)\left\{⟨⟨I,I⟩,I⟩\right\}z=\left(I\left\{⟨⟨I,I⟩,I⟩\right\}I\right)\left\{⟨⟨I,I⟩,I⟩\right\}I$$
25		oveq2	$$⊢z=I\to I\left\{⟨⟨I,I⟩,I⟩\right\}z=I\left\{⟨⟨I,I⟩,I⟩\right\}I$$
26	25	oveq2d	$$⊢z=I\to I\left\{⟨⟨I,I⟩,I⟩\right\}\left(I\left\{⟨⟨I,I⟩,I⟩\right\}z\right)=I\left\{⟨⟨I,I⟩,I⟩\right\}\left(I\left\{⟨⟨I,I⟩,I⟩\right\}I\right)$$
27	24 26	eqeq12d	$$⊢z=I\to \left(\left(I\left\{⟨⟨I,I⟩,I⟩\right\}I\right)\left\{⟨⟨I,I⟩,I⟩\right\}z=I\left\{⟨⟨I,I⟩,I⟩\right\}\left(I\left\{⟨⟨I,I⟩,I⟩\right\}z\right)\leftrightarrow \left(I\left\{⟨⟨I,I⟩,I⟩\right\}I\right)\left\{⟨⟨I,I⟩,I⟩\right\}I=I\left\{⟨⟨I,I⟩,I⟩\right\}\left(I\left\{⟨⟨I,I⟩,I⟩\right\}I\right)\right)$$
28	27	ralsng	$$⊢I\in V\to \left(\forall z\in \left\{I\right\}\left(I\left\{⟨⟨I,I⟩,I⟩\right\}I\right)\left\{⟨⟨I,I⟩,I⟩\right\}z=I\left\{⟨⟨I,I⟩,I⟩\right\}\left(I\left\{⟨⟨I,I⟩,I⟩\right\}z\right)\leftrightarrow \left(I\left\{⟨⟨I,I⟩,I⟩\right\}I\right)\left\{⟨⟨I,I⟩,I⟩\right\}I=I\left\{⟨⟨I,I⟩,I⟩\right\}\left(I\left\{⟨⟨I,I⟩,I⟩\right\}I\right)\right)$$
29	16 23 28	3bitrd	$$⊢I\in V\to \left(\forall x\in \left\{I\right\}\forall y\in \left\{I\right\}\forall z\in \left\{I\right\}\left(x\left\{⟨⟨I,I⟩,I⟩\right\}y\right)\left\{⟨⟨I,I⟩,I⟩\right\}z=x\left\{⟨⟨I,I⟩,I⟩\right\}\left(y\left\{⟨⟨I,I⟩,I⟩\right\}z\right)\leftrightarrow \left(I\left\{⟨⟨I,I⟩,I⟩\right\}I\right)\left\{⟨⟨I,I⟩,I⟩\right\}I=I\left\{⟨⟨I,I⟩,I⟩\right\}\left(I\left\{⟨⟨I,I⟩,I⟩\right\}I\right)\right)$$
30	10 29	mpbird	$$⊢I\in V\to \forall x\in \left\{I\right\}\forall y\in \left\{I\right\}\forall z\in \left\{I\right\}\left(x\left\{⟨⟨I,I⟩,I⟩\right\}y\right)\left\{⟨⟨I,I⟩,I⟩\right\}z=x\left\{⟨⟨I,I⟩,I⟩\right\}\left(y\left\{⟨⟨I,I⟩,I⟩\right\}z\right)$$
31		snex	$$⊢\left\{I\right\}\in \mathrm{V}$$
32	1	grpbase	$$⊢\left\{I\right\}\in \mathrm{V}\to \left\{I\right\}={\mathrm{Base}}_M$$
33	31 32	ax-mp	$$⊢\left\{I\right\}={\mathrm{Base}}_M$$
34		snex	$$⊢\left\{⟨⟨I,I⟩,I⟩\right\}\in \mathrm{V}$$
35	1	grpplusg	$$⊢\left\{⟨⟨I,I⟩,I⟩\right\}\in \mathrm{V}\to \left\{⟨⟨I,I⟩,I⟩\right\}={+}_M$$
36	34 35	ax-mp	$$⊢\left\{⟨⟨I,I⟩,I⟩\right\}={+}_M$$
37	33 36	issgrp	Could not format ( M e. Smgrp <-> ( M e. Mgm /\ A. x e. { I } A. y e. { I } A. z e. { I } ( ( x { <. <. I , I >. , I >. } y ) { <. <. I , I >. , I >. } z ) = ( x { <. <. I , I >. , I >. } ( y { <. <. I , I >. , I >. } z ) ) ) ) : No typesetting found for |- ( M e. Smgrp <-> ( M e. Mgm /\ A. x e. { I } A. y e. { I } A. z e. { I } ( ( x { <. <. I , I >. , I >. } y ) { <. <. I , I >. , I >. } z ) = ( x { <. <. I , I >. , I >. } ( y { <. <. I , I >. , I >. } z ) ) ) ) with typecode |-
38	2 30 37	sylanbrc	Could not format ( I e. V -> M e. Smgrp ) : No typesetting found for |- ( I e. V -> M e. Smgrp ) with typecode |-