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 ⊢ T ∈ LinFn
nlelch.2 ⊢ T ∈ ContFn
Assertion riesz3i ⊢ ∃ w ∈ ℋ ∀ v ∈ ℋ T ⁡ v = v ⋅ ih w

Proof

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