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

Theorem grplmulf1o 17688
Description: Left multiplication by a group element is a bijection on any group. (Contributed by Mario Carneiro, 17-Jan-2015.)
Hypotheses
Ref Expression
grplmulf1o.b 𝐵 = (Base‘𝐺)
grplmulf1o.p + = (+g𝐺)
grplmulf1o.n 𝐹 = (𝑥𝐵 ↦ (𝑋 + 𝑥))
Assertion
Ref Expression
grplmulf1o ((𝐺 ∈ Grp ∧ 𝑋𝐵) → 𝐹:𝐵1-1-onto𝐵)
Distinct variable groups:   𝑥,𝐵   𝑥,𝐺   𝑥, +   𝑥,𝑋
Allowed substitution hint:   𝐹(𝑥)

Proof of Theorem grplmulf1o
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 grplmulf1o.n . 2 𝐹 = (𝑥𝐵 ↦ (𝑋 + 𝑥))
2 grplmulf1o.b . . . 4 𝐵 = (Base‘𝐺)
3 grplmulf1o.p . . . 4 + = (+g𝐺)
42, 3grpcl 17629 . . 3 ((𝐺 ∈ Grp ∧ 𝑋𝐵𝑥𝐵) → (𝑋 + 𝑥) ∈ 𝐵)
543expa 1140 . 2 (((𝐺 ∈ Grp ∧ 𝑋𝐵) ∧ 𝑥𝐵) → (𝑋 + 𝑥) ∈ 𝐵)
6 simpl 470 . . . 4 ((𝐺 ∈ Grp ∧ 𝑋𝐵) → 𝐺 ∈ Grp)
7 eqid 2802 . . . . 5 (invg𝐺) = (invg𝐺)
82, 7grpinvcl 17666 . . . 4 ((𝐺 ∈ Grp ∧ 𝑋𝐵) → ((invg𝐺)‘𝑋) ∈ 𝐵)
96, 8jca 503 . . 3 ((𝐺 ∈ Grp ∧ 𝑋𝐵) → (𝐺 ∈ Grp ∧ ((invg𝐺)‘𝑋) ∈ 𝐵))
102, 3grpcl 17629 . . . 4 ((𝐺 ∈ Grp ∧ ((invg𝐺)‘𝑋) ∈ 𝐵𝑦𝐵) → (((invg𝐺)‘𝑋) + 𝑦) ∈ 𝐵)
11103expa 1140 . . 3 (((𝐺 ∈ Grp ∧ ((invg𝐺)‘𝑋) ∈ 𝐵) ∧ 𝑦𝐵) → (((invg𝐺)‘𝑋) + 𝑦) ∈ 𝐵)
129, 11sylan 571 . 2 (((𝐺 ∈ Grp ∧ 𝑋𝐵) ∧ 𝑦𝐵) → (((invg𝐺)‘𝑋) + 𝑦) ∈ 𝐵)
13 eqcom 2809 . . 3 (𝑥 = (((invg𝐺)‘𝑋) + 𝑦) ↔ (((invg𝐺)‘𝑋) + 𝑦) = 𝑥)
146adantr 468 . . . . 5 (((𝐺 ∈ Grp ∧ 𝑋𝐵) ∧ (𝑥𝐵𝑦𝐵)) → 𝐺 ∈ Grp)
1512adantrl 698 . . . . 5 (((𝐺 ∈ Grp ∧ 𝑋𝐵) ∧ (𝑥𝐵𝑦𝐵)) → (((invg𝐺)‘𝑋) + 𝑦) ∈ 𝐵)
16 simprl 778 . . . . 5 (((𝐺 ∈ Grp ∧ 𝑋𝐵) ∧ (𝑥𝐵𝑦𝐵)) → 𝑥𝐵)
17 simplr 776 . . . . 5 (((𝐺 ∈ Grp ∧ 𝑋𝐵) ∧ (𝑥𝐵𝑦𝐵)) → 𝑋𝐵)
182, 3grplcan 17676 . . . . 5 ((𝐺 ∈ Grp ∧ ((((invg𝐺)‘𝑋) + 𝑦) ∈ 𝐵𝑥𝐵𝑋𝐵)) → ((𝑋 + (((invg𝐺)‘𝑋) + 𝑦)) = (𝑋 + 𝑥) ↔ (((invg𝐺)‘𝑋) + 𝑦) = 𝑥))
1914, 15, 16, 17, 18syl13anc 1484 . . . 4 (((𝐺 ∈ Grp ∧ 𝑋𝐵) ∧ (𝑥𝐵𝑦𝐵)) → ((𝑋 + (((invg𝐺)‘𝑋) + 𝑦)) = (𝑋 + 𝑥) ↔ (((invg𝐺)‘𝑋) + 𝑦) = 𝑥))
20 eqid 2802 . . . . . . . . 9 (0g𝐺) = (0g𝐺)
212, 3, 20, 7grprinv 17668 . . . . . . . 8 ((𝐺 ∈ Grp ∧ 𝑋𝐵) → (𝑋 + ((invg𝐺)‘𝑋)) = (0g𝐺))
2221adantr 468 . . . . . . 7 (((𝐺 ∈ Grp ∧ 𝑋𝐵) ∧ (𝑥𝐵𝑦𝐵)) → (𝑋 + ((invg𝐺)‘𝑋)) = (0g𝐺))
2322oveq1d 6883 . . . . . 6 (((𝐺 ∈ Grp ∧ 𝑋𝐵) ∧ (𝑥𝐵𝑦𝐵)) → ((𝑋 + ((invg𝐺)‘𝑋)) + 𝑦) = ((0g𝐺) + 𝑦))
248adantr 468 . . . . . . 7 (((𝐺 ∈ Grp ∧ 𝑋𝐵) ∧ (𝑥𝐵𝑦𝐵)) → ((invg𝐺)‘𝑋) ∈ 𝐵)
25 simprr 780 . . . . . . 7 (((𝐺 ∈ Grp ∧ 𝑋𝐵) ∧ (𝑥𝐵𝑦𝐵)) → 𝑦𝐵)
262, 3grpass 17630 . . . . . . 7 ((𝐺 ∈ Grp ∧ (𝑋𝐵 ∧ ((invg𝐺)‘𝑋) ∈ 𝐵𝑦𝐵)) → ((𝑋 + ((invg𝐺)‘𝑋)) + 𝑦) = (𝑋 + (((invg𝐺)‘𝑋) + 𝑦)))
2714, 17, 24, 25, 26syl13anc 1484 . . . . . 6 (((𝐺 ∈ Grp ∧ 𝑋𝐵) ∧ (𝑥𝐵𝑦𝐵)) → ((𝑋 + ((invg𝐺)‘𝑋)) + 𝑦) = (𝑋 + (((invg𝐺)‘𝑋) + 𝑦)))
282, 3, 20grplid 17651 . . . . . . 7 ((𝐺 ∈ Grp ∧ 𝑦𝐵) → ((0g𝐺) + 𝑦) = 𝑦)
2928ad2ant2rl 746 . . . . . 6 (((𝐺 ∈ Grp ∧ 𝑋𝐵) ∧ (𝑥𝐵𝑦𝐵)) → ((0g𝐺) + 𝑦) = 𝑦)
3023, 27, 293eqtr3d 2844 . . . . 5 (((𝐺 ∈ Grp ∧ 𝑋𝐵) ∧ (𝑥𝐵𝑦𝐵)) → (𝑋 + (((invg𝐺)‘𝑋) + 𝑦)) = 𝑦)
3130eqeq1d 2804 . . . 4 (((𝐺 ∈ Grp ∧ 𝑋𝐵) ∧ (𝑥𝐵𝑦𝐵)) → ((𝑋 + (((invg𝐺)‘𝑋) + 𝑦)) = (𝑋 + 𝑥) ↔ 𝑦 = (𝑋 + 𝑥)))
3219, 31bitr3d 272 . . 3 (((𝐺 ∈ Grp ∧ 𝑋𝐵) ∧ (𝑥𝐵𝑦𝐵)) → ((((invg𝐺)‘𝑋) + 𝑦) = 𝑥𝑦 = (𝑋 + 𝑥)))
3313, 32syl5bb 274 . 2 (((𝐺 ∈ Grp ∧ 𝑋𝐵) ∧ (𝑥𝐵𝑦𝐵)) → (𝑥 = (((invg𝐺)‘𝑋) + 𝑦) ↔ 𝑦 = (𝑋 + 𝑥)))
341, 5, 12, 33f1o2d 7111 1 ((𝐺 ∈ Grp ∧ 𝑋𝐵) → 𝐹:𝐵1-1-onto𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wa 384   = wceq 1637  wcel 2155  cmpt 4916  1-1-ontowf1o 6094  cfv 6095  (class class class)co 6868  Basecbs 16062  +gcplusg 16147  0gc0g 16299  Grpcgrp 17621  invgcminusg 17622
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2067  ax-7 2103  ax-8 2157  ax-9 2164  ax-10 2184  ax-11 2200  ax-12 2213  ax-13 2419  ax-ext 2781  ax-rep 4957  ax-sep 4968  ax-nul 4977  ax-pow 5029  ax-pr 5090
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2060  df-eu 2633  df-mo 2634  df-clab 2789  df-cleq 2795  df-clel 2798  df-nfc 2933  df-ne 2975  df-ral 3097  df-rex 3098  df-reu 3099  df-rmo 3100  df-rab 3101  df-v 3389  df-sbc 3628  df-csb 3723  df-dif 3766  df-un 3768  df-in 3770  df-ss 3777  df-nul 4111  df-if 4274  df-sn 4365  df-pr 4367  df-op 4371  df-uni 4624  df-iun 4707  df-br 4838  df-opab 4900  df-mpt 4917  df-id 5213  df-xp 5311  df-rel 5312  df-cnv 5313  df-co 5314  df-dm 5315  df-rn 5316  df-res 5317  df-ima 5318  df-iota 6058  df-fun 6097  df-fn 6098  df-f 6099  df-f1 6100  df-fo 6101  df-f1o 6102  df-fv 6103  df-riota 6829  df-ov 6871  df-0g 16301  df-mgm 17441  df-sgrp 17483  df-mnd 17494  df-grp 17624  df-minusg 17625
This theorem is referenced by:  sylow1lem2  18209  sylow2blem1  18230
  Copyright terms: Public domain W3C validator