Users' Mathboxes Mathbox for Jeff Madsen < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  elghomlem1OLD Structured version   Visualization version   GIF version

Theorem elghomlem1OLD 36282
Description: Obsolete as of 15-Mar-2020. Lemma for elghomOLD 36284. (Contributed by Paul Chapman, 25-Feb-2008.) (New usage is discouraged.) (Proof modification is discouraged.)
Hypothesis
Ref Expression
elghomlem1OLD.1 𝑆 = {𝑓 ∣ (𝑓:ran 𝐺⟶ran 𝐻 ∧ ∀𝑥 ∈ ran 𝐺𝑦 ∈ ran 𝐺((𝑓𝑥)𝐻(𝑓𝑦)) = (𝑓‘(𝑥𝐺𝑦)))}
Assertion
Ref Expression
elghomlem1OLD ((𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp) → (𝐺 GrpOpHom 𝐻) = 𝑆)
Distinct variable groups:   𝑥,𝑓,𝑦,𝐺   𝑓,𝐻,𝑥,𝑦
Allowed substitution hints:   𝑆(𝑥,𝑦,𝑓)

Proof of Theorem elghomlem1OLD
Dummy variables 𝑔 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 rnexg 7833 . . 3 (𝐺 ∈ GrpOp → ran 𝐺 ∈ V)
2 rnexg 7833 . . 3 (𝐻 ∈ GrpOp → ran 𝐻 ∈ V)
3 elghomlem1OLD.1 . . . 4 𝑆 = {𝑓 ∣ (𝑓:ran 𝐺⟶ran 𝐻 ∧ ∀𝑥 ∈ ran 𝐺𝑦 ∈ ran 𝐺((𝑓𝑥)𝐻(𝑓𝑦)) = (𝑓‘(𝑥𝐺𝑦)))}
43fabexg 7863 . . 3 ((ran 𝐺 ∈ V ∧ ran 𝐻 ∈ V) → 𝑆 ∈ V)
51, 2, 4syl2an 596 . 2 ((𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp) → 𝑆 ∈ V)
6 rneq 5889 . . . . . 6 (𝑔 = 𝐺 → ran 𝑔 = ran 𝐺)
76feq2d 6651 . . . . 5 (𝑔 = 𝐺 → (𝑓:ran 𝑔⟶ran 𝑓:ran 𝐺⟶ran ))
8 oveq 7357 . . . . . . . . 9 (𝑔 = 𝐺 → (𝑥𝑔𝑦) = (𝑥𝐺𝑦))
98fveq2d 6843 . . . . . . . 8 (𝑔 = 𝐺 → (𝑓‘(𝑥𝑔𝑦)) = (𝑓‘(𝑥𝐺𝑦)))
109eqeq2d 2748 . . . . . . 7 (𝑔 = 𝐺 → (((𝑓𝑥)(𝑓𝑦)) = (𝑓‘(𝑥𝑔𝑦)) ↔ ((𝑓𝑥)(𝑓𝑦)) = (𝑓‘(𝑥𝐺𝑦))))
116, 10raleqbidv 3317 . . . . . 6 (𝑔 = 𝐺 → (∀𝑦 ∈ ran 𝑔((𝑓𝑥)(𝑓𝑦)) = (𝑓‘(𝑥𝑔𝑦)) ↔ ∀𝑦 ∈ ran 𝐺((𝑓𝑥)(𝑓𝑦)) = (𝑓‘(𝑥𝐺𝑦))))
126, 11raleqbidv 3317 . . . . 5 (𝑔 = 𝐺 → (∀𝑥 ∈ ran 𝑔𝑦 ∈ ran 𝑔((𝑓𝑥)(𝑓𝑦)) = (𝑓‘(𝑥𝑔𝑦)) ↔ ∀𝑥 ∈ ran 𝐺𝑦 ∈ ran 𝐺((𝑓𝑥)(𝑓𝑦)) = (𝑓‘(𝑥𝐺𝑦))))
137, 12anbi12d 631 . . . 4 (𝑔 = 𝐺 → ((𝑓:ran 𝑔⟶ran ∧ ∀𝑥 ∈ ran 𝑔𝑦 ∈ ran 𝑔((𝑓𝑥)(𝑓𝑦)) = (𝑓‘(𝑥𝑔𝑦))) ↔ (𝑓:ran 𝐺⟶ran ∧ ∀𝑥 ∈ ran 𝐺𝑦 ∈ ran 𝐺((𝑓𝑥)(𝑓𝑦)) = (𝑓‘(𝑥𝐺𝑦)))))
1413abbidv 2806 . . 3 (𝑔 = 𝐺 → {𝑓 ∣ (𝑓:ran 𝑔⟶ran ∧ ∀𝑥 ∈ ran 𝑔𝑦 ∈ ran 𝑔((𝑓𝑥)(𝑓𝑦)) = (𝑓‘(𝑥𝑔𝑦)))} = {𝑓 ∣ (𝑓:ran 𝐺⟶ran ∧ ∀𝑥 ∈ ran 𝐺𝑦 ∈ ran 𝐺((𝑓𝑥)(𝑓𝑦)) = (𝑓‘(𝑥𝐺𝑦)))})
15 rneq 5889 . . . . . . 7 ( = 𝐻 → ran = ran 𝐻)
1615feq3d 6652 . . . . . 6 ( = 𝐻 → (𝑓:ran 𝐺⟶ran 𝑓:ran 𝐺⟶ran 𝐻))
17 oveq 7357 . . . . . . . 8 ( = 𝐻 → ((𝑓𝑥)(𝑓𝑦)) = ((𝑓𝑥)𝐻(𝑓𝑦)))
1817eqeq1d 2739 . . . . . . 7 ( = 𝐻 → (((𝑓𝑥)(𝑓𝑦)) = (𝑓‘(𝑥𝐺𝑦)) ↔ ((𝑓𝑥)𝐻(𝑓𝑦)) = (𝑓‘(𝑥𝐺𝑦))))
19182ralbidv 3210 . . . . . 6 ( = 𝐻 → (∀𝑥 ∈ ran 𝐺𝑦 ∈ ran 𝐺((𝑓𝑥)(𝑓𝑦)) = (𝑓‘(𝑥𝐺𝑦)) ↔ ∀𝑥 ∈ ran 𝐺𝑦 ∈ ran 𝐺((𝑓𝑥)𝐻(𝑓𝑦)) = (𝑓‘(𝑥𝐺𝑦))))
2016, 19anbi12d 631 . . . . 5 ( = 𝐻 → ((𝑓:ran 𝐺⟶ran ∧ ∀𝑥 ∈ ran 𝐺𝑦 ∈ ran 𝐺((𝑓𝑥)(𝑓𝑦)) = (𝑓‘(𝑥𝐺𝑦))) ↔ (𝑓:ran 𝐺⟶ran 𝐻 ∧ ∀𝑥 ∈ ran 𝐺𝑦 ∈ ran 𝐺((𝑓𝑥)𝐻(𝑓𝑦)) = (𝑓‘(𝑥𝐺𝑦)))))
2120abbidv 2806 . . . 4 ( = 𝐻 → {𝑓 ∣ (𝑓:ran 𝐺⟶ran ∧ ∀𝑥 ∈ ran 𝐺𝑦 ∈ ran 𝐺((𝑓𝑥)(𝑓𝑦)) = (𝑓‘(𝑥𝐺𝑦)))} = {𝑓 ∣ (𝑓:ran 𝐺⟶ran 𝐻 ∧ ∀𝑥 ∈ ran 𝐺𝑦 ∈ ran 𝐺((𝑓𝑥)𝐻(𝑓𝑦)) = (𝑓‘(𝑥𝐺𝑦)))})
2221, 3eqtr4di 2795 . . 3 ( = 𝐻 → {𝑓 ∣ (𝑓:ran 𝐺⟶ran ∧ ∀𝑥 ∈ ran 𝐺𝑦 ∈ ran 𝐺((𝑓𝑥)(𝑓𝑦)) = (𝑓‘(𝑥𝐺𝑦)))} = 𝑆)
23 df-ghomOLD 36281 . . 3 GrpOpHom = (𝑔 ∈ GrpOp, ∈ GrpOp ↦ {𝑓 ∣ (𝑓:ran 𝑔⟶ran ∧ ∀𝑥 ∈ ran 𝑔𝑦 ∈ ran 𝑔((𝑓𝑥)(𝑓𝑦)) = (𝑓‘(𝑥𝑔𝑦)))})
2414, 22, 23ovmpog 7508 . 2 ((𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝑆 ∈ V) → (𝐺 GrpOpHom 𝐻) = 𝑆)
255, 24mpd3an3 1462 1 ((𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp) → (𝐺 GrpOpHom 𝐻) = 𝑆)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396   = wceq 1541  wcel 2106  {cab 2714  wral 3062  Vcvv 3443  ran crn 5632  wf 6489  cfv 6493  (class class class)co 7351  GrpOpcgr 29260   GrpOpHom cghomOLD 36280
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2708  ax-sep 5254  ax-nul 5261  ax-pow 5318  ax-pr 5382  ax-un 7664
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2887  df-ral 3063  df-rex 3072  df-rab 3406  df-v 3445  df-sbc 3738  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4281  df-if 4485  df-pw 4560  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4864  df-br 5104  df-opab 5166  df-id 5529  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-iota 6445  df-fun 6495  df-fn 6496  df-f 6497  df-fv 6501  df-ov 7354  df-oprab 7355  df-mpo 7356  df-ghomOLD 36281
This theorem is referenced by:  elghomlem2OLD  36283
  Copyright terms: Public domain W3C validator