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	$⊢ N = S normOp T$
	nmods.v	$⊢ V = {Base}_{S}$
	nmods.c	$⊢ C = dist (S)$
	nmods.d	$⊢ D = dist (T)$
Assertion	nmods	$⊢ (F \in (S NGHom T) \land A \in V \land B \in V) \to F (A) D F (B) \leq N (F) (A C B)$

Proof

Step	Hyp	Ref	Expression
1		nmods.n	$⊢ N = S normOp T$
2		nmods.v	$⊢ V = {Base}_{S}$
3		nmods.c	$⊢ C = dist (S)$
4		nmods.d	$⊢ D = dist (T)$
5		simp1	$⊢ (F \in (S NGHom T) \land A \in V \land B \in V) \to F \in (S NGHom T)$
6		nghmrcl1	$⊢ F \in (S NGHom T) \to S \in NrmGrp$
7		ngpgrp	$⊢ S \in NrmGrp \to S \in Grp$
8	6 7	syl	$⊢ F \in (S NGHom T) \to S \in Grp$
9		eqid	$⊢ -_{S} = -_{S}$
10	2 9	grpsubcl	$⊢ (S \in Grp \land A \in V \land B \in V) \to A -_{S} B \in V$
11	8 10	syl3an1	$⊢ (F \in (S NGHom T) \land A \in V \land B \in V) \to A -_{S} B \in V$
12		eqid	$⊢ norm (S) = norm (S)$
13		eqid	$⊢ norm (T) = norm (T)$
14	1 2 12 13	nmoi	$⊢ (F \in (S NGHom T) \land A -_{S} B \in V) \to norm (T) (F (A -_{S} B)) \leq N (F) norm (S) (A -_{S} B)$
15	5 11 14	syl2anc	$⊢ (F \in (S NGHom T) \land A \in V \land B \in V) \to norm (T) (F (A -_{S} B)) \leq N (F) norm (S) (A -_{S} B)$
16		nghmrcl2	$⊢ F \in (S NGHom T) \to T \in NrmGrp$
17	16	3ad2ant1	$⊢ (F \in (S NGHom T) \land A \in V \land B \in V) \to T \in NrmGrp$
18		nghmghm	$⊢ F \in (S NGHom T) \to F \in (S GrpHom T)$
19	18	3ad2ant1	$⊢ (F \in (S NGHom T) \land A \in V \land B \in V) \to F \in (S GrpHom T)$
20		eqid	$⊢ {Base}_{T} = {Base}_{T}$
21	2 20	ghmf	$⊢ F \in (S GrpHom T) \to F : V ⟶ {Base}_{T}$
22	19 21	syl	$⊢ (F \in (S NGHom T) \land A \in V \land B \in V) \to F : V ⟶ {Base}_{T}$
23		simp2	$⊢ (F \in (S NGHom T) \land A \in V \land B \in V) \to A \in V$
24	22 23	ffvelrnd	$⊢ (F \in (S NGHom T) \land A \in V \land B \in V) \to F (A) \in {Base}_{T}$
25		simp3	$⊢ (F \in (S NGHom T) \land A \in V \land B \in V) \to B \in V$
26	22 25	ffvelrnd	$⊢ (F \in (S NGHom T) \land A \in V \land B \in V) \to F (B) \in {Base}_{T}$
27		eqid	$⊢ -_{T} = -_{T}$
28	13 20 27 4	ngpds	$⊢ (T \in NrmGrp \land F (A) \in {Base}_{T} \land F (B) \in {Base}_{T}) \to F (A) D F (B) = norm (T) (F (A) -_{T} F (B))$
29	17 24 26 28	syl3anc	$⊢ (F \in (S NGHom T) \land A \in V \land B \in V) \to F (A) D F (B) = norm (T) (F (A) -_{T} F (B))$
30	2 9 27	ghmsub	$⊢ (F \in (S GrpHom T) \land A \in V \land B \in V) \to F (A -_{S} B) = F (A) -_{T} F (B)$
31	18 30	syl3an1	$⊢ (F \in (S NGHom T) \land A \in V \land B \in V) \to F (A -_{S} B) = F (A) -_{T} F (B)$
32	31	fveq2d	$⊢ (F \in (S NGHom T) \land A \in V \land B \in V) \to norm (T) (F (A -_{S} B)) = norm (T) (F (A) -_{T} F (B))$
33	29 32	eqtr4d	$⊢ (F \in (S NGHom T) \land A \in V \land B \in V) \to F (A) D F (B) = norm (T) (F (A -_{S} B))$
34	12 2 9 3	ngpds	$⊢ (S \in NrmGrp \land A \in V \land B \in V) \to A C B = norm (S) (A -_{S} B)$
35	6 34	syl3an1	$⊢ (F \in (S NGHom T) \land A \in V \land B \in V) \to A C B = norm (S) (A -_{S} B)$
36	35	oveq2d	$⊢ (F \in (S NGHom T) \land A \in V \land B \in V) \to N (F) (A C B) = N (F) norm (S) (A -_{S} B)$
37	15 33 36	3brtr4d	$⊢ (F \in (S NGHom T) \land A \in V \land B \in V) \to F (A) D F (B) \leq N (F) (A C B)$

Metamath Proof Explorer

Theorem nmods

Proof