Metamath Proof Explorer


Theorem riesz3i

Description: A continuous linear functional can be expressed as an inner product. Existence part of Theorem 3.9 of Beran p. 104. (Contributed by NM, 13-Feb-2006) (New usage is discouraged.)

Ref Expression
Hypotheses nlelch.1 𝑇 ∈ LinFn
nlelch.2 𝑇 ∈ ContFn
Assertion riesz3i 𝑤 ∈ ℋ ∀ 𝑣 ∈ ℋ ( 𝑇𝑣 ) = ( 𝑣 ·ih 𝑤 )

Proof

Step Hyp Ref Expression
1 nlelch.1 𝑇 ∈ LinFn
2 nlelch.2 𝑇 ∈ ContFn
3 ax-hv0cl 0 ∈ ℋ
4 1 lnfnfi 𝑇 : ℋ ⟶ ℂ
5 fveq2 ( ( ⊥ ‘ ( null ‘ 𝑇 ) ) = 0 → ( ⊥ ‘ ( ⊥ ‘ ( null ‘ 𝑇 ) ) ) = ( ⊥ ‘ 0 ) )
6 1 2 nlelchi ( null ‘ 𝑇 ) ∈ C
7 6 ococi ( ⊥ ‘ ( ⊥ ‘ ( null ‘ 𝑇 ) ) ) = ( null ‘ 𝑇 )
8 choc0 ( ⊥ ‘ 0 ) = ℋ
9 5 7 8 3eqtr3g ( ( ⊥ ‘ ( null ‘ 𝑇 ) ) = 0 → ( null ‘ 𝑇 ) = ℋ )
10 9 eleq2d ( ( ⊥ ‘ ( null ‘ 𝑇 ) ) = 0 → ( 𝑣 ∈ ( null ‘ 𝑇 ) ↔ 𝑣 ∈ ℋ ) )
11 10 biimpar ( ( ( ⊥ ‘ ( null ‘ 𝑇 ) ) = 0𝑣 ∈ ℋ ) → 𝑣 ∈ ( null ‘ 𝑇 ) )
12 elnlfn2 ( ( 𝑇 : ℋ ⟶ ℂ ∧ 𝑣 ∈ ( null ‘ 𝑇 ) ) → ( 𝑇𝑣 ) = 0 )
13 4 11 12 sylancr ( ( ( ⊥ ‘ ( null ‘ 𝑇 ) ) = 0𝑣 ∈ ℋ ) → ( 𝑇𝑣 ) = 0 )
14 hi02 ( 𝑣 ∈ ℋ → ( 𝑣 ·ih 0 ) = 0 )
15 14 adantl ( ( ( ⊥ ‘ ( null ‘ 𝑇 ) ) = 0𝑣 ∈ ℋ ) → ( 𝑣 ·ih 0 ) = 0 )
16 13 15 eqtr4d ( ( ( ⊥ ‘ ( null ‘ 𝑇 ) ) = 0𝑣 ∈ ℋ ) → ( 𝑇𝑣 ) = ( 𝑣 ·ih 0 ) )
17 16 ralrimiva ( ( ⊥ ‘ ( null ‘ 𝑇 ) ) = 0 → ∀ 𝑣 ∈ ℋ ( 𝑇𝑣 ) = ( 𝑣 ·ih 0 ) )
18 oveq2 ( 𝑤 = 0 → ( 𝑣 ·ih 𝑤 ) = ( 𝑣 ·ih 0 ) )
19 18 eqeq2d ( 𝑤 = 0 → ( ( 𝑇𝑣 ) = ( 𝑣 ·ih 𝑤 ) ↔ ( 𝑇𝑣 ) = ( 𝑣 ·ih 0 ) ) )
20 19 ralbidv ( 𝑤 = 0 → ( ∀ 𝑣 ∈ ℋ ( 𝑇𝑣 ) = ( 𝑣 ·ih 𝑤 ) ↔ ∀ 𝑣 ∈ ℋ ( 𝑇𝑣 ) = ( 𝑣 ·ih 0 ) ) )
21 20 rspcev ( ( 0 ∈ ℋ ∧ ∀ 𝑣 ∈ ℋ ( 𝑇𝑣 ) = ( 𝑣 ·ih 0 ) ) → ∃ 𝑤 ∈ ℋ ∀ 𝑣 ∈ ℋ ( 𝑇𝑣 ) = ( 𝑣 ·ih 𝑤 ) )
22 3 17 21 sylancr ( ( ⊥ ‘ ( null ‘ 𝑇 ) ) = 0 → ∃ 𝑤 ∈ ℋ ∀ 𝑣 ∈ ℋ ( 𝑇𝑣 ) = ( 𝑣 ·ih 𝑤 ) )
23 6 choccli ( ⊥ ‘ ( null ‘ 𝑇 ) ) ∈ C
24 23 chne0i ( ( ⊥ ‘ ( null ‘ 𝑇 ) ) ≠ 0 ↔ ∃ 𝑢 ∈ ( ⊥ ‘ ( null ‘ 𝑇 ) ) 𝑢 ≠ 0 )
25 23 cheli ( 𝑢 ∈ ( ⊥ ‘ ( null ‘ 𝑇 ) ) → 𝑢 ∈ ℋ )
26 4 ffvelrni ( 𝑢 ∈ ℋ → ( 𝑇𝑢 ) ∈ ℂ )
27 26 adantr ( ( 𝑢 ∈ ℋ ∧ 𝑢 ≠ 0 ) → ( 𝑇𝑢 ) ∈ ℂ )
28 hicl ( ( 𝑢 ∈ ℋ ∧ 𝑢 ∈ ℋ ) → ( 𝑢 ·ih 𝑢 ) ∈ ℂ )
29 28 anidms ( 𝑢 ∈ ℋ → ( 𝑢 ·ih 𝑢 ) ∈ ℂ )
30 29 adantr ( ( 𝑢 ∈ ℋ ∧ 𝑢 ≠ 0 ) → ( 𝑢 ·ih 𝑢 ) ∈ ℂ )
31 his6 ( 𝑢 ∈ ℋ → ( ( 𝑢 ·ih 𝑢 ) = 0 ↔ 𝑢 = 0 ) )
32 31 necon3bid ( 𝑢 ∈ ℋ → ( ( 𝑢 ·ih 𝑢 ) ≠ 0 ↔ 𝑢 ≠ 0 ) )
33 32 biimpar ( ( 𝑢 ∈ ℋ ∧ 𝑢 ≠ 0 ) → ( 𝑢 ·ih 𝑢 ) ≠ 0 )
34 27 30 33 divcld ( ( 𝑢 ∈ ℋ ∧ 𝑢 ≠ 0 ) → ( ( 𝑇𝑢 ) / ( 𝑢 ·ih 𝑢 ) ) ∈ ℂ )
35 34 cjcld ( ( 𝑢 ∈ ℋ ∧ 𝑢 ≠ 0 ) → ( ∗ ‘ ( ( 𝑇𝑢 ) / ( 𝑢 ·ih 𝑢 ) ) ) ∈ ℂ )
36 simpl ( ( 𝑢 ∈ ℋ ∧ 𝑢 ≠ 0 ) → 𝑢 ∈ ℋ )
37 hvmulcl ( ( ( ∗ ‘ ( ( 𝑇𝑢 ) / ( 𝑢 ·ih 𝑢 ) ) ) ∈ ℂ ∧ 𝑢 ∈ ℋ ) → ( ( ∗ ‘ ( ( 𝑇𝑢 ) / ( 𝑢 ·ih 𝑢 ) ) ) · 𝑢 ) ∈ ℋ )
38 35 36 37 syl2anc ( ( 𝑢 ∈ ℋ ∧ 𝑢 ≠ 0 ) → ( ( ∗ ‘ ( ( 𝑇𝑢 ) / ( 𝑢 ·ih 𝑢 ) ) ) · 𝑢 ) ∈ ℋ )
39 38 adantll ( ( ( 𝑢 ∈ ( ⊥ ‘ ( null ‘ 𝑇 ) ) ∧ 𝑢 ∈ ℋ ) ∧ 𝑢 ≠ 0 ) → ( ( ∗ ‘ ( ( 𝑇𝑢 ) / ( 𝑢 ·ih 𝑢 ) ) ) · 𝑢 ) ∈ ℋ )
40 hvmulcl ( ( ( 𝑇𝑢 ) ∈ ℂ ∧ 𝑣 ∈ ℋ ) → ( ( 𝑇𝑢 ) · 𝑣 ) ∈ ℋ )
41 26 40 sylan ( ( 𝑢 ∈ ℋ ∧ 𝑣 ∈ ℋ ) → ( ( 𝑇𝑢 ) · 𝑣 ) ∈ ℋ )
42 4 ffvelrni ( 𝑣 ∈ ℋ → ( 𝑇𝑣 ) ∈ ℂ )
43 hvmulcl ( ( ( 𝑇𝑣 ) ∈ ℂ ∧ 𝑢 ∈ ℋ ) → ( ( 𝑇𝑣 ) · 𝑢 ) ∈ ℋ )
44 42 43 sylan ( ( 𝑣 ∈ ℋ ∧ 𝑢 ∈ ℋ ) → ( ( 𝑇𝑣 ) · 𝑢 ) ∈ ℋ )
45 44 ancoms ( ( 𝑢 ∈ ℋ ∧ 𝑣 ∈ ℋ ) → ( ( 𝑇𝑣 ) · 𝑢 ) ∈ ℋ )
46 simpl ( ( 𝑢 ∈ ℋ ∧ 𝑣 ∈ ℋ ) → 𝑢 ∈ ℋ )
47 his2sub ( ( ( ( 𝑇𝑢 ) · 𝑣 ) ∈ ℋ ∧ ( ( 𝑇𝑣 ) · 𝑢 ) ∈ ℋ ∧ 𝑢 ∈ ℋ ) → ( ( ( ( 𝑇𝑢 ) · 𝑣 ) − ( ( 𝑇𝑣 ) · 𝑢 ) ) ·ih 𝑢 ) = ( ( ( ( 𝑇𝑢 ) · 𝑣 ) ·ih 𝑢 ) − ( ( ( 𝑇𝑣 ) · 𝑢 ) ·ih 𝑢 ) ) )
48 41 45 46 47 syl3anc ( ( 𝑢 ∈ ℋ ∧ 𝑣 ∈ ℋ ) → ( ( ( ( 𝑇𝑢 ) · 𝑣 ) − ( ( 𝑇𝑣 ) · 𝑢 ) ) ·ih 𝑢 ) = ( ( ( ( 𝑇𝑢 ) · 𝑣 ) ·ih 𝑢 ) − ( ( ( 𝑇𝑣 ) · 𝑢 ) ·ih 𝑢 ) ) )
49 26 adantr ( ( 𝑢 ∈ ℋ ∧ 𝑣 ∈ ℋ ) → ( 𝑇𝑢 ) ∈ ℂ )
50 simpr ( ( 𝑢 ∈ ℋ ∧ 𝑣 ∈ ℋ ) → 𝑣 ∈ ℋ )
51 ax-his3 ( ( ( 𝑇𝑢 ) ∈ ℂ ∧ 𝑣 ∈ ℋ ∧ 𝑢 ∈ ℋ ) → ( ( ( 𝑇𝑢 ) · 𝑣 ) ·ih 𝑢 ) = ( ( 𝑇𝑢 ) · ( 𝑣 ·ih 𝑢 ) ) )
52 49 50 46 51 syl3anc ( ( 𝑢 ∈ ℋ ∧ 𝑣 ∈ ℋ ) → ( ( ( 𝑇𝑢 ) · 𝑣 ) ·ih 𝑢 ) = ( ( 𝑇𝑢 ) · ( 𝑣 ·ih 𝑢 ) ) )
53 42 adantl ( ( 𝑢 ∈ ℋ ∧ 𝑣 ∈ ℋ ) → ( 𝑇𝑣 ) ∈ ℂ )
54 ax-his3 ( ( ( 𝑇𝑣 ) ∈ ℂ ∧ 𝑢 ∈ ℋ ∧ 𝑢 ∈ ℋ ) → ( ( ( 𝑇𝑣 ) · 𝑢 ) ·ih 𝑢 ) = ( ( 𝑇𝑣 ) · ( 𝑢 ·ih 𝑢 ) ) )
55 53 46 46 54 syl3anc ( ( 𝑢 ∈ ℋ ∧ 𝑣 ∈ ℋ ) → ( ( ( 𝑇𝑣 ) · 𝑢 ) ·ih 𝑢 ) = ( ( 𝑇𝑣 ) · ( 𝑢 ·ih 𝑢 ) ) )
56 52 55 oveq12d ( ( 𝑢 ∈ ℋ ∧ 𝑣 ∈ ℋ ) → ( ( ( ( 𝑇𝑢 ) · 𝑣 ) ·ih 𝑢 ) − ( ( ( 𝑇𝑣 ) · 𝑢 ) ·ih 𝑢 ) ) = ( ( ( 𝑇𝑢 ) · ( 𝑣 ·ih 𝑢 ) ) − ( ( 𝑇𝑣 ) · ( 𝑢 ·ih 𝑢 ) ) ) )
57 48 56 eqtr2d ( ( 𝑢 ∈ ℋ ∧ 𝑣 ∈ ℋ ) → ( ( ( 𝑇𝑢 ) · ( 𝑣 ·ih 𝑢 ) ) − ( ( 𝑇𝑣 ) · ( 𝑢 ·ih 𝑢 ) ) ) = ( ( ( ( 𝑇𝑢 ) · 𝑣 ) − ( ( 𝑇𝑣 ) · 𝑢 ) ) ·ih 𝑢 ) )
58 57 adantll ( ( ( 𝑢 ∈ ( ⊥ ‘ ( null ‘ 𝑇 ) ) ∧ 𝑢 ∈ ℋ ) ∧ 𝑣 ∈ ℋ ) → ( ( ( 𝑇𝑢 ) · ( 𝑣 ·ih 𝑢 ) ) − ( ( 𝑇𝑣 ) · ( 𝑢 ·ih 𝑢 ) ) ) = ( ( ( ( 𝑇𝑢 ) · 𝑣 ) − ( ( 𝑇𝑣 ) · 𝑢 ) ) ·ih 𝑢 ) )
59 hvsubcl ( ( ( ( 𝑇𝑢 ) · 𝑣 ) ∈ ℋ ∧ ( ( 𝑇𝑣 ) · 𝑢 ) ∈ ℋ ) → ( ( ( 𝑇𝑢 ) · 𝑣 ) − ( ( 𝑇𝑣 ) · 𝑢 ) ) ∈ ℋ )
60 41 45 59 syl2anc ( ( 𝑢 ∈ ℋ ∧ 𝑣 ∈ ℋ ) → ( ( ( 𝑇𝑢 ) · 𝑣 ) − ( ( 𝑇𝑣 ) · 𝑢 ) ) ∈ ℋ )
61 1 lnfnsubi ( ( ( ( 𝑇𝑢 ) · 𝑣 ) ∈ ℋ ∧ ( ( 𝑇𝑣 ) · 𝑢 ) ∈ ℋ ) → ( 𝑇 ‘ ( ( ( 𝑇𝑢 ) · 𝑣 ) − ( ( 𝑇𝑣 ) · 𝑢 ) ) ) = ( ( 𝑇 ‘ ( ( 𝑇𝑢 ) · 𝑣 ) ) − ( 𝑇 ‘ ( ( 𝑇𝑣 ) · 𝑢 ) ) ) )
62 41 45 61 syl2anc ( ( 𝑢 ∈ ℋ ∧ 𝑣 ∈ ℋ ) → ( 𝑇 ‘ ( ( ( 𝑇𝑢 ) · 𝑣 ) − ( ( 𝑇𝑣 ) · 𝑢 ) ) ) = ( ( 𝑇 ‘ ( ( 𝑇𝑢 ) · 𝑣 ) ) − ( 𝑇 ‘ ( ( 𝑇𝑣 ) · 𝑢 ) ) ) )
63 1 lnfnmuli ( ( ( 𝑇𝑢 ) ∈ ℂ ∧ 𝑣 ∈ ℋ ) → ( 𝑇 ‘ ( ( 𝑇𝑢 ) · 𝑣 ) ) = ( ( 𝑇𝑢 ) · ( 𝑇𝑣 ) ) )
64 26 63 sylan ( ( 𝑢 ∈ ℋ ∧ 𝑣 ∈ ℋ ) → ( 𝑇 ‘ ( ( 𝑇𝑢 ) · 𝑣 ) ) = ( ( 𝑇𝑢 ) · ( 𝑇𝑣 ) ) )
65 1 lnfnmuli ( ( ( 𝑇𝑣 ) ∈ ℂ ∧ 𝑢 ∈ ℋ ) → ( 𝑇 ‘ ( ( 𝑇𝑣 ) · 𝑢 ) ) = ( ( 𝑇𝑣 ) · ( 𝑇𝑢 ) ) )
66 mulcom ( ( ( 𝑇𝑣 ) ∈ ℂ ∧ ( 𝑇𝑢 ) ∈ ℂ ) → ( ( 𝑇𝑣 ) · ( 𝑇𝑢 ) ) = ( ( 𝑇𝑢 ) · ( 𝑇𝑣 ) ) )
67 26 66 sylan2 ( ( ( 𝑇𝑣 ) ∈ ℂ ∧ 𝑢 ∈ ℋ ) → ( ( 𝑇𝑣 ) · ( 𝑇𝑢 ) ) = ( ( 𝑇𝑢 ) · ( 𝑇𝑣 ) ) )
68 65 67 eqtrd ( ( ( 𝑇𝑣 ) ∈ ℂ ∧ 𝑢 ∈ ℋ ) → ( 𝑇 ‘ ( ( 𝑇𝑣 ) · 𝑢 ) ) = ( ( 𝑇𝑢 ) · ( 𝑇𝑣 ) ) )
69 42 68 sylan ( ( 𝑣 ∈ ℋ ∧ 𝑢 ∈ ℋ ) → ( 𝑇 ‘ ( ( 𝑇𝑣 ) · 𝑢 ) ) = ( ( 𝑇𝑢 ) · ( 𝑇𝑣 ) ) )
70 69 ancoms ( ( 𝑢 ∈ ℋ ∧ 𝑣 ∈ ℋ ) → ( 𝑇 ‘ ( ( 𝑇𝑣 ) · 𝑢 ) ) = ( ( 𝑇𝑢 ) · ( 𝑇𝑣 ) ) )
71 64 70 oveq12d ( ( 𝑢 ∈ ℋ ∧ 𝑣 ∈ ℋ ) → ( ( 𝑇 ‘ ( ( 𝑇𝑢 ) · 𝑣 ) ) − ( 𝑇 ‘ ( ( 𝑇𝑣 ) · 𝑢 ) ) ) = ( ( ( 𝑇𝑢 ) · ( 𝑇𝑣 ) ) − ( ( 𝑇𝑢 ) · ( 𝑇𝑣 ) ) ) )
72 mulcl ( ( ( 𝑇𝑢 ) ∈ ℂ ∧ ( 𝑇𝑣 ) ∈ ℂ ) → ( ( 𝑇𝑢 ) · ( 𝑇𝑣 ) ) ∈ ℂ )
73 26 42 72 syl2an ( ( 𝑢 ∈ ℋ ∧ 𝑣 ∈ ℋ ) → ( ( 𝑇𝑢 ) · ( 𝑇𝑣 ) ) ∈ ℂ )
74 73 subidd ( ( 𝑢 ∈ ℋ ∧ 𝑣 ∈ ℋ ) → ( ( ( 𝑇𝑢 ) · ( 𝑇𝑣 ) ) − ( ( 𝑇𝑢 ) · ( 𝑇𝑣 ) ) ) = 0 )
75 62 71 74 3eqtrd ( ( 𝑢 ∈ ℋ ∧ 𝑣 ∈ ℋ ) → ( 𝑇 ‘ ( ( ( 𝑇𝑢 ) · 𝑣 ) − ( ( 𝑇𝑣 ) · 𝑢 ) ) ) = 0 )
76 elnlfn ( 𝑇 : ℋ ⟶ ℂ → ( ( ( ( 𝑇𝑢 ) · 𝑣 ) − ( ( 𝑇𝑣 ) · 𝑢 ) ) ∈ ( null ‘ 𝑇 ) ↔ ( ( ( ( 𝑇𝑢 ) · 𝑣 ) − ( ( 𝑇𝑣 ) · 𝑢 ) ) ∈ ℋ ∧ ( 𝑇 ‘ ( ( ( 𝑇𝑢 ) · 𝑣 ) − ( ( 𝑇𝑣 ) · 𝑢 ) ) ) = 0 ) ) )
77 4 76 ax-mp ( ( ( ( 𝑇𝑢 ) · 𝑣 ) − ( ( 𝑇𝑣 ) · 𝑢 ) ) ∈ ( null ‘ 𝑇 ) ↔ ( ( ( ( 𝑇𝑢 ) · 𝑣 ) − ( ( 𝑇𝑣 ) · 𝑢 ) ) ∈ ℋ ∧ ( 𝑇 ‘ ( ( ( 𝑇𝑢 ) · 𝑣 ) − ( ( 𝑇𝑣 ) · 𝑢 ) ) ) = 0 ) )
78 60 75 77 sylanbrc ( ( 𝑢 ∈ ℋ ∧ 𝑣 ∈ ℋ ) → ( ( ( 𝑇𝑢 ) · 𝑣 ) − ( ( 𝑇𝑣 ) · 𝑢 ) ) ∈ ( null ‘ 𝑇 ) )
79 6 chssii ( null ‘ 𝑇 ) ⊆ ℋ
80 ocorth ( ( null ‘ 𝑇 ) ⊆ ℋ → ( ( ( ( ( 𝑇𝑢 ) · 𝑣 ) − ( ( 𝑇𝑣 ) · 𝑢 ) ) ∈ ( null ‘ 𝑇 ) ∧ 𝑢 ∈ ( ⊥ ‘ ( null ‘ 𝑇 ) ) ) → ( ( ( ( 𝑇𝑢 ) · 𝑣 ) − ( ( 𝑇𝑣 ) · 𝑢 ) ) ·ih 𝑢 ) = 0 ) )
81 79 80 ax-mp ( ( ( ( ( 𝑇𝑢 ) · 𝑣 ) − ( ( 𝑇𝑣 ) · 𝑢 ) ) ∈ ( null ‘ 𝑇 ) ∧ 𝑢 ∈ ( ⊥ ‘ ( null ‘ 𝑇 ) ) ) → ( ( ( ( 𝑇𝑢 ) · 𝑣 ) − ( ( 𝑇𝑣 ) · 𝑢 ) ) ·ih 𝑢 ) = 0 )
82 78 81 sylan ( ( ( 𝑢 ∈ ℋ ∧ 𝑣 ∈ ℋ ) ∧ 𝑢 ∈ ( ⊥ ‘ ( null ‘ 𝑇 ) ) ) → ( ( ( ( 𝑇𝑢 ) · 𝑣 ) − ( ( 𝑇𝑣 ) · 𝑢 ) ) ·ih 𝑢 ) = 0 )
83 82 ancoms ( ( 𝑢 ∈ ( ⊥ ‘ ( null ‘ 𝑇 ) ) ∧ ( 𝑢 ∈ ℋ ∧ 𝑣 ∈ ℋ ) ) → ( ( ( ( 𝑇𝑢 ) · 𝑣 ) − ( ( 𝑇𝑣 ) · 𝑢 ) ) ·ih 𝑢 ) = 0 )
84 83 anassrs ( ( ( 𝑢 ∈ ( ⊥ ‘ ( null ‘ 𝑇 ) ) ∧ 𝑢 ∈ ℋ ) ∧ 𝑣 ∈ ℋ ) → ( ( ( ( 𝑇𝑢 ) · 𝑣 ) − ( ( 𝑇𝑣 ) · 𝑢 ) ) ·ih 𝑢 ) = 0 )
85 58 84 eqtrd ( ( ( 𝑢 ∈ ( ⊥ ‘ ( null ‘ 𝑇 ) ) ∧ 𝑢 ∈ ℋ ) ∧ 𝑣 ∈ ℋ ) → ( ( ( 𝑇𝑢 ) · ( 𝑣 ·ih 𝑢 ) ) − ( ( 𝑇𝑣 ) · ( 𝑢 ·ih 𝑢 ) ) ) = 0 )
86 hicl ( ( 𝑣 ∈ ℋ ∧ 𝑢 ∈ ℋ ) → ( 𝑣 ·ih 𝑢 ) ∈ ℂ )
87 86 ancoms ( ( 𝑢 ∈ ℋ ∧ 𝑣 ∈ ℋ ) → ( 𝑣 ·ih 𝑢 ) ∈ ℂ )
88 49 87 mulcld ( ( 𝑢 ∈ ℋ ∧ 𝑣 ∈ ℋ ) → ( ( 𝑇𝑢 ) · ( 𝑣 ·ih 𝑢 ) ) ∈ ℂ )
89 mulcl ( ( ( 𝑇𝑣 ) ∈ ℂ ∧ ( 𝑢 ·ih 𝑢 ) ∈ ℂ ) → ( ( 𝑇𝑣 ) · ( 𝑢 ·ih 𝑢 ) ) ∈ ℂ )
90 42 29 89 syl2anr ( ( 𝑢 ∈ ℋ ∧ 𝑣 ∈ ℋ ) → ( ( 𝑇𝑣 ) · ( 𝑢 ·ih 𝑢 ) ) ∈ ℂ )
91 88 90 subeq0ad ( ( 𝑢 ∈ ℋ ∧ 𝑣 ∈ ℋ ) → ( ( ( ( 𝑇𝑢 ) · ( 𝑣 ·ih 𝑢 ) ) − ( ( 𝑇𝑣 ) · ( 𝑢 ·ih 𝑢 ) ) ) = 0 ↔ ( ( 𝑇𝑢 ) · ( 𝑣 ·ih 𝑢 ) ) = ( ( 𝑇𝑣 ) · ( 𝑢 ·ih 𝑢 ) ) ) )
92 91 adantll ( ( ( 𝑢 ∈ ( ⊥ ‘ ( null ‘ 𝑇 ) ) ∧ 𝑢 ∈ ℋ ) ∧ 𝑣 ∈ ℋ ) → ( ( ( ( 𝑇𝑢 ) · ( 𝑣 ·ih 𝑢 ) ) − ( ( 𝑇𝑣 ) · ( 𝑢 ·ih 𝑢 ) ) ) = 0 ↔ ( ( 𝑇𝑢 ) · ( 𝑣 ·ih 𝑢 ) ) = ( ( 𝑇𝑣 ) · ( 𝑢 ·ih 𝑢 ) ) ) )
93 85 92 mpbid ( ( ( 𝑢 ∈ ( ⊥ ‘ ( null ‘ 𝑇 ) ) ∧ 𝑢 ∈ ℋ ) ∧ 𝑣 ∈ ℋ ) → ( ( 𝑇𝑢 ) · ( 𝑣 ·ih 𝑢 ) ) = ( ( 𝑇𝑣 ) · ( 𝑢 ·ih 𝑢 ) ) )
94 93 adantlr ( ( ( ( 𝑢 ∈ ( ⊥ ‘ ( null ‘ 𝑇 ) ) ∧ 𝑢 ∈ ℋ ) ∧ 𝑢 ≠ 0 ) ∧ 𝑣 ∈ ℋ ) → ( ( 𝑇𝑢 ) · ( 𝑣 ·ih 𝑢 ) ) = ( ( 𝑇𝑣 ) · ( 𝑢 ·ih 𝑢 ) ) )
95 88 adantlr ( ( ( 𝑢 ∈ ℋ ∧ 𝑢 ≠ 0 ) ∧ 𝑣 ∈ ℋ ) → ( ( 𝑇𝑢 ) · ( 𝑣 ·ih 𝑢 ) ) ∈ ℂ )
96 42 adantl ( ( ( 𝑢 ∈ ℋ ∧ 𝑢 ≠ 0 ) ∧ 𝑣 ∈ ℋ ) → ( 𝑇𝑣 ) ∈ ℂ )
97 30 33 jca ( ( 𝑢 ∈ ℋ ∧ 𝑢 ≠ 0 ) → ( ( 𝑢 ·ih 𝑢 ) ∈ ℂ ∧ ( 𝑢 ·ih 𝑢 ) ≠ 0 ) )
98 97 adantr ( ( ( 𝑢 ∈ ℋ ∧ 𝑢 ≠ 0 ) ∧ 𝑣 ∈ ℋ ) → ( ( 𝑢 ·ih 𝑢 ) ∈ ℂ ∧ ( 𝑢 ·ih 𝑢 ) ≠ 0 ) )
99 divmul3 ( ( ( ( 𝑇𝑢 ) · ( 𝑣 ·ih 𝑢 ) ) ∈ ℂ ∧ ( 𝑇𝑣 ) ∈ ℂ ∧ ( ( 𝑢 ·ih 𝑢 ) ∈ ℂ ∧ ( 𝑢 ·ih 𝑢 ) ≠ 0 ) ) → ( ( ( ( 𝑇𝑢 ) · ( 𝑣 ·ih 𝑢 ) ) / ( 𝑢 ·ih 𝑢 ) ) = ( 𝑇𝑣 ) ↔ ( ( 𝑇𝑢 ) · ( 𝑣 ·ih 𝑢 ) ) = ( ( 𝑇𝑣 ) · ( 𝑢 ·ih 𝑢 ) ) ) )
100 95 96 98 99 syl3anc ( ( ( 𝑢 ∈ ℋ ∧ 𝑢 ≠ 0 ) ∧ 𝑣 ∈ ℋ ) → ( ( ( ( 𝑇𝑢 ) · ( 𝑣 ·ih 𝑢 ) ) / ( 𝑢 ·ih 𝑢 ) ) = ( 𝑇𝑣 ) ↔ ( ( 𝑇𝑢 ) · ( 𝑣 ·ih 𝑢 ) ) = ( ( 𝑇𝑣 ) · ( 𝑢 ·ih 𝑢 ) ) ) )
101 100 adantlll ( ( ( ( 𝑢 ∈ ( ⊥ ‘ ( null ‘ 𝑇 ) ) ∧ 𝑢 ∈ ℋ ) ∧ 𝑢 ≠ 0 ) ∧ 𝑣 ∈ ℋ ) → ( ( ( ( 𝑇𝑢 ) · ( 𝑣 ·ih 𝑢 ) ) / ( 𝑢 ·ih 𝑢 ) ) = ( 𝑇𝑣 ) ↔ ( ( 𝑇𝑢 ) · ( 𝑣 ·ih 𝑢 ) ) = ( ( 𝑇𝑣 ) · ( 𝑢 ·ih 𝑢 ) ) ) )
102 94 101 mpbird ( ( ( ( 𝑢 ∈ ( ⊥ ‘ ( null ‘ 𝑇 ) ) ∧ 𝑢 ∈ ℋ ) ∧ 𝑢 ≠ 0 ) ∧ 𝑣 ∈ ℋ ) → ( ( ( 𝑇𝑢 ) · ( 𝑣 ·ih 𝑢 ) ) / ( 𝑢 ·ih 𝑢 ) ) = ( 𝑇𝑣 ) )
103 27 adantr ( ( ( 𝑢 ∈ ℋ ∧ 𝑢 ≠ 0 ) ∧ 𝑣 ∈ ℋ ) → ( 𝑇𝑢 ) ∈ ℂ )
104 87 adantlr ( ( ( 𝑢 ∈ ℋ ∧ 𝑢 ≠ 0 ) ∧ 𝑣 ∈ ℋ ) → ( 𝑣 ·ih 𝑢 ) ∈ ℂ )
105 div23 ( ( ( 𝑇𝑢 ) ∈ ℂ ∧ ( 𝑣 ·ih 𝑢 ) ∈ ℂ ∧ ( ( 𝑢 ·ih 𝑢 ) ∈ ℂ ∧ ( 𝑢 ·ih 𝑢 ) ≠ 0 ) ) → ( ( ( 𝑇𝑢 ) · ( 𝑣 ·ih 𝑢 ) ) / ( 𝑢 ·ih 𝑢 ) ) = ( ( ( 𝑇𝑢 ) / ( 𝑢 ·ih 𝑢 ) ) · ( 𝑣 ·ih 𝑢 ) ) )
106 103 104 98 105 syl3anc ( ( ( 𝑢 ∈ ℋ ∧ 𝑢 ≠ 0 ) ∧ 𝑣 ∈ ℋ ) → ( ( ( 𝑇𝑢 ) · ( 𝑣 ·ih 𝑢 ) ) / ( 𝑢 ·ih 𝑢 ) ) = ( ( ( 𝑇𝑢 ) / ( 𝑢 ·ih 𝑢 ) ) · ( 𝑣 ·ih 𝑢 ) ) )
107 34 adantr ( ( ( 𝑢 ∈ ℋ ∧ 𝑢 ≠ 0 ) ∧ 𝑣 ∈ ℋ ) → ( ( 𝑇𝑢 ) / ( 𝑢 ·ih 𝑢 ) ) ∈ ℂ )
108 simpr ( ( ( 𝑢 ∈ ℋ ∧ 𝑢 ≠ 0 ) ∧ 𝑣 ∈ ℋ ) → 𝑣 ∈ ℋ )
109 simpll ( ( ( 𝑢 ∈ ℋ ∧ 𝑢 ≠ 0 ) ∧ 𝑣 ∈ ℋ ) → 𝑢 ∈ ℋ )
110 his52 ( ( ( ( 𝑇𝑢 ) / ( 𝑢 ·ih 𝑢 ) ) ∈ ℂ ∧ 𝑣 ∈ ℋ ∧ 𝑢 ∈ ℋ ) → ( 𝑣 ·ih ( ( ∗ ‘ ( ( 𝑇𝑢 ) / ( 𝑢 ·ih 𝑢 ) ) ) · 𝑢 ) ) = ( ( ( 𝑇𝑢 ) / ( 𝑢 ·ih 𝑢 ) ) · ( 𝑣 ·ih 𝑢 ) ) )
111 107 108 109 110 syl3anc ( ( ( 𝑢 ∈ ℋ ∧ 𝑢 ≠ 0 ) ∧ 𝑣 ∈ ℋ ) → ( 𝑣 ·ih ( ( ∗ ‘ ( ( 𝑇𝑢 ) / ( 𝑢 ·ih 𝑢 ) ) ) · 𝑢 ) ) = ( ( ( 𝑇𝑢 ) / ( 𝑢 ·ih 𝑢 ) ) · ( 𝑣 ·ih 𝑢 ) ) )
112 106 111 eqtr4d ( ( ( 𝑢 ∈ ℋ ∧ 𝑢 ≠ 0 ) ∧ 𝑣 ∈ ℋ ) → ( ( ( 𝑇𝑢 ) · ( 𝑣 ·ih 𝑢 ) ) / ( 𝑢 ·ih 𝑢 ) ) = ( 𝑣 ·ih ( ( ∗ ‘ ( ( 𝑇𝑢 ) / ( 𝑢 ·ih 𝑢 ) ) ) · 𝑢 ) ) )
113 112 adantlll ( ( ( ( 𝑢 ∈ ( ⊥ ‘ ( null ‘ 𝑇 ) ) ∧ 𝑢 ∈ ℋ ) ∧ 𝑢 ≠ 0 ) ∧ 𝑣 ∈ ℋ ) → ( ( ( 𝑇𝑢 ) · ( 𝑣 ·ih 𝑢 ) ) / ( 𝑢 ·ih 𝑢 ) ) = ( 𝑣 ·ih ( ( ∗ ‘ ( ( 𝑇𝑢 ) / ( 𝑢 ·ih 𝑢 ) ) ) · 𝑢 ) ) )
114 102 113 eqtr3d ( ( ( ( 𝑢 ∈ ( ⊥ ‘ ( null ‘ 𝑇 ) ) ∧ 𝑢 ∈ ℋ ) ∧ 𝑢 ≠ 0 ) ∧ 𝑣 ∈ ℋ ) → ( 𝑇𝑣 ) = ( 𝑣 ·ih ( ( ∗ ‘ ( ( 𝑇𝑢 ) / ( 𝑢 ·ih 𝑢 ) ) ) · 𝑢 ) ) )
115 114 ralrimiva ( ( ( 𝑢 ∈ ( ⊥ ‘ ( null ‘ 𝑇 ) ) ∧ 𝑢 ∈ ℋ ) ∧ 𝑢 ≠ 0 ) → ∀ 𝑣 ∈ ℋ ( 𝑇𝑣 ) = ( 𝑣 ·ih ( ( ∗ ‘ ( ( 𝑇𝑢 ) / ( 𝑢 ·ih 𝑢 ) ) ) · 𝑢 ) ) )
116 oveq2 ( 𝑤 = ( ( ∗ ‘ ( ( 𝑇𝑢 ) / ( 𝑢 ·ih 𝑢 ) ) ) · 𝑢 ) → ( 𝑣 ·ih 𝑤 ) = ( 𝑣 ·ih ( ( ∗ ‘ ( ( 𝑇𝑢 ) / ( 𝑢 ·ih 𝑢 ) ) ) · 𝑢 ) ) )
117 116 eqeq2d ( 𝑤 = ( ( ∗ ‘ ( ( 𝑇𝑢 ) / ( 𝑢 ·ih 𝑢 ) ) ) · 𝑢 ) → ( ( 𝑇𝑣 ) = ( 𝑣 ·ih 𝑤 ) ↔ ( 𝑇𝑣 ) = ( 𝑣 ·ih ( ( ∗ ‘ ( ( 𝑇𝑢 ) / ( 𝑢 ·ih 𝑢 ) ) ) · 𝑢 ) ) ) )
118 117 ralbidv ( 𝑤 = ( ( ∗ ‘ ( ( 𝑇𝑢 ) / ( 𝑢 ·ih 𝑢 ) ) ) · 𝑢 ) → ( ∀ 𝑣 ∈ ℋ ( 𝑇𝑣 ) = ( 𝑣 ·ih 𝑤 ) ↔ ∀ 𝑣 ∈ ℋ ( 𝑇𝑣 ) = ( 𝑣 ·ih ( ( ∗ ‘ ( ( 𝑇𝑢 ) / ( 𝑢 ·ih 𝑢 ) ) ) · 𝑢 ) ) ) )
119 118 rspcev ( ( ( ( ∗ ‘ ( ( 𝑇𝑢 ) / ( 𝑢 ·ih 𝑢 ) ) ) · 𝑢 ) ∈ ℋ ∧ ∀ 𝑣 ∈ ℋ ( 𝑇𝑣 ) = ( 𝑣 ·ih ( ( ∗ ‘ ( ( 𝑇𝑢 ) / ( 𝑢 ·ih 𝑢 ) ) ) · 𝑢 ) ) ) → ∃ 𝑤 ∈ ℋ ∀ 𝑣 ∈ ℋ ( 𝑇𝑣 ) = ( 𝑣 ·ih 𝑤 ) )
120 39 115 119 syl2anc ( ( ( 𝑢 ∈ ( ⊥ ‘ ( null ‘ 𝑇 ) ) ∧ 𝑢 ∈ ℋ ) ∧ 𝑢 ≠ 0 ) → ∃ 𝑤 ∈ ℋ ∀ 𝑣 ∈ ℋ ( 𝑇𝑣 ) = ( 𝑣 ·ih 𝑤 ) )
121 120 ex ( ( 𝑢 ∈ ( ⊥ ‘ ( null ‘ 𝑇 ) ) ∧ 𝑢 ∈ ℋ ) → ( 𝑢 ≠ 0 → ∃ 𝑤 ∈ ℋ ∀ 𝑣 ∈ ℋ ( 𝑇𝑣 ) = ( 𝑣 ·ih 𝑤 ) ) )
122 25 121 mpdan ( 𝑢 ∈ ( ⊥ ‘ ( null ‘ 𝑇 ) ) → ( 𝑢 ≠ 0 → ∃ 𝑤 ∈ ℋ ∀ 𝑣 ∈ ℋ ( 𝑇𝑣 ) = ( 𝑣 ·ih 𝑤 ) ) )
123 122 rexlimiv ( ∃ 𝑢 ∈ ( ⊥ ‘ ( null ‘ 𝑇 ) ) 𝑢 ≠ 0 → ∃ 𝑤 ∈ ℋ ∀ 𝑣 ∈ ℋ ( 𝑇𝑣 ) = ( 𝑣 ·ih 𝑤 ) )
124 24 123 sylbi ( ( ⊥ ‘ ( null ‘ 𝑇 ) ) ≠ 0 → ∃ 𝑤 ∈ ℋ ∀ 𝑣 ∈ ℋ ( 𝑇𝑣 ) = ( 𝑣 ·ih 𝑤 ) )
125 22 124 pm2.61ine 𝑤 ∈ ℋ ∀ 𝑣 ∈ ℋ ( 𝑇𝑣 ) = ( 𝑣 ·ih 𝑤 )