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

Metamath Proof Explorer

Theorem cnlnadjlem2

Description: Lemma for cnlnadji . G is a continuous linear functional. (Contributed by NM, 16-Feb-2006) (New usage is discouraged.)

Ref Expression
Hypotheses cnlnadjlem.1 ⊢ 𝑇 ∈ LinOp
cnlnadjlem.2 ⊢ 𝑇 ∈ ContOp
cnlnadjlem.3 ⊢ 𝐺 = ( 𝑔 ∈ ℋ ↦ ( ( 𝑇 ‘ 𝑔 ) ·ih 𝑦 ) )
Assertion cnlnadjlem2 ( 𝑦 ∈ ℋ → ( 𝐺 ∈ LinFn ∧ 𝐺 ∈ ContFn ) )

Proof

Step Hyp Ref Expression
1 cnlnadjlem.1 ⊢ 𝑇 ∈ LinOp
2 cnlnadjlem.2 ⊢ 𝑇 ∈ ContOp
3 cnlnadjlem.3 ⊢ 𝐺 = ( 𝑔 ∈ ℋ ↦ ( ( 𝑇 ‘ 𝑔 ) ·ih 𝑦 ) )
4 1 lnopfi ⊢ 𝑇 : ℋ ⟶ ℋ
5 4 ffvelcdmi ⊢ ( 𝑔 ∈ ℋ → ( 𝑇 ‘ 𝑔 ) ∈ ℋ )
6 hicl ⊢ ( ( ( 𝑇 ‘ 𝑔 ) ∈ ℋ ∧ 𝑦 ∈ ℋ ) → ( ( 𝑇 ‘ 𝑔 ) ·ih 𝑦 ) ∈ ℂ )
7 5 6 sylan ⊢ ( ( 𝑔 ∈ ℋ ∧ 𝑦 ∈ ℋ ) → ( ( 𝑇 ‘ 𝑔 ) ·ih 𝑦 ) ∈ ℂ )
8 7 ancoms ⊢ ( ( 𝑦 ∈ ℋ ∧ 𝑔 ∈ ℋ ) → ( ( 𝑇 ‘ 𝑔 ) ·ih 𝑦 ) ∈ ℂ )
9 8 3 fmptd ⊢ ( 𝑦 ∈ ℋ → 𝐺 : ℋ ⟶ ℂ )
10 hvmulcl ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑤 ∈ ℋ ) → ( 𝑥 ·ℎ 𝑤 ) ∈ ℋ )
11 1 lnopaddi ⊢ ( ( ( 𝑥 ·ℎ 𝑤 ) ∈ ℋ ∧ 𝑧 ∈ ℋ ) → ( 𝑇 ‘ ( ( 𝑥 ·ℎ 𝑤 ) +ℎ 𝑧 ) ) = ( ( 𝑇 ‘ ( 𝑥 ·ℎ 𝑤 ) ) +ℎ ( 𝑇 ‘ 𝑧 ) ) )
12 11 3adant3 ⊢ ( ( ( 𝑥 ·ℎ 𝑤 ) ∈ ℋ ∧ 𝑧 ∈ ℋ ∧ 𝑦 ∈ ℋ ) → ( 𝑇 ‘ ( ( 𝑥 ·ℎ 𝑤 ) +ℎ 𝑧 ) ) = ( ( 𝑇 ‘ ( 𝑥 ·ℎ 𝑤 ) ) +ℎ ( 𝑇 ‘ 𝑧 ) ) )
13 12 oveq1d ⊢ ( ( ( 𝑥 ·ℎ 𝑤 ) ∈ ℋ ∧ 𝑧 ∈ ℋ ∧ 𝑦 ∈ ℋ ) → ( ( 𝑇 ‘ ( ( 𝑥 ·ℎ 𝑤 ) +ℎ 𝑧 ) ) ·ih 𝑦 ) = ( ( ( 𝑇 ‘ ( 𝑥 ·ℎ 𝑤 ) ) +ℎ ( 𝑇 ‘ 𝑧 ) ) ·ih 𝑦 ) )
14 4 ffvelcdmi ⊢ ( ( 𝑥 ·ℎ 𝑤 ) ∈ ℋ → ( 𝑇 ‘ ( 𝑥 ·ℎ 𝑤 ) ) ∈ ℋ )
15 4 ffvelcdmi ⊢ ( 𝑧 ∈ ℋ → ( 𝑇 ‘ 𝑧 ) ∈ ℋ )
16 id ⊢ ( 𝑦 ∈ ℋ → 𝑦 ∈ ℋ )
17 ax-his2 ⊢ ( ( ( 𝑇 ‘ ( 𝑥 ·ℎ 𝑤 ) ) ∈ ℋ ∧ ( 𝑇 ‘ 𝑧 ) ∈ ℋ ∧ 𝑦 ∈ ℋ ) → ( ( ( 𝑇 ‘ ( 𝑥 ·ℎ 𝑤 ) ) +ℎ ( 𝑇 ‘ 𝑧 ) ) ·ih 𝑦 ) = ( ( ( 𝑇 ‘ ( 𝑥 ·ℎ 𝑤 ) ) ·ih 𝑦 ) + ( ( 𝑇 ‘ 𝑧 ) ·ih 𝑦 ) ) )
18 14 15 16 17 syl3an ⊢ ( ( ( 𝑥 ·ℎ 𝑤 ) ∈ ℋ ∧ 𝑧 ∈ ℋ ∧ 𝑦 ∈ ℋ ) → ( ( ( 𝑇 ‘ ( 𝑥 ·ℎ 𝑤 ) ) +ℎ ( 𝑇 ‘ 𝑧 ) ) ·ih 𝑦 ) = ( ( ( 𝑇 ‘ ( 𝑥 ·ℎ 𝑤 ) ) ·ih 𝑦 ) + ( ( 𝑇 ‘ 𝑧 ) ·ih 𝑦 ) ) )
19 13 18 eqtrd ⊢ ( ( ( 𝑥 ·ℎ 𝑤 ) ∈ ℋ ∧ 𝑧 ∈ ℋ ∧ 𝑦 ∈ ℋ ) → ( ( 𝑇 ‘ ( ( 𝑥 ·ℎ 𝑤 ) +ℎ 𝑧 ) ) ·ih 𝑦 ) = ( ( ( 𝑇 ‘ ( 𝑥 ·ℎ 𝑤 ) ) ·ih 𝑦 ) + ( ( 𝑇 ‘ 𝑧 ) ·ih 𝑦 ) ) )
20 19 3comr ⊢ ( ( 𝑦 ∈ ℋ ∧ ( 𝑥 ·ℎ 𝑤 ) ∈ ℋ ∧ 𝑧 ∈ ℋ ) → ( ( 𝑇 ‘ ( ( 𝑥 ·ℎ 𝑤 ) +ℎ 𝑧 ) ) ·ih 𝑦 ) = ( ( ( 𝑇 ‘ ( 𝑥 ·ℎ 𝑤 ) ) ·ih 𝑦 ) + ( ( 𝑇 ‘ 𝑧 ) ·ih 𝑦 ) ) )
21 20 3expa ⊢ ( ( ( 𝑦 ∈ ℋ ∧ ( 𝑥 ·ℎ 𝑤 ) ∈ ℋ ) ∧ 𝑧 ∈ ℋ ) → ( ( 𝑇 ‘ ( ( 𝑥 ·ℎ 𝑤 ) +ℎ 𝑧 ) ) ·ih 𝑦 ) = ( ( ( 𝑇 ‘ ( 𝑥 ·ℎ 𝑤 ) ) ·ih 𝑦 ) + ( ( 𝑇 ‘ 𝑧 ) ·ih 𝑦 ) ) )
22 10 21 sylanl2 ⊢ ( ( ( 𝑦 ∈ ℋ ∧ ( 𝑥 ∈ ℂ ∧ 𝑤 ∈ ℋ ) ) ∧ 𝑧 ∈ ℋ ) → ( ( 𝑇 ‘ ( ( 𝑥 ·ℎ 𝑤 ) +ℎ 𝑧 ) ) ·ih 𝑦 ) = ( ( ( 𝑇 ‘ ( 𝑥 ·ℎ 𝑤 ) ) ·ih 𝑦 ) + ( ( 𝑇 ‘ 𝑧 ) ·ih 𝑦 ) ) )
23 hvaddcl ⊢ ( ( ( 𝑥 ·ℎ 𝑤 ) ∈ ℋ ∧ 𝑧 ∈ ℋ ) → ( ( 𝑥 ·ℎ 𝑤 ) +ℎ 𝑧 ) ∈ ℋ )
24 10 23 sylan ⊢ ( ( ( 𝑥 ∈ ℂ ∧ 𝑤 ∈ ℋ ) ∧ 𝑧 ∈ ℋ ) → ( ( 𝑥 ·ℎ 𝑤 ) +ℎ 𝑧 ) ∈ ℋ )
25 1 2 3 cnlnadjlem1 ⊢ ( ( ( 𝑥 ·ℎ 𝑤 ) +ℎ 𝑧 ) ∈ ℋ → ( 𝐺 ‘ ( ( 𝑥 ·ℎ 𝑤 ) +ℎ 𝑧 ) ) = ( ( 𝑇 ‘ ( ( 𝑥 ·ℎ 𝑤 ) +ℎ 𝑧 ) ) ·ih 𝑦 ) )
26 24 25 syl ⊢ ( ( ( 𝑥 ∈ ℂ ∧ 𝑤 ∈ ℋ ) ∧ 𝑧 ∈ ℋ ) → ( 𝐺 ‘ ( ( 𝑥 ·ℎ 𝑤 ) +ℎ 𝑧 ) ) = ( ( 𝑇 ‘ ( ( 𝑥 ·ℎ 𝑤 ) +ℎ 𝑧 ) ) ·ih 𝑦 ) )
27 26 adantll ⊢ ( ( ( 𝑦 ∈ ℋ ∧ ( 𝑥 ∈ ℂ ∧ 𝑤 ∈ ℋ ) ) ∧ 𝑧 ∈ ℋ ) → ( 𝐺 ‘ ( ( 𝑥 ·ℎ 𝑤 ) +ℎ 𝑧 ) ) = ( ( 𝑇 ‘ ( ( 𝑥 ·ℎ 𝑤 ) +ℎ 𝑧 ) ) ·ih 𝑦 ) )
28 4 ffvelcdmi ⊢ ( 𝑤 ∈ ℋ → ( 𝑇 ‘ 𝑤 ) ∈ ℋ )
29 ax-his3 ⊢ ( ( 𝑥 ∈ ℂ ∧ ( 𝑇 ‘ 𝑤 ) ∈ ℋ ∧ 𝑦 ∈ ℋ ) → ( ( 𝑥 ·ℎ ( 𝑇 ‘ 𝑤 ) ) ·ih 𝑦 ) = ( 𝑥 · ( ( 𝑇 ‘ 𝑤 ) ·ih 𝑦 ) ) )
30 28 29 syl3an2 ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑤 ∈ ℋ ∧ 𝑦 ∈ ℋ ) → ( ( 𝑥 ·ℎ ( 𝑇 ‘ 𝑤 ) ) ·ih 𝑦 ) = ( 𝑥 · ( ( 𝑇 ‘ 𝑤 ) ·ih 𝑦 ) ) )
31 30 3comr ⊢ ( ( 𝑦 ∈ ℋ ∧ 𝑥 ∈ ℂ ∧ 𝑤 ∈ ℋ ) → ( ( 𝑥 ·ℎ ( 𝑇 ‘ 𝑤 ) ) ·ih 𝑦 ) = ( 𝑥 · ( ( 𝑇 ‘ 𝑤 ) ·ih 𝑦 ) ) )
32 31 3expb ⊢ ( ( 𝑦 ∈ ℋ ∧ ( 𝑥 ∈ ℂ ∧ 𝑤 ∈ ℋ ) ) → ( ( 𝑥 ·ℎ ( 𝑇 ‘ 𝑤 ) ) ·ih 𝑦 ) = ( 𝑥 · ( ( 𝑇 ‘ 𝑤 ) ·ih 𝑦 ) ) )
33 1 lnopmuli ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑤 ∈ ℋ ) → ( 𝑇 ‘ ( 𝑥 ·ℎ 𝑤 ) ) = ( 𝑥 ·ℎ ( 𝑇 ‘ 𝑤 ) ) )
34 33 oveq1d ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑤 ∈ ℋ ) → ( ( 𝑇 ‘ ( 𝑥 ·ℎ 𝑤 ) ) ·ih 𝑦 ) = ( ( 𝑥 ·ℎ ( 𝑇 ‘ 𝑤 ) ) ·ih 𝑦 ) )
35 34 adantl ⊢ ( ( 𝑦 ∈ ℋ ∧ ( 𝑥 ∈ ℂ ∧ 𝑤 ∈ ℋ ) ) → ( ( 𝑇 ‘ ( 𝑥 ·ℎ 𝑤 ) ) ·ih 𝑦 ) = ( ( 𝑥 ·ℎ ( 𝑇 ‘ 𝑤 ) ) ·ih 𝑦 ) )
36 1 2 3 cnlnadjlem1 ⊢ ( 𝑤 ∈ ℋ → ( 𝐺 ‘ 𝑤 ) = ( ( 𝑇 ‘ 𝑤 ) ·ih 𝑦 ) )
37 36 oveq2d ⊢ ( 𝑤 ∈ ℋ → ( 𝑥 · ( 𝐺 ‘ 𝑤 ) ) = ( 𝑥 · ( ( 𝑇 ‘ 𝑤 ) ·ih 𝑦 ) ) )
38 37 ad2antll ⊢ ( ( 𝑦 ∈ ℋ ∧ ( 𝑥 ∈ ℂ ∧ 𝑤 ∈ ℋ ) ) → ( 𝑥 · ( 𝐺 ‘ 𝑤 ) ) = ( 𝑥 · ( ( 𝑇 ‘ 𝑤 ) ·ih 𝑦 ) ) )
39 32 35 38 3eqtr4rd ⊢ ( ( 𝑦 ∈ ℋ ∧ ( 𝑥 ∈ ℂ ∧ 𝑤 ∈ ℋ ) ) → ( 𝑥 · ( 𝐺 ‘ 𝑤 ) ) = ( ( 𝑇 ‘ ( 𝑥 ·ℎ 𝑤 ) ) ·ih 𝑦 ) )
40 1 2 3 cnlnadjlem1 ⊢ ( 𝑧 ∈ ℋ → ( 𝐺 ‘ 𝑧 ) = ( ( 𝑇 ‘ 𝑧 ) ·ih 𝑦 ) )
41 39 40 oveqan12d ⊢ ( ( ( 𝑦 ∈ ℋ ∧ ( 𝑥 ∈ ℂ ∧ 𝑤 ∈ ℋ ) ) ∧ 𝑧 ∈ ℋ ) → ( ( 𝑥 · ( 𝐺 ‘ 𝑤 ) ) + ( 𝐺 ‘ 𝑧 ) ) = ( ( ( 𝑇 ‘ ( 𝑥 ·ℎ 𝑤 ) ) ·ih 𝑦 ) + ( ( 𝑇 ‘ 𝑧 ) ·ih 𝑦 ) ) )
42 22 27 41 3eqtr4d ⊢ ( ( ( 𝑦 ∈ ℋ ∧ ( 𝑥 ∈ ℂ ∧ 𝑤 ∈ ℋ ) ) ∧ 𝑧 ∈ ℋ ) → ( 𝐺 ‘ ( ( 𝑥 ·ℎ 𝑤 ) +ℎ 𝑧 ) ) = ( ( 𝑥 · ( 𝐺 ‘ 𝑤 ) ) + ( 𝐺 ‘ 𝑧 ) ) )
43 42 ralrimiva ⊢ ( ( 𝑦 ∈ ℋ ∧ ( 𝑥 ∈ ℂ ∧ 𝑤 ∈ ℋ ) ) → ∀ 𝑧 ∈ ℋ ( 𝐺 ‘ ( ( 𝑥 ·ℎ 𝑤 ) +ℎ 𝑧 ) ) = ( ( 𝑥 · ( 𝐺 ‘ 𝑤 ) ) + ( 𝐺 ‘ 𝑧 ) ) )
44 43 ralrimivva ⊢ ( 𝑦 ∈ ℋ → ∀ 𝑥 ∈ ℂ ∀ 𝑤 ∈ ℋ ∀ 𝑧 ∈ ℋ ( 𝐺 ‘ ( ( 𝑥 ·ℎ 𝑤 ) +ℎ 𝑧 ) ) = ( ( 𝑥 · ( 𝐺 ‘ 𝑤 ) ) + ( 𝐺 ‘ 𝑧 ) ) )
45 ellnfn ⊢ ( 𝐺 ∈ LinFn ↔ ( 𝐺 : ℋ ⟶ ℂ ∧ ∀ 𝑥 ∈ ℂ ∀ 𝑤 ∈ ℋ ∀ 𝑧 ∈ ℋ ( 𝐺 ‘ ( ( 𝑥 ·ℎ 𝑤 ) +ℎ 𝑧 ) ) = ( ( 𝑥 · ( 𝐺 ‘ 𝑤 ) ) + ( 𝐺 ‘ 𝑧 ) ) ) )
46 9 44 45 sylanbrc ⊢ ( 𝑦 ∈ ℋ → 𝐺 ∈ LinFn )
47 1 2 nmcopexi ⊢ ( normop ‘ 𝑇 ) ∈ ℝ
48 normcl ⊢ ( 𝑦 ∈ ℋ → ( normℎ ‘ 𝑦 ) ∈ ℝ )
49 remulcl ⊢ ( ( ( normop ‘ 𝑇 ) ∈ ℝ ∧ ( normℎ ‘ 𝑦 ) ∈ ℝ ) → ( ( normop ‘ 𝑇 ) · ( normℎ ‘ 𝑦 ) ) ∈ ℝ )
50 47 48 49 sylancr ⊢ ( 𝑦 ∈ ℋ → ( ( normop ‘ 𝑇 ) · ( normℎ ‘ 𝑦 ) ) ∈ ℝ )
51 40 adantr ⊢ ( ( 𝑧 ∈ ℋ ∧ 𝑦 ∈ ℋ ) → ( 𝐺 ‘ 𝑧 ) = ( ( 𝑇 ‘ 𝑧 ) ·ih 𝑦 ) )
52 hicl ⊢ ( ( ( 𝑇 ‘ 𝑧 ) ∈ ℋ ∧ 𝑦 ∈ ℋ ) → ( ( 𝑇 ‘ 𝑧 ) ·ih 𝑦 ) ∈ ℂ )
53 15 52 sylan ⊢ ( ( 𝑧 ∈ ℋ ∧ 𝑦 ∈ ℋ ) → ( ( 𝑇 ‘ 𝑧 ) ·ih 𝑦 ) ∈ ℂ )
54 51 53 eqeltrd ⊢ ( ( 𝑧 ∈ ℋ ∧ 𝑦 ∈ ℋ ) → ( 𝐺 ‘ 𝑧 ) ∈ ℂ )
55 54 abscld ⊢ ( ( 𝑧 ∈ ℋ ∧ 𝑦 ∈ ℋ ) → ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ∈ ℝ )
56 normcl ⊢ ( ( 𝑇 ‘ 𝑧 ) ∈ ℋ → ( normℎ ‘ ( 𝑇 ‘ 𝑧 ) ) ∈ ℝ )
57 15 56 syl ⊢ ( 𝑧 ∈ ℋ → ( normℎ ‘ ( 𝑇 ‘ 𝑧 ) ) ∈ ℝ )
58 remulcl ⊢ ( ( ( normℎ ‘ ( 𝑇 ‘ 𝑧 ) ) ∈ ℝ ∧ ( normℎ ‘ 𝑦 ) ∈ ℝ ) → ( ( normℎ ‘ ( 𝑇 ‘ 𝑧 ) ) · ( normℎ ‘ 𝑦 ) ) ∈ ℝ )
59 57 48 58 syl2an ⊢ ( ( 𝑧 ∈ ℋ ∧ 𝑦 ∈ ℋ ) → ( ( normℎ ‘ ( 𝑇 ‘ 𝑧 ) ) · ( normℎ ‘ 𝑦 ) ) ∈ ℝ )
60 normcl ⊢ ( 𝑧 ∈ ℋ → ( normℎ ‘ 𝑧 ) ∈ ℝ )
61 remulcl ⊢ ( ( ( normop ‘ 𝑇 ) ∈ ℝ ∧ ( normℎ ‘ 𝑧 ) ∈ ℝ ) → ( ( normop ‘ 𝑇 ) · ( normℎ ‘ 𝑧 ) ) ∈ ℝ )
62 47 60 61 sylancr ⊢ ( 𝑧 ∈ ℋ → ( ( normop ‘ 𝑇 ) · ( normℎ ‘ 𝑧 ) ) ∈ ℝ )
63 remulcl ⊢ ( ( ( ( normop ‘ 𝑇 ) · ( normℎ ‘ 𝑧 ) ) ∈ ℝ ∧ ( normℎ ‘ 𝑦 ) ∈ ℝ ) → ( ( ( normop ‘ 𝑇 ) · ( normℎ ‘ 𝑧 ) ) · ( normℎ ‘ 𝑦 ) ) ∈ ℝ )
64 62 48 63 syl2an ⊢ ( ( 𝑧 ∈ ℋ ∧ 𝑦 ∈ ℋ ) → ( ( ( normop ‘ 𝑇 ) · ( normℎ ‘ 𝑧 ) ) · ( normℎ ‘ 𝑦 ) ) ∈ ℝ )
65 51 fveq2d ⊢ ( ( 𝑧 ∈ ℋ ∧ 𝑦 ∈ ℋ ) → ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) = ( abs ‘ ( ( 𝑇 ‘ 𝑧 ) ·ih 𝑦 ) ) )
66 bcs ⊢ ( ( ( 𝑇 ‘ 𝑧 ) ∈ ℋ ∧ 𝑦 ∈ ℋ ) → ( abs ‘ ( ( 𝑇 ‘ 𝑧 ) ·ih 𝑦 ) ) ≤ ( ( normℎ ‘ ( 𝑇 ‘ 𝑧 ) ) · ( normℎ ‘ 𝑦 ) ) )
67 15 66 sylan ⊢ ( ( 𝑧 ∈ ℋ ∧ 𝑦 ∈ ℋ ) → ( abs ‘ ( ( 𝑇 ‘ 𝑧 ) ·ih 𝑦 ) ) ≤ ( ( normℎ ‘ ( 𝑇 ‘ 𝑧 ) ) · ( normℎ ‘ 𝑦 ) ) )
68 65 67 eqbrtrd ⊢ ( ( 𝑧 ∈ ℋ ∧ 𝑦 ∈ ℋ ) → ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ≤ ( ( normℎ ‘ ( 𝑇 ‘ 𝑧 ) ) · ( normℎ ‘ 𝑦 ) ) )
69 57 adantr ⊢ ( ( 𝑧 ∈ ℋ ∧ 𝑦 ∈ ℋ ) → ( normℎ ‘ ( 𝑇 ‘ 𝑧 ) ) ∈ ℝ )
70 62 adantr ⊢ ( ( 𝑧 ∈ ℋ ∧ 𝑦 ∈ ℋ ) → ( ( normop ‘ 𝑇 ) · ( normℎ ‘ 𝑧 ) ) ∈ ℝ )
71 normge0 ⊢ ( 𝑦 ∈ ℋ → 0 ≤ ( normℎ ‘ 𝑦 ) )
72 48 71 jca ⊢ ( 𝑦 ∈ ℋ → ( ( normℎ ‘ 𝑦 ) ∈ ℝ ∧ 0 ≤ ( normℎ ‘ 𝑦 ) ) )
73 72 adantl ⊢ ( ( 𝑧 ∈ ℋ ∧ 𝑦 ∈ ℋ ) → ( ( normℎ ‘ 𝑦 ) ∈ ℝ ∧ 0 ≤ ( normℎ ‘ 𝑦 ) ) )
74 1 2 nmcoplbi ⊢ ( 𝑧 ∈ ℋ → ( normℎ ‘ ( 𝑇 ‘ 𝑧 ) ) ≤ ( ( normop ‘ 𝑇 ) · ( normℎ ‘ 𝑧 ) ) )
75 74 adantr ⊢ ( ( 𝑧 ∈ ℋ ∧ 𝑦 ∈ ℋ ) → ( normℎ ‘ ( 𝑇 ‘ 𝑧 ) ) ≤ ( ( normop ‘ 𝑇 ) · ( normℎ ‘ 𝑧 ) ) )
76 lemul1a ⊢ ( ( ( ( normℎ ‘ ( 𝑇 ‘ 𝑧 ) ) ∈ ℝ ∧ ( ( normop ‘ 𝑇 ) · ( normℎ ‘ 𝑧 ) ) ∈ ℝ ∧ ( ( normℎ ‘ 𝑦 ) ∈ ℝ ∧ 0 ≤ ( normℎ ‘ 𝑦 ) ) ) ∧ ( normℎ ‘ ( 𝑇 ‘ 𝑧 ) ) ≤ ( ( normop ‘ 𝑇 ) · ( normℎ ‘ 𝑧 ) ) ) → ( ( normℎ ‘ ( 𝑇 ‘ 𝑧 ) ) · ( normℎ ‘ 𝑦 ) ) ≤ ( ( ( normop ‘ 𝑇 ) · ( normℎ ‘ 𝑧 ) ) · ( normℎ ‘ 𝑦 ) ) )
77 69 70 73 75 76 syl31anc ⊢ ( ( 𝑧 ∈ ℋ ∧ 𝑦 ∈ ℋ ) → ( ( normℎ ‘ ( 𝑇 ‘ 𝑧 ) ) · ( normℎ ‘ 𝑦 ) ) ≤ ( ( ( normop ‘ 𝑇 ) · ( normℎ ‘ 𝑧 ) ) · ( normℎ ‘ 𝑦 ) ) )
78 55 59 64 68 77 letrd ⊢ ( ( 𝑧 ∈ ℋ ∧ 𝑦 ∈ ℋ ) → ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ≤ ( ( ( normop ‘ 𝑇 ) · ( normℎ ‘ 𝑧 ) ) · ( normℎ ‘ 𝑦 ) ) )
79 60 recnd ⊢ ( 𝑧 ∈ ℋ → ( normℎ ‘ 𝑧 ) ∈ ℂ )
80 48 recnd ⊢ ( 𝑦 ∈ ℋ → ( normℎ ‘ 𝑦 ) ∈ ℂ )
81 47 recni ⊢ ( normop ‘ 𝑇 ) ∈ ℂ
82 mul32 ⊢ ( ( ( normop ‘ 𝑇 ) ∈ ℂ ∧ ( normℎ ‘ 𝑧 ) ∈ ℂ ∧ ( normℎ ‘ 𝑦 ) ∈ ℂ ) → ( ( ( normop ‘ 𝑇 ) · ( normℎ ‘ 𝑧 ) ) · ( normℎ ‘ 𝑦 ) ) = ( ( ( normop ‘ 𝑇 ) · ( normℎ ‘ 𝑦 ) ) · ( normℎ ‘ 𝑧 ) ) )
83 81 82 mp3an1 ⊢ ( ( ( normℎ ‘ 𝑧 ) ∈ ℂ ∧ ( normℎ ‘ 𝑦 ) ∈ ℂ ) → ( ( ( normop ‘ 𝑇 ) · ( normℎ ‘ 𝑧 ) ) · ( normℎ ‘ 𝑦 ) ) = ( ( ( normop ‘ 𝑇 ) · ( normℎ ‘ 𝑦 ) ) · ( normℎ ‘ 𝑧 ) ) )
84 79 80 83 syl2an ⊢ ( ( 𝑧 ∈ ℋ ∧ 𝑦 ∈ ℋ ) → ( ( ( normop ‘ 𝑇 ) · ( normℎ ‘ 𝑧 ) ) · ( normℎ ‘ 𝑦 ) ) = ( ( ( normop ‘ 𝑇 ) · ( normℎ ‘ 𝑦 ) ) · ( normℎ ‘ 𝑧 ) ) )
85 78 84 breqtrd ⊢ ( ( 𝑧 ∈ ℋ ∧ 𝑦 ∈ ℋ ) → ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ≤ ( ( ( normop ‘ 𝑇 ) · ( normℎ ‘ 𝑦 ) ) · ( normℎ ‘ 𝑧 ) ) )
86 85 ancoms ⊢ ( ( 𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ ) → ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ≤ ( ( ( normop ‘ 𝑇 ) · ( normℎ ‘ 𝑦 ) ) · ( normℎ ‘ 𝑧 ) ) )
87 86 ralrimiva ⊢ ( 𝑦 ∈ ℋ → ∀ 𝑧 ∈ ℋ ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ≤ ( ( ( normop ‘ 𝑇 ) · ( normℎ ‘ 𝑦 ) ) · ( normℎ ‘ 𝑧 ) ) )
88 oveq1 ⊢ ( 𝑥 = ( ( normop ‘ 𝑇 ) · ( normℎ ‘ 𝑦 ) ) → ( 𝑥 · ( normℎ ‘ 𝑧 ) ) = ( ( ( normop ‘ 𝑇 ) · ( normℎ ‘ 𝑦 ) ) · ( normℎ ‘ 𝑧 ) ) )
89 88 breq2d ⊢ ( 𝑥 = ( ( normop ‘ 𝑇 ) · ( normℎ ‘ 𝑦 ) ) → ( ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ≤ ( 𝑥 · ( normℎ ‘ 𝑧 ) ) ↔ ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ≤ ( ( ( normop ‘ 𝑇 ) · ( normℎ ‘ 𝑦 ) ) · ( normℎ ‘ 𝑧 ) ) ) )
90 89 ralbidv ⊢ ( 𝑥 = ( ( normop ‘ 𝑇 ) · ( normℎ ‘ 𝑦 ) ) → ( ∀ 𝑧 ∈ ℋ ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ≤ ( 𝑥 · ( normℎ ‘ 𝑧 ) ) ↔ ∀ 𝑧 ∈ ℋ ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ≤ ( ( ( normop ‘ 𝑇 ) · ( normℎ ‘ 𝑦 ) ) · ( normℎ ‘ 𝑧 ) ) ) )
91 90 rspcev ⊢ ( ( ( ( normop ‘ 𝑇 ) · ( normℎ ‘ 𝑦 ) ) ∈ ℝ ∧ ∀ 𝑧 ∈ ℋ ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ≤ ( ( ( normop ‘ 𝑇 ) · ( normℎ ‘ 𝑦 ) ) · ( normℎ ‘ 𝑧 ) ) ) → ∃ 𝑥 ∈ ℝ ∀ 𝑧 ∈ ℋ ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ≤ ( 𝑥 · ( normℎ ‘ 𝑧 ) ) )
92 50 87 91 syl2anc ⊢ ( 𝑦 ∈ ℋ → ∃ 𝑥 ∈ ℝ ∀ 𝑧 ∈ ℋ ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ≤ ( 𝑥 · ( normℎ ‘ 𝑧 ) ) )
93 lnfncon ⊢ ( 𝐺 ∈ LinFn → ( 𝐺 ∈ ContFn ↔ ∃ 𝑥 ∈ ℝ ∀ 𝑧 ∈ ℋ ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ≤ ( 𝑥 · ( normℎ ‘ 𝑧 ) ) ) )
94 46 93 syl ⊢ ( 𝑦 ∈ ℋ → ( 𝐺 ∈ ContFn ↔ ∃ 𝑥 ∈ ℝ ∀ 𝑧 ∈ ℋ ( abs ‘ ( 𝐺 ‘ 𝑧 ) ) ≤ ( 𝑥 · ( normℎ ‘ 𝑧 ) ) ) )
95 92 94 mpbird ⊢ ( 𝑦 ∈ ℋ → 𝐺 ∈ ContFn )
96 46 95 jca ⊢ ( 𝑦 ∈ ℋ → ( 𝐺 ∈ LinFn ∧ 𝐺 ∈ ContFn ) )