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 -> ( ps <-> ch ) )
mndind.th 
|- ( x = ( y .+ z ) -> ( ps <-> th ) )
mndind.ta 
|- ( x = .0. -> ( ps <-> ta ) )
mndind.et 
|- ( x = A -> ( ps <-> et ) )
mndind.0g 
|- .0. = ( 0g ` M )
mndind.pg 
|- .+ = ( +g ` M )
mndind.b 
|- B = ( Base ` M )
mndind.m 
|- ( ph -> M e. Mnd )
mndind.g 
|- ( ph -> G C_ B )
mndind.k 
|- ( ph -> B = ( ( mrCls ` ( SubMnd ` M ) ) ` G ) )
mndind.i1 
|- ( ph -> ta )
mndind.i2 
|- ( ( ( ph /\ y e. B /\ z e. G ) /\ ch ) -> th )
mndind.a 
|- ( ph -> A e. B )
Assertion mndind 
|- ( ph -> et )

Proof

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