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

Theorem ghmf1 17736
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 17713 . . . . . . 7 (𝐹 ∈ (𝑆 GrpHom 𝑇) → (𝐹0 ) = 𝑈)
43ad2antrr 762 . . . . . 6 (((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝐹:𝑋1-1𝑌) ∧ 𝑥𝑋) → (𝐹0 ) = 𝑈)
54eqeq2d 2661 . . . . 5 (((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝐹:𝑋1-1𝑌) ∧ 𝑥𝑋) → ((𝐹𝑥) = (𝐹0 ) ↔ (𝐹𝑥) = 𝑈))
6 simplr 807 . . . . . 6 (((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝐹:𝑋1-1𝑌) ∧ 𝑥𝑋) → 𝐹:𝑋1-1𝑌)
7 simpr 476 . . . . . 6 (((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝐹:𝑋1-1𝑌) ∧ 𝑥𝑋) → 𝑥𝑋)
8 ghmgrp1 17709 . . . . . . . 8 (𝐹 ∈ (𝑆 GrpHom 𝑇) → 𝑆 ∈ Grp)
98ad2antrr 762 . . . . . . 7 (((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝐹:𝑋1-1𝑌) ∧ 𝑥𝑋) → 𝑆 ∈ Grp)
10 ghmf1.x . . . . . . . 8 𝑋 = (Base‘𝑆)
1110, 1grpidcl 17497 . . . . . . 7 (𝑆 ∈ Grp → 0𝑋)
129, 11syl 17 . . . . . 6 (((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝐹:𝑋1-1𝑌) ∧ 𝑥𝑋) → 0𝑋)
13 f1fveq 6559 . . . . . 6 ((𝐹:𝑋1-1𝑌 ∧ (𝑥𝑋0𝑋)) → ((𝐹𝑥) = (𝐹0 ) ↔ 𝑥 = 0 ))
146, 7, 12, 13syl12anc 1364 . . . . 5 (((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝐹:𝑋1-1𝑌) ∧ 𝑥𝑋) → ((𝐹𝑥) = (𝐹0 ) ↔ 𝑥 = 0 ))
155, 14bitr3d 270 . . . 4 (((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝐹:𝑋1-1𝑌) ∧ 𝑥𝑋) → ((𝐹𝑥) = 𝑈𝑥 = 0 ))
1615biimpd 219 . . 3 (((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝐹:𝑋1-1𝑌) ∧ 𝑥𝑋) → ((𝐹𝑥) = 𝑈𝑥 = 0 ))
1716ralrimiva 2995 . 2 ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝐹:𝑋1-1𝑌) → ∀𝑥𝑋 ((𝐹𝑥) = 𝑈𝑥 = 0 ))
18 ghmf1.y . . . . 5 𝑌 = (Base‘𝑇)
1910, 18ghmf 17711 . . . 4 (𝐹 ∈ (𝑆 GrpHom 𝑇) → 𝐹:𝑋𝑌)
2019adantr 480 . . 3 ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ ∀𝑥𝑋 ((𝐹𝑥) = 𝑈𝑥 = 0 )) → 𝐹:𝑋𝑌)
21 eqid 2651 . . . . . . . . . 10 (-g𝑆) = (-g𝑆)
22 eqid 2651 . . . . . . . . . 10 (-g𝑇) = (-g𝑇)
2310, 21, 22ghmsub 17715 . . . . . . . . 9 ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑦𝑋𝑧𝑋) → (𝐹‘(𝑦(-g𝑆)𝑧)) = ((𝐹𝑦)(-g𝑇)(𝐹𝑧)))
24233expb 1285 . . . . . . . 8 ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ (𝑦𝑋𝑧𝑋)) → (𝐹‘(𝑦(-g𝑆)𝑧)) = ((𝐹𝑦)(-g𝑇)(𝐹𝑧)))
2524adantlr 751 . . . . . . 7 (((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ ∀𝑥𝑋 ((𝐹𝑥) = 𝑈𝑥 = 0 )) ∧ (𝑦𝑋𝑧𝑋)) → (𝐹‘(𝑦(-g𝑆)𝑧)) = ((𝐹𝑦)(-g𝑇)(𝐹𝑧)))
2625eqeq1d 2653 . . . . . 6 (((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ ∀𝑥𝑋 ((𝐹𝑥) = 𝑈𝑥 = 0 )) ∧ (𝑦𝑋𝑧𝑋)) → ((𝐹‘(𝑦(-g𝑆)𝑧)) = 𝑈 ↔ ((𝐹𝑦)(-g𝑇)(𝐹𝑧)) = 𝑈))
278adantr 480 . . . . . . . 8 ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ ∀𝑥𝑋 ((𝐹𝑥) = 𝑈𝑥 = 0 )) → 𝑆 ∈ Grp)
2810, 21grpsubcl 17542 . . . . . . . . 9 ((𝑆 ∈ Grp ∧ 𝑦𝑋𝑧𝑋) → (𝑦(-g𝑆)𝑧) ∈ 𝑋)
29283expb 1285 . . . . . . . 8 ((𝑆 ∈ Grp ∧ (𝑦𝑋𝑧𝑋)) → (𝑦(-g𝑆)𝑧) ∈ 𝑋)
3027, 29sylan 487 . . . . . . 7 (((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ ∀𝑥𝑋 ((𝐹𝑥) = 𝑈𝑥 = 0 )) ∧ (𝑦𝑋𝑧𝑋)) → (𝑦(-g𝑆)𝑧) ∈ 𝑋)
31 simplr 807 . . . . . . 7 (((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ ∀𝑥𝑋 ((𝐹𝑥) = 𝑈𝑥 = 0 )) ∧ (𝑦𝑋𝑧𝑋)) → ∀𝑥𝑋 ((𝐹𝑥) = 𝑈𝑥 = 0 ))
32 fveq2 6229 . . . . . . . . . 10 (𝑥 = (𝑦(-g𝑆)𝑧) → (𝐹𝑥) = (𝐹‘(𝑦(-g𝑆)𝑧)))
3332eqeq1d 2653 . . . . . . . . 9 (𝑥 = (𝑦(-g𝑆)𝑧) → ((𝐹𝑥) = 𝑈 ↔ (𝐹‘(𝑦(-g𝑆)𝑧)) = 𝑈))
34 eqeq1 2655 . . . . . . . . 9 (𝑥 = (𝑦(-g𝑆)𝑧) → (𝑥 = 0 ↔ (𝑦(-g𝑆)𝑧) = 0 ))
3533, 34imbi12d 333 . . . . . . . 8 (𝑥 = (𝑦(-g𝑆)𝑧) → (((𝐹𝑥) = 𝑈𝑥 = 0 ) ↔ ((𝐹‘(𝑦(-g𝑆)𝑧)) = 𝑈 → (𝑦(-g𝑆)𝑧) = 0 )))
3635rspcv 3336 . . . . . . 7 ((𝑦(-g𝑆)𝑧) ∈ 𝑋 → (∀𝑥𝑋 ((𝐹𝑥) = 𝑈𝑥 = 0 ) → ((𝐹‘(𝑦(-g𝑆)𝑧)) = 𝑈 → (𝑦(-g𝑆)𝑧) = 0 )))
3730, 31, 36sylc 65 . . . . . 6 (((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ ∀𝑥𝑋 ((𝐹𝑥) = 𝑈𝑥 = 0 )) ∧ (𝑦𝑋𝑧𝑋)) → ((𝐹‘(𝑦(-g𝑆)𝑧)) = 𝑈 → (𝑦(-g𝑆)𝑧) = 0 ))
3826, 37sylbird 250 . . . . 5 (((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ ∀𝑥𝑋 ((𝐹𝑥) = 𝑈𝑥 = 0 )) ∧ (𝑦𝑋𝑧𝑋)) → (((𝐹𝑦)(-g𝑇)(𝐹𝑧)) = 𝑈 → (𝑦(-g𝑆)𝑧) = 0 ))
39 ghmgrp2 17710 . . . . . . 7 (𝐹 ∈ (𝑆 GrpHom 𝑇) → 𝑇 ∈ Grp)
4039ad2antrr 762 . . . . . 6 (((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ ∀𝑥𝑋 ((𝐹𝑥) = 𝑈𝑥 = 0 )) ∧ (𝑦𝑋𝑧𝑋)) → 𝑇 ∈ Grp)
4119ad2antrr 762 . . . . . . 7 (((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ ∀𝑥𝑋 ((𝐹𝑥) = 𝑈𝑥 = 0 )) ∧ (𝑦𝑋𝑧𝑋)) → 𝐹:𝑋𝑌)
42 simprl 809 . . . . . . 7 (((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ ∀𝑥𝑋 ((𝐹𝑥) = 𝑈𝑥 = 0 )) ∧ (𝑦𝑋𝑧𝑋)) → 𝑦𝑋)
4341, 42ffvelrnd 6400 . . . . . 6 (((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ ∀𝑥𝑋 ((𝐹𝑥) = 𝑈𝑥 = 0 )) ∧ (𝑦𝑋𝑧𝑋)) → (𝐹𝑦) ∈ 𝑌)
44 simprr 811 . . . . . . 7 (((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ ∀𝑥𝑋 ((𝐹𝑥) = 𝑈𝑥 = 0 )) ∧ (𝑦𝑋𝑧𝑋)) → 𝑧𝑋)
4541, 44ffvelrnd 6400 . . . . . 6 (((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ ∀𝑥𝑋 ((𝐹𝑥) = 𝑈𝑥 = 0 )) ∧ (𝑦𝑋𝑧𝑋)) → (𝐹𝑧) ∈ 𝑌)
4618, 2, 22grpsubeq0 17548 . . . . . 6 ((𝑇 ∈ Grp ∧ (𝐹𝑦) ∈ 𝑌 ∧ (𝐹𝑧) ∈ 𝑌) → (((𝐹𝑦)(-g𝑇)(𝐹𝑧)) = 𝑈 ↔ (𝐹𝑦) = (𝐹𝑧)))
4740, 43, 45, 46syl3anc 1366 . . . . 5 (((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ ∀𝑥𝑋 ((𝐹𝑥) = 𝑈𝑥 = 0 )) ∧ (𝑦𝑋𝑧𝑋)) → (((𝐹𝑦)(-g𝑇)(𝐹𝑧)) = 𝑈 ↔ (𝐹𝑦) = (𝐹𝑧)))
488ad2antrr 762 . . . . . 6 (((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ ∀𝑥𝑋 ((𝐹𝑥) = 𝑈𝑥 = 0 )) ∧ (𝑦𝑋𝑧𝑋)) → 𝑆 ∈ Grp)
4910, 1, 21grpsubeq0 17548 . . . . . 6 ((𝑆 ∈ Grp ∧ 𝑦𝑋𝑧𝑋) → ((𝑦(-g𝑆)𝑧) = 0𝑦 = 𝑧))
5048, 42, 44, 49syl3anc 1366 . . . . 5 (((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ ∀𝑥𝑋 ((𝐹𝑥) = 𝑈𝑥 = 0 )) ∧ (𝑦𝑋𝑧𝑋)) → ((𝑦(-g𝑆)𝑧) = 0𝑦 = 𝑧))
5138, 47, 503imtr3d 282 . . . 4 (((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ ∀𝑥𝑋 ((𝐹𝑥) = 𝑈𝑥 = 0 )) ∧ (𝑦𝑋𝑧𝑋)) → ((𝐹𝑦) = (𝐹𝑧) → 𝑦 = 𝑧))
5251ralrimivva 3000 . . 3 ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ ∀𝑥𝑋 ((𝐹𝑥) = 𝑈𝑥 = 0 )) → ∀𝑦𝑋𝑧𝑋 ((𝐹𝑦) = (𝐹𝑧) → 𝑦 = 𝑧))
53 dff13 6552 . . 3 (𝐹:𝑋1-1𝑌 ↔ (𝐹:𝑋𝑌 ∧ ∀𝑦𝑋𝑧𝑋 ((𝐹𝑦) = (𝐹𝑧) → 𝑦 = 𝑧)))
5420, 52, 53sylanbrc 699 . 2 ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ ∀𝑥𝑋 ((𝐹𝑥) = 𝑈𝑥 = 0 )) → 𝐹:𝑋1-1𝑌)
5517, 54impbida 895 1 (𝐹 ∈ (𝑆 GrpHom 𝑇) → (𝐹:𝑋1-1𝑌 ↔ ∀𝑥𝑋 ((𝐹𝑥) = 𝑈𝑥 = 0 )))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383   = wceq 1523  wcel 2030  wral 2941  wf 5922  1-1wf1 5923  cfv 5926  (class class class)co 6690  Basecbs 15904  0gc0g 16147  Grpcgrp 17469  -gcsg 17471   GrpHom cghm 17704
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-rep 4804  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-ral 2946  df-rex 2947  df-reu 2948  df-rmo 2949  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-op 4217  df-uni 4469  df-iun 4554  df-br 4686  df-opab 4746  df-mpt 4763  df-id 5053  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-riota 6651  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-1st 7210  df-2nd 7211  df-0g 16149  df-mgm 17289  df-sgrp 17331  df-mnd 17342  df-grp 17472  df-minusg 17473  df-sbg 17474  df-ghm 17705
This theorem is referenced by:  cayleylem2  17879  f1rhm0to0ALT  18789  fidomndrnglem  19354  islindf5  20226  pwssplit4  37976
  Copyright terms: Public domain W3C validator