Metamath Proof Explorer

Theorem copisnmnd

Description: A structure with a constant group addition operation and at least two elements is not a monoid. (Contributed by AV, 16-Feb-2020)

Ref Expression
Hypotheses copisnmnd.b 
|- B = ( Base ` M )
copisnmnd.p 
|- ( +g ` M ) = ( x e. B , y e. B |-> C )
copisnmnd.c 
|- ( ph -> C e. B )
copisnmnd.n 
|- ( ph -> 1 < ( # ` B ) )
Assertion copisnmnd 
|- ( ph -> M e/ Mnd )

Proof

Step Hyp Ref Expression
1 copisnmnd.b 
 |-  B = ( Base ` M )
2 copisnmnd.p 
 |-  ( +g ` M ) = ( x e. B , y e. B |-> C )
3 copisnmnd.c 
 |-  ( ph -> C e. B )
4 copisnmnd.n 
 |-  ( ph -> 1 < ( # ` B ) )
5 1 fvexi 
 |-  B e. _V
6 5 a1i 
 |-  ( ( C e. B /\ 1 < ( # ` B ) ) -> B e. _V )
7 simpr 
 |-  ( ( C e. B /\ 1 < ( # ` B ) ) -> 1 < ( # ` B ) )
8 simpl 
 |-  ( ( C e. B /\ 1 < ( # ` B ) ) -> C e. B )
9 hashgt12el2 
 |-  ( ( B e. _V /\ 1 < ( # ` B ) /\ C e. B ) -> E. c e. B C =/= c )
10 6 7 8 9 syl3anc 
 |-  ( ( C e. B /\ 1 < ( # ` B ) ) -> E. c e. B C =/= c )
11 df-ne 
 |-  ( C =/= c <-> -. C = c )
12 11 rexbii 
 |-  ( E. c e. B C =/= c <-> E. c e. B -. C = c )
13 rexnal 
 |-  ( E. c e. B -. C = c <-> -. A. c e. B C = c )
14 12 13 bitri 
 |-  ( E. c e. B C =/= c <-> -. A. c e. B C = c )
15 eqidd 
 |-  ( ( ( ph /\ a e. B ) /\ c e. B ) -> ( x e. B , y e. B |-> C ) = ( x e. B , y e. B |-> C ) )
16 eqidd 
 |-  ( ( ( ( ph /\ a e. B ) /\ c e. B ) /\ ( x = a /\ y = c ) ) -> C = C )
17 simpr 
 |-  ( ( ph /\ a e. B ) -> a e. B )
18 17 adantr 
 |-  ( ( ( ph /\ a e. B ) /\ c e. B ) -> a e. B )
19 simpr 
 |-  ( ( ( ph /\ a e. B ) /\ c e. B ) -> c e. B )
20 3 adantr 
 |-  ( ( ph /\ a e. B ) -> C e. B )
21 20 adantr 
 |-  ( ( ( ph /\ a e. B ) /\ c e. B ) -> C e. B )
22 15 16 18 19 21 ovmpod 
 |-  ( ( ( ph /\ a e. B ) /\ c e. B ) -> ( a ( x e. B , y e. B |-> C ) c ) = C )
23 22 adantr 
 |-  ( ( ( ( ph /\ a e. B ) /\ c e. B ) /\ ( a ( x e. B , y e. B |-> C ) c ) = c ) -> ( a ( x e. B , y e. B |-> C ) c ) = C )
24 simpr 
 |-  ( ( ( ( ph /\ a e. B ) /\ c e. B ) /\ ( a ( x e. B , y e. B |-> C ) c ) = c ) -> ( a ( x e. B , y e. B |-> C ) c ) = c )
25 23 24 eqtr3d 
 |-  ( ( ( ( ph /\ a e. B ) /\ c e. B ) /\ ( a ( x e. B , y e. B |-> C ) c ) = c ) -> C = c )
26 25 ex 
 |-  ( ( ( ph /\ a e. B ) /\ c e. B ) -> ( ( a ( x e. B , y e. B |-> C ) c ) = c -> C = c ) )
27 26 ralimdva 
 |-  ( ( ph /\ a e. B ) -> ( A. c e. B ( a ( x e. B , y e. B |-> C ) c ) = c -> A. c e. B C = c ) )
28 27 rexlimdva 
 |-  ( ph -> ( E. a e. B A. c e. B ( a ( x e. B , y e. B |-> C ) c ) = c -> A. c e. B C = c ) )
29 28 con3d 
 |-  ( ph -> ( -. A. c e. B C = c -> -. E. a e. B A. c e. B ( a ( x e. B , y e. B |-> C ) c ) = c ) )
30 rexnal 
 |-  ( E. c e. B -. ( a ( x e. B , y e. B |-> C ) c ) = c <-> -. A. c e. B ( a ( x e. B , y e. B |-> C ) c ) = c )
31 30 bicomi 
 |-  ( -. A. c e. B ( a ( x e. B , y e. B |-> C ) c ) = c <-> E. c e. B -. ( a ( x e. B , y e. B |-> C ) c ) = c )
32 31 ralbii 
 |-  ( A. a e. B -. A. c e. B ( a ( x e. B , y e. B |-> C ) c ) = c <-> A. a e. B E. c e. B -. ( a ( x e. B , y e. B |-> C ) c ) = c )
33 ralnex 
 |-  ( A. a e. B -. A. c e. B ( a ( x e. B , y e. B |-> C ) c ) = c <-> -. E. a e. B A. c e. B ( a ( x e. B , y e. B |-> C ) c ) = c )
34 df-ne 
 |-  ( ( a ( x e. B , y e. B |-> C ) c ) =/= c <-> -. ( a ( x e. B , y e. B |-> C ) c ) = c )
35 34 bicomi 
 |-  ( -. ( a ( x e. B , y e. B |-> C ) c ) = c <-> ( a ( x e. B , y e. B |-> C ) c ) =/= c )
36 35 rexbii 
 |-  ( E. c e. B -. ( a ( x e. B , y e. B |-> C ) c ) = c <-> E. c e. B ( a ( x e. B , y e. B |-> C ) c ) =/= c )
37 36 ralbii 
 |-  ( A. a e. B E. c e. B -. ( a ( x e. B , y e. B |-> C ) c ) = c <-> A. a e. B E. c e. B ( a ( x e. B , y e. B |-> C ) c ) =/= c )
38 32 33 37 3bitr3i 
 |-  ( -. E. a e. B A. c e. B ( a ( x e. B , y e. B |-> C ) c ) = c <-> A. a e. B E. c e. B ( a ( x e. B , y e. B |-> C ) c ) =/= c )
39 29 38 syl6ib 
 |-  ( ph -> ( -. A. c e. B C = c -> A. a e. B E. c e. B ( a ( x e. B , y e. B |-> C ) c ) =/= c ) )
40 14 39 syl5bi 
 |-  ( ph -> ( E. c e. B C =/= c -> A. a e. B E. c e. B ( a ( x e. B , y e. B |-> C ) c ) =/= c ) )
41 10 40 syl5 
 |-  ( ph -> ( ( C e. B /\ 1 < ( # ` B ) ) -> A. a e. B E. c e. B ( a ( x e. B , y e. B |-> C ) c ) =/= c ) )
42 3 4 41 mp2and 
 |-  ( ph -> A. a e. B E. c e. B ( a ( x e. B , y e. B |-> C ) c ) =/= c )
43 2 eqcomi 
 |-  ( x e. B , y e. B |-> C ) = ( +g ` M )
44 1 43 isnmnd 
 |-  ( A. a e. B E. c e. B ( a ( x e. B , y e. B |-> C ) c ) =/= c -> M e/ Mnd )
45 42 44 syl 
 |-  ( ph -> M e/ Mnd )