Metamath Proof Explorer

Theorem mndpropd

Description: If two structures have the same base set, and the values of their group (addition) operations are equal for all pairs of elements of the base set, one is a monoid iff the other one is. (Contributed by Mario Carneiro, 6-Jan-2015)

Ref Expression
Hypotheses mndpropd.1 ⊢φ→B=BaseK
mndpropd.2 ⊢φ→B=BaseL
mndpropd.3 ⊢φ∧x∈B∧y∈B→x+Ky=x+Ly
Assertion mndpropd ⊢φ→K∈Mnd↔L∈Mnd

Proof

Step Hyp Ref Expression
1 mndpropd.1 ⊢φ→B=BaseK
2 mndpropd.2 ⊢φ→B=BaseL
3 mndpropd.3 ⊢φ∧x∈B∧y∈B→x+Ky=x+Ly
4 simplr ⊢φ∧K∈Mnd∧x∈B∧y∈B→K∈Mnd
5 simprl ⊢φ∧K∈Mnd∧x∈B∧y∈B→x∈B
6 1 ad2antrr ⊢φ∧K∈Mnd∧x∈B∧y∈B→B=BaseK
7 5 6 eleqtrd ⊢φ∧K∈Mnd∧x∈B∧y∈B→x∈BaseK
8 simprr ⊢φ∧K∈Mnd∧x∈B∧y∈B→y∈B
9 8 6 eleqtrd ⊢φ∧K∈Mnd∧x∈B∧y∈B→y∈BaseK
10 eqid ⊢BaseK=BaseK
11 eqid ⊢+K=+K
12 10 11 mndcl ⊢K∈Mnd∧x∈BaseK∧y∈BaseK→x+Ky∈BaseK
13 4 7 9 12 syl3anc ⊢φ∧K∈Mnd∧x∈B∧y∈B→x+Ky∈BaseK
14 13 6 eleqtrrd ⊢φ∧K∈Mnd∧x∈B∧y∈B→x+Ky∈B
15 14 ralrimivva ⊢φ∧K∈Mnd→∀x∈B∀y∈Bx+Ky∈B
16 15 ex ⊢φ→K∈Mnd→∀x∈B∀y∈Bx+Ky∈B
17 simplr ⊢φ∧L∈Mnd∧x∈B∧y∈B→L∈Mnd
18 simprl ⊢φ∧L∈Mnd∧x∈B∧y∈B→x∈B
19 2 ad2antrr ⊢φ∧L∈Mnd∧x∈B∧y∈B→B=BaseL
20 18 19 eleqtrd ⊢φ∧L∈Mnd∧x∈B∧y∈B→x∈BaseL
21 simprr ⊢φ∧L∈Mnd∧x∈B∧y∈B→y∈B
22 21 19 eleqtrd ⊢φ∧L∈Mnd∧x∈B∧y∈B→y∈BaseL
23 eqid ⊢BaseL=BaseL
24 eqid ⊢+L=+L
25 23 24 mndcl ⊢L∈Mnd∧x∈BaseL∧y∈BaseL→x+Ly∈BaseL
26 17 20 22 25 syl3anc ⊢φ∧L∈Mnd∧x∈B∧y∈B→x+Ly∈BaseL
27 3 adantlr ⊢φ∧L∈Mnd∧x∈B∧y∈B→x+Ky=x+Ly
28 26 27 19 3eltr4d ⊢φ∧L∈Mnd∧x∈B∧y∈B→x+Ky∈B
29 28 ralrimivva ⊢φ∧L∈Mnd→∀x∈B∀y∈Bx+Ky∈B
30 29 ex ⊢φ→L∈Mnd→∀x∈B∀y∈Bx+Ky∈B
31 3 oveqrspc2v ⊢φ∧u∈B∧v∈B→u+Kv=u+Lv
32 31 adantlr ⊢φ∧∀x∈B∀y∈Bx+Ky∈B∧u∈B∧v∈B→u+Kv=u+Lv
33 32 eleq1d ⊢φ∧∀x∈B∀y∈Bx+Ky∈B∧u∈B∧v∈B→u+Kv∈B↔u+Lv∈B
34 simplll ⊢φ∧∀x∈B∀y∈Bx+Ky∈B∧u∈B∧v∈B∧w∈B→φ
35 simplrl ⊢φ∧∀x∈B∀y∈Bx+Ky∈B∧u∈B∧v∈B∧w∈B→u∈B
36 simplrr ⊢φ∧∀x∈B∀y∈Bx+Ky∈B∧u∈B∧v∈B∧w∈B→v∈B
37 simpllr ⊢φ∧∀x∈B∀y∈Bx+Ky∈B∧u∈B∧v∈B∧w∈B→∀x∈B∀y∈Bx+Ky∈B
38 ovrspc2v ⊢u∈B∧v∈B∧∀x∈B∀y∈Bx+Ky∈B→u+Kv∈B
39 35 36 37 38 syl21anc ⊢φ∧∀x∈B∀y∈Bx+Ky∈B∧u∈B∧v∈B∧w∈B→u+Kv∈B
40 simpr ⊢φ∧∀x∈B∀y∈Bx+Ky∈B∧u∈B∧v∈B∧w∈B→w∈B
41 3 oveqrspc2v ⊢φ∧u+Kv∈B∧w∈B→u+Kv+Kw=u+Kv+Lw
42 34 39 40 41 syl12anc ⊢φ∧∀x∈B∀y∈Bx+Ky∈B∧u∈B∧v∈B∧w∈B→u+Kv+Kw=u+Kv+Lw
43 34 35 36 31 syl12anc ⊢φ∧∀x∈B∀y∈Bx+Ky∈B∧u∈B∧v∈B∧w∈B→u+Kv=u+Lv
44 43 oveq1d ⊢φ∧∀x∈B∀y∈Bx+Ky∈B∧u∈B∧v∈B∧w∈B→u+Kv+Lw=u+Lv+Lw
45 42 44 eqtrd ⊢φ∧∀x∈B∀y∈Bx+Ky∈B∧u∈B∧v∈B∧w∈B→u+Kv+Kw=u+Lv+Lw
46 ovrspc2v ⊢v∈B∧w∈B∧∀x∈B∀y∈Bx+Ky∈B→v+Kw∈B
47 36 40 37 46 syl21anc ⊢φ∧∀x∈B∀y∈Bx+Ky∈B∧u∈B∧v∈B∧w∈B→v+Kw∈B
48 3 oveqrspc2v ⊢φ∧u∈B∧v+Kw∈B→u+Kv+Kw=u+Lv+Kw
49 34 35 47 48 syl12anc ⊢φ∧∀x∈B∀y∈Bx+Ky∈B∧u∈B∧v∈B∧w∈B→u+Kv+Kw=u+Lv+Kw
50 3 oveqrspc2v ⊢φ∧v∈B∧w∈B→v+Kw=v+Lw
51 34 36 40 50 syl12anc ⊢φ∧∀x∈B∀y∈Bx+Ky∈B∧u∈B∧v∈B∧w∈B→v+Kw=v+Lw
52 51 oveq2d ⊢φ∧∀x∈B∀y∈Bx+Ky∈B∧u∈B∧v∈B∧w∈B→u+Lv+Kw=u+Lv+Lw
53 49 52 eqtrd ⊢φ∧∀x∈B∀y∈Bx+Ky∈B∧u∈B∧v∈B∧w∈B→u+Kv+Kw=u+Lv+Lw
54 45 53 eqeq12d ⊢φ∧∀x∈B∀y∈Bx+Ky∈B∧u∈B∧v∈B∧w∈B→u+Kv+Kw=u+Kv+Kw↔u+Lv+Lw=u+Lv+Lw
55 54 ralbidva ⊢φ∧∀x∈B∀y∈Bx+Ky∈B∧u∈B∧v∈B→∀w∈Bu+Kv+Kw=u+Kv+Kw↔∀w∈Bu+Lv+Lw=u+Lv+Lw
56 33 55 anbi12d ⊢φ∧∀x∈B∀y∈Bx+Ky∈B∧u∈B∧v∈B→u+Kv∈B∧∀w∈Bu+Kv+Kw=u+Kv+Kw↔u+Lv∈B∧∀w∈Bu+Lv+Lw=u+Lv+Lw
57 56 2ralbidva ⊢φ∧∀x∈B∀y∈Bx+Ky∈B→∀u∈B∀v∈Bu+Kv∈B∧∀w∈Bu+Kv+Kw=u+Kv+Kw↔∀u∈B∀v∈Bu+Lv∈B∧∀w∈Bu+Lv+Lw=u+Lv+Lw
58 1 adantr ⊢φ∧∀x∈B∀y∈Bx+Ky∈B→B=BaseK
59 58 eleq2d ⊢φ∧∀x∈B∀y∈Bx+Ky∈B→u+Kv∈B↔u+Kv∈BaseK
60 58 raleqdv ⊢φ∧∀x∈B∀y∈Bx+Ky∈B→∀w∈Bu+Kv+Kw=u+Kv+Kw↔∀w∈BaseKu+Kv+Kw=u+Kv+Kw
61 59 60 anbi12d ⊢φ∧∀x∈B∀y∈Bx+Ky∈B→u+Kv∈B∧∀w∈Bu+Kv+Kw=u+Kv+Kw↔u+Kv∈BaseK∧∀w∈BaseKu+Kv+Kw=u+Kv+Kw
62 58 61 raleqbidv ⊢φ∧∀x∈B∀y∈Bx+Ky∈B→∀v∈Bu+Kv∈B∧∀w∈Bu+Kv+Kw=u+Kv+Kw↔∀v∈BaseKu+Kv∈BaseK∧∀w∈BaseKu+Kv+Kw=u+Kv+Kw
63 58 62 raleqbidv ⊢φ∧∀x∈B∀y∈Bx+Ky∈B→∀u∈B∀v∈Bu+Kv∈B∧∀w∈Bu+Kv+Kw=u+Kv+Kw↔∀u∈BaseK∀v∈BaseKu+Kv∈BaseK∧∀w∈BaseKu+Kv+Kw=u+Kv+Kw
64 2 adantr ⊢φ∧∀x∈B∀y∈Bx+Ky∈B→B=BaseL
65 64 eleq2d ⊢φ∧∀x∈B∀y∈Bx+Ky∈B→u+Lv∈B↔u+Lv∈BaseL
66 64 raleqdv ⊢φ∧∀x∈B∀y∈Bx+Ky∈B→∀w∈Bu+Lv+Lw=u+Lv+Lw↔∀w∈BaseLu+Lv+Lw=u+Lv+Lw
67 65 66 anbi12d ⊢φ∧∀x∈B∀y∈Bx+Ky∈B→u+Lv∈B∧∀w∈Bu+Lv+Lw=u+Lv+Lw↔u+Lv∈BaseL∧∀w∈BaseLu+Lv+Lw=u+Lv+Lw
68 64 67 raleqbidv ⊢φ∧∀x∈B∀y∈Bx+Ky∈B→∀v∈Bu+Lv∈B∧∀w∈Bu+Lv+Lw=u+Lv+Lw↔∀v∈BaseLu+Lv∈BaseL∧∀w∈BaseLu+Lv+Lw=u+Lv+Lw
69 64 68 raleqbidv ⊢φ∧∀x∈B∀y∈Bx+Ky∈B→∀u∈B∀v∈Bu+Lv∈B∧∀w∈Bu+Lv+Lw=u+Lv+Lw↔∀u∈BaseL∀v∈BaseLu+Lv∈BaseL∧∀w∈BaseLu+Lv+Lw=u+Lv+Lw
70 57 63 69 3bitr3d ⊢φ∧∀x∈B∀y∈Bx+Ky∈B→∀u∈BaseK∀v∈BaseKu+Kv∈BaseK∧∀w∈BaseKu+Kv+Kw=u+Kv+Kw↔∀u∈BaseL∀v∈BaseLu+Lv∈BaseL∧∀w∈BaseLu+Lv+Lw=u+Lv+Lw
71 simplll ⊢φ∧∀x∈B∀y∈Bx+Ky∈B∧s∈B∧u∈B→φ
72 simplr ⊢φ∧∀x∈B∀y∈Bx+Ky∈B∧s∈B∧u∈B→s∈B
73 simpr ⊢φ∧∀x∈B∀y∈Bx+Ky∈B∧s∈B∧u∈B→u∈B
74 3 oveqrspc2v ⊢φ∧s∈B∧u∈B→s+Ku=s+Lu
75 71 72 73 74 syl12anc ⊢φ∧∀x∈B∀y∈Bx+Ky∈B∧s∈B∧u∈B→s+Ku=s+Lu
76 75 eqeq1d ⊢φ∧∀x∈B∀y∈Bx+Ky∈B∧s∈B∧u∈B→s+Ku=u↔s+Lu=u
77 3 oveqrspc2v ⊢φ∧u∈B∧s∈B→u+Ks=u+Ls
78 71 73 72 77 syl12anc ⊢φ∧∀x∈B∀y∈Bx+Ky∈B∧s∈B∧u∈B→u+Ks=u+Ls
79 78 eqeq1d ⊢φ∧∀x∈B∀y∈Bx+Ky∈B∧s∈B∧u∈B→u+Ks=u↔u+Ls=u
80 76 79 anbi12d ⊢φ∧∀x∈B∀y∈Bx+Ky∈B∧s∈B∧u∈B→s+Ku=u∧u+Ks=u↔s+Lu=u∧u+Ls=u
81 80 ralbidva ⊢φ∧∀x∈B∀y∈Bx+Ky∈B∧s∈B→∀u∈Bs+Ku=u∧u+Ks=u↔∀u∈Bs+Lu=u∧u+Ls=u
82 81 rexbidva ⊢φ∧∀x∈B∀y∈Bx+Ky∈B→∃s∈B∀u∈Bs+Ku=u∧u+Ks=u↔∃s∈B∀u∈Bs+Lu=u∧u+Ls=u
83 58 raleqdv ⊢φ∧∀x∈B∀y∈Bx+Ky∈B→∀u∈Bs+Ku=u∧u+Ks=u↔∀u∈BaseKs+Ku=u∧u+Ks=u
84 58 83 rexeqbidv ⊢φ∧∀x∈B∀y∈Bx+Ky∈B→∃s∈B∀u∈Bs+Ku=u∧u+Ks=u↔∃s∈BaseK∀u∈BaseKs+Ku=u∧u+Ks=u
85 64 raleqdv ⊢φ∧∀x∈B∀y∈Bx+Ky∈B→∀u∈Bs+Lu=u∧u+Ls=u↔∀u∈BaseLs+Lu=u∧u+Ls=u
86 64 85 rexeqbidv ⊢φ∧∀x∈B∀y∈Bx+Ky∈B→∃s∈B∀u∈Bs+Lu=u∧u+Ls=u↔∃s∈BaseL∀u∈BaseLs+Lu=u∧u+Ls=u
87 82 84 86 3bitr3d ⊢φ∧∀x∈B∀y∈Bx+Ky∈B→∃s∈BaseK∀u∈BaseKs+Ku=u∧u+Ks=u↔∃s∈BaseL∀u∈BaseLs+Lu=u∧u+Ls=u
88 70 87 anbi12d ⊢φ∧∀x∈B∀y∈Bx+Ky∈B→∀u∈BaseK∀v∈BaseKu+Kv∈BaseK∧∀w∈BaseKu+Kv+Kw=u+Kv+Kw∧∃s∈BaseK∀u∈BaseKs+Ku=u∧u+Ks=u↔∀u∈BaseL∀v∈BaseLu+Lv∈BaseL∧∀w∈BaseLu+Lv+Lw=u+Lv+Lw∧∃s∈BaseL∀u∈BaseLs+Lu=u∧u+Ls=u
89 10 11 ismnd ⊢K∈Mnd↔∀u∈BaseK∀v∈BaseKu+Kv∈BaseK∧∀w∈BaseKu+Kv+Kw=u+Kv+Kw∧∃s∈BaseK∀u∈BaseKs+Ku=u∧u+Ks=u
90 23 24 ismnd ⊢L∈Mnd↔∀u∈BaseL∀v∈BaseLu+Lv∈BaseL∧∀w∈BaseLu+Lv+Lw=u+Lv+Lw∧∃s∈BaseL∀u∈BaseLs+Lu=u∧u+Ls=u
91 88 89 90 3bitr4g ⊢φ∧∀x∈B∀y∈Bx+Ky∈B→K∈Mnd↔L∈Mnd
92 91 ex ⊢φ→∀x∈B∀y∈Bx+Ky∈B→K∈Mnd↔L∈Mnd
93 16 30 92 pm5.21ndd ⊢φ→K∈Mnd↔L∈Mnd