Metamath Proof Explorer

Theorem nmods

Description: Upper bound for the distance between the values of a bounded linear operator. (Contributed by Mario Carneiro, 22-Oct-2015)

Ref Expression
Hypotheses nmods.n ⊢ 𝑁 = ( 𝑆 normOp 𝑇 )
nmods.v ⊢ 𝑉 = ( Base ‘ 𝑆 )
nmods.c ⊢ 𝐶 = ( dist ‘ 𝑆 )
nmods.d ⊢ 𝐷 = ( dist ‘ 𝑇 )
Assertion nmods ( ( 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( ( 𝐹 ‘ 𝐴 ) 𝐷 ( 𝐹 ‘ 𝐵 ) ) ≤ ( ( 𝑁 ‘ 𝐹 ) · ( 𝐴 𝐶 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 nmods.n ⊢ 𝑁 = ( 𝑆 normOp 𝑇 )
2 nmods.v ⊢ 𝑉 = ( Base ‘ 𝑆 )
3 nmods.c ⊢ 𝐶 = ( dist ‘ 𝑆 )
4 nmods.d ⊢ 𝐷 = ( dist ‘ 𝑇 )
5 simp1 ⊢ ( ( 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) )
6 nghmrcl1 ⊢ ( 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) → 𝑆 ∈ NrmGrp )
7 ngpgrp ⊢ ( 𝑆 ∈ NrmGrp → 𝑆 ∈ Grp )
8 6 7 syl ⊢ ( 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) → 𝑆 ∈ Grp )
9 eqid ⊢ ( -g ‘ 𝑆 ) = ( -g ‘ 𝑆 )
10 2 9 grpsubcl ⊢ ( ( 𝑆 ∈ Grp ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( 𝐴 ( -g ‘ 𝑆 ) 𝐵 ) ∈ 𝑉 )
11 8 10 syl3an1 ⊢ ( ( 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( 𝐴 ( -g ‘ 𝑆 ) 𝐵 ) ∈ 𝑉 )
12 eqid ⊢ ( norm ‘ 𝑆 ) = ( norm ‘ 𝑆 )
13 eqid ⊢ ( norm ‘ 𝑇 ) = ( norm ‘ 𝑇 )
14 1 2 12 13 nmoi ⊢ ( ( 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ∧ ( 𝐴 ( -g ‘ 𝑆 ) 𝐵 ) ∈ 𝑉 ) → ( ( norm ‘ 𝑇 ) ‘ ( 𝐹 ‘ ( 𝐴 ( -g ‘ 𝑆 ) 𝐵 ) ) ) ≤ ( ( 𝑁 ‘ 𝐹 ) · ( ( norm ‘ 𝑆 ) ‘ ( 𝐴 ( -g ‘ 𝑆 ) 𝐵 ) ) ) )
15 5 11 14 syl2anc ⊢ ( ( 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( ( norm ‘ 𝑇 ) ‘ ( 𝐹 ‘ ( 𝐴 ( -g ‘ 𝑆 ) 𝐵 ) ) ) ≤ ( ( 𝑁 ‘ 𝐹 ) · ( ( norm ‘ 𝑆 ) ‘ ( 𝐴 ( -g ‘ 𝑆 ) 𝐵 ) ) ) )
16 nghmrcl2 ⊢ ( 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) → 𝑇 ∈ NrmGrp )
17 16 3ad2ant1 ⊢ ( ( 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → 𝑇 ∈ NrmGrp )
18 nghmghm ⊢ ( 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) → 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) )
19 18 3ad2ant1 ⊢ ( ( 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) )
20 eqid ⊢ ( Base ‘ 𝑇 ) = ( Base ‘ 𝑇 )
21 2 20 ghmf ⊢ ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) → 𝐹 : 𝑉 ⟶ ( Base ‘ 𝑇 ) )
22 19 21 syl ⊢ ( ( 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → 𝐹 : 𝑉 ⟶ ( Base ‘ 𝑇 ) )
23 simp2 ⊢ ( ( 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → 𝐴 ∈ 𝑉 )
24 22 23 ffvelrnd ⊢ ( ( 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( 𝐹 ‘ 𝐴 ) ∈ ( Base ‘ 𝑇 ) )
25 simp3 ⊢ ( ( 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → 𝐵 ∈ 𝑉 )
26 22 25 ffvelrnd ⊢ ( ( 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( 𝐹 ‘ 𝐵 ) ∈ ( Base ‘ 𝑇 ) )
27 eqid ⊢ ( -g ‘ 𝑇 ) = ( -g ‘ 𝑇 )
28 13 20 27 4 ngpds ⊢ ( ( 𝑇 ∈ NrmGrp ∧ ( 𝐹 ‘ 𝐴 ) ∈ ( Base ‘ 𝑇 ) ∧ ( 𝐹 ‘ 𝐵 ) ∈ ( Base ‘ 𝑇 ) ) → ( ( 𝐹 ‘ 𝐴 ) 𝐷 ( 𝐹 ‘ 𝐵 ) ) = ( ( norm ‘ 𝑇 ) ‘ ( ( 𝐹 ‘ 𝐴 ) ( -g ‘ 𝑇 ) ( 𝐹 ‘ 𝐵 ) ) ) )
29 17 24 26 28 syl3anc ⊢ ( ( 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( ( 𝐹 ‘ 𝐴 ) 𝐷 ( 𝐹 ‘ 𝐵 ) ) = ( ( norm ‘ 𝑇 ) ‘ ( ( 𝐹 ‘ 𝐴 ) ( -g ‘ 𝑇 ) ( 𝐹 ‘ 𝐵 ) ) ) )
30 2 9 27 ghmsub ⊢ ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( 𝐹 ‘ ( 𝐴 ( -g ‘ 𝑆 ) 𝐵 ) ) = ( ( 𝐹 ‘ 𝐴 ) ( -g ‘ 𝑇 ) ( 𝐹 ‘ 𝐵 ) ) )
31 18 30 syl3an1 ⊢ ( ( 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( 𝐹 ‘ ( 𝐴 ( -g ‘ 𝑆 ) 𝐵 ) ) = ( ( 𝐹 ‘ 𝐴 ) ( -g ‘ 𝑇 ) ( 𝐹 ‘ 𝐵 ) ) )
32 31 fveq2d ⊢ ( ( 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( ( norm ‘ 𝑇 ) ‘ ( 𝐹 ‘ ( 𝐴 ( -g ‘ 𝑆 ) 𝐵 ) ) ) = ( ( norm ‘ 𝑇 ) ‘ ( ( 𝐹 ‘ 𝐴 ) ( -g ‘ 𝑇 ) ( 𝐹 ‘ 𝐵 ) ) ) )
33 29 32 eqtr4d ⊢ ( ( 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( ( 𝐹 ‘ 𝐴 ) 𝐷 ( 𝐹 ‘ 𝐵 ) ) = ( ( norm ‘ 𝑇 ) ‘ ( 𝐹 ‘ ( 𝐴 ( -g ‘ 𝑆 ) 𝐵 ) ) ) )
34 12 2 9 3 ngpds ⊢ ( ( 𝑆 ∈ NrmGrp ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( 𝐴 𝐶 𝐵 ) = ( ( norm ‘ 𝑆 ) ‘ ( 𝐴 ( -g ‘ 𝑆 ) 𝐵 ) ) )
35 6 34 syl3an1 ⊢ ( ( 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( 𝐴 𝐶 𝐵 ) = ( ( norm ‘ 𝑆 ) ‘ ( 𝐴 ( -g ‘ 𝑆 ) 𝐵 ) ) )
36 35 oveq2d ⊢ ( ( 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( ( 𝑁 ‘ 𝐹 ) · ( 𝐴 𝐶 𝐵 ) ) = ( ( 𝑁 ‘ 𝐹 ) · ( ( norm ‘ 𝑆 ) ‘ ( 𝐴 ( -g ‘ 𝑆 ) 𝐵 ) ) ) )
37 15 33 36 3brtr4d ⊢ ( ( 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( ( 𝐹 ‘ 𝐴 ) 𝐷 ( 𝐹 ‘ 𝐵 ) ) ≤ ( ( 𝑁 ‘ 𝐹 ) · ( 𝐴 𝐶 𝐵 ) ) )