Theorem idnghm

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

	Ref	Expression
Hypothesis	idnghm.2	⊢ 𝑉 = ( Base ‘ 𝑆 )
Assertion	idnghm	⊢ ( 𝑆 ∈ NrmGrp → ( I ↾ 𝑉 ) ∈ ( 𝑆 NGHom 𝑆 ) )

Proof

Step	Hyp	Ref	Expression
1		idnghm.2	⊢ 𝑉 = ( Base ‘ 𝑆 )
2		eqid	⊢ ( 𝑆 normOp 𝑆 ) = ( 𝑆 normOp 𝑆 )
3		eqid	⊢ ( 0g ‘ 𝑆 ) = ( 0g ‘ 𝑆 )
4	2 1 3	nmoid	⊢ ( ( 𝑆 ∈ NrmGrp ∧ { ( 0g ‘ 𝑆 ) } ⊊ 𝑉 ) → ( ( 𝑆 normOp 𝑆 ) ‘ ( I ↾ 𝑉 ) ) = 1 )
5		1re	⊢ 1 ∈ ℝ
6	4 5	eqeltrdi	⊢ ( ( 𝑆 ∈ NrmGrp ∧ { ( 0g ‘ 𝑆 ) } ⊊ 𝑉 ) → ( ( 𝑆 normOp 𝑆 ) ‘ ( I ↾ 𝑉 ) ) ∈ ℝ )
7		eleq2	⊢ ( { ( 0g ‘ 𝑆 ) } = 𝑉 → ( 𝑥 ∈ { ( 0g ‘ 𝑆 ) } ↔ 𝑥 ∈ 𝑉 ) )
8	7	biimpar	⊢ ( ( { ( 0g ‘ 𝑆 ) } = 𝑉 ∧ 𝑥 ∈ 𝑉 ) → 𝑥 ∈ { ( 0g ‘ 𝑆 ) } )
9		elsni	⊢ ( 𝑥 ∈ { ( 0g ‘ 𝑆 ) } → 𝑥 = ( 0g ‘ 𝑆 ) )
10	8 9	syl	⊢ ( ( { ( 0g ‘ 𝑆 ) } = 𝑉 ∧ 𝑥 ∈ 𝑉 ) → 𝑥 = ( 0g ‘ 𝑆 ) )
11	10	mpteq2dva	⊢ ( { ( 0g ‘ 𝑆 ) } = 𝑉 → ( 𝑥 ∈ 𝑉 ↦ 𝑥 ) = ( 𝑥 ∈ 𝑉 ↦ ( 0g ‘ 𝑆 ) ) )
12		mptresid	⊢ ( I ↾ 𝑉 ) = ( 𝑥 ∈ 𝑉 ↦ 𝑥 )
13		fconstmpt	⊢ ( 𝑉 × { ( 0g ‘ 𝑆 ) } ) = ( 𝑥 ∈ 𝑉 ↦ ( 0g ‘ 𝑆 ) )
14	11 12 13	3eqtr4g	⊢ ( { ( 0g ‘ 𝑆 ) } = 𝑉 → ( I ↾ 𝑉 ) = ( 𝑉 × { ( 0g ‘ 𝑆 ) } ) )
15	14	fveq2d	⊢ ( { ( 0g ‘ 𝑆 ) } = 𝑉 → ( ( 𝑆 normOp 𝑆 ) ‘ ( I ↾ 𝑉 ) ) = ( ( 𝑆 normOp 𝑆 ) ‘ ( 𝑉 × { ( 0g ‘ 𝑆 ) } ) ) )
16	2 1 3	nmo0	⊢ ( ( 𝑆 ∈ NrmGrp ∧ 𝑆 ∈ NrmGrp ) → ( ( 𝑆 normOp 𝑆 ) ‘ ( 𝑉 × { ( 0g ‘ 𝑆 ) } ) ) = 0 )
17	16	anidms	⊢ ( 𝑆 ∈ NrmGrp → ( ( 𝑆 normOp 𝑆 ) ‘ ( 𝑉 × { ( 0g ‘ 𝑆 ) } ) ) = 0 )
18	15 17	sylan9eqr	⊢ ( ( 𝑆 ∈ NrmGrp ∧ { ( 0g ‘ 𝑆 ) } = 𝑉 ) → ( ( 𝑆 normOp 𝑆 ) ‘ ( I ↾ 𝑉 ) ) = 0 )
19		0re	⊢ 0 ∈ ℝ
20	18 19	eqeltrdi	⊢ ( ( 𝑆 ∈ NrmGrp ∧ { ( 0g ‘ 𝑆 ) } = 𝑉 ) → ( ( 𝑆 normOp 𝑆 ) ‘ ( I ↾ 𝑉 ) ) ∈ ℝ )
21		ngpgrp	⊢ ( 𝑆 ∈ NrmGrp → 𝑆 ∈ Grp )
22	1 3	grpidcl	⊢ ( 𝑆 ∈ Grp → ( 0g ‘ 𝑆 ) ∈ 𝑉 )
23	21 22	syl	⊢ ( 𝑆 ∈ NrmGrp → ( 0g ‘ 𝑆 ) ∈ 𝑉 )
24	23	snssd	⊢ ( 𝑆 ∈ NrmGrp → { ( 0g ‘ 𝑆 ) } ⊆ 𝑉 )
25		sspss	⊢ ( { ( 0g ‘ 𝑆 ) } ⊆ 𝑉 ↔ ( { ( 0g ‘ 𝑆 ) } ⊊ 𝑉 ∨ { ( 0g ‘ 𝑆 ) } = 𝑉 ) )
26	24 25	sylib	⊢ ( 𝑆 ∈ NrmGrp → ( { ( 0g ‘ 𝑆 ) } ⊊ 𝑉 ∨ { ( 0g ‘ 𝑆 ) } = 𝑉 ) )
27	6 20 26	mpjaodan	⊢ ( 𝑆 ∈ NrmGrp → ( ( 𝑆 normOp 𝑆 ) ‘ ( I ↾ 𝑉 ) ) ∈ ℝ )
28		id	⊢ ( 𝑆 ∈ NrmGrp → 𝑆 ∈ NrmGrp )
29	1	idghm	⊢ ( 𝑆 ∈ Grp → ( I ↾ 𝑉 ) ∈ ( 𝑆 GrpHom 𝑆 ) )
30	21 29	syl	⊢ ( 𝑆 ∈ NrmGrp → ( I ↾ 𝑉 ) ∈ ( 𝑆 GrpHom 𝑆 ) )
31	2	isnghm2	⊢ ( ( 𝑆 ∈ NrmGrp ∧ 𝑆 ∈ NrmGrp ∧ ( I ↾ 𝑉 ) ∈ ( 𝑆 GrpHom 𝑆 ) ) → ( ( I ↾ 𝑉 ) ∈ ( 𝑆 NGHom 𝑆 ) ↔ ( ( 𝑆 normOp 𝑆 ) ‘ ( I ↾ 𝑉 ) ) ∈ ℝ ) )
32	28 30 31	mpd3an23	⊢ ( 𝑆 ∈ NrmGrp → ( ( I ↾ 𝑉 ) ∈ ( 𝑆 NGHom 𝑆 ) ↔ ( ( 𝑆 normOp 𝑆 ) ‘ ( I ↾ 𝑉 ) ) ∈ ℝ ) )
33	27 32	mpbird	⊢ ( 𝑆 ∈ NrmGrp → ( I ↾ 𝑉 ) ∈ ( 𝑆 NGHom 𝑆 ) )