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 e. LinFn
nlelch.2 
|- T e. ContFn
Assertion riesz3i 
|- E. w e. ~H A. v e. ~H ( T ` v ) = ( v .ih w )

Proof

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