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 ๐‘ค )