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

Theorem ghmf1 17512
Description: Two ways of saying a group homomorphism is 1-1 into its codomain. (Contributed by Paul Chapman, 3-Mar-2008.) (Revised by Mario Carneiro, 13-Jan-2015.)
Hypotheses
Ref Expression
ghmf1.x 𝑋 = (Base‘𝑆)
ghmf1.y 𝑌 = (Base‘𝑇)
ghmf1.z 0 = (0g𝑆)
ghmf1.u 𝑈 = (0g𝑇)
Assertion
Ref Expression
ghmf1 (𝐹 ∈ (𝑆 GrpHom 𝑇) → (𝐹:𝑋1-1𝑌 ↔ ∀𝑥𝑋 ((𝐹𝑥) = 𝑈𝑥 = 0 )))
Distinct variable groups:   𝑥,𝐹   𝑥,𝑆   𝑥,𝑇   𝑥,𝑈   𝑥,𝑋   𝑥,𝑌   𝑥, 0

Proof of Theorem ghmf1
Dummy variables 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ghmf1.z . . . . . . . 8 0 = (0g𝑆)
2 ghmf1.u . . . . . . . 8 𝑈 = (0g𝑇)
31, 2ghmid 17489 . . . . . . 7 (𝐹 ∈ (𝑆 GrpHom 𝑇) → (𝐹0 ) = 𝑈)
43ad2antrr 758 . . . . . 6 (((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝐹:𝑋1-1𝑌) ∧ 𝑥𝑋) → (𝐹0 ) = 𝑈)
54eqeq2d 2620 . . . . 5 (((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝐹:𝑋1-1𝑌) ∧ 𝑥𝑋) → ((𝐹𝑥) = (𝐹0 ) ↔ (𝐹𝑥) = 𝑈))
6 simplr 788 . . . . . 6 (((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝐹:𝑋1-1𝑌) ∧ 𝑥𝑋) → 𝐹:𝑋1-1𝑌)
7 simpr 476 . . . . . 6 (((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝐹:𝑋1-1𝑌) ∧ 𝑥𝑋) → 𝑥𝑋)
8 ghmgrp1 17485 . . . . . . . 8 (𝐹 ∈ (𝑆 GrpHom 𝑇) → 𝑆 ∈ Grp)
98ad2antrr 758 . . . . . . 7 (((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝐹:𝑋1-1𝑌) ∧ 𝑥𝑋) → 𝑆 ∈ Grp)
10 ghmf1.x . . . . . . . 8 𝑋 = (Base‘𝑆)
1110, 1grpidcl 17273 . . . . . . 7 (𝑆 ∈ Grp → 0𝑋)
129, 11syl 17 . . . . . 6 (((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝐹:𝑋1-1𝑌) ∧ 𝑥𝑋) → 0𝑋)
13 f1fveq 6420 . . . . . 6 ((𝐹:𝑋1-1𝑌 ∧ (𝑥𝑋0𝑋)) → ((𝐹𝑥) = (𝐹0 ) ↔ 𝑥 = 0 ))
146, 7, 12, 13syl12anc 1316 . . . . 5 (((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝐹:𝑋1-1𝑌) ∧ 𝑥𝑋) → ((𝐹𝑥) = (𝐹0 ) ↔ 𝑥 = 0 ))
155, 14bitr3d 269 . . . 4 (((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝐹:𝑋1-1𝑌) ∧ 𝑥𝑋) → ((𝐹𝑥) = 𝑈𝑥 = 0 ))
1615biimpd 218 . . 3 (((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝐹:𝑋1-1𝑌) ∧ 𝑥𝑋) → ((𝐹𝑥) = 𝑈𝑥 = 0 ))
1716ralrimiva 2949 . 2 ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝐹:𝑋1-1𝑌) → ∀𝑥𝑋 ((𝐹𝑥) = 𝑈𝑥 = 0 ))
18 ghmf1.y . . . . 5 𝑌 = (Base‘𝑇)
1910, 18ghmf 17487 . . . 4 (𝐹 ∈ (𝑆 GrpHom 𝑇) → 𝐹:𝑋𝑌)
2019adantr 480 . . 3 ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ ∀𝑥𝑋 ((𝐹𝑥) = 𝑈𝑥 = 0 )) → 𝐹:𝑋𝑌)
21 eqid 2610 . . . . . . . . . 10 (-g𝑆) = (-g𝑆)
22 eqid 2610 . . . . . . . . . 10 (-g𝑇) = (-g𝑇)
2310, 21, 22ghmsub 17491 . . . . . . . . 9 ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑦𝑋𝑧𝑋) → (𝐹‘(𝑦(-g𝑆)𝑧)) = ((𝐹𝑦)(-g𝑇)(𝐹𝑧)))
24233expb 1258 . . . . . . . 8 ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ (𝑦𝑋𝑧𝑋)) → (𝐹‘(𝑦(-g𝑆)𝑧)) = ((𝐹𝑦)(-g𝑇)(𝐹𝑧)))
2524adantlr 747 . . . . . . 7 (((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ ∀𝑥𝑋 ((𝐹𝑥) = 𝑈𝑥 = 0 )) ∧ (𝑦𝑋𝑧𝑋)) → (𝐹‘(𝑦(-g𝑆)𝑧)) = ((𝐹𝑦)(-g𝑇)(𝐹𝑧)))
2625eqeq1d 2612 . . . . . 6 (((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ ∀𝑥𝑋 ((𝐹𝑥) = 𝑈𝑥 = 0 )) ∧ (𝑦𝑋𝑧𝑋)) → ((𝐹‘(𝑦(-g𝑆)𝑧)) = 𝑈 ↔ ((𝐹𝑦)(-g𝑇)(𝐹𝑧)) = 𝑈))
278adantr 480 . . . . . . . 8 ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ ∀𝑥𝑋 ((𝐹𝑥) = 𝑈𝑥 = 0 )) → 𝑆 ∈ Grp)
2810, 21grpsubcl 17318 . . . . . . . . 9 ((𝑆 ∈ Grp ∧ 𝑦𝑋𝑧𝑋) → (𝑦(-g𝑆)𝑧) ∈ 𝑋)
29283expb 1258 . . . . . . . 8 ((𝑆 ∈ Grp ∧ (𝑦𝑋𝑧𝑋)) → (𝑦(-g𝑆)𝑧) ∈ 𝑋)
3027, 29sylan 487 . . . . . . 7 (((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ ∀𝑥𝑋 ((𝐹𝑥) = 𝑈𝑥 = 0 )) ∧ (𝑦𝑋𝑧𝑋)) → (𝑦(-g𝑆)𝑧) ∈ 𝑋)
31 simplr 788 . . . . . . 7 (((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ ∀𝑥𝑋 ((𝐹𝑥) = 𝑈𝑥 = 0 )) ∧ (𝑦𝑋𝑧𝑋)) → ∀𝑥𝑋 ((𝐹𝑥) = 𝑈𝑥 = 0 ))
32 fveq2 6103 . . . . . . . . . 10 (𝑥 = (𝑦(-g𝑆)𝑧) → (𝐹𝑥) = (𝐹‘(𝑦(-g𝑆)𝑧)))
3332eqeq1d 2612 . . . . . . . . 9 (𝑥 = (𝑦(-g𝑆)𝑧) → ((𝐹𝑥) = 𝑈 ↔ (𝐹‘(𝑦(-g𝑆)𝑧)) = 𝑈))
34 eqeq1 2614 . . . . . . . . 9 (𝑥 = (𝑦(-g𝑆)𝑧) → (𝑥 = 0 ↔ (𝑦(-g𝑆)𝑧) = 0 ))
3533, 34imbi12d 333 . . . . . . . 8 (𝑥 = (𝑦(-g𝑆)𝑧) → (((𝐹𝑥) = 𝑈𝑥 = 0 ) ↔ ((𝐹‘(𝑦(-g𝑆)𝑧)) = 𝑈 → (𝑦(-g𝑆)𝑧) = 0 )))
3635rspcv 3278 . . . . . . 7 ((𝑦(-g𝑆)𝑧) ∈ 𝑋 → (∀𝑥𝑋 ((𝐹𝑥) = 𝑈𝑥 = 0 ) → ((𝐹‘(𝑦(-g𝑆)𝑧)) = 𝑈 → (𝑦(-g𝑆)𝑧) = 0 )))
3730, 31, 36sylc 63 . . . . . 6 (((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ ∀𝑥𝑋 ((𝐹𝑥) = 𝑈𝑥 = 0 )) ∧ (𝑦𝑋𝑧𝑋)) → ((𝐹‘(𝑦(-g𝑆)𝑧)) = 𝑈 → (𝑦(-g𝑆)𝑧) = 0 ))
3826, 37sylbird 249 . . . . 5 (((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ ∀𝑥𝑋 ((𝐹𝑥) = 𝑈𝑥 = 0 )) ∧ (𝑦𝑋𝑧𝑋)) → (((𝐹𝑦)(-g𝑇)(𝐹𝑧)) = 𝑈 → (𝑦(-g𝑆)𝑧) = 0 ))
39 ghmgrp2 17486 . . . . . . 7 (𝐹 ∈ (𝑆 GrpHom 𝑇) → 𝑇 ∈ Grp)
4039ad2antrr 758 . . . . . 6 (((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ ∀𝑥𝑋 ((𝐹𝑥) = 𝑈𝑥 = 0 )) ∧ (𝑦𝑋𝑧𝑋)) → 𝑇 ∈ Grp)
4119ad2antrr 758 . . . . . . 7 (((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ ∀𝑥𝑋 ((𝐹𝑥) = 𝑈𝑥 = 0 )) ∧ (𝑦𝑋𝑧𝑋)) → 𝐹:𝑋𝑌)
42 simprl 790 . . . . . . 7 (((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ ∀𝑥𝑋 ((𝐹𝑥) = 𝑈𝑥 = 0 )) ∧ (𝑦𝑋𝑧𝑋)) → 𝑦𝑋)
4341, 42ffvelrnd 6268 . . . . . 6 (((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ ∀𝑥𝑋 ((𝐹𝑥) = 𝑈𝑥 = 0 )) ∧ (𝑦𝑋𝑧𝑋)) → (𝐹𝑦) ∈ 𝑌)
44 simprr 792 . . . . . . 7 (((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ ∀𝑥𝑋 ((𝐹𝑥) = 𝑈𝑥 = 0 )) ∧ (𝑦𝑋𝑧𝑋)) → 𝑧𝑋)
4541, 44ffvelrnd 6268 . . . . . 6 (((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ ∀𝑥𝑋 ((𝐹𝑥) = 𝑈𝑥 = 0 )) ∧ (𝑦𝑋𝑧𝑋)) → (𝐹𝑧) ∈ 𝑌)
4618, 2, 22grpsubeq0 17324 . . . . . 6 ((𝑇 ∈ Grp ∧ (𝐹𝑦) ∈ 𝑌 ∧ (𝐹𝑧) ∈ 𝑌) → (((𝐹𝑦)(-g𝑇)(𝐹𝑧)) = 𝑈 ↔ (𝐹𝑦) = (𝐹𝑧)))
4740, 43, 45, 46syl3anc 1318 . . . . 5 (((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ ∀𝑥𝑋 ((𝐹𝑥) = 𝑈𝑥 = 0 )) ∧ (𝑦𝑋𝑧𝑋)) → (((𝐹𝑦)(-g𝑇)(𝐹𝑧)) = 𝑈 ↔ (𝐹𝑦) = (𝐹𝑧)))
488ad2antrr 758 . . . . . 6 (((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ ∀𝑥𝑋 ((𝐹𝑥) = 𝑈𝑥 = 0 )) ∧ (𝑦𝑋𝑧𝑋)) → 𝑆 ∈ Grp)
4910, 1, 21grpsubeq0 17324 . . . . . 6 ((𝑆 ∈ Grp ∧ 𝑦𝑋𝑧𝑋) → ((𝑦(-g𝑆)𝑧) = 0𝑦 = 𝑧))
5048, 42, 44, 49syl3anc 1318 . . . . 5 (((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ ∀𝑥𝑋 ((𝐹𝑥) = 𝑈𝑥 = 0 )) ∧ (𝑦𝑋𝑧𝑋)) → ((𝑦(-g𝑆)𝑧) = 0𝑦 = 𝑧))
5138, 47, 503imtr3d 281 . . . 4 (((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ ∀𝑥𝑋 ((𝐹𝑥) = 𝑈𝑥 = 0 )) ∧ (𝑦𝑋𝑧𝑋)) → ((𝐹𝑦) = (𝐹𝑧) → 𝑦 = 𝑧))
5251ralrimivva 2954 . . 3 ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ ∀𝑥𝑋 ((𝐹𝑥) = 𝑈𝑥 = 0 )) → ∀𝑦𝑋𝑧𝑋 ((𝐹𝑦) = (𝐹𝑧) → 𝑦 = 𝑧))
53 dff13 6416 . . 3 (𝐹:𝑋1-1𝑌 ↔ (𝐹:𝑋𝑌 ∧ ∀𝑦𝑋𝑧𝑋 ((𝐹𝑦) = (𝐹𝑧) → 𝑦 = 𝑧)))
5420, 52, 53sylanbrc 695 . 2 ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ ∀𝑥𝑋 ((𝐹𝑥) = 𝑈𝑥 = 0 )) → 𝐹:𝑋1-1𝑌)
5517, 54impbida 873 1 (𝐹 ∈ (𝑆 GrpHom 𝑇) → (𝐹:𝑋1-1𝑌 ↔ ∀𝑥𝑋 ((𝐹𝑥) = 𝑈𝑥 = 0 )))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 195  wa 383   = wceq 1475  wcel 1977  wral 2896  wf 5800  1-1wf1 5801  cfv 5804  (class class class)co 6549  Basecbs 15695  0gc0g 15923  Grpcgrp 17245  -gcsg 17247   GrpHom cghm 17480
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-reu 2903  df-rmo 2904  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-id 4953  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-1st 7059  df-2nd 7060  df-0g 15925  df-mgm 17065  df-sgrp 17107  df-mnd 17118  df-grp 17248  df-minusg 17249  df-sbg 17250  df-ghm 17481
This theorem is referenced by:  cayleylem2  17656  f1rhm0to0ALT  18564  fidomndrnglem  19127  islindf5  19997  pwssplit4  36677
  Copyright terms: Public domain W3C validator