Metamath Proof Explorer

Theorem adjlnop

Description: The adjoint of an operator is linear. Proposition 1 of AkhiezerGlazman p. 80. (Contributed by NM, 17-Jun-2006) (New usage is discouraged.)

Ref Expression
Assertion adjlnop ( ๐‘‡ โˆˆ dom adjโ„Ž โ†’ ( adjโ„Ž โ€˜ ๐‘‡ ) โˆˆ LinOp )

Proof

Step Hyp Ref Expression
1 dmadjrn โŠข ( ๐‘‡ โˆˆ dom adjโ„Ž โ†’ ( adjโ„Ž โ€˜ ๐‘‡ ) โˆˆ dom adjโ„Ž )
2 dmadjop โŠข ( ( adjโ„Ž โ€˜ ๐‘‡ ) โˆˆ dom adjโ„Ž โ†’ ( adjโ„Ž โ€˜ ๐‘‡ ) : โ„‹ โŸถ โ„‹ )
3 1 2 syl โŠข ( ๐‘‡ โˆˆ dom adjโ„Ž โ†’ ( adjโ„Ž โ€˜ ๐‘‡ ) : โ„‹ โŸถ โ„‹ )
4 simp2 โŠข ( ( ๐‘‡ โˆˆ dom adjโ„Ž โˆง ๐‘ค โˆˆ โ„‹ โˆง ( ( ๐‘ฅ โˆˆ โ„‚ โˆง ๐‘ฆ โˆˆ โ„‹ ) โˆง ๐‘ง โˆˆ โ„‹ ) ) โ†’ ๐‘ค โˆˆ โ„‹ )
5 adjcl โŠข ( ( ๐‘‡ โˆˆ dom adjโ„Ž โˆง ๐‘ฆ โˆˆ โ„‹ ) โ†’ ( ( adjโ„Ž โ€˜ ๐‘‡ ) โ€˜ ๐‘ฆ ) โˆˆ โ„‹ )
6 hvmulcl โŠข ( ( ๐‘ฅ โˆˆ โ„‚ โˆง ( ( adjโ„Ž โ€˜ ๐‘‡ ) โ€˜ ๐‘ฆ ) โˆˆ โ„‹ ) โ†’ ( ๐‘ฅ ยทโ„Ž ( ( adjโ„Ž โ€˜ ๐‘‡ ) โ€˜ ๐‘ฆ ) ) โˆˆ โ„‹ )
7 5 6 sylan2 โŠข ( ( ๐‘ฅ โˆˆ โ„‚ โˆง ( ๐‘‡ โˆˆ dom adjโ„Ž โˆง ๐‘ฆ โˆˆ โ„‹ ) ) โ†’ ( ๐‘ฅ ยทโ„Ž ( ( adjโ„Ž โ€˜ ๐‘‡ ) โ€˜ ๐‘ฆ ) ) โˆˆ โ„‹ )
8 7 an12s โŠข ( ( ๐‘‡ โˆˆ dom adjโ„Ž โˆง ( ๐‘ฅ โˆˆ โ„‚ โˆง ๐‘ฆ โˆˆ โ„‹ ) ) โ†’ ( ๐‘ฅ ยทโ„Ž ( ( adjโ„Ž โ€˜ ๐‘‡ ) โ€˜ ๐‘ฆ ) ) โˆˆ โ„‹ )
9 8 adantrr โŠข ( ( ๐‘‡ โˆˆ dom adjโ„Ž โˆง ( ( ๐‘ฅ โˆˆ โ„‚ โˆง ๐‘ฆ โˆˆ โ„‹ ) โˆง ๐‘ง โˆˆ โ„‹ ) ) โ†’ ( ๐‘ฅ ยทโ„Ž ( ( adjโ„Ž โ€˜ ๐‘‡ ) โ€˜ ๐‘ฆ ) ) โˆˆ โ„‹ )
10 9 3adant2 โŠข ( ( ๐‘‡ โˆˆ dom adjโ„Ž โˆง ๐‘ค โˆˆ โ„‹ โˆง ( ( ๐‘ฅ โˆˆ โ„‚ โˆง ๐‘ฆ โˆˆ โ„‹ ) โˆง ๐‘ง โˆˆ โ„‹ ) ) โ†’ ( ๐‘ฅ ยทโ„Ž ( ( adjโ„Ž โ€˜ ๐‘‡ ) โ€˜ ๐‘ฆ ) ) โˆˆ โ„‹ )
11 adjcl โŠข ( ( ๐‘‡ โˆˆ dom adjโ„Ž โˆง ๐‘ง โˆˆ โ„‹ ) โ†’ ( ( adjโ„Ž โ€˜ ๐‘‡ ) โ€˜ ๐‘ง ) โˆˆ โ„‹ )
12 11 adantrl โŠข ( ( ๐‘‡ โˆˆ dom adjโ„Ž โˆง ( ( ๐‘ฅ โˆˆ โ„‚ โˆง ๐‘ฆ โˆˆ โ„‹ ) โˆง ๐‘ง โˆˆ โ„‹ ) ) โ†’ ( ( adjโ„Ž โ€˜ ๐‘‡ ) โ€˜ ๐‘ง ) โˆˆ โ„‹ )
13 12 3adant2 โŠข ( ( ๐‘‡ โˆˆ dom adjโ„Ž โˆง ๐‘ค โˆˆ โ„‹ โˆง ( ( ๐‘ฅ โˆˆ โ„‚ โˆง ๐‘ฆ โˆˆ โ„‹ ) โˆง ๐‘ง โˆˆ โ„‹ ) ) โ†’ ( ( adjโ„Ž โ€˜ ๐‘‡ ) โ€˜ ๐‘ง ) โˆˆ โ„‹ )
14 his7 โŠข ( ( ๐‘ค โˆˆ โ„‹ โˆง ( ๐‘ฅ ยทโ„Ž ( ( adjโ„Ž โ€˜ ๐‘‡ ) โ€˜ ๐‘ฆ ) ) โˆˆ โ„‹ โˆง ( ( adjโ„Ž โ€˜ ๐‘‡ ) โ€˜ ๐‘ง ) โˆˆ โ„‹ ) โ†’ ( ๐‘ค ยทih ( ( ๐‘ฅ ยทโ„Ž ( ( adjโ„Ž โ€˜ ๐‘‡ ) โ€˜ ๐‘ฆ ) ) +โ„Ž ( ( adjโ„Ž โ€˜ ๐‘‡ ) โ€˜ ๐‘ง ) ) ) = ( ( ๐‘ค ยทih ( ๐‘ฅ ยทโ„Ž ( ( adjโ„Ž โ€˜ ๐‘‡ ) โ€˜ ๐‘ฆ ) ) ) + ( ๐‘ค ยทih ( ( adjโ„Ž โ€˜ ๐‘‡ ) โ€˜ ๐‘ง ) ) ) )
15 4 10 13 14 syl3anc โŠข ( ( ๐‘‡ โˆˆ dom adjโ„Ž โˆง ๐‘ค โˆˆ โ„‹ โˆง ( ( ๐‘ฅ โˆˆ โ„‚ โˆง ๐‘ฆ โˆˆ โ„‹ ) โˆง ๐‘ง โˆˆ โ„‹ ) ) โ†’ ( ๐‘ค ยทih ( ( ๐‘ฅ ยทโ„Ž ( ( adjโ„Ž โ€˜ ๐‘‡ ) โ€˜ ๐‘ฆ ) ) +โ„Ž ( ( adjโ„Ž โ€˜ ๐‘‡ ) โ€˜ ๐‘ง ) ) ) = ( ( ๐‘ค ยทih ( ๐‘ฅ ยทโ„Ž ( ( adjโ„Ž โ€˜ ๐‘‡ ) โ€˜ ๐‘ฆ ) ) ) + ( ๐‘ค ยทih ( ( adjโ„Ž โ€˜ ๐‘‡ ) โ€˜ ๐‘ง ) ) ) )
16 adj2 โŠข ( ( ๐‘‡ โˆˆ dom adjโ„Ž โˆง ๐‘ค โˆˆ โ„‹ โˆง ๐‘ฆ โˆˆ โ„‹ ) โ†’ ( ( ๐‘‡ โ€˜ ๐‘ค ) ยทih ๐‘ฆ ) = ( ๐‘ค ยทih ( ( adjโ„Ž โ€˜ ๐‘‡ ) โ€˜ ๐‘ฆ ) ) )
17 16 3adant3l โŠข ( ( ๐‘‡ โˆˆ dom adjโ„Ž โˆง ๐‘ค โˆˆ โ„‹ โˆง ( ๐‘ฅ โˆˆ โ„‚ โˆง ๐‘ฆ โˆˆ โ„‹ ) ) โ†’ ( ( ๐‘‡ โ€˜ ๐‘ค ) ยทih ๐‘ฆ ) = ( ๐‘ค ยทih ( ( adjโ„Ž โ€˜ ๐‘‡ ) โ€˜ ๐‘ฆ ) ) )
18 17 oveq2d โŠข ( ( ๐‘‡ โˆˆ dom adjโ„Ž โˆง ๐‘ค โˆˆ โ„‹ โˆง ( ๐‘ฅ โˆˆ โ„‚ โˆง ๐‘ฆ โˆˆ โ„‹ ) ) โ†’ ( ( โˆ— โ€˜ ๐‘ฅ ) ยท ( ( ๐‘‡ โ€˜ ๐‘ค ) ยทih ๐‘ฆ ) ) = ( ( โˆ— โ€˜ ๐‘ฅ ) ยท ( ๐‘ค ยทih ( ( adjโ„Ž โ€˜ ๐‘‡ ) โ€˜ ๐‘ฆ ) ) ) )
19 simp3l โŠข ( ( ๐‘‡ โˆˆ dom adjโ„Ž โˆง ๐‘ค โˆˆ โ„‹ โˆง ( ๐‘ฅ โˆˆ โ„‚ โˆง ๐‘ฆ โˆˆ โ„‹ ) ) โ†’ ๐‘ฅ โˆˆ โ„‚ )
20 dmadjop โŠข ( ๐‘‡ โˆˆ dom adjโ„Ž โ†’ ๐‘‡ : โ„‹ โŸถ โ„‹ )
21 20 ffvelcdmda โŠข ( ( ๐‘‡ โˆˆ dom adjโ„Ž โˆง ๐‘ค โˆˆ โ„‹ ) โ†’ ( ๐‘‡ โ€˜ ๐‘ค ) โˆˆ โ„‹ )
22 21 3adant3 โŠข ( ( ๐‘‡ โˆˆ dom adjโ„Ž โˆง ๐‘ค โˆˆ โ„‹ โˆง ( ๐‘ฅ โˆˆ โ„‚ โˆง ๐‘ฆ โˆˆ โ„‹ ) ) โ†’ ( ๐‘‡ โ€˜ ๐‘ค ) โˆˆ โ„‹ )
23 simp3r โŠข ( ( ๐‘‡ โˆˆ dom adjโ„Ž โˆง ๐‘ค โˆˆ โ„‹ โˆง ( ๐‘ฅ โˆˆ โ„‚ โˆง ๐‘ฆ โˆˆ โ„‹ ) ) โ†’ ๐‘ฆ โˆˆ โ„‹ )
24 his5 โŠข ( ( ๐‘ฅ โˆˆ โ„‚ โˆง ( ๐‘‡ โ€˜ ๐‘ค ) โˆˆ โ„‹ โˆง ๐‘ฆ โˆˆ โ„‹ ) โ†’ ( ( ๐‘‡ โ€˜ ๐‘ค ) ยทih ( ๐‘ฅ ยทโ„Ž ๐‘ฆ ) ) = ( ( โˆ— โ€˜ ๐‘ฅ ) ยท ( ( ๐‘‡ โ€˜ ๐‘ค ) ยทih ๐‘ฆ ) ) )
25 19 22 23 24 syl3anc โŠข ( ( ๐‘‡ โˆˆ dom adjโ„Ž โˆง ๐‘ค โˆˆ โ„‹ โˆง ( ๐‘ฅ โˆˆ โ„‚ โˆง ๐‘ฆ โˆˆ โ„‹ ) ) โ†’ ( ( ๐‘‡ โ€˜ ๐‘ค ) ยทih ( ๐‘ฅ ยทโ„Ž ๐‘ฆ ) ) = ( ( โˆ— โ€˜ ๐‘ฅ ) ยท ( ( ๐‘‡ โ€˜ ๐‘ค ) ยทih ๐‘ฆ ) ) )
26 simp2 โŠข ( ( ๐‘‡ โˆˆ dom adjโ„Ž โˆง ๐‘ค โˆˆ โ„‹ โˆง ( ๐‘ฅ โˆˆ โ„‚ โˆง ๐‘ฆ โˆˆ โ„‹ ) ) โ†’ ๐‘ค โˆˆ โ„‹ )
27 5 adantrl โŠข ( ( ๐‘‡ โˆˆ dom adjโ„Ž โˆง ( ๐‘ฅ โˆˆ โ„‚ โˆง ๐‘ฆ โˆˆ โ„‹ ) ) โ†’ ( ( adjโ„Ž โ€˜ ๐‘‡ ) โ€˜ ๐‘ฆ ) โˆˆ โ„‹ )
28 27 3adant2 โŠข ( ( ๐‘‡ โˆˆ dom adjโ„Ž โˆง ๐‘ค โˆˆ โ„‹ โˆง ( ๐‘ฅ โˆˆ โ„‚ โˆง ๐‘ฆ โˆˆ โ„‹ ) ) โ†’ ( ( adjโ„Ž โ€˜ ๐‘‡ ) โ€˜ ๐‘ฆ ) โˆˆ โ„‹ )
29 his5 โŠข ( ( ๐‘ฅ โˆˆ โ„‚ โˆง ๐‘ค โˆˆ โ„‹ โˆง ( ( adjโ„Ž โ€˜ ๐‘‡ ) โ€˜ ๐‘ฆ ) โˆˆ โ„‹ ) โ†’ ( ๐‘ค ยทih ( ๐‘ฅ ยทโ„Ž ( ( adjโ„Ž โ€˜ ๐‘‡ ) โ€˜ ๐‘ฆ ) ) ) = ( ( โˆ— โ€˜ ๐‘ฅ ) ยท ( ๐‘ค ยทih ( ( adjโ„Ž โ€˜ ๐‘‡ ) โ€˜ ๐‘ฆ ) ) ) )
30 19 26 28 29 syl3anc โŠข ( ( ๐‘‡ โˆˆ dom adjโ„Ž โˆง ๐‘ค โˆˆ โ„‹ โˆง ( ๐‘ฅ โˆˆ โ„‚ โˆง ๐‘ฆ โˆˆ โ„‹ ) ) โ†’ ( ๐‘ค ยทih ( ๐‘ฅ ยทโ„Ž ( ( adjโ„Ž โ€˜ ๐‘‡ ) โ€˜ ๐‘ฆ ) ) ) = ( ( โˆ— โ€˜ ๐‘ฅ ) ยท ( ๐‘ค ยทih ( ( adjโ„Ž โ€˜ ๐‘‡ ) โ€˜ ๐‘ฆ ) ) ) )
31 18 25 30 3eqtr4d โŠข ( ( ๐‘‡ โˆˆ dom adjโ„Ž โˆง ๐‘ค โˆˆ โ„‹ โˆง ( ๐‘ฅ โˆˆ โ„‚ โˆง ๐‘ฆ โˆˆ โ„‹ ) ) โ†’ ( ( ๐‘‡ โ€˜ ๐‘ค ) ยทih ( ๐‘ฅ ยทโ„Ž ๐‘ฆ ) ) = ( ๐‘ค ยทih ( ๐‘ฅ ยทโ„Ž ( ( adjโ„Ž โ€˜ ๐‘‡ ) โ€˜ ๐‘ฆ ) ) ) )
32 31 3adant3r โŠข ( ( ๐‘‡ โˆˆ dom adjโ„Ž โˆง ๐‘ค โˆˆ โ„‹ โˆง ( ( ๐‘ฅ โˆˆ โ„‚ โˆง ๐‘ฆ โˆˆ โ„‹ ) โˆง ๐‘ง โˆˆ โ„‹ ) ) โ†’ ( ( ๐‘‡ โ€˜ ๐‘ค ) ยทih ( ๐‘ฅ ยทโ„Ž ๐‘ฆ ) ) = ( ๐‘ค ยทih ( ๐‘ฅ ยทโ„Ž ( ( adjโ„Ž โ€˜ ๐‘‡ ) โ€˜ ๐‘ฆ ) ) ) )
33 adj2 โŠข ( ( ๐‘‡ โˆˆ dom adjโ„Ž โˆง ๐‘ค โˆˆ โ„‹ โˆง ๐‘ง โˆˆ โ„‹ ) โ†’ ( ( ๐‘‡ โ€˜ ๐‘ค ) ยทih ๐‘ง ) = ( ๐‘ค ยทih ( ( adjโ„Ž โ€˜ ๐‘‡ ) โ€˜ ๐‘ง ) ) )
34 33 3adant3l โŠข ( ( ๐‘‡ โˆˆ dom adjโ„Ž โˆง ๐‘ค โˆˆ โ„‹ โˆง ( ( ๐‘ฅ โˆˆ โ„‚ โˆง ๐‘ฆ โˆˆ โ„‹ ) โˆง ๐‘ง โˆˆ โ„‹ ) ) โ†’ ( ( ๐‘‡ โ€˜ ๐‘ค ) ยทih ๐‘ง ) = ( ๐‘ค ยทih ( ( adjโ„Ž โ€˜ ๐‘‡ ) โ€˜ ๐‘ง ) ) )
35 32 34 oveq12d โŠข ( ( ๐‘‡ โˆˆ dom adjโ„Ž โˆง ๐‘ค โˆˆ โ„‹ โˆง ( ( ๐‘ฅ โˆˆ โ„‚ โˆง ๐‘ฆ โˆˆ โ„‹ ) โˆง ๐‘ง โˆˆ โ„‹ ) ) โ†’ ( ( ( ๐‘‡ โ€˜ ๐‘ค ) ยทih ( ๐‘ฅ ยทโ„Ž ๐‘ฆ ) ) + ( ( ๐‘‡ โ€˜ ๐‘ค ) ยทih ๐‘ง ) ) = ( ( ๐‘ค ยทih ( ๐‘ฅ ยทโ„Ž ( ( adjโ„Ž โ€˜ ๐‘‡ ) โ€˜ ๐‘ฆ ) ) ) + ( ๐‘ค ยทih ( ( adjโ„Ž โ€˜ ๐‘‡ ) โ€˜ ๐‘ง ) ) ) )
36 21 3adant3 โŠข ( ( ๐‘‡ โˆˆ dom adjโ„Ž โˆง ๐‘ค โˆˆ โ„‹ โˆง ( ( ๐‘ฅ โˆˆ โ„‚ โˆง ๐‘ฆ โˆˆ โ„‹ ) โˆง ๐‘ง โˆˆ โ„‹ ) ) โ†’ ( ๐‘‡ โ€˜ ๐‘ค ) โˆˆ โ„‹ )
37 hvmulcl โŠข ( ( ๐‘ฅ โˆˆ โ„‚ โˆง ๐‘ฆ โˆˆ โ„‹ ) โ†’ ( ๐‘ฅ ยทโ„Ž ๐‘ฆ ) โˆˆ โ„‹ )
38 37 adantr โŠข ( ( ( ๐‘ฅ โˆˆ โ„‚ โˆง ๐‘ฆ โˆˆ โ„‹ ) โˆง ๐‘ง โˆˆ โ„‹ ) โ†’ ( ๐‘ฅ ยทโ„Ž ๐‘ฆ ) โˆˆ โ„‹ )
39 38 3ad2ant3 โŠข ( ( ๐‘‡ โˆˆ dom adjโ„Ž โˆง ๐‘ค โˆˆ โ„‹ โˆง ( ( ๐‘ฅ โˆˆ โ„‚ โˆง ๐‘ฆ โˆˆ โ„‹ ) โˆง ๐‘ง โˆˆ โ„‹ ) ) โ†’ ( ๐‘ฅ ยทโ„Ž ๐‘ฆ ) โˆˆ โ„‹ )
40 simp3r โŠข ( ( ๐‘‡ โˆˆ dom adjโ„Ž โˆง ๐‘ค โˆˆ โ„‹ โˆง ( ( ๐‘ฅ โˆˆ โ„‚ โˆง ๐‘ฆ โˆˆ โ„‹ ) โˆง ๐‘ง โˆˆ โ„‹ ) ) โ†’ ๐‘ง โˆˆ โ„‹ )
41 his7 โŠข ( ( ( ๐‘‡ โ€˜ ๐‘ค ) โˆˆ โ„‹ โˆง ( ๐‘ฅ ยทโ„Ž ๐‘ฆ ) โˆˆ โ„‹ โˆง ๐‘ง โˆˆ โ„‹ ) โ†’ ( ( ๐‘‡ โ€˜ ๐‘ค ) ยทih ( ( ๐‘ฅ ยทโ„Ž ๐‘ฆ ) +โ„Ž ๐‘ง ) ) = ( ( ( ๐‘‡ โ€˜ ๐‘ค ) ยทih ( ๐‘ฅ ยทโ„Ž ๐‘ฆ ) ) + ( ( ๐‘‡ โ€˜ ๐‘ค ) ยทih ๐‘ง ) ) )
42 36 39 40 41 syl3anc โŠข ( ( ๐‘‡ โˆˆ dom adjโ„Ž โˆง ๐‘ค โˆˆ โ„‹ โˆง ( ( ๐‘ฅ โˆˆ โ„‚ โˆง ๐‘ฆ โˆˆ โ„‹ ) โˆง ๐‘ง โˆˆ โ„‹ ) ) โ†’ ( ( ๐‘‡ โ€˜ ๐‘ค ) ยทih ( ( ๐‘ฅ ยทโ„Ž ๐‘ฆ ) +โ„Ž ๐‘ง ) ) = ( ( ( ๐‘‡ โ€˜ ๐‘ค ) ยทih ( ๐‘ฅ ยทโ„Ž ๐‘ฆ ) ) + ( ( ๐‘‡ โ€˜ ๐‘ค ) ยทih ๐‘ง ) ) )
43 hvaddcl โŠข ( ( ( ๐‘ฅ ยทโ„Ž ๐‘ฆ ) โˆˆ โ„‹ โˆง ๐‘ง โˆˆ โ„‹ ) โ†’ ( ( ๐‘ฅ ยทโ„Ž ๐‘ฆ ) +โ„Ž ๐‘ง ) โˆˆ โ„‹ )
44 37 43 sylan โŠข ( ( ( ๐‘ฅ โˆˆ โ„‚ โˆง ๐‘ฆ โˆˆ โ„‹ ) โˆง ๐‘ง โˆˆ โ„‹ ) โ†’ ( ( ๐‘ฅ ยทโ„Ž ๐‘ฆ ) +โ„Ž ๐‘ง ) โˆˆ โ„‹ )
45 adj2 โŠข ( ( ๐‘‡ โˆˆ dom adjโ„Ž โˆง ๐‘ค โˆˆ โ„‹ โˆง ( ( ๐‘ฅ ยทโ„Ž ๐‘ฆ ) +โ„Ž ๐‘ง ) โˆˆ โ„‹ ) โ†’ ( ( ๐‘‡ โ€˜ ๐‘ค ) ยทih ( ( ๐‘ฅ ยทโ„Ž ๐‘ฆ ) +โ„Ž ๐‘ง ) ) = ( ๐‘ค ยทih ( ( adjโ„Ž โ€˜ ๐‘‡ ) โ€˜ ( ( ๐‘ฅ ยทโ„Ž ๐‘ฆ ) +โ„Ž ๐‘ง ) ) ) )
46 44 45 syl3an3 โŠข ( ( ๐‘‡ โˆˆ dom adjโ„Ž โˆง ๐‘ค โˆˆ โ„‹ โˆง ( ( ๐‘ฅ โˆˆ โ„‚ โˆง ๐‘ฆ โˆˆ โ„‹ ) โˆง ๐‘ง โˆˆ โ„‹ ) ) โ†’ ( ( ๐‘‡ โ€˜ ๐‘ค ) ยทih ( ( ๐‘ฅ ยทโ„Ž ๐‘ฆ ) +โ„Ž ๐‘ง ) ) = ( ๐‘ค ยทih ( ( adjโ„Ž โ€˜ ๐‘‡ ) โ€˜ ( ( ๐‘ฅ ยทโ„Ž ๐‘ฆ ) +โ„Ž ๐‘ง ) ) ) )
47 42 46 eqtr3d โŠข ( ( ๐‘‡ โˆˆ dom adjโ„Ž โˆง ๐‘ค โˆˆ โ„‹ โˆง ( ( ๐‘ฅ โˆˆ โ„‚ โˆง ๐‘ฆ โˆˆ โ„‹ ) โˆง ๐‘ง โˆˆ โ„‹ ) ) โ†’ ( ( ( ๐‘‡ โ€˜ ๐‘ค ) ยทih ( ๐‘ฅ ยทโ„Ž ๐‘ฆ ) ) + ( ( ๐‘‡ โ€˜ ๐‘ค ) ยทih ๐‘ง ) ) = ( ๐‘ค ยทih ( ( adjโ„Ž โ€˜ ๐‘‡ ) โ€˜ ( ( ๐‘ฅ ยทโ„Ž ๐‘ฆ ) +โ„Ž ๐‘ง ) ) ) )
48 15 35 47 3eqtr2rd โŠข ( ( ๐‘‡ โˆˆ dom adjโ„Ž โˆง ๐‘ค โˆˆ โ„‹ โˆง ( ( ๐‘ฅ โˆˆ โ„‚ โˆง ๐‘ฆ โˆˆ โ„‹ ) โˆง ๐‘ง โˆˆ โ„‹ ) ) โ†’ ( ๐‘ค ยทih ( ( adjโ„Ž โ€˜ ๐‘‡ ) โ€˜ ( ( ๐‘ฅ ยทโ„Ž ๐‘ฆ ) +โ„Ž ๐‘ง ) ) ) = ( ๐‘ค ยทih ( ( ๐‘ฅ ยทโ„Ž ( ( adjโ„Ž โ€˜ ๐‘‡ ) โ€˜ ๐‘ฆ ) ) +โ„Ž ( ( adjโ„Ž โ€˜ ๐‘‡ ) โ€˜ ๐‘ง ) ) ) )
49 48 3com23 โŠข ( ( ๐‘‡ โˆˆ dom adjโ„Ž โˆง ( ( ๐‘ฅ โˆˆ โ„‚ โˆง ๐‘ฆ โˆˆ โ„‹ ) โˆง ๐‘ง โˆˆ โ„‹ ) โˆง ๐‘ค โˆˆ โ„‹ ) โ†’ ( ๐‘ค ยทih ( ( adjโ„Ž โ€˜ ๐‘‡ ) โ€˜ ( ( ๐‘ฅ ยทโ„Ž ๐‘ฆ ) +โ„Ž ๐‘ง ) ) ) = ( ๐‘ค ยทih ( ( ๐‘ฅ ยทโ„Ž ( ( adjโ„Ž โ€˜ ๐‘‡ ) โ€˜ ๐‘ฆ ) ) +โ„Ž ( ( adjโ„Ž โ€˜ ๐‘‡ ) โ€˜ ๐‘ง ) ) ) )
50 49 3expa โŠข ( ( ( ๐‘‡ โˆˆ dom adjโ„Ž โˆง ( ( ๐‘ฅ โˆˆ โ„‚ โˆง ๐‘ฆ โˆˆ โ„‹ ) โˆง ๐‘ง โˆˆ โ„‹ ) ) โˆง ๐‘ค โˆˆ โ„‹ ) โ†’ ( ๐‘ค ยทih ( ( adjโ„Ž โ€˜ ๐‘‡ ) โ€˜ ( ( ๐‘ฅ ยทโ„Ž ๐‘ฆ ) +โ„Ž ๐‘ง ) ) ) = ( ๐‘ค ยทih ( ( ๐‘ฅ ยทโ„Ž ( ( adjโ„Ž โ€˜ ๐‘‡ ) โ€˜ ๐‘ฆ ) ) +โ„Ž ( ( adjโ„Ž โ€˜ ๐‘‡ ) โ€˜ ๐‘ง ) ) ) )
51 50 ralrimiva โŠข ( ( ๐‘‡ โˆˆ dom adjโ„Ž โˆง ( ( ๐‘ฅ โˆˆ โ„‚ โˆง ๐‘ฆ โˆˆ โ„‹ ) โˆง ๐‘ง โˆˆ โ„‹ ) ) โ†’ โˆ€ ๐‘ค โˆˆ โ„‹ ( ๐‘ค ยทih ( ( adjโ„Ž โ€˜ ๐‘‡ ) โ€˜ ( ( ๐‘ฅ ยทโ„Ž ๐‘ฆ ) +โ„Ž ๐‘ง ) ) ) = ( ๐‘ค ยทih ( ( ๐‘ฅ ยทโ„Ž ( ( adjโ„Ž โ€˜ ๐‘‡ ) โ€˜ ๐‘ฆ ) ) +โ„Ž ( ( adjโ„Ž โ€˜ ๐‘‡ ) โ€˜ ๐‘ง ) ) ) )
52 adjcl โŠข ( ( ๐‘‡ โˆˆ dom adjโ„Ž โˆง ( ( ๐‘ฅ ยทโ„Ž ๐‘ฆ ) +โ„Ž ๐‘ง ) โˆˆ โ„‹ ) โ†’ ( ( adjโ„Ž โ€˜ ๐‘‡ ) โ€˜ ( ( ๐‘ฅ ยทโ„Ž ๐‘ฆ ) +โ„Ž ๐‘ง ) ) โˆˆ โ„‹ )
53 44 52 sylan2 โŠข ( ( ๐‘‡ โˆˆ dom adjโ„Ž โˆง ( ( ๐‘ฅ โˆˆ โ„‚ โˆง ๐‘ฆ โˆˆ โ„‹ ) โˆง ๐‘ง โˆˆ โ„‹ ) ) โ†’ ( ( adjโ„Ž โ€˜ ๐‘‡ ) โ€˜ ( ( ๐‘ฅ ยทโ„Ž ๐‘ฆ ) +โ„Ž ๐‘ง ) ) โˆˆ โ„‹ )
54 hvaddcl โŠข ( ( ( ๐‘ฅ ยทโ„Ž ( ( adjโ„Ž โ€˜ ๐‘‡ ) โ€˜ ๐‘ฆ ) ) โˆˆ โ„‹ โˆง ( ( adjโ„Ž โ€˜ ๐‘‡ ) โ€˜ ๐‘ง ) โˆˆ โ„‹ ) โ†’ ( ( ๐‘ฅ ยทโ„Ž ( ( adjโ„Ž โ€˜ ๐‘‡ ) โ€˜ ๐‘ฆ ) ) +โ„Ž ( ( adjโ„Ž โ€˜ ๐‘‡ ) โ€˜ ๐‘ง ) ) โˆˆ โ„‹ )
55 8 11 54 syl2an โŠข ( ( ( ๐‘‡ โˆˆ dom adjโ„Ž โˆง ( ๐‘ฅ โˆˆ โ„‚ โˆง ๐‘ฆ โˆˆ โ„‹ ) ) โˆง ( ๐‘‡ โˆˆ dom adjโ„Ž โˆง ๐‘ง โˆˆ โ„‹ ) ) โ†’ ( ( ๐‘ฅ ยทโ„Ž ( ( adjโ„Ž โ€˜ ๐‘‡ ) โ€˜ ๐‘ฆ ) ) +โ„Ž ( ( adjโ„Ž โ€˜ ๐‘‡ ) โ€˜ ๐‘ง ) ) โˆˆ โ„‹ )
56 55 anandis โŠข ( ( ๐‘‡ โˆˆ dom adjโ„Ž โˆง ( ( ๐‘ฅ โˆˆ โ„‚ โˆง ๐‘ฆ โˆˆ โ„‹ ) โˆง ๐‘ง โˆˆ โ„‹ ) ) โ†’ ( ( ๐‘ฅ ยทโ„Ž ( ( adjโ„Ž โ€˜ ๐‘‡ ) โ€˜ ๐‘ฆ ) ) +โ„Ž ( ( adjโ„Ž โ€˜ ๐‘‡ ) โ€˜ ๐‘ง ) ) โˆˆ โ„‹ )
57 hial2eq2 โŠข ( ( ( ( adjโ„Ž โ€˜ ๐‘‡ ) โ€˜ ( ( ๐‘ฅ ยทโ„Ž ๐‘ฆ ) +โ„Ž ๐‘ง ) ) โˆˆ โ„‹ โˆง ( ( ๐‘ฅ ยทโ„Ž ( ( adjโ„Ž โ€˜ ๐‘‡ ) โ€˜ ๐‘ฆ ) ) +โ„Ž ( ( adjโ„Ž โ€˜ ๐‘‡ ) โ€˜ ๐‘ง ) ) โˆˆ โ„‹ ) โ†’ ( โˆ€ ๐‘ค โˆˆ โ„‹ ( ๐‘ค ยทih ( ( adjโ„Ž โ€˜ ๐‘‡ ) โ€˜ ( ( ๐‘ฅ ยทโ„Ž ๐‘ฆ ) +โ„Ž ๐‘ง ) ) ) = ( ๐‘ค ยทih ( ( ๐‘ฅ ยทโ„Ž ( ( adjโ„Ž โ€˜ ๐‘‡ ) โ€˜ ๐‘ฆ ) ) +โ„Ž ( ( adjโ„Ž โ€˜ ๐‘‡ ) โ€˜ ๐‘ง ) ) ) โ†” ( ( adjโ„Ž โ€˜ ๐‘‡ ) โ€˜ ( ( ๐‘ฅ ยทโ„Ž ๐‘ฆ ) +โ„Ž ๐‘ง ) ) = ( ( ๐‘ฅ ยทโ„Ž ( ( adjโ„Ž โ€˜ ๐‘‡ ) โ€˜ ๐‘ฆ ) ) +โ„Ž ( ( adjโ„Ž โ€˜ ๐‘‡ ) โ€˜ ๐‘ง ) ) ) )
58 53 56 57 syl2anc โŠข ( ( ๐‘‡ โˆˆ dom adjโ„Ž โˆง ( ( ๐‘ฅ โˆˆ โ„‚ โˆง ๐‘ฆ โˆˆ โ„‹ ) โˆง ๐‘ง โˆˆ โ„‹ ) ) โ†’ ( โˆ€ ๐‘ค โˆˆ โ„‹ ( ๐‘ค ยทih ( ( adjโ„Ž โ€˜ ๐‘‡ ) โ€˜ ( ( ๐‘ฅ ยทโ„Ž ๐‘ฆ ) +โ„Ž ๐‘ง ) ) ) = ( ๐‘ค ยทih ( ( ๐‘ฅ ยทโ„Ž ( ( adjโ„Ž โ€˜ ๐‘‡ ) โ€˜ ๐‘ฆ ) ) +โ„Ž ( ( adjโ„Ž โ€˜ ๐‘‡ ) โ€˜ ๐‘ง ) ) ) โ†” ( ( adjโ„Ž โ€˜ ๐‘‡ ) โ€˜ ( ( ๐‘ฅ ยทโ„Ž ๐‘ฆ ) +โ„Ž ๐‘ง ) ) = ( ( ๐‘ฅ ยทโ„Ž ( ( adjโ„Ž โ€˜ ๐‘‡ ) โ€˜ ๐‘ฆ ) ) +โ„Ž ( ( adjโ„Ž โ€˜ ๐‘‡ ) โ€˜ ๐‘ง ) ) ) )
59 51 58 mpbid โŠข ( ( ๐‘‡ โˆˆ dom adjโ„Ž โˆง ( ( ๐‘ฅ โˆˆ โ„‚ โˆง ๐‘ฆ โˆˆ โ„‹ ) โˆง ๐‘ง โˆˆ โ„‹ ) ) โ†’ ( ( adjโ„Ž โ€˜ ๐‘‡ ) โ€˜ ( ( ๐‘ฅ ยทโ„Ž ๐‘ฆ ) +โ„Ž ๐‘ง ) ) = ( ( ๐‘ฅ ยทโ„Ž ( ( adjโ„Ž โ€˜ ๐‘‡ ) โ€˜ ๐‘ฆ ) ) +โ„Ž ( ( adjโ„Ž โ€˜ ๐‘‡ ) โ€˜ ๐‘ง ) ) )
60 59 exp32 โŠข ( ๐‘‡ โˆˆ dom adjโ„Ž โ†’ ( ( ๐‘ฅ โˆˆ โ„‚ โˆง ๐‘ฆ โˆˆ โ„‹ ) โ†’ ( ๐‘ง โˆˆ โ„‹ โ†’ ( ( adjโ„Ž โ€˜ ๐‘‡ ) โ€˜ ( ( ๐‘ฅ ยทโ„Ž ๐‘ฆ ) +โ„Ž ๐‘ง ) ) = ( ( ๐‘ฅ ยทโ„Ž ( ( adjโ„Ž โ€˜ ๐‘‡ ) โ€˜ ๐‘ฆ ) ) +โ„Ž ( ( adjโ„Ž โ€˜ ๐‘‡ ) โ€˜ ๐‘ง ) ) ) ) )
61 60 ralrimdv โŠข ( ๐‘‡ โˆˆ dom adjโ„Ž โ†’ ( ( ๐‘ฅ โˆˆ โ„‚ โˆง ๐‘ฆ โˆˆ โ„‹ ) โ†’ โˆ€ ๐‘ง โˆˆ โ„‹ ( ( adjโ„Ž โ€˜ ๐‘‡ ) โ€˜ ( ( ๐‘ฅ ยทโ„Ž ๐‘ฆ ) +โ„Ž ๐‘ง ) ) = ( ( ๐‘ฅ ยทโ„Ž ( ( adjโ„Ž โ€˜ ๐‘‡ ) โ€˜ ๐‘ฆ ) ) +โ„Ž ( ( adjโ„Ž โ€˜ ๐‘‡ ) โ€˜ ๐‘ง ) ) ) )
62 61 ralrimivv โŠข ( ๐‘‡ โˆˆ dom adjโ„Ž โ†’ โˆ€ ๐‘ฅ โˆˆ โ„‚ โˆ€ ๐‘ฆ โˆˆ โ„‹ โˆ€ ๐‘ง โˆˆ โ„‹ ( ( adjโ„Ž โ€˜ ๐‘‡ ) โ€˜ ( ( ๐‘ฅ ยทโ„Ž ๐‘ฆ ) +โ„Ž ๐‘ง ) ) = ( ( ๐‘ฅ ยทโ„Ž ( ( adjโ„Ž โ€˜ ๐‘‡ ) โ€˜ ๐‘ฆ ) ) +โ„Ž ( ( adjโ„Ž โ€˜ ๐‘‡ ) โ€˜ ๐‘ง ) ) )
63 ellnop โŠข ( ( adjโ„Ž โ€˜ ๐‘‡ ) โˆˆ LinOp โ†” ( ( adjโ„Ž โ€˜ ๐‘‡ ) : โ„‹ โŸถ โ„‹ โˆง โˆ€ ๐‘ฅ โˆˆ โ„‚ โˆ€ ๐‘ฆ โˆˆ โ„‹ โˆ€ ๐‘ง โˆˆ โ„‹ ( ( adjโ„Ž โ€˜ ๐‘‡ ) โ€˜ ( ( ๐‘ฅ ยทโ„Ž ๐‘ฆ ) +โ„Ž ๐‘ง ) ) = ( ( ๐‘ฅ ยทโ„Ž ( ( adjโ„Ž โ€˜ ๐‘‡ ) โ€˜ ๐‘ฆ ) ) +โ„Ž ( ( adjโ„Ž โ€˜ ๐‘‡ ) โ€˜ ๐‘ง ) ) ) )
64 3 62 63 sylanbrc โŠข ( ๐‘‡ โˆˆ dom adjโ„Ž โ†’ ( adjโ„Ž โ€˜ ๐‘‡ ) โˆˆ LinOp )