idnghm

Description: The identity operator is a normed group homomorphism. (Contributed by Mario Carneiro, 18-Oct-2015)

		Ref	Expression
	Hypothesis	idnghm.2	$⊢ V = {Base}_{S}$
	Assertion	idnghm	$⊢ S \in NrmGrp \to {I ↾}_{V} \in (S NGHom S)$

Proof

Step	Hyp	Ref	Expression
1		idnghm.2	$⊢ V = {Base}_{S}$
2		eqid	$⊢ S normOp S = S normOp S$
3		eqid	$⊢ 0_{S} = 0_{S}$
4	2 1 3	nmoid	$⊢ (S \in NrmGrp \land \{0_{S}\} \subset V) \to (S normOp S) ({I ↾}_{V}) = 1$
5		1re	$⊢ 1 \in ℝ$
6	4 5	eqeltrdi	$⊢ (S \in NrmGrp \land \{0_{S}\} \subset V) \to (S normOp S) ({I ↾}_{V}) \in ℝ$
7		eleq2	$⊢ \{0_{S}\} = V \to (x \in \{0_{S}\} \leftrightarrow x \in V)$
8	7	biimpar	$⊢ (\{0_{S}\} = V \land x \in V) \to x \in \{0_{S}\}$
9		elsni	$⊢ x \in \{0_{S}\} \to x = 0_{S}$
10	8 9	syl	$⊢ (\{0_{S}\} = V \land x \in V) \to x = 0_{S}$
11	10	mpteq2dva	$⊢ \{0_{S}\} = V \to (x \in V ⟼ x) = (x \in V ⟼ 0_{S})$
12		mptresid	$⊢ {I ↾}_{V} = (x \in V ⟼ x)$
13		fconstmpt	$⊢ V \times \{0_{S}\} = (x \in V ⟼ 0_{S})$
14	11 12 13	3eqtr4g	$⊢ \{0_{S}\} = V \to {I ↾}_{V} = V \times \{0_{S}\}$
15	14	fveq2d	$⊢ \{0_{S}\} = V \to (S normOp S) ({I ↾}_{V}) = (S normOp S) (V \times \{0_{S}\})$
16	2 1 3	nmo0	$⊢ (S \in NrmGrp \land S \in NrmGrp) \to (S normOp S) (V \times \{0_{S}\}) = 0$
17	16	anidms	$⊢ S \in NrmGrp \to (S normOp S) (V \times \{0_{S}\}) = 0$
18	15 17	sylan9eqr	$⊢ (S \in NrmGrp \land \{0_{S}\} = V) \to (S normOp S) ({I ↾}_{V}) = 0$
19		0re	$⊢ 0 \in ℝ$
20	18 19	eqeltrdi	$⊢ (S \in NrmGrp \land \{0_{S}\} = V) \to (S normOp S) ({I ↾}_{V}) \in ℝ$
21		ngpgrp	$⊢ S \in NrmGrp \to S \in Grp$
22	1 3	grpidcl	$⊢ S \in Grp \to 0_{S} \in V$
23	21 22	syl	$⊢ S \in NrmGrp \to 0_{S} \in V$
24	23	snssd	$⊢ S \in NrmGrp \to \{0_{S}\} \subseteq V$
25		sspss	$⊢ \{0_{S}\} \subseteq V \leftrightarrow (\{0_{S}\} \subset V \lor \{0_{S}\} = V)$
26	24 25	sylib	$⊢ S \in NrmGrp \to (\{0_{S}\} \subset V \lor \{0_{S}\} = V)$
27	6 20 26	mpjaodan	$⊢ S \in NrmGrp \to (S normOp S) ({I ↾}_{V}) \in ℝ$
28		id	$⊢ S \in NrmGrp \to S \in NrmGrp$
29	1	idghm	$⊢ S \in Grp \to {I ↾}_{V} \in (S GrpHom S)$
30	21 29	syl	$⊢ S \in NrmGrp \to {I ↾}_{V} \in (S GrpHom S)$
31	2	isnghm2	$⊢ (S \in NrmGrp \land S \in NrmGrp \land {I ↾}_{V} \in (S GrpHom S)) \to ({I ↾}_{V} \in (S NGHom S) \leftrightarrow (S normOp S) ({I ↾}_{V}) \in ℝ)$
32	28 30 31	mpd3an23	$⊢ S \in NrmGrp \to ({I ↾}_{V} \in (S NGHom S) \leftrightarrow (S normOp S) ({I ↾}_{V}) \in ℝ)$
33	27 32	mpbird	$⊢ S \in NrmGrp \to {I ↾}_{V} \in (S NGHom S)$

Metamath Proof Explorer

Theorem idnghm

Proof