Theorem abl1

Description: The (smallest) structure representing atrivial abelian group. (Contributed by AV, 28-Apr-2019)

	Ref	Expression
Hypothesis	abl1.m	$$⊢M=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\left\{I\right\}⟩,⟨{+}_{\mathrm{ndx}},\left\{⟨⟨I,I⟩,I⟩\right\}⟩\right\}$$
Assertion	abl1	$$⊢I\in V\to M\in \mathrm{Abel}$$

Proof

Step	Hyp	Ref	Expression
1		abl1.m	$$⊢M=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\left\{I\right\}⟩,⟨{+}_{\mathrm{ndx}},\left\{⟨⟨I,I⟩,I⟩\right\}⟩\right\}$$
2	1	grp1	$$⊢I\in V\to M\in \mathrm{Grp}$$
3		eqidd	$$⊢I\in V\to I\left\{⟨⟨I,I⟩,I⟩\right\}I=I\left\{⟨⟨I,I⟩,I⟩\right\}I$$
4		oveq1	$$⊢a=I\to a\left\{⟨⟨I,I⟩,I⟩\right\}b=I\left\{⟨⟨I,I⟩,I⟩\right\}b$$
5		oveq2	$$⊢a=I\to b\left\{⟨⟨I,I⟩,I⟩\right\}a=b\left\{⟨⟨I,I⟩,I⟩\right\}I$$
6	4 5	eqeq12d	$$⊢a=I\to \left(a\left\{⟨⟨I,I⟩,I⟩\right\}b=b\left\{⟨⟨I,I⟩,I⟩\right\}a\leftrightarrow I\left\{⟨⟨I,I⟩,I⟩\right\}b=b\left\{⟨⟨I,I⟩,I⟩\right\}I\right)$$
7	6	ralbidv	$$⊢a=I\to \left(\forall b\in \left\{I\right\}a\left\{⟨⟨I,I⟩,I⟩\right\}b=b\left\{⟨⟨I,I⟩,I⟩\right\}a\leftrightarrow \forall b\in \left\{I\right\}I\left\{⟨⟨I,I⟩,I⟩\right\}b=b\left\{⟨⟨I,I⟩,I⟩\right\}I\right)$$
8	7	ralsng	$$⊢I\in V\to \left(\forall a\in \left\{I\right\}\forall b\in \left\{I\right\}a\left\{⟨⟨I,I⟩,I⟩\right\}b=b\left\{⟨⟨I,I⟩,I⟩\right\}a\leftrightarrow \forall b\in \left\{I\right\}I\left\{⟨⟨I,I⟩,I⟩\right\}b=b\left\{⟨⟨I,I⟩,I⟩\right\}I\right)$$
9		oveq2	$$⊢b=I\to I\left\{⟨⟨I,I⟩,I⟩\right\}b=I\left\{⟨⟨I,I⟩,I⟩\right\}I$$
10		oveq1	$$⊢b=I\to b\left\{⟨⟨I,I⟩,I⟩\right\}I=I\left\{⟨⟨I,I⟩,I⟩\right\}I$$
11	9 10	eqeq12d	$$⊢b=I\to \left(I\left\{⟨⟨I,I⟩,I⟩\right\}b=b\left\{⟨⟨I,I⟩,I⟩\right\}I\leftrightarrow I\left\{⟨⟨I,I⟩,I⟩\right\}I=I\left\{⟨⟨I,I⟩,I⟩\right\}I\right)$$
12	11	ralsng	$$⊢I\in V\to \left(\forall b\in \left\{I\right\}I\left\{⟨⟨I,I⟩,I⟩\right\}b=b\left\{⟨⟨I,I⟩,I⟩\right\}I\leftrightarrow I\left\{⟨⟨I,I⟩,I⟩\right\}I=I\left\{⟨⟨I,I⟩,I⟩\right\}I\right)$$
13	8 12	bitrd	$$⊢I\in V\to \left(\forall a\in \left\{I\right\}\forall b\in \left\{I\right\}a\left\{⟨⟨I,I⟩,I⟩\right\}b=b\left\{⟨⟨I,I⟩,I⟩\right\}a\leftrightarrow I\left\{⟨⟨I,I⟩,I⟩\right\}I=I\left\{⟨⟨I,I⟩,I⟩\right\}I\right)$$
14	3 13	mpbird	$$⊢I\in V\to \forall a\in \left\{I\right\}\forall b\in \left\{I\right\}a\left\{⟨⟨I,I⟩,I⟩\right\}b=b\left\{⟨⟨I,I⟩,I⟩\right\}a$$
15		snex	$$⊢\left\{I\right\}\in \mathrm{V}$$
16	1	grpbase	$$⊢\left\{I\right\}\in \mathrm{V}\to \left\{I\right\}={\mathrm{Base}}_M$$
17	15 16	ax-mp	$$⊢\left\{I\right\}={\mathrm{Base}}_M$$
18		snex	$$⊢\left\{⟨⟨I,I⟩,I⟩\right\}\in \mathrm{V}$$
19	1	grpplusg	$$⊢\left\{⟨⟨I,I⟩,I⟩\right\}\in \mathrm{V}\to \left\{⟨⟨I,I⟩,I⟩\right\}={+}_M$$
20	18 19	ax-mp	$$⊢\left\{⟨⟨I,I⟩,I⟩\right\}={+}_M$$
21	17 20	isabl2	$$⊢M\in \mathrm{Abel}\leftrightarrow \left(M\in \mathrm{Grp}\wedge \forall a\in \left\{I\right\}\forall b\in \left\{I\right\}a\left\{⟨⟨I,I⟩,I⟩\right\}b=b\left\{⟨⟨I,I⟩,I⟩\right\}a\right)$$
22	2 14 21	sylanbrc	$$⊢I\in V\to M\in \mathrm{Abel}$$