Theorem dfgrp3

Description: Alternate definition of a group as semigroup (with at least one element) which is also a quasigroup, i.e. a magma in which solutions x and y of the equations ( a .+ x ) = b and ( x .+ a ) = b exist. Theorem 3.2 of Bruck p. 28. (Contributed by AV, 28-Aug-2021)

	Ref	Expression
Hypotheses	dfgrp3.b	$$⊢B={\mathrm{Base}}_G$$
	dfgrp3.p	$$⊢\underset{\dot{}}{+}={+}_G$$
Assertion	dfgrp3	Could not format assertion : No typesetting found for |- ( G e. Grp <-> ( G e. Smgrp /\ B =/= (/) /\ A. x e. B A. y e. B ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		dfgrp3.b	$$⊢B={\mathrm{Base}}_G$$
2		dfgrp3.p	$$⊢\underset{\dot{}}{+}={+}_G$$
3		grpsgrp	Could not format ( G e. Grp -> G e. Smgrp ) : No typesetting found for |- ( G e. Grp -> G e. Smgrp ) with typecode |-
4	1	grpbn0	$$⊢G\in \mathrm{Grp}\to B\ne \varnothing$$
5		simpl	$$⊢\left(G\in \mathrm{Grp}\wedge \left(x\in B\wedge y\in B\right)\right)\to G\in \mathrm{Grp}$$
6		simpr	$$⊢\left(x\in B\wedge y\in B\right)\to y\in B$$
7	6	adantl	$$⊢\left(G\in \mathrm{Grp}\wedge \left(x\in B\wedge y\in B\right)\right)\to y\in B$$
8		simpl	$$⊢\left(x\in B\wedge y\in B\right)\to x\in B$$
9	8	adantl	$$⊢\left(G\in \mathrm{Grp}\wedge \left(x\in B\wedge y\in B\right)\right)\to x\in B$$
10		eqid	$$⊢{-}_G={-}_G$$
11	1 10	grpsubcl	$$⊢\left(G\in \mathrm{Grp}\wedge y\in B\wedge x\in B\right)\to y{-}_{G}x\in B$$
12	5 7 9 11	syl3anc	$$⊢\left(G\in \mathrm{Grp}\wedge \left(x\in B\wedge y\in B\right)\right)\to y{-}_{G}x\in B$$
13		oveq1	$$⊢l=y{-}_{G}x\to l\underset{\dot{}}{+}x=\left(y{-}_{G}x\right)\underset{\dot{}}{+}x$$
14	13	eqeq1d	$$⊢l=y{-}_{G}x\to \left(l\underset{\dot{}}{+}x=y\leftrightarrow \left(y{-}_{G}x\right)\underset{\dot{}}{+}x=y\right)$$
15	14	adantl	$$⊢\left(\left(G\in \mathrm{Grp}\wedge \left(x\in B\wedge y\in B\right)\right)\wedge l=y{-}_{G}x\right)\to \left(l\underset{\dot{}}{+}x=y\leftrightarrow \left(y{-}_{G}x\right)\underset{\dot{}}{+}x=y\right)$$
16	1 2 10	grpnpcan	$$⊢\left(G\in \mathrm{Grp}\wedge y\in B\wedge x\in B\right)\to \left(y{-}_{G}x\right)\underset{\dot{}}{+}x=y$$
17	5 7 9 16	syl3anc	$$⊢\left(G\in \mathrm{Grp}\wedge \left(x\in B\wedge y\in B\right)\right)\to \left(y{-}_{G}x\right)\underset{\dot{}}{+}x=y$$
18	12 15 17	rspcedvd	$$⊢\left(G\in \mathrm{Grp}\wedge \left(x\in B\wedge y\in B\right)\right)\to \exists l\in Bl\underset{\dot{}}{+}x=y$$
19		eqid	$$⊢{inv}_g\left(G\right)={inv}_g\left(G\right)$$
20	1 19	grpinvcl	$$⊢\left(G\in \mathrm{Grp}\wedge x\in B\right)\to {inv}_g\left(G\right)\left(x\right)\in B$$
21	20	adantrr	$$⊢\left(G\in \mathrm{Grp}\wedge \left(x\in B\wedge y\in B\right)\right)\to {inv}_g\left(G\right)\left(x\right)\in B$$
22	1 2	grpcl	$$⊢\left(G\in \mathrm{Grp}\wedge {inv}_g\left(G\right)\left(x\right)\in B\wedge y\in B\right)\to {inv}_g\left(G\right)\left(x\right)\underset{\dot{}}{+}y\in B$$
23	5 21 7 22	syl3anc	$$⊢\left(G\in \mathrm{Grp}\wedge \left(x\in B\wedge y\in B\right)\right)\to {inv}_g\left(G\right)\left(x\right)\underset{\dot{}}{+}y\in B$$
24		oveq2	$$⊢r={inv}_g\left(G\right)\left(x\right)\underset{\dot{}}{+}y\to x\underset{\dot{}}{+}r=x\underset{\dot{}}{+}\left({inv}_g\left(G\right)\left(x\right)\underset{\dot{}}{+}y\right)$$
25	24	eqeq1d	$$⊢r={inv}_g\left(G\right)\left(x\right)\underset{\dot{}}{+}y\to \left(x\underset{\dot{}}{+}r=y\leftrightarrow x\underset{\dot{}}{+}\left({inv}_g\left(G\right)\left(x\right)\underset{\dot{}}{+}y\right)=y\right)$$
26	25	adantl	$$⊢\left(\left(G\in \mathrm{Grp}\wedge \left(x\in B\wedge y\in B\right)\right)\wedge r={inv}_g\left(G\right)\left(x\right)\underset{\dot{}}{+}y\right)\to \left(x\underset{\dot{}}{+}r=y\leftrightarrow x\underset{\dot{}}{+}\left({inv}_g\left(G\right)\left(x\right)\underset{\dot{}}{+}y\right)=y\right)$$
27		eqid	$$⊢0_G=0_G$$
28	1 2 27 19	grprinv	$$⊢\left(G\in \mathrm{Grp}\wedge x\in B\right)\to x\underset{\dot{}}{+}{inv}_g\left(G\right)\left(x\right)=0_G$$
29	28	adantrr	$$⊢\left(G\in \mathrm{Grp}\wedge \left(x\in B\wedge y\in B\right)\right)\to x\underset{\dot{}}{+}{inv}_g\left(G\right)\left(x\right)=0_G$$
30	29	oveq1d	$$⊢\left(G\in \mathrm{Grp}\wedge \left(x\in B\wedge y\in B\right)\right)\to \left(x\underset{\dot{}}{+}{inv}_g\left(G\right)\left(x\right)\right)\underset{\dot{}}{+}y=0_G\underset{\dot{}}{+}y$$
31	1 2	grpass	$$⊢\left(G\in \mathrm{Grp}\wedge \left(x\in B\wedge {inv}_g\left(G\right)\left(x\right)\in B\wedge y\in B\right)\right)\to \left(x\underset{\dot{}}{+}{inv}_g\left(G\right)\left(x\right)\right)\underset{\dot{}}{+}y=x\underset{\dot{}}{+}\left({inv}_g\left(G\right)\left(x\right)\underset{\dot{}}{+}y\right)$$
32	5 9 21 7 31	syl13anc	$$⊢\left(G\in \mathrm{Grp}\wedge \left(x\in B\wedge y\in B\right)\right)\to \left(x\underset{\dot{}}{+}{inv}_g\left(G\right)\left(x\right)\right)\underset{\dot{}}{+}y=x\underset{\dot{}}{+}\left({inv}_g\left(G\right)\left(x\right)\underset{\dot{}}{+}y\right)$$
33		grpmnd	$$⊢G\in \mathrm{Grp}\to G\in \mathrm{Mnd}$$
34	1 2 27	mndlid	$$⊢\left(G\in \mathrm{Mnd}\wedge y\in B\right)\to 0_G\underset{\dot{}}{+}y=y$$
35	33 6 34	syl2an	$$⊢\left(G\in \mathrm{Grp}\wedge \left(x\in B\wedge y\in B\right)\right)\to 0_G\underset{\dot{}}{+}y=y$$
36	30 32 35	3eqtr3d	$$⊢\left(G\in \mathrm{Grp}\wedge \left(x\in B\wedge y\in B\right)\right)\to x\underset{\dot{}}{+}\left({inv}_g\left(G\right)\left(x\right)\underset{\dot{}}{+}y\right)=y$$
37	23 26 36	rspcedvd	$$⊢\left(G\in \mathrm{Grp}\wedge \left(x\in B\wedge y\in B\right)\right)\to \exists r\in Bx\underset{\dot{}}{+}r=y$$
38	18 37	jca	$$⊢\left(G\in \mathrm{Grp}\wedge \left(x\in B\wedge y\in B\right)\right)\to \left(\exists l\in Bl\underset{\dot{}}{+}x=y\wedge \exists r\in Bx\underset{\dot{}}{+}r=y\right)$$
39	38	ralrimivva	$$⊢G\in \mathrm{Grp}\to \forall x\in B\forall y\in B\left(\exists l\in Bl\underset{\dot{}}{+}x=y\wedge \exists r\in Bx\underset{\dot{}}{+}r=y\right)$$
40	3 4 39	3jca	Could not format ( G e. Grp -> ( G e. Smgrp /\ B =/= (/) /\ A. x e. B A. y e. B ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) ) ) : No typesetting found for |- ( G e. Grp -> ( G e. Smgrp /\ B =/= (/) /\ A. x e. B A. y e. B ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) ) ) with typecode |-
41		simp1	Could not format ( ( G e. Smgrp /\ B =/= (/) /\ A. x e. B A. y e. B ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) ) -> G e. Smgrp ) : No typesetting found for |- ( ( G e. Smgrp /\ B =/= (/) /\ A. x e. B A. y e. B ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) ) -> G e. Smgrp ) with typecode |-
42	1 2	dfgrp3lem	Could not format ( ( G e. Smgrp /\ B =/= (/) /\ A. x e. B A. y e. B ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) ) -> E. u e. B A. a e. B ( ( u .+ a ) = a /\ E. i e. B ( i .+ a ) = u ) ) : No typesetting found for |- ( ( G e. Smgrp /\ B =/= (/) /\ A. x e. B A. y e. B ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) ) -> E. u e. B A. a e. B ( ( u .+ a ) = a /\ E. i e. B ( i .+ a ) = u ) ) with typecode |-
43	1 2	dfgrp2	Could not format ( G e. Grp <-> ( G e. Smgrp /\ E. u e. B A. a e. B ( ( u .+ a ) = a /\ E. i e. B ( i .+ a ) = u ) ) ) : No typesetting found for |- ( G e. Grp <-> ( G e. Smgrp /\ E. u e. B A. a e. B ( ( u .+ a ) = a /\ E. i e. B ( i .+ a ) = u ) ) ) with typecode |-
44	41 42 43	sylanbrc	Could not format ( ( G e. Smgrp /\ B =/= (/) /\ A. x e. B A. y e. B ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) ) -> G e. Grp ) : No typesetting found for |- ( ( G e. Smgrp /\ B =/= (/) /\ A. x e. B A. y e. B ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) ) -> G e. Grp ) with typecode |-
45	40 44	impbii	Could not format ( G e. Grp <-> ( G e. Smgrp /\ B =/= (/) /\ A. x e. B A. y e. B ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) ) ) : No typesetting found for |- ( G e. Grp <-> ( G e. Smgrp /\ B =/= (/) /\ A. x e. B A. y e. B ( E. l e. B ( l .+ x ) = y /\ E. r e. B ( x .+ r ) = y ) ) ) with typecode |-