isnghm - Metamath Proof Explorer

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

Theorem isnghm 22508

Description: A normed group homomorphism is a group homomorphism with bounded norm. (Contributed by Mario Carneiro, 18-Oct-2015.)

**Hypothesis**
Ref	Expression
nmofval.1	⊢ 𝑁 = (𝑆 normOp 𝑇)

**Assertion**
Ref	Expression
isnghm	⊢ (𝐹 ∈ (𝑆 NGHom 𝑇) ↔ ((𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp) ∧ (𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ (𝑁‘𝐹) ∈ ℝ)))

**Proof of Theorem isnghm**
Step	Hyp	Ref	Expression
1		nmofval.1	. . . 4 ⊢ 𝑁 = (𝑆 normOp 𝑇)
2	1	nghmfval 22507	. . 3 ⊢ (𝑆 NGHom 𝑇) = (^◡𝑁 “ ℝ)
3	2	eleq2i 2691	. 2 ⊢ (𝐹 ∈ (𝑆 NGHom 𝑇) ↔ 𝐹 ∈ (^◡𝑁 “ ℝ))
4		n0i 3912	. . . 4 ⊢ (𝐹 ∈ (^◡𝑁 “ ℝ) → ¬ (^◡𝑁 “ ℝ) = ∅)
5		nmoffn 22496	. . . . . . . . . . 11 ⊢ normOp Fn (NrmGrp × NrmGrp)
6		fndm 5978	. . . . . . . . . . 11 ⊢ ( normOp Fn (NrmGrp × NrmGrp) → dom normOp = (NrmGrp × NrmGrp))
7	5, 6	ax-mp 5	. . . . . . . . . 10 ⊢ dom normOp = (NrmGrp × NrmGrp)
8	7	ndmov 6803	. . . . . . . . 9 ⊢ (¬ (𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp) → (𝑆 normOp 𝑇) = ∅)
9	1, 8	syl5eq 2666	. . . . . . . 8 ⊢ (¬ (𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp) → 𝑁 = ∅)
10	9	cnveqd 5287	. . . . . . 7 ⊢ (¬ (𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp) → ^◡𝑁 = ^◡∅)
11		cnv0 5523	. . . . . . 7 ⊢ ^◡∅ = ∅
12	10, 11	syl6eq 2670	. . . . . 6 ⊢ (¬ (𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp) → ^◡𝑁 = ∅)
13	12	imaeq1d 5453	. . . . 5 ⊢ (¬ (𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp) → (^◡𝑁 “ ℝ) = (∅ “ ℝ))
14		0ima 5470	. . . . 5 ⊢ (∅ “ ℝ) = ∅
15	13, 14	syl6eq 2670	. . . 4 ⊢ (¬ (𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp) → (^◡𝑁 “ ℝ) = ∅)
16	4, 15	nsyl2 142	. . 3 ⊢ (𝐹 ∈ (^◡𝑁 “ ℝ) → (𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp))
17	1	nmof 22504	. . . 4 ⊢ ((𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp) → 𝑁:(𝑆 GrpHom 𝑇)⟶ℝ^*)
18		ffn 6032	. . . 4 ⊢ (𝑁:(𝑆 GrpHom 𝑇)⟶ℝ^* → 𝑁 Fn (𝑆 GrpHom 𝑇))
19		elpreima 6323	. . . 4 ⊢ (𝑁 Fn (𝑆 GrpHom 𝑇) → (𝐹 ∈ (^◡𝑁 “ ℝ) ↔ (𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ (𝑁‘𝐹) ∈ ℝ)))
20	17, 18, 19	3syl 18	. . 3 ⊢ ((𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp) → (𝐹 ∈ (^◡𝑁 “ ℝ) ↔ (𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ (𝑁‘𝐹) ∈ ℝ)))
21	16, 20	biadan2 673	. 2 ⊢ (𝐹 ∈ (^◡𝑁 “ ℝ) ↔ ((𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp) ∧ (𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ (𝑁‘𝐹) ∈ ℝ)))
22	3, 21	bitri 264	1 ⊢ (𝐹 ∈ (𝑆 NGHom 𝑇) ↔ ((𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp) ∧ (𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ (𝑁‘𝐹) ∈ ℝ)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 ↔ wb 196 ∧ wa 384 = wceq 1481 ∈ wcel 1988 ∅c0 3907 × cxp 5102 ^◡ccnv 5103 dom cdm 5104 “ cima 5107 Fn wfn 5871 ⟶wf 5872 ‘cfv 5876 (class class class)co 6635 ℝcr 9920 ℝ^*cxr 10058 GrpHom cghm 17638 NrmGrpcngp 22363 normOp cnmo 22490 NGHom cnghm 22491

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1720 ax-4 1735 ax-5 1837 ax-6 1886 ax-7 1933 ax-8 1990 ax-9 1997 ax-10 2017 ax-11 2032 ax-12 2045 ax-13 2244 ax-ext 2600 ax-sep 4772 ax-nul 4780 ax-pow 4834 ax-pr 4897 ax-un 6934 ax-cnex 9977 ax-resscn 9978 ax-1cn 9979 ax-icn 9980 ax-addcl 9981 ax-addrcl 9982 ax-mulcl 9983 ax-mulrcl 9984 ax-mulcom 9985 ax-addass 9986 ax-mulass 9987 ax-distr 9988 ax-i2m1 9989 ax-1ne0 9990 ax-1rid 9991 ax-rnegex 9992 ax-rrecex 9993 ax-cnre 9994 ax-pre-lttri 9995 ax-pre-lttrn 9996 ax-pre-ltadd 9997 ax-pre-mulgt0 9998 ax-pre-sup 9999

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3or 1037 df-3an 1038 df-tru 1484 df-ex 1703 df-nf 1708 df-sb 1879 df-eu 2472 df-mo 2473 df-clab 2607 df-cleq 2613 df-clel 2616 df-nfc 2751 df-ne 2792 df-nel 2895 df-ral 2914 df-rex 2915 df-reu 2916 df-rmo 2917 df-rab 2918 df-v 3197 df-sbc 3430 df-csb 3527 df-dif 3570 df-un 3572 df-in 3574 df-ss 3581 df-nul 3908 df-if 4078 df-pw 4151 df-sn 4169 df-pr 4171 df-op 4175 df-uni 4428 df-iun 4513 df-br 4645 df-opab 4704 df-mpt 4721 df-id 5014 df-po 5025 df-so 5026 df-xp 5110 df-rel 5111 df-cnv 5112 df-co 5113 df-dm 5114 df-rn 5115 df-res 5116 df-ima 5117 df-iota 5839 df-fun 5878 df-fn 5879 df-f 5880 df-f1 5881 df-fo 5882 df-f1o 5883 df-fv 5884 df-riota 6596 df-ov 6638 df-oprab 6639 df-mpt2 6640 df-1st 7153 df-2nd 7154 df-er 7727 df-en 7941 df-dom 7942 df-sdom 7943 df-sup 8333 df-inf 8334 df-pnf 10061 df-mnf 10062 df-xr 10063 df-ltxr 10064 df-le 10065 df-sub 10253 df-neg 10254 df-ico 12166 df-nmo 22493 df-nghm 22494

This theorem is referenced by: isnghm2 22509 nghmcl 22512 nmoi 22513 nghmrcl1 22517 nghmrcl2 22518 nghmghm 22519 isnmhm2 22537

W3C validator