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 ffvelcdmi ⊢ ( 𝑢 ∈ ℋ → ( 𝑇 ‘ 𝑢 ) ∈ ℂ )
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 ffvelcdmi ⊢ ( 𝑣 ∈ ℋ → ( 𝑇 ‘ 𝑣 ) ∈ ℂ )
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 𝑤 )