This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 𝑆 ) )