isghm3 - Metamath Proof Explorer

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

Theorem isghm3 18908

Description: Property of a group homomorphism, similar to ismhm 18506. (Contributed by Mario Carneiro, 7-Mar-2015.)

**Hypotheses**
Ref	Expression
isghm.w	⊢ 𝑋 = (Base‘𝑆)
isghm.x	⊢ 𝑌 = (Base‘𝑇)
isghm.a	⊢ + = (+_g‘𝑆)
isghm.b	⊢ ⨣ = (+_g‘𝑇)

**Assertion**
Ref	Expression
isghm3	⊢ ((𝑆 ∈ Grp ∧ 𝑇 ∈ Grp) → (𝐹 ∈ (𝑆 GrpHom 𝑇) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑢 ∈ 𝑋 ∀𝑣 ∈ 𝑋 (𝐹‘(𝑢 + 𝑣)) = ((𝐹‘𝑢) ⨣ (𝐹‘𝑣)))))

Distinct variable groups: 𝑣,𝑢,𝑆 𝑢,𝑇,𝑣 𝑢,𝑋,𝑣 𝑢, + ,𝑣 𝑢,𝑌,𝑣 𝑢, ⨣ ,𝑣 𝑢,𝐹,𝑣

**Proof of Theorem isghm3**
Step	Hyp	Ref	Expression
1		isghm.w	. . 3 ⊢ 𝑋 = (Base‘𝑆)
2		isghm.x	. . 3 ⊢ 𝑌 = (Base‘𝑇)
3		isghm.a	. . 3 ⊢ + = (+_g‘𝑆)
4		isghm.b	. . 3 ⊢ ⨣ = (+_g‘𝑇)
5	1, 2, 3, 4	isghm 18907	. 2 ⊢ (𝐹 ∈ (𝑆 GrpHom 𝑇) ↔ ((𝑆 ∈ Grp ∧ 𝑇 ∈ Grp) ∧ (𝐹:𝑋⟶𝑌 ∧ ∀𝑢 ∈ 𝑋 ∀𝑣 ∈ 𝑋 (𝐹‘(𝑢 + 𝑣)) = ((𝐹‘𝑢) ⨣ (𝐹‘𝑣)))))
6	5	baib 536	1 ⊢ ((𝑆 ∈ Grp ∧ 𝑇 ∈ Grp) → (𝐹 ∈ (𝑆 GrpHom 𝑇) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑢 ∈ 𝑋 ∀𝑣 ∈ 𝑋 (𝐹‘(𝑢 + 𝑣)) = ((𝐹‘𝑢) ⨣ (𝐹‘𝑣)))))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 205 ∧ wa 396 = wceq 1540 ∈ wcel 2105 ∀wral 3061 ⟶wf 6461 ‘cfv 6465 (class class class)co 7316 Basecbs 16986 +_gcplusg 17036 Grpcgrp 18650 GrpHom cghm 18904

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1912 ax-6 1970 ax-7 2010 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2153 ax-12 2170 ax-ext 2707 ax-rep 5223 ax-sep 5237 ax-nul 5244 ax-pow 5302 ax-pr 5366 ax-un 7629

This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1781 df-nf 1785 df-sb 2067 df-mo 2538 df-eu 2567 df-clab 2714 df-cleq 2728 df-clel 2814 df-nfc 2886 df-ne 2941 df-ral 3062 df-rex 3071 df-reu 3350 df-rab 3404 df-v 3442 df-sbc 3726 df-csb 3842 df-dif 3899 df-un 3901 df-in 3903 df-ss 3913 df-nul 4267 df-if 4471 df-pw 4546 df-sn 4571 df-pr 4573 df-op 4577 df-uni 4850 df-iun 4938 df-br 5087 df-opab 5149 df-mpt 5170 df-id 5506 df-xp 5613 df-rel 5614 df-cnv 5615 df-co 5616 df-dm 5617 df-rn 5618 df-res 5619 df-ima 5620 df-iota 6417 df-fun 6467 df-fn 6468 df-f 6469 df-f1 6470 df-fo 6471 df-f1o 6472 df-fv 6473 df-ov 7319 df-oprab 7320 df-mpo 7321 df-ghm 18905

This theorem is referenced by: dfrhm2 20033

W3C validator