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 ψ χ
mndind.th x = y + ˙ z ψ θ
mndind.ta x = 0 ˙ ψ τ
mndind.et x = A ψ η
mndind.0g 0 ˙ = 0 M
mndind.pg + ˙ = + M
mndind.b B = Base M
mndind.m φ M Mnd
mndind.g φ G B
mndind.k φ B = mrCls SubMnd M G
mndind.i1 φ τ
mndind.i2 φ y B z G χ θ
mndind.a φ A B
Assertion mndind φ η

Proof

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