# Metamath Proof Explorer

## Theorem mndind

Description: Induction in a monoid. In this theorem, ps ( x ) is the "generic" proposition to be be proved (the first four hypotheses tell its values at y, y+z, 0, A respectively). The two induction hypotheses mndind.i1 and mndind.i2 tell that it is true at 0, that if it is true at y then it is true at y+z (provided z is in G ). The hypothesis mndind.k tells that G is generating. (Contributed by SO, 14-Jul-2018)

Ref Expression
Hypotheses mndind.ch ${⊢}{x}={y}\to \left({\psi }↔{\chi }\right)$
mndind.th
mndind.ta
mndind.et ${⊢}{x}={A}\to \left({\psi }↔{\eta }\right)$
mndind.0g
mndind.pg
mndind.b ${⊢}{B}={\mathrm{Base}}_{{M}}$
mndind.m ${⊢}{\phi }\to {M}\in \mathrm{Mnd}$
mndind.g ${⊢}{\phi }\to {G}\subseteq {B}$
mndind.k ${⊢}{\phi }\to {B}=\mathrm{mrCls}\left(\mathrm{SubMnd}\left({M}\right)\right)\left({G}\right)$
mndind.i1 ${⊢}{\phi }\to {\tau }$
mndind.i2 ${⊢}\left(\left({\phi }\wedge {y}\in {B}\wedge {z}\in {G}\right)\wedge {\chi }\right)\to {\theta }$
mndind.a ${⊢}{\phi }\to {A}\in {B}$
Assertion mndind ${⊢}{\phi }\to {\eta }$

### Proof

Step Hyp Ref Expression
1 mndind.ch ${⊢}{x}={y}\to \left({\psi }↔{\chi }\right)$
2 mndind.th
3 mndind.ta
4 mndind.et ${⊢}{x}={A}\to \left({\psi }↔{\eta }\right)$
5 mndind.0g
6 mndind.pg
7 mndind.b ${⊢}{B}={\mathrm{Base}}_{{M}}$
8 mndind.m ${⊢}{\phi }\to {M}\in \mathrm{Mnd}$
9 mndind.g ${⊢}{\phi }\to {G}\subseteq {B}$
10 mndind.k ${⊢}{\phi }\to {B}=\mathrm{mrCls}\left(\mathrm{SubMnd}\left({M}\right)\right)\left({G}\right)$
11 mndind.i1 ${⊢}{\phi }\to {\tau }$
12 mndind.i2 ${⊢}\left(\left({\phi }\wedge {y}\in {B}\wedge {z}\in {G}\right)\wedge {\chi }\right)\to {\theta }$
13 mndind.a ${⊢}{\phi }\to {A}\in {B}$
14 7 5 mndidcl
15 8 14 syl
16 3 sbcieg
17 15 16 syl
18 11 17 mpbird
19 dfsbcq
20 oveq1
21 20 sbceq1d
22 19 21 imbi12d
23 7 submacs ${⊢}{M}\in \mathrm{Mnd}\to \mathrm{SubMnd}\left({M}\right)\in \mathrm{ACS}\left({B}\right)$
24 8 23 syl ${⊢}{\phi }\to \mathrm{SubMnd}\left({M}\right)\in \mathrm{ACS}\left({B}\right)$
25 24 acsmred ${⊢}{\phi }\to \mathrm{SubMnd}\left({M}\right)\in \mathrm{Moore}\left({B}\right)$
26 eleq1w ${⊢}{y}={a}\to \left({y}\in {B}↔{a}\in {B}\right)$
27 26 anbi2d ${⊢}{y}={a}\to \left(\left(\left({\phi }\wedge {b}\in {G}\right)\wedge {y}\in {B}\right)↔\left(\left({\phi }\wedge {b}\in {G}\right)\wedge {a}\in {B}\right)\right)$
28 vex ${⊢}{y}\in \mathrm{V}$
29 28 1 sbcie
30 dfsbcq
31 29 30 syl5bbr
32 oveq1
33 32 sbceq1d
34 31 33 imbi12d
35 27 34 imbi12d
36 eleq1w ${⊢}{z}={b}\to \left({z}\in {G}↔{b}\in {G}\right)$
37 36 anbi2d ${⊢}{z}={b}\to \left(\left({\phi }\wedge {z}\in {G}\right)↔\left({\phi }\wedge {b}\in {G}\right)\right)$
38 37 anbi1d ${⊢}{z}={b}\to \left(\left(\left({\phi }\wedge {z}\in {G}\right)\wedge {y}\in {B}\right)↔\left(\left({\phi }\wedge {b}\in {G}\right)\wedge {y}\in {B}\right)\right)$
39 ovex
40 39 2 sbcie
41 oveq2
42 41 sbceq1d
43 40 42 syl5bbr
44 43 imbi2d
45 38 44 imbi12d
46 12 ex ${⊢}\left({\phi }\wedge {y}\in {B}\wedge {z}\in {G}\right)\to \left({\chi }\to {\theta }\right)$
47 46 3expa ${⊢}\left(\left({\phi }\wedge {y}\in {B}\right)\wedge {z}\in {G}\right)\to \left({\chi }\to {\theta }\right)$
48 47 an32s ${⊢}\left(\left({\phi }\wedge {z}\in {G}\right)\wedge {y}\in {B}\right)\to \left({\chi }\to {\theta }\right)$
49 45 48 chvarvv
50 35 49 chvarvv
51 50 ralrimiva
52 9 51 ssrabdv
53 7 6 5 mndrid
54 8 53 sylan
55 54 sbceq1d
56 55 biimprd
57 56 ralrimiva
58 simprrl
59 8 ad2antrr ${⊢}\left(\left({\phi }\wedge \left({c}\in {B}\wedge {d}\in {B}\right)\right)\wedge {b}\in {B}\right)\to {M}\in \mathrm{Mnd}$
60 simpr ${⊢}\left(\left({\phi }\wedge \left({c}\in {B}\wedge {d}\in {B}\right)\right)\wedge {b}\in {B}\right)\to {b}\in {B}$
61 simplrl ${⊢}\left(\left({\phi }\wedge \left({c}\in {B}\wedge {d}\in {B}\right)\right)\wedge {b}\in {B}\right)\to {c}\in {B}$
62 7 6 mndcl
63 59 60 61 62 syl3anc
64 simpr
65 64 sbceq1d
66 oveq1
67 simplrr ${⊢}\left(\left({\phi }\wedge \left({c}\in {B}\wedge {d}\in {B}\right)\right)\wedge {b}\in {B}\right)\to {d}\in {B}$
68 7 6 mndass
69 59 60 61 67 68 syl13anc
70 66 69 sylan9eqr
71 70 sbceq1d
72 65 71 imbi12d
73 63 72 rspcdv
74 73 ralrimdva
75 74 impr
76 oveq1
77 76 sbceq1d
78 oveq1
79 78 sbceq1d
80 77 79 imbi12d
81 80 cbvralvw
82 75 81 sylib
84 imim1
85 84 ral2imi
86 58 83 85 sylc
87 oveq2
88 87 sbceq1d
89 88 imbi2d
90 89 ralbidv
91 oveq2
92 91 sbceq1d
93 92 imbi2d
94 93 ralbidv
95 oveq2
96 95 sbceq1d
97 96 imbi2d
98 97 ralbidv
99 oveq2
100 99 sbceq1d
101 100 imbi2d
102 101 ralbidv
103 7 6 5 8 57 86 90 94 98 102 issubmd
104 eqid ${⊢}\mathrm{mrCls}\left(\mathrm{SubMnd}\left({M}\right)\right)=\mathrm{mrCls}\left(\mathrm{SubMnd}\left({M}\right)\right)$
105 104 mrcsscl
106 25 52 103 105 syl3anc
107 10 106 eqsstrd
108 107 13 sseldd
109 oveq2
110 109 sbceq1d
111 110 imbi2d
112 111 ralbidv
113 112 elrab
114 113 simprbi
115 108 114 syl
116 22 115 15 rspcdva
117 18 116 mpd
118 7 6 5 mndlid
119 8 13 118 syl2anc
120 119 sbceq1d
121 4 sbcieg
122 13 121 syl
123 120 122 bitrd
124 117 123 mpbid ${⊢}{\phi }\to {\eta }$