Metamath Proof Explorer

Theorem unoplin

Description: A unitary operator is linear. Theorem in AkhiezerGlazman p. 72. (Contributed by NM, 22-Jan-2006) (New usage is discouraged.)

Ref Expression
Assertion unoplin ( ๐‘‡ โˆˆ UniOp โ†’ ๐‘‡ โˆˆ LinOp )

Proof

Step Hyp Ref Expression
1 unopf1o โŠข ( ๐‘‡ โˆˆ UniOp โ†’ ๐‘‡ : โ„‹ โ€“1-1-ontoโ†’ โ„‹ )
2 f1of โŠข ( ๐‘‡ : โ„‹ โ€“1-1-ontoโ†’ โ„‹ โ†’ ๐‘‡ : โ„‹ โŸถ โ„‹ )
3 1 2 syl โŠข ( ๐‘‡ โˆˆ UniOp โ†’ ๐‘‡ : โ„‹ โŸถ โ„‹ )
4 simplll โŠข ( ( ( ( ๐‘‡ โˆˆ UniOp โˆง ( ๐‘ฅ โˆˆ โ„‚ โˆง ๐‘ฆ โˆˆ โ„‹ ) ) โˆง ๐‘ง โˆˆ โ„‹ ) โˆง ๐‘ค โˆˆ โ„‹ ) โ†’ ๐‘‡ โˆˆ UniOp )
5 hvmulcl โŠข ( ( ๐‘ฅ โˆˆ โ„‚ โˆง ๐‘ฆ โˆˆ โ„‹ ) โ†’ ( ๐‘ฅ ยทโ„Ž ๐‘ฆ ) โˆˆ โ„‹ )
6 hvaddcl โŠข ( ( ( ๐‘ฅ ยทโ„Ž ๐‘ฆ ) โˆˆ โ„‹ โˆง ๐‘ง โˆˆ โ„‹ ) โ†’ ( ( ๐‘ฅ ยทโ„Ž ๐‘ฆ ) +โ„Ž ๐‘ง ) โˆˆ โ„‹ )
7 5 6 sylan โŠข ( ( ( ๐‘ฅ โˆˆ โ„‚ โˆง ๐‘ฆ โˆˆ โ„‹ ) โˆง ๐‘ง โˆˆ โ„‹ ) โ†’ ( ( ๐‘ฅ ยทโ„Ž ๐‘ฆ ) +โ„Ž ๐‘ง ) โˆˆ โ„‹ )
8 7 adantll โŠข ( ( ( ๐‘‡ โˆˆ UniOp โˆง ( ๐‘ฅ โˆˆ โ„‚ โˆง ๐‘ฆ โˆˆ โ„‹ ) ) โˆง ๐‘ง โˆˆ โ„‹ ) โ†’ ( ( ๐‘ฅ ยทโ„Ž ๐‘ฆ ) +โ„Ž ๐‘ง ) โˆˆ โ„‹ )
9 8 adantr โŠข ( ( ( ( ๐‘‡ โˆˆ UniOp โˆง ( ๐‘ฅ โˆˆ โ„‚ โˆง ๐‘ฆ โˆˆ โ„‹ ) ) โˆง ๐‘ง โˆˆ โ„‹ ) โˆง ๐‘ค โˆˆ โ„‹ ) โ†’ ( ( ๐‘ฅ ยทโ„Ž ๐‘ฆ ) +โ„Ž ๐‘ง ) โˆˆ โ„‹ )
10 simpr โŠข ( ( ( ( ๐‘‡ โˆˆ UniOp โˆง ( ๐‘ฅ โˆˆ โ„‚ โˆง ๐‘ฆ โˆˆ โ„‹ ) ) โˆง ๐‘ง โˆˆ โ„‹ ) โˆง ๐‘ค โˆˆ โ„‹ ) โ†’ ๐‘ค โˆˆ โ„‹ )
11 unopadj โŠข ( ( ๐‘‡ โˆˆ UniOp โˆง ( ( ๐‘ฅ ยทโ„Ž ๐‘ฆ ) +โ„Ž ๐‘ง ) โˆˆ โ„‹ โˆง ๐‘ค โˆˆ โ„‹ ) โ†’ ( ( ๐‘‡ โ€˜ ( ( ๐‘ฅ ยทโ„Ž ๐‘ฆ ) +โ„Ž ๐‘ง ) ) ยทih ๐‘ค ) = ( ( ( ๐‘ฅ ยทโ„Ž ๐‘ฆ ) +โ„Ž ๐‘ง ) ยทih ( โ—ก ๐‘‡ โ€˜ ๐‘ค ) ) )
12 4 9 10 11 syl3anc โŠข ( ( ( ( ๐‘‡ โˆˆ UniOp โˆง ( ๐‘ฅ โˆˆ โ„‚ โˆง ๐‘ฆ โˆˆ โ„‹ ) ) โˆง ๐‘ง โˆˆ โ„‹ ) โˆง ๐‘ค โˆˆ โ„‹ ) โ†’ ( ( ๐‘‡ โ€˜ ( ( ๐‘ฅ ยทโ„Ž ๐‘ฆ ) +โ„Ž ๐‘ง ) ) ยทih ๐‘ค ) = ( ( ( ๐‘ฅ ยทโ„Ž ๐‘ฆ ) +โ„Ž ๐‘ง ) ยทih ( โ—ก ๐‘‡ โ€˜ ๐‘ค ) ) )
13 simprl โŠข ( ( ๐‘‡ โˆˆ UniOp โˆง ( ๐‘ฅ โˆˆ โ„‚ โˆง ๐‘ฆ โˆˆ โ„‹ ) ) โ†’ ๐‘ฅ โˆˆ โ„‚ )
14 13 ad2antrr โŠข ( ( ( ( ๐‘‡ โˆˆ UniOp โˆง ( ๐‘ฅ โˆˆ โ„‚ โˆง ๐‘ฆ โˆˆ โ„‹ ) ) โˆง ๐‘ง โˆˆ โ„‹ ) โˆง ๐‘ค โˆˆ โ„‹ ) โ†’ ๐‘ฅ โˆˆ โ„‚ )
15 simprr โŠข ( ( ๐‘‡ โˆˆ UniOp โˆง ( ๐‘ฅ โˆˆ โ„‚ โˆง ๐‘ฆ โˆˆ โ„‹ ) ) โ†’ ๐‘ฆ โˆˆ โ„‹ )
16 15 ad2antrr โŠข ( ( ( ( ๐‘‡ โˆˆ UniOp โˆง ( ๐‘ฅ โˆˆ โ„‚ โˆง ๐‘ฆ โˆˆ โ„‹ ) ) โˆง ๐‘ง โˆˆ โ„‹ ) โˆง ๐‘ค โˆˆ โ„‹ ) โ†’ ๐‘ฆ โˆˆ โ„‹ )
17 simplr โŠข ( ( ( ( ๐‘‡ โˆˆ UniOp โˆง ( ๐‘ฅ โˆˆ โ„‚ โˆง ๐‘ฆ โˆˆ โ„‹ ) ) โˆง ๐‘ง โˆˆ โ„‹ ) โˆง ๐‘ค โˆˆ โ„‹ ) โ†’ ๐‘ง โˆˆ โ„‹ )
18 cnvunop โŠข ( ๐‘‡ โˆˆ UniOp โ†’ โ—ก ๐‘‡ โˆˆ UniOp )
19 unopf1o โŠข ( โ—ก ๐‘‡ โˆˆ UniOp โ†’ โ—ก ๐‘‡ : โ„‹ โ€“1-1-ontoโ†’ โ„‹ )
20 f1of โŠข ( โ—ก ๐‘‡ : โ„‹ โ€“1-1-ontoโ†’ โ„‹ โ†’ โ—ก ๐‘‡ : โ„‹ โŸถ โ„‹ )
21 18 19 20 3syl โŠข ( ๐‘‡ โˆˆ UniOp โ†’ โ—ก ๐‘‡ : โ„‹ โŸถ โ„‹ )
22 21 ffvelcdmda โŠข ( ( ๐‘‡ โˆˆ UniOp โˆง ๐‘ค โˆˆ โ„‹ ) โ†’ ( โ—ก ๐‘‡ โ€˜ ๐‘ค ) โˆˆ โ„‹ )
23 22 adantlr โŠข ( ( ( ๐‘‡ โˆˆ UniOp โˆง ๐‘ง โˆˆ โ„‹ ) โˆง ๐‘ค โˆˆ โ„‹ ) โ†’ ( โ—ก ๐‘‡ โ€˜ ๐‘ค ) โˆˆ โ„‹ )
24 23 adantllr โŠข ( ( ( ( ๐‘‡ โˆˆ UniOp โˆง ( ๐‘ฅ โˆˆ โ„‚ โˆง ๐‘ฆ โˆˆ โ„‹ ) ) โˆง ๐‘ง โˆˆ โ„‹ ) โˆง ๐‘ค โˆˆ โ„‹ ) โ†’ ( โ—ก ๐‘‡ โ€˜ ๐‘ค ) โˆˆ โ„‹ )
25 hiassdi โŠข ( ( ( ๐‘ฅ โˆˆ โ„‚ โˆง ๐‘ฆ โˆˆ โ„‹ ) โˆง ( ๐‘ง โˆˆ โ„‹ โˆง ( โ—ก ๐‘‡ โ€˜ ๐‘ค ) โˆˆ โ„‹ ) ) โ†’ ( ( ( ๐‘ฅ ยทโ„Ž ๐‘ฆ ) +โ„Ž ๐‘ง ) ยทih ( โ—ก ๐‘‡ โ€˜ ๐‘ค ) ) = ( ( ๐‘ฅ ยท ( ๐‘ฆ ยทih ( โ—ก ๐‘‡ โ€˜ ๐‘ค ) ) ) + ( ๐‘ง ยทih ( โ—ก ๐‘‡ โ€˜ ๐‘ค ) ) ) )
26 14 16 17 24 25 syl22anc โŠข ( ( ( ( ๐‘‡ โˆˆ UniOp โˆง ( ๐‘ฅ โˆˆ โ„‚ โˆง ๐‘ฆ โˆˆ โ„‹ ) ) โˆง ๐‘ง โˆˆ โ„‹ ) โˆง ๐‘ค โˆˆ โ„‹ ) โ†’ ( ( ( ๐‘ฅ ยทโ„Ž ๐‘ฆ ) +โ„Ž ๐‘ง ) ยทih ( โ—ก ๐‘‡ โ€˜ ๐‘ค ) ) = ( ( ๐‘ฅ ยท ( ๐‘ฆ ยทih ( โ—ก ๐‘‡ โ€˜ ๐‘ค ) ) ) + ( ๐‘ง ยทih ( โ—ก ๐‘‡ โ€˜ ๐‘ค ) ) ) )
27 3 ffvelcdmda โŠข ( ( ๐‘‡ โˆˆ UniOp โˆง ๐‘ฆ โˆˆ โ„‹ ) โ†’ ( ๐‘‡ โ€˜ ๐‘ฆ ) โˆˆ โ„‹ )
28 27 adantrl โŠข ( ( ๐‘‡ โˆˆ UniOp โˆง ( ๐‘ฅ โˆˆ โ„‚ โˆง ๐‘ฆ โˆˆ โ„‹ ) ) โ†’ ( ๐‘‡ โ€˜ ๐‘ฆ ) โˆˆ โ„‹ )
29 28 ad2antrr โŠข ( ( ( ( ๐‘‡ โˆˆ UniOp โˆง ( ๐‘ฅ โˆˆ โ„‚ โˆง ๐‘ฆ โˆˆ โ„‹ ) ) โˆง ๐‘ง โˆˆ โ„‹ ) โˆง ๐‘ค โˆˆ โ„‹ ) โ†’ ( ๐‘‡ โ€˜ ๐‘ฆ ) โˆˆ โ„‹ )
30 3 ffvelcdmda โŠข ( ( ๐‘‡ โˆˆ UniOp โˆง ๐‘ง โˆˆ โ„‹ ) โ†’ ( ๐‘‡ โ€˜ ๐‘ง ) โˆˆ โ„‹ )
31 30 adantr โŠข ( ( ( ๐‘‡ โˆˆ UniOp โˆง ๐‘ง โˆˆ โ„‹ ) โˆง ๐‘ค โˆˆ โ„‹ ) โ†’ ( ๐‘‡ โ€˜ ๐‘ง ) โˆˆ โ„‹ )
32 31 adantllr โŠข ( ( ( ( ๐‘‡ โˆˆ UniOp โˆง ( ๐‘ฅ โˆˆ โ„‚ โˆง ๐‘ฆ โˆˆ โ„‹ ) ) โˆง ๐‘ง โˆˆ โ„‹ ) โˆง ๐‘ค โˆˆ โ„‹ ) โ†’ ( ๐‘‡ โ€˜ ๐‘ง ) โˆˆ โ„‹ )
33 hiassdi โŠข ( ( ( ๐‘ฅ โˆˆ โ„‚ โˆง ( ๐‘‡ โ€˜ ๐‘ฆ ) โˆˆ โ„‹ ) โˆง ( ( ๐‘‡ โ€˜ ๐‘ง ) โˆˆ โ„‹ โˆง ๐‘ค โˆˆ โ„‹ ) ) โ†’ ( ( ( ๐‘ฅ ยทโ„Ž ( ๐‘‡ โ€˜ ๐‘ฆ ) ) +โ„Ž ( ๐‘‡ โ€˜ ๐‘ง ) ) ยทih ๐‘ค ) = ( ( ๐‘ฅ ยท ( ( ๐‘‡ โ€˜ ๐‘ฆ ) ยทih ๐‘ค ) ) + ( ( ๐‘‡ โ€˜ ๐‘ง ) ยทih ๐‘ค ) ) )
34 14 29 32 10 33 syl22anc โŠข ( ( ( ( ๐‘‡ โˆˆ UniOp โˆง ( ๐‘ฅ โˆˆ โ„‚ โˆง ๐‘ฆ โˆˆ โ„‹ ) ) โˆง ๐‘ง โˆˆ โ„‹ ) โˆง ๐‘ค โˆˆ โ„‹ ) โ†’ ( ( ( ๐‘ฅ ยทโ„Ž ( ๐‘‡ โ€˜ ๐‘ฆ ) ) +โ„Ž ( ๐‘‡ โ€˜ ๐‘ง ) ) ยทih ๐‘ค ) = ( ( ๐‘ฅ ยท ( ( ๐‘‡ โ€˜ ๐‘ฆ ) ยทih ๐‘ค ) ) + ( ( ๐‘‡ โ€˜ ๐‘ง ) ยทih ๐‘ค ) ) )
35 unopadj โŠข ( ( ๐‘‡ โˆˆ UniOp โˆง ๐‘ฆ โˆˆ โ„‹ โˆง ๐‘ค โˆˆ โ„‹ ) โ†’ ( ( ๐‘‡ โ€˜ ๐‘ฆ ) ยทih ๐‘ค ) = ( ๐‘ฆ ยทih ( โ—ก ๐‘‡ โ€˜ ๐‘ค ) ) )
36 35 3expa โŠข ( ( ( ๐‘‡ โˆˆ UniOp โˆง ๐‘ฆ โˆˆ โ„‹ ) โˆง ๐‘ค โˆˆ โ„‹ ) โ†’ ( ( ๐‘‡ โ€˜ ๐‘ฆ ) ยทih ๐‘ค ) = ( ๐‘ฆ ยทih ( โ—ก ๐‘‡ โ€˜ ๐‘ค ) ) )
37 36 oveq2d โŠข ( ( ( ๐‘‡ โˆˆ UniOp โˆง ๐‘ฆ โˆˆ โ„‹ ) โˆง ๐‘ค โˆˆ โ„‹ ) โ†’ ( ๐‘ฅ ยท ( ( ๐‘‡ โ€˜ ๐‘ฆ ) ยทih ๐‘ค ) ) = ( ๐‘ฅ ยท ( ๐‘ฆ ยทih ( โ—ก ๐‘‡ โ€˜ ๐‘ค ) ) ) )
38 37 adantlrl โŠข ( ( ( ๐‘‡ โˆˆ UniOp โˆง ( ๐‘ฅ โˆˆ โ„‚ โˆง ๐‘ฆ โˆˆ โ„‹ ) ) โˆง ๐‘ค โˆˆ โ„‹ ) โ†’ ( ๐‘ฅ ยท ( ( ๐‘‡ โ€˜ ๐‘ฆ ) ยทih ๐‘ค ) ) = ( ๐‘ฅ ยท ( ๐‘ฆ ยทih ( โ—ก ๐‘‡ โ€˜ ๐‘ค ) ) ) )
39 38 adantlr โŠข ( ( ( ( ๐‘‡ โˆˆ UniOp โˆง ( ๐‘ฅ โˆˆ โ„‚ โˆง ๐‘ฆ โˆˆ โ„‹ ) ) โˆง ๐‘ง โˆˆ โ„‹ ) โˆง ๐‘ค โˆˆ โ„‹ ) โ†’ ( ๐‘ฅ ยท ( ( ๐‘‡ โ€˜ ๐‘ฆ ) ยทih ๐‘ค ) ) = ( ๐‘ฅ ยท ( ๐‘ฆ ยทih ( โ—ก ๐‘‡ โ€˜ ๐‘ค ) ) ) )
40 unopadj โŠข ( ( ๐‘‡ โˆˆ UniOp โˆง ๐‘ง โˆˆ โ„‹ โˆง ๐‘ค โˆˆ โ„‹ ) โ†’ ( ( ๐‘‡ โ€˜ ๐‘ง ) ยทih ๐‘ค ) = ( ๐‘ง ยทih ( โ—ก ๐‘‡ โ€˜ ๐‘ค ) ) )
41 40 3expa โŠข ( ( ( ๐‘‡ โˆˆ UniOp โˆง ๐‘ง โˆˆ โ„‹ ) โˆง ๐‘ค โˆˆ โ„‹ ) โ†’ ( ( ๐‘‡ โ€˜ ๐‘ง ) ยทih ๐‘ค ) = ( ๐‘ง ยทih ( โ—ก ๐‘‡ โ€˜ ๐‘ค ) ) )
42 41 adantllr โŠข ( ( ( ( ๐‘‡ โˆˆ UniOp โˆง ( ๐‘ฅ โˆˆ โ„‚ โˆง ๐‘ฆ โˆˆ โ„‹ ) ) โˆง ๐‘ง โˆˆ โ„‹ ) โˆง ๐‘ค โˆˆ โ„‹ ) โ†’ ( ( ๐‘‡ โ€˜ ๐‘ง ) ยทih ๐‘ค ) = ( ๐‘ง ยทih ( โ—ก ๐‘‡ โ€˜ ๐‘ค ) ) )
43 39 42 oveq12d โŠข ( ( ( ( ๐‘‡ โˆˆ UniOp โˆง ( ๐‘ฅ โˆˆ โ„‚ โˆง ๐‘ฆ โˆˆ โ„‹ ) ) โˆง ๐‘ง โˆˆ โ„‹ ) โˆง ๐‘ค โˆˆ โ„‹ ) โ†’ ( ( ๐‘ฅ ยท ( ( ๐‘‡ โ€˜ ๐‘ฆ ) ยทih ๐‘ค ) ) + ( ( ๐‘‡ โ€˜ ๐‘ง ) ยทih ๐‘ค ) ) = ( ( ๐‘ฅ ยท ( ๐‘ฆ ยทih ( โ—ก ๐‘‡ โ€˜ ๐‘ค ) ) ) + ( ๐‘ง ยทih ( โ—ก ๐‘‡ โ€˜ ๐‘ค ) ) ) )
44 34 43 eqtr2d โŠข ( ( ( ( ๐‘‡ โˆˆ UniOp โˆง ( ๐‘ฅ โˆˆ โ„‚ โˆง ๐‘ฆ โˆˆ โ„‹ ) ) โˆง ๐‘ง โˆˆ โ„‹ ) โˆง ๐‘ค โˆˆ โ„‹ ) โ†’ ( ( ๐‘ฅ ยท ( ๐‘ฆ ยทih ( โ—ก ๐‘‡ โ€˜ ๐‘ค ) ) ) + ( ๐‘ง ยทih ( โ—ก ๐‘‡ โ€˜ ๐‘ค ) ) ) = ( ( ( ๐‘ฅ ยทโ„Ž ( ๐‘‡ โ€˜ ๐‘ฆ ) ) +โ„Ž ( ๐‘‡ โ€˜ ๐‘ง ) ) ยทih ๐‘ค ) )
45 12 26 44 3eqtrd โŠข ( ( ( ( ๐‘‡ โˆˆ UniOp โˆง ( ๐‘ฅ โˆˆ โ„‚ โˆง ๐‘ฆ โˆˆ โ„‹ ) ) โˆง ๐‘ง โˆˆ โ„‹ ) โˆง ๐‘ค โˆˆ โ„‹ ) โ†’ ( ( ๐‘‡ โ€˜ ( ( ๐‘ฅ ยทโ„Ž ๐‘ฆ ) +โ„Ž ๐‘ง ) ) ยทih ๐‘ค ) = ( ( ( ๐‘ฅ ยทโ„Ž ( ๐‘‡ โ€˜ ๐‘ฆ ) ) +โ„Ž ( ๐‘‡ โ€˜ ๐‘ง ) ) ยทih ๐‘ค ) )
46 45 ralrimiva โŠข ( ( ( ๐‘‡ โˆˆ UniOp โˆง ( ๐‘ฅ โˆˆ โ„‚ โˆง ๐‘ฆ โˆˆ โ„‹ ) ) โˆง ๐‘ง โˆˆ โ„‹ ) โ†’ โˆ€ ๐‘ค โˆˆ โ„‹ ( ( ๐‘‡ โ€˜ ( ( ๐‘ฅ ยทโ„Ž ๐‘ฆ ) +โ„Ž ๐‘ง ) ) ยทih ๐‘ค ) = ( ( ( ๐‘ฅ ยทโ„Ž ( ๐‘‡ โ€˜ ๐‘ฆ ) ) +โ„Ž ( ๐‘‡ โ€˜ ๐‘ง ) ) ยทih ๐‘ค ) )
47 ffvelcdm โŠข ( ( ๐‘‡ : โ„‹ โŸถ โ„‹ โˆง ( ( ๐‘ฅ ยทโ„Ž ๐‘ฆ ) +โ„Ž ๐‘ง ) โˆˆ โ„‹ ) โ†’ ( ๐‘‡ โ€˜ ( ( ๐‘ฅ ยทโ„Ž ๐‘ฆ ) +โ„Ž ๐‘ง ) ) โˆˆ โ„‹ )
48 7 47 sylan2 โŠข ( ( ๐‘‡ : โ„‹ โŸถ โ„‹ โˆง ( ( ๐‘ฅ โˆˆ โ„‚ โˆง ๐‘ฆ โˆˆ โ„‹ ) โˆง ๐‘ง โˆˆ โ„‹ ) ) โ†’ ( ๐‘‡ โ€˜ ( ( ๐‘ฅ ยทโ„Ž ๐‘ฆ ) +โ„Ž ๐‘ง ) ) โˆˆ โ„‹ )
49 48 anassrs โŠข ( ( ( ๐‘‡ : โ„‹ โŸถ โ„‹ โˆง ( ๐‘ฅ โˆˆ โ„‚ โˆง ๐‘ฆ โˆˆ โ„‹ ) ) โˆง ๐‘ง โˆˆ โ„‹ ) โ†’ ( ๐‘‡ โ€˜ ( ( ๐‘ฅ ยทโ„Ž ๐‘ฆ ) +โ„Ž ๐‘ง ) ) โˆˆ โ„‹ )
50 ffvelcdm โŠข ( ( ๐‘‡ : โ„‹ โŸถ โ„‹ โˆง ๐‘ฆ โˆˆ โ„‹ ) โ†’ ( ๐‘‡ โ€˜ ๐‘ฆ ) โˆˆ โ„‹ )
51 hvmulcl โŠข ( ( ๐‘ฅ โˆˆ โ„‚ โˆง ( ๐‘‡ โ€˜ ๐‘ฆ ) โˆˆ โ„‹ ) โ†’ ( ๐‘ฅ ยทโ„Ž ( ๐‘‡ โ€˜ ๐‘ฆ ) ) โˆˆ โ„‹ )
52 50 51 sylan2 โŠข ( ( ๐‘ฅ โˆˆ โ„‚ โˆง ( ๐‘‡ : โ„‹ โŸถ โ„‹ โˆง ๐‘ฆ โˆˆ โ„‹ ) ) โ†’ ( ๐‘ฅ ยทโ„Ž ( ๐‘‡ โ€˜ ๐‘ฆ ) ) โˆˆ โ„‹ )
53 52 an12s โŠข ( ( ๐‘‡ : โ„‹ โŸถ โ„‹ โˆง ( ๐‘ฅ โˆˆ โ„‚ โˆง ๐‘ฆ โˆˆ โ„‹ ) ) โ†’ ( ๐‘ฅ ยทโ„Ž ( ๐‘‡ โ€˜ ๐‘ฆ ) ) โˆˆ โ„‹ )
54 53 adantr โŠข ( ( ( ๐‘‡ : โ„‹ โŸถ โ„‹ โˆง ( ๐‘ฅ โˆˆ โ„‚ โˆง ๐‘ฆ โˆˆ โ„‹ ) ) โˆง ๐‘ง โˆˆ โ„‹ ) โ†’ ( ๐‘ฅ ยทโ„Ž ( ๐‘‡ โ€˜ ๐‘ฆ ) ) โˆˆ โ„‹ )
55 ffvelcdm โŠข ( ( ๐‘‡ : โ„‹ โŸถ โ„‹ โˆง ๐‘ง โˆˆ โ„‹ ) โ†’ ( ๐‘‡ โ€˜ ๐‘ง ) โˆˆ โ„‹ )
56 55 adantlr โŠข ( ( ( ๐‘‡ : โ„‹ โŸถ โ„‹ โˆง ( ๐‘ฅ โˆˆ โ„‚ โˆง ๐‘ฆ โˆˆ โ„‹ ) ) โˆง ๐‘ง โˆˆ โ„‹ ) โ†’ ( ๐‘‡ โ€˜ ๐‘ง ) โˆˆ โ„‹ )
57 hvaddcl โŠข ( ( ( ๐‘ฅ ยทโ„Ž ( ๐‘‡ โ€˜ ๐‘ฆ ) ) โˆˆ โ„‹ โˆง ( ๐‘‡ โ€˜ ๐‘ง ) โˆˆ โ„‹ ) โ†’ ( ( ๐‘ฅ ยทโ„Ž ( ๐‘‡ โ€˜ ๐‘ฆ ) ) +โ„Ž ( ๐‘‡ โ€˜ ๐‘ง ) ) โˆˆ โ„‹ )
58 54 56 57 syl2anc โŠข ( ( ( ๐‘‡ : โ„‹ โŸถ โ„‹ โˆง ( ๐‘ฅ โˆˆ โ„‚ โˆง ๐‘ฆ โˆˆ โ„‹ ) ) โˆง ๐‘ง โˆˆ โ„‹ ) โ†’ ( ( ๐‘ฅ ยทโ„Ž ( ๐‘‡ โ€˜ ๐‘ฆ ) ) +โ„Ž ( ๐‘‡ โ€˜ ๐‘ง ) ) โˆˆ โ„‹ )
59 hial2eq โŠข ( ( ( ๐‘‡ โ€˜ ( ( ๐‘ฅ ยทโ„Ž ๐‘ฆ ) +โ„Ž ๐‘ง ) ) โˆˆ โ„‹ โˆง ( ( ๐‘ฅ ยทโ„Ž ( ๐‘‡ โ€˜ ๐‘ฆ ) ) +โ„Ž ( ๐‘‡ โ€˜ ๐‘ง ) ) โˆˆ โ„‹ ) โ†’ ( โˆ€ ๐‘ค โˆˆ โ„‹ ( ( ๐‘‡ โ€˜ ( ( ๐‘ฅ ยทโ„Ž ๐‘ฆ ) +โ„Ž ๐‘ง ) ) ยทih ๐‘ค ) = ( ( ( ๐‘ฅ ยทโ„Ž ( ๐‘‡ โ€˜ ๐‘ฆ ) ) +โ„Ž ( ๐‘‡ โ€˜ ๐‘ง ) ) ยทih ๐‘ค ) โ†” ( ๐‘‡ โ€˜ ( ( ๐‘ฅ ยทโ„Ž ๐‘ฆ ) +โ„Ž ๐‘ง ) ) = ( ( ๐‘ฅ ยทโ„Ž ( ๐‘‡ โ€˜ ๐‘ฆ ) ) +โ„Ž ( ๐‘‡ โ€˜ ๐‘ง ) ) ) )
60 49 58 59 syl2anc โŠข ( ( ( ๐‘‡ : โ„‹ โŸถ โ„‹ โˆง ( ๐‘ฅ โˆˆ โ„‚ โˆง ๐‘ฆ โˆˆ โ„‹ ) ) โˆง ๐‘ง โˆˆ โ„‹ ) โ†’ ( โˆ€ ๐‘ค โˆˆ โ„‹ ( ( ๐‘‡ โ€˜ ( ( ๐‘ฅ ยทโ„Ž ๐‘ฆ ) +โ„Ž ๐‘ง ) ) ยทih ๐‘ค ) = ( ( ( ๐‘ฅ ยทโ„Ž ( ๐‘‡ โ€˜ ๐‘ฆ ) ) +โ„Ž ( ๐‘‡ โ€˜ ๐‘ง ) ) ยทih ๐‘ค ) โ†” ( ๐‘‡ โ€˜ ( ( ๐‘ฅ ยทโ„Ž ๐‘ฆ ) +โ„Ž ๐‘ง ) ) = ( ( ๐‘ฅ ยทโ„Ž ( ๐‘‡ โ€˜ ๐‘ฆ ) ) +โ„Ž ( ๐‘‡ โ€˜ ๐‘ง ) ) ) )
61 3 60 sylanl1 โŠข ( ( ( ๐‘‡ โˆˆ UniOp โˆง ( ๐‘ฅ โˆˆ โ„‚ โˆง ๐‘ฆ โˆˆ โ„‹ ) ) โˆง ๐‘ง โˆˆ โ„‹ ) โ†’ ( โˆ€ ๐‘ค โˆˆ โ„‹ ( ( ๐‘‡ โ€˜ ( ( ๐‘ฅ ยทโ„Ž ๐‘ฆ ) +โ„Ž ๐‘ง ) ) ยทih ๐‘ค ) = ( ( ( ๐‘ฅ ยทโ„Ž ( ๐‘‡ โ€˜ ๐‘ฆ ) ) +โ„Ž ( ๐‘‡ โ€˜ ๐‘ง ) ) ยทih ๐‘ค ) โ†” ( ๐‘‡ โ€˜ ( ( ๐‘ฅ ยทโ„Ž ๐‘ฆ ) +โ„Ž ๐‘ง ) ) = ( ( ๐‘ฅ ยทโ„Ž ( ๐‘‡ โ€˜ ๐‘ฆ ) ) +โ„Ž ( ๐‘‡ โ€˜ ๐‘ง ) ) ) )
62 46 61 mpbid โŠข ( ( ( ๐‘‡ โˆˆ UniOp โˆง ( ๐‘ฅ โˆˆ โ„‚ โˆง ๐‘ฆ โˆˆ โ„‹ ) ) โˆง ๐‘ง โˆˆ โ„‹ ) โ†’ ( ๐‘‡ โ€˜ ( ( ๐‘ฅ ยทโ„Ž ๐‘ฆ ) +โ„Ž ๐‘ง ) ) = ( ( ๐‘ฅ ยทโ„Ž ( ๐‘‡ โ€˜ ๐‘ฆ ) ) +โ„Ž ( ๐‘‡ โ€˜ ๐‘ง ) ) )
63 62 ralrimiva โŠข ( ( ๐‘‡ โˆˆ UniOp โˆง ( ๐‘ฅ โˆˆ โ„‚ โˆง ๐‘ฆ โˆˆ โ„‹ ) ) โ†’ โˆ€ ๐‘ง โˆˆ โ„‹ ( ๐‘‡ โ€˜ ( ( ๐‘ฅ ยทโ„Ž ๐‘ฆ ) +โ„Ž ๐‘ง ) ) = ( ( ๐‘ฅ ยทโ„Ž ( ๐‘‡ โ€˜ ๐‘ฆ ) ) +โ„Ž ( ๐‘‡ โ€˜ ๐‘ง ) ) )
64 63 ralrimivva โŠข ( ๐‘‡ โˆˆ UniOp โ†’ โˆ€ ๐‘ฅ โˆˆ โ„‚ โˆ€ ๐‘ฆ โˆˆ โ„‹ โˆ€ ๐‘ง โˆˆ โ„‹ ( ๐‘‡ โ€˜ ( ( ๐‘ฅ ยทโ„Ž ๐‘ฆ ) +โ„Ž ๐‘ง ) ) = ( ( ๐‘ฅ ยทโ„Ž ( ๐‘‡ โ€˜ ๐‘ฆ ) ) +โ„Ž ( ๐‘‡ โ€˜ ๐‘ง ) ) )
65 ellnop โŠข ( ๐‘‡ โˆˆ LinOp โ†” ( ๐‘‡ : โ„‹ โŸถ โ„‹ โˆง โˆ€ ๐‘ฅ โˆˆ โ„‚ โˆ€ ๐‘ฆ โˆˆ โ„‹ โˆ€ ๐‘ง โˆˆ โ„‹ ( ๐‘‡ โ€˜ ( ( ๐‘ฅ ยทโ„Ž ๐‘ฆ ) +โ„Ž ๐‘ง ) ) = ( ( ๐‘ฅ ยทโ„Ž ( ๐‘‡ โ€˜ ๐‘ฆ ) ) +โ„Ž ( ๐‘‡ โ€˜ ๐‘ง ) ) ) )
66 3 64 65 sylanbrc โŠข ( ๐‘‡ โˆˆ UniOp โ†’ ๐‘‡ โˆˆ LinOp )