Metamath Proof Explorer


Theorem ellnfn

Description: Property defining a linear functional. (Contributed by NM, 11-Feb-2006) (Revised by Mario Carneiro, 16-Nov-2013) (New usage is discouraged.)

Ref Expression
Assertion ellnfn ( ๐‘‡ โˆˆ LinFn โ†” ( ๐‘‡ : โ„‹ โŸถ โ„‚ โˆง โˆ€ ๐‘ฅ โˆˆ โ„‚ โˆ€ ๐‘ฆ โˆˆ โ„‹ โˆ€ ๐‘ง โˆˆ โ„‹ ( ๐‘‡ โ€˜ ( ( ๐‘ฅ ยทโ„Ž ๐‘ฆ ) +โ„Ž ๐‘ง ) ) = ( ( ๐‘ฅ ยท ( ๐‘‡ โ€˜ ๐‘ฆ ) ) + ( ๐‘‡ โ€˜ ๐‘ง ) ) ) )

Proof

Step Hyp Ref Expression
1 fveq1 โŠข ( ๐‘ก = ๐‘‡ โ†’ ( ๐‘ก โ€˜ ( ( ๐‘ฅ ยทโ„Ž ๐‘ฆ ) +โ„Ž ๐‘ง ) ) = ( ๐‘‡ โ€˜ ( ( ๐‘ฅ ยทโ„Ž ๐‘ฆ ) +โ„Ž ๐‘ง ) ) )
2 fveq1 โŠข ( ๐‘ก = ๐‘‡ โ†’ ( ๐‘ก โ€˜ ๐‘ฆ ) = ( ๐‘‡ โ€˜ ๐‘ฆ ) )
3 2 oveq2d โŠข ( ๐‘ก = ๐‘‡ โ†’ ( ๐‘ฅ ยท ( ๐‘ก โ€˜ ๐‘ฆ ) ) = ( ๐‘ฅ ยท ( ๐‘‡ โ€˜ ๐‘ฆ ) ) )
4 fveq1 โŠข ( ๐‘ก = ๐‘‡ โ†’ ( ๐‘ก โ€˜ ๐‘ง ) = ( ๐‘‡ โ€˜ ๐‘ง ) )
5 3 4 oveq12d โŠข ( ๐‘ก = ๐‘‡ โ†’ ( ( ๐‘ฅ ยท ( ๐‘ก โ€˜ ๐‘ฆ ) ) + ( ๐‘ก โ€˜ ๐‘ง ) ) = ( ( ๐‘ฅ ยท ( ๐‘‡ โ€˜ ๐‘ฆ ) ) + ( ๐‘‡ โ€˜ ๐‘ง ) ) )
6 1 5 eqeq12d โŠข ( ๐‘ก = ๐‘‡ โ†’ ( ( ๐‘ก โ€˜ ( ( ๐‘ฅ ยทโ„Ž ๐‘ฆ ) +โ„Ž ๐‘ง ) ) = ( ( ๐‘ฅ ยท ( ๐‘ก โ€˜ ๐‘ฆ ) ) + ( ๐‘ก โ€˜ ๐‘ง ) ) โ†” ( ๐‘‡ โ€˜ ( ( ๐‘ฅ ยทโ„Ž ๐‘ฆ ) +โ„Ž ๐‘ง ) ) = ( ( ๐‘ฅ ยท ( ๐‘‡ โ€˜ ๐‘ฆ ) ) + ( ๐‘‡ โ€˜ ๐‘ง ) ) ) )
7 6 ralbidv โŠข ( ๐‘ก = ๐‘‡ โ†’ ( โˆ€ ๐‘ง โˆˆ โ„‹ ( ๐‘ก โ€˜ ( ( ๐‘ฅ ยทโ„Ž ๐‘ฆ ) +โ„Ž ๐‘ง ) ) = ( ( ๐‘ฅ ยท ( ๐‘ก โ€˜ ๐‘ฆ ) ) + ( ๐‘ก โ€˜ ๐‘ง ) ) โ†” โˆ€ ๐‘ง โˆˆ โ„‹ ( ๐‘‡ โ€˜ ( ( ๐‘ฅ ยทโ„Ž ๐‘ฆ ) +โ„Ž ๐‘ง ) ) = ( ( ๐‘ฅ ยท ( ๐‘‡ โ€˜ ๐‘ฆ ) ) + ( ๐‘‡ โ€˜ ๐‘ง ) ) ) )
8 7 2ralbidv โŠข ( ๐‘ก = ๐‘‡ โ†’ ( โˆ€ ๐‘ฅ โˆˆ โ„‚ โˆ€ ๐‘ฆ โˆˆ โ„‹ โˆ€ ๐‘ง โˆˆ โ„‹ ( ๐‘ก โ€˜ ( ( ๐‘ฅ ยทโ„Ž ๐‘ฆ ) +โ„Ž ๐‘ง ) ) = ( ( ๐‘ฅ ยท ( ๐‘ก โ€˜ ๐‘ฆ ) ) + ( ๐‘ก โ€˜ ๐‘ง ) ) โ†” โˆ€ ๐‘ฅ โˆˆ โ„‚ โˆ€ ๐‘ฆ โˆˆ โ„‹ โˆ€ ๐‘ง โˆˆ โ„‹ ( ๐‘‡ โ€˜ ( ( ๐‘ฅ ยทโ„Ž ๐‘ฆ ) +โ„Ž ๐‘ง ) ) = ( ( ๐‘ฅ ยท ( ๐‘‡ โ€˜ ๐‘ฆ ) ) + ( ๐‘‡ โ€˜ ๐‘ง ) ) ) )
9 df-lnfn โŠข LinFn = { ๐‘ก โˆˆ ( โ„‚ โ†‘m โ„‹ ) โˆฃ โˆ€ ๐‘ฅ โˆˆ โ„‚ โˆ€ ๐‘ฆ โˆˆ โ„‹ โˆ€ ๐‘ง โˆˆ โ„‹ ( ๐‘ก โ€˜ ( ( ๐‘ฅ ยทโ„Ž ๐‘ฆ ) +โ„Ž ๐‘ง ) ) = ( ( ๐‘ฅ ยท ( ๐‘ก โ€˜ ๐‘ฆ ) ) + ( ๐‘ก โ€˜ ๐‘ง ) ) }
10 8 9 elrab2 โŠข ( ๐‘‡ โˆˆ LinFn โ†” ( ๐‘‡ โˆˆ ( โ„‚ โ†‘m โ„‹ ) โˆง โˆ€ ๐‘ฅ โˆˆ โ„‚ โˆ€ ๐‘ฆ โˆˆ โ„‹ โˆ€ ๐‘ง โˆˆ โ„‹ ( ๐‘‡ โ€˜ ( ( ๐‘ฅ ยทโ„Ž ๐‘ฆ ) +โ„Ž ๐‘ง ) ) = ( ( ๐‘ฅ ยท ( ๐‘‡ โ€˜ ๐‘ฆ ) ) + ( ๐‘‡ โ€˜ ๐‘ง ) ) ) )
11 cnex โŠข โ„‚ โˆˆ V
12 ax-hilex โŠข โ„‹ โˆˆ V
13 11 12 elmap โŠข ( ๐‘‡ โˆˆ ( โ„‚ โ†‘m โ„‹ ) โ†” ๐‘‡ : โ„‹ โŸถ โ„‚ )
14 13 anbi1i โŠข ( ( ๐‘‡ โˆˆ ( โ„‚ โ†‘m โ„‹ ) โˆง โˆ€ ๐‘ฅ โˆˆ โ„‚ โˆ€ ๐‘ฆ โˆˆ โ„‹ โˆ€ ๐‘ง โˆˆ โ„‹ ( ๐‘‡ โ€˜ ( ( ๐‘ฅ ยทโ„Ž ๐‘ฆ ) +โ„Ž ๐‘ง ) ) = ( ( ๐‘ฅ ยท ( ๐‘‡ โ€˜ ๐‘ฆ ) ) + ( ๐‘‡ โ€˜ ๐‘ง ) ) ) โ†” ( ๐‘‡ : โ„‹ โŸถ โ„‚ โˆง โˆ€ ๐‘ฅ โˆˆ โ„‚ โˆ€ ๐‘ฆ โˆˆ โ„‹ โˆ€ ๐‘ง โˆˆ โ„‹ ( ๐‘‡ โ€˜ ( ( ๐‘ฅ ยทโ„Ž ๐‘ฆ ) +โ„Ž ๐‘ง ) ) = ( ( ๐‘ฅ ยท ( ๐‘‡ โ€˜ ๐‘ฆ ) ) + ( ๐‘‡ โ€˜ ๐‘ง ) ) ) )
15 10 14 bitri โŠข ( ๐‘‡ โˆˆ LinFn โ†” ( ๐‘‡ : โ„‹ โŸถ โ„‚ โˆง โˆ€ ๐‘ฅ โˆˆ โ„‚ โˆ€ ๐‘ฆ โˆˆ โ„‹ โˆ€ ๐‘ง โˆˆ โ„‹ ( ๐‘‡ โ€˜ ( ( ๐‘ฅ ยทโ„Ž ๐‘ฆ ) +โ„Ž ๐‘ง ) ) = ( ( ๐‘ฅ ยท ( ๐‘‡ โ€˜ ๐‘ฆ ) ) + ( ๐‘‡ โ€˜ ๐‘ง ) ) ) )