MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mndind Structured version   Visualization version   GIF version

Theorem mndind 18709
Description: Induction in a monoid. In this theorem, πœ“(π‘₯) 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 𝐺). The hypothesis mndind.k tells that 𝐺 is generating. (Contributed by SO, 14-Jul-2018.)
Hypotheses
Ref Expression
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
Ref Expression
mndind (πœ‘ β†’ πœ‚)
Distinct variable groups:   πœ‘,π‘₯,𝑦,𝑧   πœ“,𝑦,𝑧   πœ’,π‘₯,𝑧   πœƒ,π‘₯   π‘₯, 0   π‘₯,𝐴   𝜏,π‘₯   πœ‚,π‘₯   𝑦,𝐺,𝑧   𝑦,𝐡,𝑧   π‘₯, + ,𝑦,𝑧
Allowed substitution hints:   πœ“(π‘₯)   πœ’(𝑦)   πœƒ(𝑦,𝑧)   𝜏(𝑦,𝑧)   πœ‚(𝑦,𝑧)   𝐴(𝑦,𝑧)   𝐡(π‘₯)   𝐺(π‘₯)   𝑀(π‘₯,𝑦,𝑧)   0 (𝑦,𝑧)

Proof of Theorem mndind
Dummy variables π‘Ž 𝑏 𝑐 𝑑 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 mndind.i1 . . . 4 (πœ‘ β†’ 𝜏)
2 mndind.m . . . . . 6 (πœ‘ β†’ 𝑀 ∈ Mnd)
3 mndind.b . . . . . . 7 𝐡 = (Baseβ€˜π‘€)
4 mndind.0g . . . . . . 7 0 = (0gβ€˜π‘€)
53, 4mndidcl 18640 . . . . . 6 (𝑀 ∈ Mnd β†’ 0 ∈ 𝐡)
62, 5syl 17 . . . . 5 (πœ‘ β†’ 0 ∈ 𝐡)
7 mndind.ta . . . . . 6 (π‘₯ = 0 β†’ (πœ“ ↔ 𝜏))
87sbcieg 3818 . . . . 5 ( 0 ∈ 𝐡 β†’ ([ 0 / π‘₯]πœ“ ↔ 𝜏))
96, 8syl 17 . . . 4 (πœ‘ β†’ ([ 0 / π‘₯]πœ“ ↔ 𝜏))
101, 9mpbird 257 . . 3 (πœ‘ β†’ [ 0 / π‘₯]πœ“)
11 dfsbcq 3780 . . . . 5 (π‘Ž = 0 β†’ ([π‘Ž / π‘₯]πœ“ ↔ [ 0 / π‘₯]πœ“))
12 oveq1 7416 . . . . . 6 (π‘Ž = 0 β†’ (π‘Ž + 𝐴) = ( 0 + 𝐴))
1312sbceq1d 3783 . . . . 5 (π‘Ž = 0 β†’ ([(π‘Ž + 𝐴) / π‘₯]πœ“ ↔ [( 0 + 𝐴) / π‘₯]πœ“))
1411, 13imbi12d 345 . . . 4 (π‘Ž = 0 β†’ (([π‘Ž / π‘₯]πœ“ β†’ [(π‘Ž + 𝐴) / π‘₯]πœ“) ↔ ([ 0 / π‘₯]πœ“ β†’ [( 0 + 𝐴) / π‘₯]πœ“)))
15 mndind.k . . . . . . 7 (πœ‘ β†’ 𝐡 = ((mrClsβ€˜(SubMndβ€˜π‘€))β€˜πΊ))
163submacs 18708 . . . . . . . . . 10 (𝑀 ∈ Mnd β†’ (SubMndβ€˜π‘€) ∈ (ACSβ€˜π΅))
172, 16syl 17 . . . . . . . . 9 (πœ‘ β†’ (SubMndβ€˜π‘€) ∈ (ACSβ€˜π΅))
1817acsmred 17600 . . . . . . . 8 (πœ‘ β†’ (SubMndβ€˜π‘€) ∈ (Mooreβ€˜π΅))
19 mndind.g . . . . . . . . 9 (πœ‘ β†’ 𝐺 βŠ† 𝐡)
20 eleq1w 2817 . . . . . . . . . . . . 13 (𝑦 = π‘Ž β†’ (𝑦 ∈ 𝐡 ↔ π‘Ž ∈ 𝐡))
2120anbi2d 630 . . . . . . . . . . . 12 (𝑦 = π‘Ž β†’ (((πœ‘ ∧ 𝑏 ∈ 𝐺) ∧ 𝑦 ∈ 𝐡) ↔ ((πœ‘ ∧ 𝑏 ∈ 𝐺) ∧ π‘Ž ∈ 𝐡)))
22 vex 3479 . . . . . . . . . . . . . . 15 𝑦 ∈ V
23 mndind.ch . . . . . . . . . . . . . . 15 (π‘₯ = 𝑦 β†’ (πœ“ ↔ πœ’))
2422, 23sbcie 3821 . . . . . . . . . . . . . 14 ([𝑦 / π‘₯]πœ“ ↔ πœ’)
25 dfsbcq 3780 . . . . . . . . . . . . . 14 (𝑦 = π‘Ž β†’ ([𝑦 / π‘₯]πœ“ ↔ [π‘Ž / π‘₯]πœ“))
2624, 25bitr3id 285 . . . . . . . . . . . . 13 (𝑦 = π‘Ž β†’ (πœ’ ↔ [π‘Ž / π‘₯]πœ“))
27 oveq1 7416 . . . . . . . . . . . . . 14 (𝑦 = π‘Ž β†’ (𝑦 + 𝑏) = (π‘Ž + 𝑏))
2827sbceq1d 3783 . . . . . . . . . . . . 13 (𝑦 = π‘Ž β†’ ([(𝑦 + 𝑏) / π‘₯]πœ“ ↔ [(π‘Ž + 𝑏) / π‘₯]πœ“))
2926, 28imbi12d 345 . . . . . . . . . . . 12 (𝑦 = π‘Ž β†’ ((πœ’ β†’ [(𝑦 + 𝑏) / π‘₯]πœ“) ↔ ([π‘Ž / π‘₯]πœ“ β†’ [(π‘Ž + 𝑏) / π‘₯]πœ“)))
3021, 29imbi12d 345 . . . . . . . . . . 11 (𝑦 = π‘Ž β†’ ((((πœ‘ ∧ 𝑏 ∈ 𝐺) ∧ 𝑦 ∈ 𝐡) β†’ (πœ’ β†’ [(𝑦 + 𝑏) / π‘₯]πœ“)) ↔ (((πœ‘ ∧ 𝑏 ∈ 𝐺) ∧ π‘Ž ∈ 𝐡) β†’ ([π‘Ž / π‘₯]πœ“ β†’ [(π‘Ž + 𝑏) / π‘₯]πœ“))))
31 eleq1w 2817 . . . . . . . . . . . . . . 15 (𝑧 = 𝑏 β†’ (𝑧 ∈ 𝐺 ↔ 𝑏 ∈ 𝐺))
3231anbi2d 630 . . . . . . . . . . . . . 14 (𝑧 = 𝑏 β†’ ((πœ‘ ∧ 𝑧 ∈ 𝐺) ↔ (πœ‘ ∧ 𝑏 ∈ 𝐺)))
3332anbi1d 631 . . . . . . . . . . . . 13 (𝑧 = 𝑏 β†’ (((πœ‘ ∧ 𝑧 ∈ 𝐺) ∧ 𝑦 ∈ 𝐡) ↔ ((πœ‘ ∧ 𝑏 ∈ 𝐺) ∧ 𝑦 ∈ 𝐡)))
34 ovex 7442 . . . . . . . . . . . . . . . 16 (𝑦 + 𝑧) ∈ V
35 mndind.th . . . . . . . . . . . . . . . 16 (π‘₯ = (𝑦 + 𝑧) β†’ (πœ“ ↔ πœƒ))
3634, 35sbcie 3821 . . . . . . . . . . . . . . 15 ([(𝑦 + 𝑧) / π‘₯]πœ“ ↔ πœƒ)
37 oveq2 7417 . . . . . . . . . . . . . . . 16 (𝑧 = 𝑏 β†’ (𝑦 + 𝑧) = (𝑦 + 𝑏))
3837sbceq1d 3783 . . . . . . . . . . . . . . 15 (𝑧 = 𝑏 β†’ ([(𝑦 + 𝑧) / π‘₯]πœ“ ↔ [(𝑦 + 𝑏) / π‘₯]πœ“))
3936, 38bitr3id 285 . . . . . . . . . . . . . 14 (𝑧 = 𝑏 β†’ (πœƒ ↔ [(𝑦 + 𝑏) / π‘₯]πœ“))
4039imbi2d 341 . . . . . . . . . . . . 13 (𝑧 = 𝑏 β†’ ((πœ’ β†’ πœƒ) ↔ (πœ’ β†’ [(𝑦 + 𝑏) / π‘₯]πœ“)))
4133, 40imbi12d 345 . . . . . . . . . . . 12 (𝑧 = 𝑏 β†’ ((((πœ‘ ∧ 𝑧 ∈ 𝐺) ∧ 𝑦 ∈ 𝐡) β†’ (πœ’ β†’ πœƒ)) ↔ (((πœ‘ ∧ 𝑏 ∈ 𝐺) ∧ 𝑦 ∈ 𝐡) β†’ (πœ’ β†’ [(𝑦 + 𝑏) / π‘₯]πœ“))))
42 mndind.i2 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐺) ∧ πœ’) β†’ πœƒ)
4342ex 414 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑦 ∈ 𝐡 ∧ 𝑧 ∈ 𝐺) β†’ (πœ’ β†’ πœƒ))
44433expa 1119 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 ∈ 𝐺) β†’ (πœ’ β†’ πœƒ))
4544an32s 651 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑧 ∈ 𝐺) ∧ 𝑦 ∈ 𝐡) β†’ (πœ’ β†’ πœƒ))
4641, 45chvarvv 2003 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑏 ∈ 𝐺) ∧ 𝑦 ∈ 𝐡) β†’ (πœ’ β†’ [(𝑦 + 𝑏) / π‘₯]πœ“))
4730, 46chvarvv 2003 . . . . . . . . . 10 (((πœ‘ ∧ 𝑏 ∈ 𝐺) ∧ π‘Ž ∈ 𝐡) β†’ ([π‘Ž / π‘₯]πœ“ β†’ [(π‘Ž + 𝑏) / π‘₯]πœ“))
4847ralrimiva 3147 . . . . . . . . 9 ((πœ‘ ∧ 𝑏 ∈ 𝐺) β†’ βˆ€π‘Ž ∈ 𝐡 ([π‘Ž / π‘₯]πœ“ β†’ [(π‘Ž + 𝑏) / π‘₯]πœ“))
4919, 48ssrabdv 4072 . . . . . . . 8 (πœ‘ β†’ 𝐺 βŠ† {𝑏 ∈ 𝐡 ∣ βˆ€π‘Ž ∈ 𝐡 ([π‘Ž / π‘₯]πœ“ β†’ [(π‘Ž + 𝑏) / π‘₯]πœ“)})
50 mndind.pg . . . . . . . . 9 + = (+gβ€˜π‘€)
513, 50, 4mndrid 18646 . . . . . . . . . . . . 13 ((𝑀 ∈ Mnd ∧ π‘Ž ∈ 𝐡) β†’ (π‘Ž + 0 ) = π‘Ž)
522, 51sylan 581 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘Ž ∈ 𝐡) β†’ (π‘Ž + 0 ) = π‘Ž)
5352sbceq1d 3783 . . . . . . . . . . 11 ((πœ‘ ∧ π‘Ž ∈ 𝐡) β†’ ([(π‘Ž + 0 ) / π‘₯]πœ“ ↔ [π‘Ž / π‘₯]πœ“))
5453biimprd 247 . . . . . . . . . 10 ((πœ‘ ∧ π‘Ž ∈ 𝐡) β†’ ([π‘Ž / π‘₯]πœ“ β†’ [(π‘Ž + 0 ) / π‘₯]πœ“))
5554ralrimiva 3147 . . . . . . . . 9 (πœ‘ β†’ βˆ€π‘Ž ∈ 𝐡 ([π‘Ž / π‘₯]πœ“ β†’ [(π‘Ž + 0 ) / π‘₯]πœ“))
56 simprrl 780 . . . . . . . . . 10 ((πœ‘ ∧ ((𝑐 ∈ 𝐡 ∧ 𝑑 ∈ 𝐡) ∧ (βˆ€π‘Ž ∈ 𝐡 ([π‘Ž / π‘₯]πœ“ β†’ [(π‘Ž + 𝑐) / π‘₯]πœ“) ∧ βˆ€π‘Ž ∈ 𝐡 ([π‘Ž / π‘₯]πœ“ β†’ [(π‘Ž + 𝑑) / π‘₯]πœ“)))) β†’ βˆ€π‘Ž ∈ 𝐡 ([π‘Ž / π‘₯]πœ“ β†’ [(π‘Ž + 𝑐) / π‘₯]πœ“))
572ad2antrr 725 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ (𝑐 ∈ 𝐡 ∧ 𝑑 ∈ 𝐡)) ∧ 𝑏 ∈ 𝐡) β†’ 𝑀 ∈ Mnd)
58 simpr 486 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ (𝑐 ∈ 𝐡 ∧ 𝑑 ∈ 𝐡)) ∧ 𝑏 ∈ 𝐡) β†’ 𝑏 ∈ 𝐡)
59 simplrl 776 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ (𝑐 ∈ 𝐡 ∧ 𝑑 ∈ 𝐡)) ∧ 𝑏 ∈ 𝐡) β†’ 𝑐 ∈ 𝐡)
603, 50mndcl 18633 . . . . . . . . . . . . . . . 16 ((𝑀 ∈ Mnd ∧ 𝑏 ∈ 𝐡 ∧ 𝑐 ∈ 𝐡) β†’ (𝑏 + 𝑐) ∈ 𝐡)
6157, 58, 59, 60syl3anc 1372 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ (𝑐 ∈ 𝐡 ∧ 𝑑 ∈ 𝐡)) ∧ 𝑏 ∈ 𝐡) β†’ (𝑏 + 𝑐) ∈ 𝐡)
62 simpr 486 . . . . . . . . . . . . . . . . 17 ((((πœ‘ ∧ (𝑐 ∈ 𝐡 ∧ 𝑑 ∈ 𝐡)) ∧ 𝑏 ∈ 𝐡) ∧ π‘Ž = (𝑏 + 𝑐)) β†’ π‘Ž = (𝑏 + 𝑐))
6362sbceq1d 3783 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ (𝑐 ∈ 𝐡 ∧ 𝑑 ∈ 𝐡)) ∧ 𝑏 ∈ 𝐡) ∧ π‘Ž = (𝑏 + 𝑐)) β†’ ([π‘Ž / π‘₯]πœ“ ↔ [(𝑏 + 𝑐) / π‘₯]πœ“))
64 oveq1 7416 . . . . . . . . . . . . . . . . . 18 (π‘Ž = (𝑏 + 𝑐) β†’ (π‘Ž + 𝑑) = ((𝑏 + 𝑐) + 𝑑))
65 simplrr 777 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ (𝑐 ∈ 𝐡 ∧ 𝑑 ∈ 𝐡)) ∧ 𝑏 ∈ 𝐡) β†’ 𝑑 ∈ 𝐡)
663, 50mndass 18634 . . . . . . . . . . . . . . . . . . 19 ((𝑀 ∈ Mnd ∧ (𝑏 ∈ 𝐡 ∧ 𝑐 ∈ 𝐡 ∧ 𝑑 ∈ 𝐡)) β†’ ((𝑏 + 𝑐) + 𝑑) = (𝑏 + (𝑐 + 𝑑)))
6757, 58, 59, 65, 66syl13anc 1373 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ (𝑐 ∈ 𝐡 ∧ 𝑑 ∈ 𝐡)) ∧ 𝑏 ∈ 𝐡) β†’ ((𝑏 + 𝑐) + 𝑑) = (𝑏 + (𝑐 + 𝑑)))
6864, 67sylan9eqr 2795 . . . . . . . . . . . . . . . . 17 ((((πœ‘ ∧ (𝑐 ∈ 𝐡 ∧ 𝑑 ∈ 𝐡)) ∧ 𝑏 ∈ 𝐡) ∧ π‘Ž = (𝑏 + 𝑐)) β†’ (π‘Ž + 𝑑) = (𝑏 + (𝑐 + 𝑑)))
6968sbceq1d 3783 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ (𝑐 ∈ 𝐡 ∧ 𝑑 ∈ 𝐡)) ∧ 𝑏 ∈ 𝐡) ∧ π‘Ž = (𝑏 + 𝑐)) β†’ ([(π‘Ž + 𝑑) / π‘₯]πœ“ ↔ [(𝑏 + (𝑐 + 𝑑)) / π‘₯]πœ“))
7063, 69imbi12d 345 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ (𝑐 ∈ 𝐡 ∧ 𝑑 ∈ 𝐡)) ∧ 𝑏 ∈ 𝐡) ∧ π‘Ž = (𝑏 + 𝑐)) β†’ (([π‘Ž / π‘₯]πœ“ β†’ [(π‘Ž + 𝑑) / π‘₯]πœ“) ↔ ([(𝑏 + 𝑐) / π‘₯]πœ“ β†’ [(𝑏 + (𝑐 + 𝑑)) / π‘₯]πœ“)))
7161, 70rspcdv 3605 . . . . . . . . . . . . . 14 (((πœ‘ ∧ (𝑐 ∈ 𝐡 ∧ 𝑑 ∈ 𝐡)) ∧ 𝑏 ∈ 𝐡) β†’ (βˆ€π‘Ž ∈ 𝐡 ([π‘Ž / π‘₯]πœ“ β†’ [(π‘Ž + 𝑑) / π‘₯]πœ“) β†’ ([(𝑏 + 𝑐) / π‘₯]πœ“ β†’ [(𝑏 + (𝑐 + 𝑑)) / π‘₯]πœ“)))
7271ralrimdva 3155 . . . . . . . . . . . . 13 ((πœ‘ ∧ (𝑐 ∈ 𝐡 ∧ 𝑑 ∈ 𝐡)) β†’ (βˆ€π‘Ž ∈ 𝐡 ([π‘Ž / π‘₯]πœ“ β†’ [(π‘Ž + 𝑑) / π‘₯]πœ“) β†’ βˆ€π‘ ∈ 𝐡 ([(𝑏 + 𝑐) / π‘₯]πœ“ β†’ [(𝑏 + (𝑐 + 𝑑)) / π‘₯]πœ“)))
7372impr 456 . . . . . . . . . . . 12 ((πœ‘ ∧ ((𝑐 ∈ 𝐡 ∧ 𝑑 ∈ 𝐡) ∧ βˆ€π‘Ž ∈ 𝐡 ([π‘Ž / π‘₯]πœ“ β†’ [(π‘Ž + 𝑑) / π‘₯]πœ“))) β†’ βˆ€π‘ ∈ 𝐡 ([(𝑏 + 𝑐) / π‘₯]πœ“ β†’ [(𝑏 + (𝑐 + 𝑑)) / π‘₯]πœ“))
74 oveq1 7416 . . . . . . . . . . . . . . 15 (𝑏 = π‘Ž β†’ (𝑏 + 𝑐) = (π‘Ž + 𝑐))
7574sbceq1d 3783 . . . . . . . . . . . . . 14 (𝑏 = π‘Ž β†’ ([(𝑏 + 𝑐) / π‘₯]πœ“ ↔ [(π‘Ž + 𝑐) / π‘₯]πœ“))
76 oveq1 7416 . . . . . . . . . . . . . . 15 (𝑏 = π‘Ž β†’ (𝑏 + (𝑐 + 𝑑)) = (π‘Ž + (𝑐 + 𝑑)))
7776sbceq1d 3783 . . . . . . . . . . . . . 14 (𝑏 = π‘Ž β†’ ([(𝑏 + (𝑐 + 𝑑)) / π‘₯]πœ“ ↔ [(π‘Ž + (𝑐 + 𝑑)) / π‘₯]πœ“))
7875, 77imbi12d 345 . . . . . . . . . . . . 13 (𝑏 = π‘Ž β†’ (([(𝑏 + 𝑐) / π‘₯]πœ“ β†’ [(𝑏 + (𝑐 + 𝑑)) / π‘₯]πœ“) ↔ ([(π‘Ž + 𝑐) / π‘₯]πœ“ β†’ [(π‘Ž + (𝑐 + 𝑑)) / π‘₯]πœ“)))
7978cbvralvw 3235 . . . . . . . . . . . 12 (βˆ€π‘ ∈ 𝐡 ([(𝑏 + 𝑐) / π‘₯]πœ“ β†’ [(𝑏 + (𝑐 + 𝑑)) / π‘₯]πœ“) ↔ βˆ€π‘Ž ∈ 𝐡 ([(π‘Ž + 𝑐) / π‘₯]πœ“ β†’ [(π‘Ž + (𝑐 + 𝑑)) / π‘₯]πœ“))
8073, 79sylib 217 . . . . . . . . . . 11 ((πœ‘ ∧ ((𝑐 ∈ 𝐡 ∧ 𝑑 ∈ 𝐡) ∧ βˆ€π‘Ž ∈ 𝐡 ([π‘Ž / π‘₯]πœ“ β†’ [(π‘Ž + 𝑑) / π‘₯]πœ“))) β†’ βˆ€π‘Ž ∈ 𝐡 ([(π‘Ž + 𝑐) / π‘₯]πœ“ β†’ [(π‘Ž + (𝑐 + 𝑑)) / π‘₯]πœ“))
8180adantrrl 723 . . . . . . . . . 10 ((πœ‘ ∧ ((𝑐 ∈ 𝐡 ∧ 𝑑 ∈ 𝐡) ∧ (βˆ€π‘Ž ∈ 𝐡 ([π‘Ž / π‘₯]πœ“ β†’ [(π‘Ž + 𝑐) / π‘₯]πœ“) ∧ βˆ€π‘Ž ∈ 𝐡 ([π‘Ž / π‘₯]πœ“ β†’ [(π‘Ž + 𝑑) / π‘₯]πœ“)))) β†’ βˆ€π‘Ž ∈ 𝐡 ([(π‘Ž + 𝑐) / π‘₯]πœ“ β†’ [(π‘Ž + (𝑐 + 𝑑)) / π‘₯]πœ“))
82 imim1 83 . . . . . . . . . . 11 (([π‘Ž / π‘₯]πœ“ β†’ [(π‘Ž + 𝑐) / π‘₯]πœ“) β†’ (([(π‘Ž + 𝑐) / π‘₯]πœ“ β†’ [(π‘Ž + (𝑐 + 𝑑)) / π‘₯]πœ“) β†’ ([π‘Ž / π‘₯]πœ“ β†’ [(π‘Ž + (𝑐 + 𝑑)) / π‘₯]πœ“)))
8382ral2imi 3086 . . . . . . . . . 10 (βˆ€π‘Ž ∈ 𝐡 ([π‘Ž / π‘₯]πœ“ β†’ [(π‘Ž + 𝑐) / π‘₯]πœ“) β†’ (βˆ€π‘Ž ∈ 𝐡 ([(π‘Ž + 𝑐) / π‘₯]πœ“ β†’ [(π‘Ž + (𝑐 + 𝑑)) / π‘₯]πœ“) β†’ βˆ€π‘Ž ∈ 𝐡 ([π‘Ž / π‘₯]πœ“ β†’ [(π‘Ž + (𝑐 + 𝑑)) / π‘₯]πœ“)))
8456, 81, 83sylc 65 . . . . . . . . 9 ((πœ‘ ∧ ((𝑐 ∈ 𝐡 ∧ 𝑑 ∈ 𝐡) ∧ (βˆ€π‘Ž ∈ 𝐡 ([π‘Ž / π‘₯]πœ“ β†’ [(π‘Ž + 𝑐) / π‘₯]πœ“) ∧ βˆ€π‘Ž ∈ 𝐡 ([π‘Ž / π‘₯]πœ“ β†’ [(π‘Ž + 𝑑) / π‘₯]πœ“)))) β†’ βˆ€π‘Ž ∈ 𝐡 ([π‘Ž / π‘₯]πœ“ β†’ [(π‘Ž + (𝑐 + 𝑑)) / π‘₯]πœ“))
85 oveq2 7417 . . . . . . . . . . . 12 (𝑏 = 0 β†’ (π‘Ž + 𝑏) = (π‘Ž + 0 ))
8685sbceq1d 3783 . . . . . . . . . . 11 (𝑏 = 0 β†’ ([(π‘Ž + 𝑏) / π‘₯]πœ“ ↔ [(π‘Ž + 0 ) / π‘₯]πœ“))
8786imbi2d 341 . . . . . . . . . 10 (𝑏 = 0 β†’ (([π‘Ž / π‘₯]πœ“ β†’ [(π‘Ž + 𝑏) / π‘₯]πœ“) ↔ ([π‘Ž / π‘₯]πœ“ β†’ [(π‘Ž + 0 ) / π‘₯]πœ“)))
8887ralbidv 3178 . . . . . . . . 9 (𝑏 = 0 β†’ (βˆ€π‘Ž ∈ 𝐡 ([π‘Ž / π‘₯]πœ“ β†’ [(π‘Ž + 𝑏) / π‘₯]πœ“) ↔ βˆ€π‘Ž ∈ 𝐡 ([π‘Ž / π‘₯]πœ“ β†’ [(π‘Ž + 0 ) / π‘₯]πœ“)))
89 oveq2 7417 . . . . . . . . . . . 12 (𝑏 = 𝑐 β†’ (π‘Ž + 𝑏) = (π‘Ž + 𝑐))
9089sbceq1d 3783 . . . . . . . . . . 11 (𝑏 = 𝑐 β†’ ([(π‘Ž + 𝑏) / π‘₯]πœ“ ↔ [(π‘Ž + 𝑐) / π‘₯]πœ“))
9190imbi2d 341 . . . . . . . . . 10 (𝑏 = 𝑐 β†’ (([π‘Ž / π‘₯]πœ“ β†’ [(π‘Ž + 𝑏) / π‘₯]πœ“) ↔ ([π‘Ž / π‘₯]πœ“ β†’ [(π‘Ž + 𝑐) / π‘₯]πœ“)))
9291ralbidv 3178 . . . . . . . . 9 (𝑏 = 𝑐 β†’ (βˆ€π‘Ž ∈ 𝐡 ([π‘Ž / π‘₯]πœ“ β†’ [(π‘Ž + 𝑏) / π‘₯]πœ“) ↔ βˆ€π‘Ž ∈ 𝐡 ([π‘Ž / π‘₯]πœ“ β†’ [(π‘Ž + 𝑐) / π‘₯]πœ“)))
93 oveq2 7417 . . . . . . . . . . . 12 (𝑏 = 𝑑 β†’ (π‘Ž + 𝑏) = (π‘Ž + 𝑑))
9493sbceq1d 3783 . . . . . . . . . . 11 (𝑏 = 𝑑 β†’ ([(π‘Ž + 𝑏) / π‘₯]πœ“ ↔ [(π‘Ž + 𝑑) / π‘₯]πœ“))
9594imbi2d 341 . . . . . . . . . 10 (𝑏 = 𝑑 β†’ (([π‘Ž / π‘₯]πœ“ β†’ [(π‘Ž + 𝑏) / π‘₯]πœ“) ↔ ([π‘Ž / π‘₯]πœ“ β†’ [(π‘Ž + 𝑑) / π‘₯]πœ“)))
9695ralbidv 3178 . . . . . . . . 9 (𝑏 = 𝑑 β†’ (βˆ€π‘Ž ∈ 𝐡 ([π‘Ž / π‘₯]πœ“ β†’ [(π‘Ž + 𝑏) / π‘₯]πœ“) ↔ βˆ€π‘Ž ∈ 𝐡 ([π‘Ž / π‘₯]πœ“ β†’ [(π‘Ž + 𝑑) / π‘₯]πœ“)))
97 oveq2 7417 . . . . . . . . . . . 12 (𝑏 = (𝑐 + 𝑑) β†’ (π‘Ž + 𝑏) = (π‘Ž + (𝑐 + 𝑑)))
9897sbceq1d 3783 . . . . . . . . . . 11 (𝑏 = (𝑐 + 𝑑) β†’ ([(π‘Ž + 𝑏) / π‘₯]πœ“ ↔ [(π‘Ž + (𝑐 + 𝑑)) / π‘₯]πœ“))
9998imbi2d 341 . . . . . . . . . 10 (𝑏 = (𝑐 + 𝑑) β†’ (([π‘Ž / π‘₯]πœ“ β†’ [(π‘Ž + 𝑏) / π‘₯]πœ“) ↔ ([π‘Ž / π‘₯]πœ“ β†’ [(π‘Ž + (𝑐 + 𝑑)) / π‘₯]πœ“)))
10099ralbidv 3178 . . . . . . . . 9 (𝑏 = (𝑐 + 𝑑) β†’ (βˆ€π‘Ž ∈ 𝐡 ([π‘Ž / π‘₯]πœ“ β†’ [(π‘Ž + 𝑏) / π‘₯]πœ“) ↔ βˆ€π‘Ž ∈ 𝐡 ([π‘Ž / π‘₯]πœ“ β†’ [(π‘Ž + (𝑐 + 𝑑)) / π‘₯]πœ“)))
1013, 50, 4, 2, 55, 84, 88, 92, 96, 100issubmd 18687 . . . . . . . 8 (πœ‘ β†’ {𝑏 ∈ 𝐡 ∣ βˆ€π‘Ž ∈ 𝐡 ([π‘Ž / π‘₯]πœ“ β†’ [(π‘Ž + 𝑏) / π‘₯]πœ“)} ∈ (SubMndβ€˜π‘€))
102 eqid 2733 . . . . . . . . 9 (mrClsβ€˜(SubMndβ€˜π‘€)) = (mrClsβ€˜(SubMndβ€˜π‘€))
103102mrcsscl 17564 . . . . . . . 8 (((SubMndβ€˜π‘€) ∈ (Mooreβ€˜π΅) ∧ 𝐺 βŠ† {𝑏 ∈ 𝐡 ∣ βˆ€π‘Ž ∈ 𝐡 ([π‘Ž / π‘₯]πœ“ β†’ [(π‘Ž + 𝑏) / π‘₯]πœ“)} ∧ {𝑏 ∈ 𝐡 ∣ βˆ€π‘Ž ∈ 𝐡 ([π‘Ž / π‘₯]πœ“ β†’ [(π‘Ž + 𝑏) / π‘₯]πœ“)} ∈ (SubMndβ€˜π‘€)) β†’ ((mrClsβ€˜(SubMndβ€˜π‘€))β€˜πΊ) βŠ† {𝑏 ∈ 𝐡 ∣ βˆ€π‘Ž ∈ 𝐡 ([π‘Ž / π‘₯]πœ“ β†’ [(π‘Ž + 𝑏) / π‘₯]πœ“)})
10418, 49, 101, 103syl3anc 1372 . . . . . . 7 (πœ‘ β†’ ((mrClsβ€˜(SubMndβ€˜π‘€))β€˜πΊ) βŠ† {𝑏 ∈ 𝐡 ∣ βˆ€π‘Ž ∈ 𝐡 ([π‘Ž / π‘₯]πœ“ β†’ [(π‘Ž + 𝑏) / π‘₯]πœ“)})
10515, 104eqsstrd 4021 . . . . . 6 (πœ‘ β†’ 𝐡 βŠ† {𝑏 ∈ 𝐡 ∣ βˆ€π‘Ž ∈ 𝐡 ([π‘Ž / π‘₯]πœ“ β†’ [(π‘Ž + 𝑏) / π‘₯]πœ“)})
106 mndind.a . . . . . 6 (πœ‘ β†’ 𝐴 ∈ 𝐡)
107105, 106sseldd 3984 . . . . 5 (πœ‘ β†’ 𝐴 ∈ {𝑏 ∈ 𝐡 ∣ βˆ€π‘Ž ∈ 𝐡 ([π‘Ž / π‘₯]πœ“ β†’ [(π‘Ž + 𝑏) / π‘₯]πœ“)})
108 oveq2 7417 . . . . . . . . . 10 (𝑏 = 𝐴 β†’ (π‘Ž + 𝑏) = (π‘Ž + 𝐴))
109108sbceq1d 3783 . . . . . . . . 9 (𝑏 = 𝐴 β†’ ([(π‘Ž + 𝑏) / π‘₯]πœ“ ↔ [(π‘Ž + 𝐴) / π‘₯]πœ“))
110109imbi2d 341 . . . . . . . 8 (𝑏 = 𝐴 β†’ (([π‘Ž / π‘₯]πœ“ β†’ [(π‘Ž + 𝑏) / π‘₯]πœ“) ↔ ([π‘Ž / π‘₯]πœ“ β†’ [(π‘Ž + 𝐴) / π‘₯]πœ“)))
111110ralbidv 3178 . . . . . . 7 (𝑏 = 𝐴 β†’ (βˆ€π‘Ž ∈ 𝐡 ([π‘Ž / π‘₯]πœ“ β†’ [(π‘Ž + 𝑏) / π‘₯]πœ“) ↔ βˆ€π‘Ž ∈ 𝐡 ([π‘Ž / π‘₯]πœ“ β†’ [(π‘Ž + 𝐴) / π‘₯]πœ“)))
112111elrab 3684 . . . . . 6 (𝐴 ∈ {𝑏 ∈ 𝐡 ∣ βˆ€π‘Ž ∈ 𝐡 ([π‘Ž / π‘₯]πœ“ β†’ [(π‘Ž + 𝑏) / π‘₯]πœ“)} ↔ (𝐴 ∈ 𝐡 ∧ βˆ€π‘Ž ∈ 𝐡 ([π‘Ž / π‘₯]πœ“ β†’ [(π‘Ž + 𝐴) / π‘₯]πœ“)))
113112simprbi 498 . . . . 5 (𝐴 ∈ {𝑏 ∈ 𝐡 ∣ βˆ€π‘Ž ∈ 𝐡 ([π‘Ž / π‘₯]πœ“ β†’ [(π‘Ž + 𝑏) / π‘₯]πœ“)} β†’ βˆ€π‘Ž ∈ 𝐡 ([π‘Ž / π‘₯]πœ“ β†’ [(π‘Ž + 𝐴) / π‘₯]πœ“))
114107, 113syl 17 . . . 4 (πœ‘ β†’ βˆ€π‘Ž ∈ 𝐡 ([π‘Ž / π‘₯]πœ“ β†’ [(π‘Ž + 𝐴) / π‘₯]πœ“))
11514, 114, 6rspcdva 3614 . . 3 (πœ‘ β†’ ([ 0 / π‘₯]πœ“ β†’ [( 0 + 𝐴) / π‘₯]πœ“))
11610, 115mpd 15 . 2 (πœ‘ β†’ [( 0 + 𝐴) / π‘₯]πœ“)
1173, 50, 4mndlid 18645 . . . . 5 ((𝑀 ∈ Mnd ∧ 𝐴 ∈ 𝐡) β†’ ( 0 + 𝐴) = 𝐴)
1182, 106, 117syl2anc 585 . . . 4 (πœ‘ β†’ ( 0 + 𝐴) = 𝐴)
119118sbceq1d 3783 . . 3 (πœ‘ β†’ ([( 0 + 𝐴) / π‘₯]πœ“ ↔ [𝐴 / π‘₯]πœ“))
120 mndind.et . . . . 5 (π‘₯ = 𝐴 β†’ (πœ“ ↔ πœ‚))
121120sbcieg 3818 . . . 4 (𝐴 ∈ 𝐡 β†’ ([𝐴 / π‘₯]πœ“ ↔ πœ‚))
122106, 121syl 17 . . 3 (πœ‘ β†’ ([𝐴 / π‘₯]πœ“ ↔ πœ‚))
123119, 122bitrd 279 . 2 (πœ‘ β†’ ([( 0 + 𝐴) / π‘₯]πœ“ ↔ πœ‚))
124116, 123mpbid 231 1 (πœ‘ β†’ πœ‚)
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 397   ∧ w3a 1088   = wceq 1542   ∈ wcel 2107  βˆ€wral 3062  {crab 3433  [wsbc 3778   βŠ† wss 3949  β€˜cfv 6544  (class class class)co 7409  Basecbs 17144  +gcplusg 17197  0gc0g 17385  Moorecmre 17526  mrClscmrc 17527  ACScacs 17529  Mndcmnd 18625  SubMndcsubmnd 18670
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5300  ax-nul 5307  ax-pow 5364  ax-pr 5428  ax-un 7725
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-ral 3063  df-rex 3072  df-rmo 3377  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-int 4952  df-iun 5000  df-iin 5001  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5575  df-eprel 5581  df-po 5589  df-so 5590  df-fr 5632  df-we 5634  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-riota 7365  df-ov 7412  df-om 7856  df-1o 8466  df-en 8940  df-fin 8943  df-0g 17387  df-mre 17530  df-mrc 17531  df-acs 17533  df-mgm 18561  df-sgrp 18610  df-mnd 18626  df-submnd 18672
This theorem is referenced by:  mdetunilem7  22120
  Copyright terms: Public domain W3C validator