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 ⊢ ( 𝑥 = 𝑦 → ( 𝜓 ↔ 𝜒 ) )
mndind.th ⊢ ( 𝑥 = ( 𝑦 + 𝑧 ) → ( 𝜓 ↔ 𝜃 ) )
mndind.ta ⊢ ( 𝑥 = 0 → ( 𝜓 ↔ 𝜏 ) )
mndind.et ⊢ ( 𝑥 = 𝐴 → ( 𝜓 ↔ 𝜂 ) )
mndind.0g ⊢ 0 = ( 0g ‘ 𝑀 )
mndind.pg ⊢ + = ( +g ‘ 𝑀 )
mndind.b ⊢ 𝐵 = ( Base ‘ 𝑀 )
mndind.m ⊢ ( 𝜑 → 𝑀 ∈ Mnd )
mndind.g ⊢ ( 𝜑 → 𝐺 ⊆ 𝐵 )
mndind.k ⊢ ( 𝜑 → 𝐵 = ( ( mrCls ‘ ( SubMnd ‘ 𝑀 ) ) ‘ 𝐺 ) )
mndind.i1 ⊢ ( 𝜑 → 𝜏 )
mndind.i2 ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐺 ) ∧ 𝜒 ) → 𝜃 )
mndind.a ⊢ ( 𝜑 → 𝐴 ∈ 𝐵 )
Assertion mndind ( 𝜑 → 𝜂 )

Proof

Step Hyp Ref Expression
1 mndind.ch ⊢ ( 𝑥 = 𝑦 → ( 𝜓 ↔ 𝜒 ) )
2 mndind.th ⊢ ( 𝑥 = ( 𝑦 + 𝑧 ) → ( 𝜓 ↔ 𝜃 ) )
3 mndind.ta ⊢ ( 𝑥 = 0 → ( 𝜓 ↔ 𝜏 ) )
4 mndind.et ⊢ ( 𝑥 = 𝐴 → ( 𝜓 ↔ 𝜂 ) )
5 mndind.0g ⊢ 0 = ( 0g ‘ 𝑀 )
6 mndind.pg ⊢ + = ( +g ‘ 𝑀 )
7 mndind.b ⊢ 𝐵 = ( Base ‘ 𝑀 )
8 mndind.m ⊢ ( 𝜑 → 𝑀 ∈ Mnd )
9 mndind.g ⊢ ( 𝜑 → 𝐺 ⊆ 𝐵 )
10 mndind.k ⊢ ( 𝜑 → 𝐵 = ( ( mrCls ‘ ( SubMnd ‘ 𝑀 ) ) ‘ 𝐺 ) )
11 mndind.i1 ⊢ ( 𝜑 → 𝜏 )
12 mndind.i2 ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐺 ) ∧ 𝜒 ) → 𝜃 )
13 mndind.a ⊢ ( 𝜑 → 𝐴 ∈ 𝐵 )
14 7 5 mndidcl ⊢ ( 𝑀 ∈ Mnd → 0 ∈ 𝐵 )
15 8 14 syl ⊢ ( 𝜑 → 0 ∈ 𝐵 )
16 3 sbcieg ⊢ ( 0 ∈ 𝐵 → ( [ 0 / 𝑥 ] 𝜓 ↔ 𝜏 ) )
17 15 16 syl ⊢ ( 𝜑 → ( [ 0 / 𝑥 ] 𝜓 ↔ 𝜏 ) )
18 11 17 mpbird ⊢ ( 𝜑 → [ 0 / 𝑥 ] 𝜓 )
19 dfsbcq ⊢ ( 𝑎 = 0 → ( [ 𝑎 / 𝑥 ] 𝜓 ↔ [ 0 / 𝑥 ] 𝜓 ) )
20 oveq1 ⊢ ( 𝑎 = 0 → ( 𝑎 + 𝐴 ) = ( 0 + 𝐴 ) )
21 20 sbceq1d ⊢ ( 𝑎 = 0 → ( [ ( 𝑎 + 𝐴 ) / 𝑥 ] 𝜓 ↔ [ ( 0 + 𝐴 ) / 𝑥 ] 𝜓 ) )
22 19 21 imbi12d ⊢ ( 𝑎 = 0 → ( ( [ 𝑎 / 𝑥 ] 𝜓 → [ ( 𝑎 + 𝐴 ) / 𝑥 ] 𝜓 ) ↔ ( [ 0 / 𝑥 ] 𝜓 → [ ( 0 + 𝐴 ) / 𝑥 ] 𝜓 ) ) )
23 7 submacs ⊢ ( 𝑀 ∈ Mnd → ( SubMnd ‘ 𝑀 ) ∈ ( ACS ‘ 𝐵 ) )
24 8 23 syl ⊢ ( 𝜑 → ( SubMnd ‘ 𝑀 ) ∈ ( ACS ‘ 𝐵 ) )
25 24 acsmred ⊢ ( 𝜑 → ( SubMnd ‘ 𝑀 ) ∈ ( Moore ‘ 𝐵 ) )
26 eleq1w ⊢ ( 𝑦 = 𝑎 → ( 𝑦 ∈ 𝐵 ↔ 𝑎 ∈ 𝐵 ) )
27 26 anbi2d ⊢ ( 𝑦 = 𝑎 → ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐺 ) ∧ 𝑦 ∈ 𝐵 ) ↔ ( ( 𝜑 ∧ 𝑏 ∈ 𝐺 ) ∧ 𝑎 ∈ 𝐵 ) ) )
28 vex ⊢ 𝑦 ∈ V
29 28 1 sbcie ⊢ ( [ 𝑦 / 𝑥 ] 𝜓 ↔ 𝜒 )
30 dfsbcq ⊢ ( 𝑦 = 𝑎 → ( [ 𝑦 / 𝑥 ] 𝜓 ↔ [ 𝑎 / 𝑥 ] 𝜓 ) )
31 29 30 bitr3id ⊢ ( 𝑦 = 𝑎 → ( 𝜒 ↔ [ 𝑎 / 𝑥 ] 𝜓 ) )
32 oveq1 ⊢ ( 𝑦 = 𝑎 → ( 𝑦 + 𝑏 ) = ( 𝑎 + 𝑏 ) )
33 32 sbceq1d ⊢ ( 𝑦 = 𝑎 → ( [ ( 𝑦 + 𝑏 ) / 𝑥 ] 𝜓 ↔ [ ( 𝑎 + 𝑏 ) / 𝑥 ] 𝜓 ) )
34 31 33 imbi12d ⊢ ( 𝑦 = 𝑎 → ( ( 𝜒 → [ ( 𝑦 + 𝑏 ) / 𝑥 ] 𝜓 ) ↔ ( [ 𝑎 / 𝑥 ] 𝜓 → [ ( 𝑎 + 𝑏 ) / 𝑥 ] 𝜓 ) ) )
35 27 34 imbi12d ⊢ ( 𝑦 = 𝑎 → ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐺 ) ∧ 𝑦 ∈ 𝐵 ) → ( 𝜒 → [ ( 𝑦 + 𝑏 ) / 𝑥 ] 𝜓 ) ) ↔ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐺 ) ∧ 𝑎 ∈ 𝐵 ) → ( [ 𝑎 / 𝑥 ] 𝜓 → [ ( 𝑎 + 𝑏 ) / 𝑥 ] 𝜓 ) ) ) )
36 eleq1w ⊢ ( 𝑧 = 𝑏 → ( 𝑧 ∈ 𝐺 ↔ 𝑏 ∈ 𝐺 ) )
37 36 anbi2d ⊢ ( 𝑧 = 𝑏 → ( ( 𝜑 ∧ 𝑧 ∈ 𝐺 ) ↔ ( 𝜑 ∧ 𝑏 ∈ 𝐺 ) ) )
38 37 anbi1d ⊢ ( 𝑧 = 𝑏 → ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐺 ) ∧ 𝑦 ∈ 𝐵 ) ↔ ( ( 𝜑 ∧ 𝑏 ∈ 𝐺 ) ∧ 𝑦 ∈ 𝐵 ) ) )
39 ovex ⊢ ( 𝑦 + 𝑧 ) ∈ V
40 39 2 sbcie ⊢ ( [ ( 𝑦 + 𝑧 ) / 𝑥 ] 𝜓 ↔ 𝜃 )
41 oveq2 ⊢ ( 𝑧 = 𝑏 → ( 𝑦 + 𝑧 ) = ( 𝑦 + 𝑏 ) )
42 41 sbceq1d ⊢ ( 𝑧 = 𝑏 → ( [ ( 𝑦 + 𝑧 ) / 𝑥 ] 𝜓 ↔ [ ( 𝑦 + 𝑏 ) / 𝑥 ] 𝜓 ) )
43 40 42 bitr3id ⊢ ( 𝑧 = 𝑏 → ( 𝜃 ↔ [ ( 𝑦 + 𝑏 ) / 𝑥 ] 𝜓 ) )
44 43 imbi2d ⊢ ( 𝑧 = 𝑏 → ( ( 𝜒 → 𝜃 ) ↔ ( 𝜒 → [ ( 𝑦 + 𝑏 ) / 𝑥 ] 𝜓 ) ) )
45 38 44 imbi12d ⊢ ( 𝑧 = 𝑏 → ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐺 ) ∧ 𝑦 ∈ 𝐵 ) → ( 𝜒 → 𝜃 ) ) ↔ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐺 ) ∧ 𝑦 ∈ 𝐵 ) → ( 𝜒 → [ ( 𝑦 + 𝑏 ) / 𝑥 ] 𝜓 ) ) ) )
46 12 ex ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐺 ) → ( 𝜒 → 𝜃 ) )
47 46 3expa ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 ∈ 𝐺 ) → ( 𝜒 → 𝜃 ) )
48 47 an32s ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐺 ) ∧ 𝑦 ∈ 𝐵 ) → ( 𝜒 → 𝜃 ) )
49 45 48 chvarvv ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐺 ) ∧ 𝑦 ∈ 𝐵 ) → ( 𝜒 → [ ( 𝑦 + 𝑏 ) / 𝑥 ] 𝜓 ) )
50 35 49 chvarvv ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐺 ) ∧ 𝑎 ∈ 𝐵 ) → ( [ 𝑎 / 𝑥 ] 𝜓 → [ ( 𝑎 + 𝑏 ) / 𝑥 ] 𝜓 ) )
51 50 ralrimiva ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐺 ) → ∀ 𝑎 ∈ 𝐵 ( [ 𝑎 / 𝑥 ] 𝜓 → [ ( 𝑎 + 𝑏 ) / 𝑥 ] 𝜓 ) )
52 9 51 ssrabdv ⊢ ( 𝜑 → 𝐺 ⊆ { 𝑏 ∈ 𝐵 ∣ ∀ 𝑎 ∈ 𝐵 ( [ 𝑎 / 𝑥 ] 𝜓 → [ ( 𝑎 + 𝑏 ) / 𝑥 ] 𝜓 ) } )
53 7 6 5 mndrid ⊢ ( ( 𝑀 ∈ Mnd ∧ 𝑎 ∈ 𝐵 ) → ( 𝑎 + 0 ) = 𝑎 )
54 8 53 sylan ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) → ( 𝑎 + 0 ) = 𝑎 )
55 54 sbceq1d ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) → ( [ ( 𝑎 + 0 ) / 𝑥 ] 𝜓 ↔ [ 𝑎 / 𝑥 ] 𝜓 ) )
56 55 biimprd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) → ( [ 𝑎 / 𝑥 ] 𝜓 → [ ( 𝑎 + 0 ) / 𝑥 ] 𝜓 ) )
57 56 ralrimiva ⊢ ( 𝜑 → ∀ 𝑎 ∈ 𝐵 ( [ 𝑎 / 𝑥 ] 𝜓 → [ ( 𝑎 + 0 ) / 𝑥 ] 𝜓 ) )
58 simprrl ⊢ ( ( 𝜑 ∧ ( ( 𝑐 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵 ) ∧ ( ∀ 𝑎 ∈ 𝐵 ( [ 𝑎 / 𝑥 ] 𝜓 → [ ( 𝑎 + 𝑐 ) / 𝑥 ] 𝜓 ) ∧ ∀ 𝑎 ∈ 𝐵 ( [ 𝑎 / 𝑥 ] 𝜓 → [ ( 𝑎 + 𝑑 ) / 𝑥 ] 𝜓 ) ) ) ) → ∀ 𝑎 ∈ 𝐵 ( [ 𝑎 / 𝑥 ] 𝜓 → [ ( 𝑎 + 𝑐 ) / 𝑥 ] 𝜓 ) )
59 8 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑐 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵 ) ) ∧ 𝑏 ∈ 𝐵 ) → 𝑀 ∈ Mnd )
60 simpr ⊢ ( ( ( 𝜑 ∧ ( 𝑐 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵 ) ) ∧ 𝑏 ∈ 𝐵 ) → 𝑏 ∈ 𝐵 )
61 simplrl ⊢ ( ( ( 𝜑 ∧ ( 𝑐 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵 ) ) ∧ 𝑏 ∈ 𝐵 ) → 𝑐 ∈ 𝐵 )
62 7 6 mndcl ⊢ ( ( 𝑀 ∈ Mnd ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) → ( 𝑏 + 𝑐 ) ∈ 𝐵 )
63 59 60 61 62 syl3anc ⊢ ( ( ( 𝜑 ∧ ( 𝑐 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵 ) ) ∧ 𝑏 ∈ 𝐵 ) → ( 𝑏 + 𝑐 ) ∈ 𝐵 )
64 simpr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑐 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵 ) ) ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑎 = ( 𝑏 + 𝑐 ) ) → 𝑎 = ( 𝑏 + 𝑐 ) )
65 64 sbceq1d ⊢ ( ( ( ( 𝜑 ∧ ( 𝑐 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵 ) ) ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑎 = ( 𝑏 + 𝑐 ) ) → ( [ 𝑎 / 𝑥 ] 𝜓 ↔ [ ( 𝑏 + 𝑐 ) / 𝑥 ] 𝜓 ) )
66 oveq1 ⊢ ( 𝑎 = ( 𝑏 + 𝑐 ) → ( 𝑎 + 𝑑 ) = ( ( 𝑏 + 𝑐 ) + 𝑑 ) )
67 simplrr ⊢ ( ( ( 𝜑 ∧ ( 𝑐 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵 ) ) ∧ 𝑏 ∈ 𝐵 ) → 𝑑 ∈ 𝐵 )
68 7 6 mndass ⊢ ( ( 𝑀 ∈ Mnd ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵 ) ) → ( ( 𝑏 + 𝑐 ) + 𝑑 ) = ( 𝑏 + ( 𝑐 + 𝑑 ) ) )
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 ⊢ ( ( 𝜑 ∧ ( ( 𝑐 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵 ) ∧ ∀ 𝑎 ∈ 𝐵 ( [ 𝑎 / 𝑥 ] 𝜓 → [ ( 𝑎 + 𝑑 ) / 𝑥 ] 𝜓 ) ) ) → ∀ 𝑎 ∈ 𝐵 ( [ ( 𝑎 + 𝑐 ) / 𝑥 ] 𝜓 → [ ( 𝑎 + ( 𝑐 + 𝑑 ) ) / 𝑥 ] 𝜓 ) )
83 82 adantrrl ⊢ ( ( 𝜑 ∧ ( ( 𝑐 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵 ) ∧ ( ∀ 𝑎 ∈ 𝐵 ( [ 𝑎 / 𝑥 ] 𝜓 → [ ( 𝑎 + 𝑐 ) / 𝑥 ] 𝜓 ) ∧ ∀ 𝑎 ∈ 𝐵 ( [ 𝑎 / 𝑥 ] 𝜓 → [ ( 𝑎 + 𝑑 ) / 𝑥 ] 𝜓 ) ) ) ) → ∀ 𝑎 ∈ 𝐵 ( [ ( 𝑎 + 𝑐 ) / 𝑥 ] 𝜓 → [ ( 𝑎 + ( 𝑐 + 𝑑 ) ) / 𝑥 ] 𝜓 ) )
84 imim1 ⊢ ( ( [ 𝑎 / 𝑥 ] 𝜓 → [ ( 𝑎 + 𝑐 ) / 𝑥 ] 𝜓 ) → ( ( [ ( 𝑎 + 𝑐 ) / 𝑥 ] 𝜓 → [ ( 𝑎 + ( 𝑐 + 𝑑 ) ) / 𝑥 ] 𝜓 ) → ( [ 𝑎 / 𝑥 ] 𝜓 → [ ( 𝑎 + ( 𝑐 + 𝑑 ) ) / 𝑥 ] 𝜓 ) ) )
85 84 ral2imi ⊢ ( ∀ 𝑎 ∈ 𝐵 ( [ 𝑎 / 𝑥 ] 𝜓 → [ ( 𝑎 + 𝑐 ) / 𝑥 ] 𝜓 ) → ( ∀ 𝑎 ∈ 𝐵 ( [ ( 𝑎 + 𝑐 ) / 𝑥 ] 𝜓 → [ ( 𝑎 + ( 𝑐 + 𝑑 ) ) / 𝑥 ] 𝜓 ) → ∀ 𝑎 ∈ 𝐵 ( [ 𝑎 / 𝑥 ] 𝜓 → [ ( 𝑎 + ( 𝑐 + 𝑑 ) ) / 𝑥 ] 𝜓 ) ) )
86 58 83 85 sylc ⊢ ( ( 𝜑 ∧ ( ( 𝑐 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵 ) ∧ ( ∀ 𝑎 ∈ 𝐵 ( [ 𝑎 / 𝑥 ] 𝜓 → [ ( 𝑎 + 𝑐 ) / 𝑥 ] 𝜓 ) ∧ ∀ 𝑎 ∈ 𝐵 ( [ 𝑎 / 𝑥 ] 𝜓 → [ ( 𝑎 + 𝑑 ) / 𝑥 ] 𝜓 ) ) ) ) → ∀ 𝑎 ∈ 𝐵 ( [ 𝑎 / 𝑥 ] 𝜓 → [ ( 𝑎 + ( 𝑐 + 𝑑 ) ) / 𝑥 ] 𝜓 ) )
87 oveq2 ⊢ ( 𝑏 = 0 → ( 𝑎 + 𝑏 ) = ( 𝑎 + 0 ) )
88 87 sbceq1d ⊢ ( 𝑏 = 0 → ( [ ( 𝑎 + 𝑏 ) / 𝑥 ] 𝜓 ↔ [ ( 𝑎 + 0 ) / 𝑥 ] 𝜓 ) )
89 88 imbi2d ⊢ ( 𝑏 = 0 → ( ( [ 𝑎 / 𝑥 ] 𝜓 → [ ( 𝑎 + 𝑏 ) / 𝑥 ] 𝜓 ) ↔ ( [ 𝑎 / 𝑥 ] 𝜓 → [ ( 𝑎 + 0 ) / 𝑥 ] 𝜓 ) ) )
90 89 ralbidv ⊢ ( 𝑏 = 0 → ( ∀ 𝑎 ∈ 𝐵 ( [ 𝑎 / 𝑥 ] 𝜓 → [ ( 𝑎 + 𝑏 ) / 𝑥 ] 𝜓 ) ↔ ∀ 𝑎 ∈ 𝐵 ( [ 𝑎 / 𝑥 ] 𝜓 → [ ( 𝑎 + 0 ) / 𝑥 ] 𝜓 ) ) )
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 ⊢ ( 𝜑 → { 𝑏 ∈ 𝐵 ∣ ∀ 𝑎 ∈ 𝐵 ( [ 𝑎 / 𝑥 ] 𝜓 → [ ( 𝑎 + 𝑏 ) / 𝑥 ] 𝜓 ) } ∈ ( SubMnd ‘ 𝑀 ) )
104 eqid ⊢ ( mrCls ‘ ( SubMnd ‘ 𝑀 ) ) = ( mrCls ‘ ( SubMnd ‘ 𝑀 ) )
105 104 mrcsscl ⊢ ( ( ( SubMnd ‘ 𝑀 ) ∈ ( Moore ‘ 𝐵 ) ∧ 𝐺 ⊆ { 𝑏 ∈ 𝐵 ∣ ∀ 𝑎 ∈ 𝐵 ( [ 𝑎 / 𝑥 ] 𝜓 → [ ( 𝑎 + 𝑏 ) / 𝑥 ] 𝜓 ) } ∧ { 𝑏 ∈ 𝐵 ∣ ∀ 𝑎 ∈ 𝐵 ( [ 𝑎 / 𝑥 ] 𝜓 → [ ( 𝑎 + 𝑏 ) / 𝑥 ] 𝜓 ) } ∈ ( SubMnd ‘ 𝑀 ) ) → ( ( mrCls ‘ ( SubMnd ‘ 𝑀 ) ) ‘ 𝐺 ) ⊆ { 𝑏 ∈ 𝐵 ∣ ∀ 𝑎 ∈ 𝐵 ( [ 𝑎 / 𝑥 ] 𝜓 → [ ( 𝑎 + 𝑏 ) / 𝑥 ] 𝜓 ) } )
106 25 52 103 105 syl3anc ⊢ ( 𝜑 → ( ( mrCls ‘ ( SubMnd ‘ 𝑀 ) ) ‘ 𝐺 ) ⊆ { 𝑏 ∈ 𝐵 ∣ ∀ 𝑎 ∈ 𝐵 ( [ 𝑎 / 𝑥 ] 𝜓 → [ ( 𝑎 + 𝑏 ) / 𝑥 ] 𝜓 ) } )
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 ⊢ ( 𝜑 → ( [ 0 / 𝑥 ] 𝜓 → [ ( 0 + 𝐴 ) / 𝑥 ] 𝜓 ) )
117 18 116 mpd ⊢ ( 𝜑 → [ ( 0 + 𝐴 ) / 𝑥 ] 𝜓 )
118 7 6 5 mndlid ⊢ ( ( 𝑀 ∈ Mnd ∧ 𝐴 ∈ 𝐵 ) → ( 0 + 𝐴 ) = 𝐴 )
119 8 13 118 syl2anc ⊢ ( 𝜑 → ( 0 + 𝐴 ) = 𝐴 )
120 119 sbceq1d ⊢ ( 𝜑 → ( [ ( 0 + 𝐴 ) / 𝑥 ] 𝜓 ↔ [ 𝐴 / 𝑥 ] 𝜓 ) )
121 4 sbcieg ⊢ ( 𝐴 ∈ 𝐵 → ( [ 𝐴 / 𝑥 ] 𝜓 ↔ 𝜂 ) )
122 13 121 syl ⊢ ( 𝜑 → ( [ 𝐴 / 𝑥 ] 𝜓 ↔ 𝜂 ) )
123 120 122 bitrd ⊢ ( 𝜑 → ( [ ( 0 + 𝐴 ) / 𝑥 ] 𝜓 ↔ 𝜂 ) )
124 117 123 mpbid ⊢ ( 𝜑 → 𝜂 )