Metamath Proof Explorer

Theorem issgrpd

Description: Deduce a semigroup from its properties. (Contributed by AV, 13-Feb-2025)

Ref Expression
Hypotheses issgrpd.b 
|- ( ph -> B = ( Base ` G ) )
issgrpd.p 
|- ( ph -> .+ = ( +g ` G ) )
issgrpd.c 
|- ( ( ph /\ x e. B /\ y e. B ) -> ( x .+ y ) e. B )
issgrpd.a 
|- ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) ) -> ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) )
issgrpd.v 
|- ( ph -> G e. V )
Assertion issgrpd 
|- ( ph -> G e. Smgrp )

Proof

Step Hyp Ref Expression
1 issgrpd.b 
 |-  ( ph -> B = ( Base ` G ) )
2 issgrpd.p 
 |-  ( ph -> .+ = ( +g ` G ) )
3 issgrpd.c 
 |-  ( ( ph /\ x e. B /\ y e. B ) -> ( x .+ y ) e. B )
4 issgrpd.a 
 |-  ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) ) -> ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) )
5 issgrpd.v 
 |-  ( ph -> G e. V )
6 3 3expib 
 |-  ( ph -> ( ( x e. B /\ y e. B ) -> ( x .+ y ) e. B ) )
7 1 eleq2d 
 |-  ( ph -> ( x e. B <-> x e. ( Base ` G ) ) )
8 1 eleq2d 
 |-  ( ph -> ( y e. B <-> y e. ( Base ` G ) ) )
9 7 8 anbi12d 
 |-  ( ph -> ( ( x e. B /\ y e. B ) <-> ( x e. ( Base ` G ) /\ y e. ( Base ` G ) ) ) )
10 2 oveqd 
 |-  ( ph -> ( x .+ y ) = ( x ( +g ` G ) y ) )
11 10 1 eleq12d 
 |-  ( ph -> ( ( x .+ y ) e. B <-> ( x ( +g ` G ) y ) e. ( Base ` G ) ) )
12 6 9 11 3imtr3d 
 |-  ( ph -> ( ( x e. ( Base ` G ) /\ y e. ( Base ` G ) ) -> ( x ( +g ` G ) y ) e. ( Base ` G ) ) )
13 12 imp 
 |-  ( ( ph /\ ( x e. ( Base ` G ) /\ y e. ( Base ` G ) ) ) -> ( x ( +g ` G ) y ) e. ( Base ` G ) )
14 df-3an 
 |-  ( ( x e. B /\ y e. B /\ z e. B ) <-> ( ( x e. B /\ y e. B ) /\ z e. B ) )
15 14 4 sylan2br 
 |-  ( ( ph /\ ( ( x e. B /\ y e. B ) /\ z e. B ) ) -> ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) )
16 15 ex 
 |-  ( ph -> ( ( ( x e. B /\ y e. B ) /\ z e. B ) -> ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) ) )
17 1 eleq2d 
 |-  ( ph -> ( z e. B <-> z e. ( Base ` G ) ) )
18 9 17 anbi12d 
 |-  ( ph -> ( ( ( x e. B /\ y e. B ) /\ z e. B ) <-> ( ( x e. ( Base ` G ) /\ y e. ( Base ` G ) ) /\ z e. ( Base ` G ) ) ) )
19 eqidd 
 |-  ( ph -> z = z )
20 2 10 19 oveq123d 
 |-  ( ph -> ( ( x .+ y ) .+ z ) = ( ( x ( +g ` G ) y ) ( +g ` G ) z ) )
21 eqidd 
 |-  ( ph -> x = x )
22 2 oveqd 
 |-  ( ph -> ( y .+ z ) = ( y ( +g ` G ) z ) )
23 2 21 22 oveq123d 
 |-  ( ph -> ( x .+ ( y .+ z ) ) = ( x ( +g ` G ) ( y ( +g ` G ) z ) ) )
24 20 23 eqeq12d 
 |-  ( ph -> ( ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) <-> ( ( x ( +g ` G ) y ) ( +g ` G ) z ) = ( x ( +g ` G ) ( y ( +g ` G ) z ) ) ) )
25 16 18 24 3imtr3d 
 |-  ( ph -> ( ( ( x e. ( Base ` G ) /\ y e. ( Base ` G ) ) /\ z e. ( Base ` G ) ) -> ( ( x ( +g ` G ) y ) ( +g ` G ) z ) = ( x ( +g ` G ) ( y ( +g ` G ) z ) ) ) )
26 25 impl 
 |-  ( ( ( ph /\ ( x e. ( Base ` G ) /\ y e. ( Base ` G ) ) ) /\ z e. ( Base ` G ) ) -> ( ( x ( +g ` G ) y ) ( +g ` G ) z ) = ( x ( +g ` G ) ( y ( +g ` G ) z ) ) )
27 26 ralrimiva 
 |-  ( ( ph /\ ( x e. ( Base ` G ) /\ y e. ( Base ` G ) ) ) -> A. z e. ( Base ` G ) ( ( x ( +g ` G ) y ) ( +g ` G ) z ) = ( x ( +g ` G ) ( y ( +g ` G ) z ) ) )
28 13 27 jca 
 |-  ( ( ph /\ ( x e. ( Base ` G ) /\ y e. ( Base ` G ) ) ) -> ( ( x ( +g ` G ) y ) e. ( Base ` G ) /\ A. z e. ( Base ` G ) ( ( x ( +g ` G ) y ) ( +g ` G ) z ) = ( x ( +g ` G ) ( y ( +g ` G ) z ) ) ) )
29 28 ralrimivva 
 |-  ( ph -> A. x e. ( Base ` G ) A. y e. ( Base ` G ) ( ( x ( +g ` G ) y ) e. ( Base ` G ) /\ A. z e. ( Base ` G ) ( ( x ( +g ` G ) y ) ( +g ` G ) z ) = ( x ( +g ` G ) ( y ( +g ` G ) z ) ) ) )
30 eqid 
 |-  ( Base ` G ) = ( Base ` G )
31 eqid 
 |-  ( +g ` G ) = ( +g ` G )
32 30 31 issgrpv 
 |-  ( G e. V -> ( G e. Smgrp <-> A. x e. ( Base ` G ) A. y e. ( Base ` G ) ( ( x ( +g ` G ) y ) e. ( Base ` G ) /\ A. z e. ( Base ` G ) ( ( x ( +g ` G ) y ) ( +g ` G ) z ) = ( x ( +g ` G ) ( y ( +g ` G ) z ) ) ) ) )
33 5 32 syl 
 |-  ( ph -> ( G e. Smgrp <-> A. x e. ( Base ` G ) A. y e. ( Base ` G ) ( ( x ( +g ` G ) y ) e. ( Base ` G ) /\ A. z e. ( Base ` G ) ( ( x ( +g ` G ) y ) ( +g ` G ) z ) = ( x ( +g ` G ) ( y ( +g ` G ) z ) ) ) ) )
34 29 33 mpbird 
 |-  ( ph -> G e. Smgrp )