Metamath Proof Explorer

Theorem ismndd

Description: Deduce a monoid from its properties. (Contributed by Mario Carneiro, 6-Jan-2015)

Ref Expression
Hypotheses ismndd.b 
|- ( ph -> B = ( Base ` G ) )
ismndd.p 
|- ( ph -> .+ = ( +g ` G ) )
ismndd.c 
|- ( ( ph /\ x e. B /\ y e. B ) -> ( x .+ y ) e. B )
ismndd.a 
|- ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) ) -> ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) )
ismndd.z 
|- ( ph -> .0. e. B )
ismndd.i 
|- ( ( ph /\ x e. B ) -> ( .0. .+ x ) = x )
ismndd.j 
|- ( ( ph /\ x e. B ) -> ( x .+ .0. ) = x )
Assertion ismndd 
|- ( ph -> G e. Mnd )

Proof

Step Hyp Ref Expression
1 ismndd.b 
 |-  ( ph -> B = ( Base ` G ) )
2 ismndd.p 
 |-  ( ph -> .+ = ( +g ` G ) )
3 ismndd.c 
 |-  ( ( ph /\ x e. B /\ y e. B ) -> ( x .+ y ) e. B )
4 ismndd.a 
 |-  ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) ) -> ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) )
5 ismndd.z 
 |-  ( ph -> .0. e. B )
6 ismndd.i 
 |-  ( ( ph /\ x e. B ) -> ( .0. .+ x ) = x )
7 ismndd.j 
 |-  ( ( ph /\ x e. B ) -> ( x .+ .0. ) = x )
8 3 3expb 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x .+ y ) e. B )
9 simpll 
 |-  ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ z e. B ) -> ph )
10 simplrl 
 |-  ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ z e. B ) -> x e. B )
11 simplrr 
 |-  ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ z e. B ) -> y e. B )
12 simpr 
 |-  ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ z e. B ) -> z e. B )
13 9 10 11 12 4 syl13anc 
 |-  ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ z e. B ) -> ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) )
14 13 ralrimiva 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> A. z e. B ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) )
15 8 14 jca 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( ( x .+ y ) e. B /\ A. z e. B ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) ) )
16 15 ralrimivva 
 |-  ( ph -> A. x e. B A. y e. B ( ( x .+ y ) e. B /\ A. z e. B ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) ) )
17 2 oveqd 
 |-  ( ph -> ( x .+ y ) = ( x ( +g ` G ) y ) )
18 17 1 eleq12d 
 |-  ( ph -> ( ( x .+ y ) e. B <-> ( x ( +g ` G ) y ) e. ( Base ` G ) ) )
19 eqidd 
 |-  ( ph -> z = z )
20 2 17 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 1 24 raleqbidv 
 |-  ( ph -> ( A. z e. B ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) <-> A. z e. ( Base ` G ) ( ( x ( +g ` G ) y ) ( +g ` G ) z ) = ( x ( +g ` G ) ( y ( +g ` G ) z ) ) ) )
26 18 25 anbi12d 
 |-  ( ph -> ( ( ( x .+ y ) e. B /\ A. z e. B ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) ) <-> ( ( 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 ) ) ) ) )
27 1 26 raleqbidv 
 |-  ( ph -> ( A. y e. B ( ( x .+ y ) e. B /\ A. z e. B ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) ) <-> 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 ) ) ) ) )
28 1 27 raleqbidv 
 |-  ( ph -> ( A. x e. B A. y e. B ( ( x .+ y ) e. B /\ A. z e. B ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) ) <-> 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 ) ) ) ) )
29 16 28 mpbid 
 |-  ( 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 5 1 eleqtrd 
 |-  ( ph -> .0. e. ( Base ` G ) )
31 1 eleq2d 
 |-  ( ph -> ( x e. B <-> x e. ( Base ` G ) ) )
32 31 biimpar 
 |-  ( ( ph /\ x e. ( Base ` G ) ) -> x e. B )
33 2 adantr 
 |-  ( ( ph /\ x e. B ) -> .+ = ( +g ` G ) )
34 33 oveqd 
 |-  ( ( ph /\ x e. B ) -> ( .0. .+ x ) = ( .0. ( +g ` G ) x ) )
35 34 6 eqtr3d 
 |-  ( ( ph /\ x e. B ) -> ( .0. ( +g ` G ) x ) = x )
36 33 oveqd 
 |-  ( ( ph /\ x e. B ) -> ( x .+ .0. ) = ( x ( +g ` G ) .0. ) )
37 36 7 eqtr3d 
 |-  ( ( ph /\ x e. B ) -> ( x ( +g ` G ) .0. ) = x )
38 35 37 jca 
 |-  ( ( ph /\ x e. B ) -> ( ( .0. ( +g ` G ) x ) = x /\ ( x ( +g ` G ) .0. ) = x ) )
39 32 38 syldan 
 |-  ( ( ph /\ x e. ( Base ` G ) ) -> ( ( .0. ( +g ` G ) x ) = x /\ ( x ( +g ` G ) .0. ) = x ) )
40 39 ralrimiva 
 |-  ( ph -> A. x e. ( Base ` G ) ( ( .0. ( +g ` G ) x ) = x /\ ( x ( +g ` G ) .0. ) = x ) )
41 oveq1 
 |-  ( u = .0. -> ( u ( +g ` G ) x ) = ( .0. ( +g ` G ) x ) )
42 41 eqeq1d 
 |-  ( u = .0. -> ( ( u ( +g ` G ) x ) = x <-> ( .0. ( +g ` G ) x ) = x ) )
43 42 ovanraleqv 
 |-  ( u = .0. -> ( A. x e. ( Base ` G ) ( ( u ( +g ` G ) x ) = x /\ ( x ( +g ` G ) u ) = x ) <-> A. x e. ( Base ` G ) ( ( .0. ( +g ` G ) x ) = x /\ ( x ( +g ` G ) .0. ) = x ) ) )
44 43 rspcev 
 |-  ( ( .0. e. ( Base ` G ) /\ A. x e. ( Base ` G ) ( ( .0. ( +g ` G ) x ) = x /\ ( x ( +g ` G ) .0. ) = x ) ) -> E. u e. ( Base ` G ) A. x e. ( Base ` G ) ( ( u ( +g ` G ) x ) = x /\ ( x ( +g ` G ) u ) = x ) )
45 30 40 44 syl2anc 
 |-  ( ph -> E. u e. ( Base ` G ) A. x e. ( Base ` G ) ( ( u ( +g ` G ) x ) = x /\ ( x ( +g ` G ) u ) = x ) )
46 eqid 
 |-  ( Base ` G ) = ( Base ` G )
47 eqid 
 |-  ( +g ` G ) = ( +g ` G )
48 46 47 ismnd 
 |-  ( G e. Mnd <-> ( 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 ) ) ) /\ E. u e. ( Base ` G ) A. x e. ( Base ` G ) ( ( u ( +g ` G ) x ) = x /\ ( x ( +g ` G ) u ) = x ) ) )
49 29 45 48 sylanbrc 
 |-  ( ph -> G e. Mnd )