Metamath Proof Explorer


Theorem nmolb2d

Description: Any upper bound on the values of a linear operator at nonzero vectors translates to an upper bound on the operator norm. (Contributed by Mario Carneiro, 18-Oct-2015)

Ref Expression
Hypotheses nmofval.1 N=SnormOpT
nmofval.2 V=BaseS
nmofval.3 L=normS
nmofval.4 M=normT
nmolb2d.z 0˙=0S
nmolb2d.1 φSNrmGrp
nmolb2d.2 φTNrmGrp
nmolb2d.3 φFSGrpHomT
nmolb2d.4 φA
nmolb2d.5 φ0A
nmolb2d.6 φxVx0˙MFxALx
Assertion nmolb2d φNFA

Proof

Step Hyp Ref Expression
1 nmofval.1 N=SnormOpT
2 nmofval.2 V=BaseS
3 nmofval.3 L=normS
4 nmofval.4 M=normT
5 nmolb2d.z 0˙=0S
6 nmolb2d.1 φSNrmGrp
7 nmolb2d.2 φTNrmGrp
8 nmolb2d.3 φFSGrpHomT
9 nmolb2d.4 φA
10 nmolb2d.5 φ0A
11 nmolb2d.6 φxVx0˙MFxALx
12 2fveq3 x=0˙MFx=MF0˙
13 fveq2 x=0˙Lx=L0˙
14 13 oveq2d x=0˙ALx=AL0˙
15 12 14 breq12d x=0˙MFxALxMF0˙AL0˙
16 11 anassrs φxVx0˙MFxALx
17 0le0 00
18 9 recnd φA
19 18 mul01d φA0=0
20 17 19 breqtrrid φ0A0
21 eqid 0T=0T
22 5 21 ghmid FSGrpHomTF0˙=0T
23 8 22 syl φF0˙=0T
24 23 fveq2d φMF0˙=M0T
25 4 21 nm0 TNrmGrpM0T=0
26 7 25 syl φM0T=0
27 24 26 eqtrd φMF0˙=0
28 3 5 nm0 SNrmGrpL0˙=0
29 6 28 syl φL0˙=0
30 29 oveq2d φAL0˙=A0
31 20 27 30 3brtr4d φMF0˙AL0˙
32 31 adantr φxVMF0˙AL0˙
33 15 16 32 pm2.61ne φxVMFxALx
34 33 ralrimiva φxVMFxALx
35 1 2 3 4 nmolb SNrmGrpTNrmGrpFSGrpHomTA0AxVMFxALxNFA
36 6 7 8 9 10 35 syl311anc φxVMFxALxNFA
37 34 36 mpd φNFA