Metamath Proof Explorer

Theorem elunop2

Description: An operator is unitary iff it is linear, onto, and idempotent in the norm. Similar to theorem in AkhiezerGlazman p. 73, and its converse. (Contributed by NM, 24-Feb-2006) (New usage is discouraged.)

Ref Expression
Assertion elunop2 ( ๐‘‡ โˆˆ UniOp โ†” ( ๐‘‡ โˆˆ LinOp โˆง ๐‘‡ : โ„‹ โ€“ontoโ†’ โ„‹ โˆง โˆ€ ๐‘ฅ โˆˆ โ„‹ ( normโ„Ž โ€˜ ( ๐‘‡ โ€˜ ๐‘ฅ ) ) = ( normโ„Ž โ€˜ ๐‘ฅ ) ) )

Proof

Step Hyp Ref Expression
1 unoplin โŠข ( ๐‘‡ โˆˆ UniOp โ†’ ๐‘‡ โˆˆ LinOp )
2 elunop โŠข ( ๐‘‡ โˆˆ UniOp โ†” ( ๐‘‡ : โ„‹ โ€“ontoโ†’ โ„‹ โˆง โˆ€ ๐‘ฅ โˆˆ โ„‹ โˆ€ ๐‘ฆ โˆˆ โ„‹ ( ( ๐‘‡ โ€˜ ๐‘ฅ ) ยทih ( ๐‘‡ โ€˜ ๐‘ฆ ) ) = ( ๐‘ฅ ยทih ๐‘ฆ ) ) )
3 2 simplbi โŠข ( ๐‘‡ โˆˆ UniOp โ†’ ๐‘‡ : โ„‹ โ€“ontoโ†’ โ„‹ )
4 unopnorm โŠข ( ( ๐‘‡ โˆˆ UniOp โˆง ๐‘ฅ โˆˆ โ„‹ ) โ†’ ( normโ„Ž โ€˜ ( ๐‘‡ โ€˜ ๐‘ฅ ) ) = ( normโ„Ž โ€˜ ๐‘ฅ ) )
5 4 ralrimiva โŠข ( ๐‘‡ โˆˆ UniOp โ†’ โˆ€ ๐‘ฅ โˆˆ โ„‹ ( normโ„Ž โ€˜ ( ๐‘‡ โ€˜ ๐‘ฅ ) ) = ( normโ„Ž โ€˜ ๐‘ฅ ) )
6 1 3 5 3jca โŠข ( ๐‘‡ โˆˆ UniOp โ†’ ( ๐‘‡ โˆˆ LinOp โˆง ๐‘‡ : โ„‹ โ€“ontoโ†’ โ„‹ โˆง โˆ€ ๐‘ฅ โˆˆ โ„‹ ( normโ„Ž โ€˜ ( ๐‘‡ โ€˜ ๐‘ฅ ) ) = ( normโ„Ž โ€˜ ๐‘ฅ ) ) )
7 eleq1 โŠข ( ๐‘‡ = if ( ( ๐‘‡ โˆˆ LinOp โˆง ๐‘‡ : โ„‹ โ€“ontoโ†’ โ„‹ โˆง โˆ€ ๐‘ฅ โˆˆ โ„‹ ( normโ„Ž โ€˜ ( ๐‘‡ โ€˜ ๐‘ฅ ) ) = ( normโ„Ž โ€˜ ๐‘ฅ ) ) , ๐‘‡ , ( I โ†พ โ„‹ ) ) โ†’ ( ๐‘‡ โˆˆ UniOp โ†” if ( ( ๐‘‡ โˆˆ LinOp โˆง ๐‘‡ : โ„‹ โ€“ontoโ†’ โ„‹ โˆง โˆ€ ๐‘ฅ โˆˆ โ„‹ ( normโ„Ž โ€˜ ( ๐‘‡ โ€˜ ๐‘ฅ ) ) = ( normโ„Ž โ€˜ ๐‘ฅ ) ) , ๐‘‡ , ( I โ†พ โ„‹ ) ) โˆˆ UniOp ) )
8 eleq1 โŠข ( ๐‘‡ = if ( ( ๐‘‡ โˆˆ LinOp โˆง ๐‘‡ : โ„‹ โ€“ontoโ†’ โ„‹ โˆง โˆ€ ๐‘ฅ โˆˆ โ„‹ ( normโ„Ž โ€˜ ( ๐‘‡ โ€˜ ๐‘ฅ ) ) = ( normโ„Ž โ€˜ ๐‘ฅ ) ) , ๐‘‡ , ( I โ†พ โ„‹ ) ) โ†’ ( ๐‘‡ โˆˆ LinOp โ†” if ( ( ๐‘‡ โˆˆ LinOp โˆง ๐‘‡ : โ„‹ โ€“ontoโ†’ โ„‹ โˆง โˆ€ ๐‘ฅ โˆˆ โ„‹ ( normโ„Ž โ€˜ ( ๐‘‡ โ€˜ ๐‘ฅ ) ) = ( normโ„Ž โ€˜ ๐‘ฅ ) ) , ๐‘‡ , ( I โ†พ โ„‹ ) ) โˆˆ LinOp ) )
9 foeq1 โŠข ( ๐‘‡ = if ( ( ๐‘‡ โˆˆ LinOp โˆง ๐‘‡ : โ„‹ โ€“ontoโ†’ โ„‹ โˆง โˆ€ ๐‘ฅ โˆˆ โ„‹ ( normโ„Ž โ€˜ ( ๐‘‡ โ€˜ ๐‘ฅ ) ) = ( normโ„Ž โ€˜ ๐‘ฅ ) ) , ๐‘‡ , ( I โ†พ โ„‹ ) ) โ†’ ( ๐‘‡ : โ„‹ โ€“ontoโ†’ โ„‹ โ†” if ( ( ๐‘‡ โˆˆ LinOp โˆง ๐‘‡ : โ„‹ โ€“ontoโ†’ โ„‹ โˆง โˆ€ ๐‘ฅ โˆˆ โ„‹ ( normโ„Ž โ€˜ ( ๐‘‡ โ€˜ ๐‘ฅ ) ) = ( normโ„Ž โ€˜ ๐‘ฅ ) ) , ๐‘‡ , ( I โ†พ โ„‹ ) ) : โ„‹ โ€“ontoโ†’ โ„‹ ) )
10 2fveq3 โŠข ( ๐‘ฅ = ๐‘ฆ โ†’ ( normโ„Ž โ€˜ ( ๐‘‡ โ€˜ ๐‘ฅ ) ) = ( normโ„Ž โ€˜ ( ๐‘‡ โ€˜ ๐‘ฆ ) ) )
11 fveq2 โŠข ( ๐‘ฅ = ๐‘ฆ โ†’ ( normโ„Ž โ€˜ ๐‘ฅ ) = ( normโ„Ž โ€˜ ๐‘ฆ ) )
12 10 11 eqeq12d โŠข ( ๐‘ฅ = ๐‘ฆ โ†’ ( ( normโ„Ž โ€˜ ( ๐‘‡ โ€˜ ๐‘ฅ ) ) = ( normโ„Ž โ€˜ ๐‘ฅ ) โ†” ( normโ„Ž โ€˜ ( ๐‘‡ โ€˜ ๐‘ฆ ) ) = ( normโ„Ž โ€˜ ๐‘ฆ ) ) )
13 12 cbvralvw โŠข ( โˆ€ ๐‘ฅ โˆˆ โ„‹ ( normโ„Ž โ€˜ ( ๐‘‡ โ€˜ ๐‘ฅ ) ) = ( normโ„Ž โ€˜ ๐‘ฅ ) โ†” โˆ€ ๐‘ฆ โˆˆ โ„‹ ( normโ„Ž โ€˜ ( ๐‘‡ โ€˜ ๐‘ฆ ) ) = ( normโ„Ž โ€˜ ๐‘ฆ ) )
14 fveq1 โŠข ( ๐‘‡ = if ( ( ๐‘‡ โˆˆ LinOp โˆง ๐‘‡ : โ„‹ โ€“ontoโ†’ โ„‹ โˆง โˆ€ ๐‘ฅ โˆˆ โ„‹ ( normโ„Ž โ€˜ ( ๐‘‡ โ€˜ ๐‘ฅ ) ) = ( normโ„Ž โ€˜ ๐‘ฅ ) ) , ๐‘‡ , ( I โ†พ โ„‹ ) ) โ†’ ( ๐‘‡ โ€˜ ๐‘ฆ ) = ( if ( ( ๐‘‡ โˆˆ LinOp โˆง ๐‘‡ : โ„‹ โ€“ontoโ†’ โ„‹ โˆง โˆ€ ๐‘ฅ โˆˆ โ„‹ ( normโ„Ž โ€˜ ( ๐‘‡ โ€˜ ๐‘ฅ ) ) = ( normโ„Ž โ€˜ ๐‘ฅ ) ) , ๐‘‡ , ( I โ†พ โ„‹ ) ) โ€˜ ๐‘ฆ ) )
15 14 fveqeq2d โŠข ( ๐‘‡ = if ( ( ๐‘‡ โˆˆ LinOp โˆง ๐‘‡ : โ„‹ โ€“ontoโ†’ โ„‹ โˆง โˆ€ ๐‘ฅ โˆˆ โ„‹ ( normโ„Ž โ€˜ ( ๐‘‡ โ€˜ ๐‘ฅ ) ) = ( normโ„Ž โ€˜ ๐‘ฅ ) ) , ๐‘‡ , ( I โ†พ โ„‹ ) ) โ†’ ( ( normโ„Ž โ€˜ ( ๐‘‡ โ€˜ ๐‘ฆ ) ) = ( normโ„Ž โ€˜ ๐‘ฆ ) โ†” ( normโ„Ž โ€˜ ( if ( ( ๐‘‡ โˆˆ LinOp โˆง ๐‘‡ : โ„‹ โ€“ontoโ†’ โ„‹ โˆง โˆ€ ๐‘ฅ โˆˆ โ„‹ ( normโ„Ž โ€˜ ( ๐‘‡ โ€˜ ๐‘ฅ ) ) = ( normโ„Ž โ€˜ ๐‘ฅ ) ) , ๐‘‡ , ( I โ†พ โ„‹ ) ) โ€˜ ๐‘ฆ ) ) = ( normโ„Ž โ€˜ ๐‘ฆ ) ) )
16 15 ralbidv โŠข ( ๐‘‡ = if ( ( ๐‘‡ โˆˆ LinOp โˆง ๐‘‡ : โ„‹ โ€“ontoโ†’ โ„‹ โˆง โˆ€ ๐‘ฅ โˆˆ โ„‹ ( normโ„Ž โ€˜ ( ๐‘‡ โ€˜ ๐‘ฅ ) ) = ( normโ„Ž โ€˜ ๐‘ฅ ) ) , ๐‘‡ , ( I โ†พ โ„‹ ) ) โ†’ ( โˆ€ ๐‘ฆ โˆˆ โ„‹ ( normโ„Ž โ€˜ ( ๐‘‡ โ€˜ ๐‘ฆ ) ) = ( normโ„Ž โ€˜ ๐‘ฆ ) โ†” โˆ€ ๐‘ฆ โˆˆ โ„‹ ( normโ„Ž โ€˜ ( if ( ( ๐‘‡ โˆˆ LinOp โˆง ๐‘‡ : โ„‹ โ€“ontoโ†’ โ„‹ โˆง โˆ€ ๐‘ฅ โˆˆ โ„‹ ( normโ„Ž โ€˜ ( ๐‘‡ โ€˜ ๐‘ฅ ) ) = ( normโ„Ž โ€˜ ๐‘ฅ ) ) , ๐‘‡ , ( I โ†พ โ„‹ ) ) โ€˜ ๐‘ฆ ) ) = ( normโ„Ž โ€˜ ๐‘ฆ ) ) )
17 13 16 bitrid โŠข ( ๐‘‡ = if ( ( ๐‘‡ โˆˆ LinOp โˆง ๐‘‡ : โ„‹ โ€“ontoโ†’ โ„‹ โˆง โˆ€ ๐‘ฅ โˆˆ โ„‹ ( normโ„Ž โ€˜ ( ๐‘‡ โ€˜ ๐‘ฅ ) ) = ( normโ„Ž โ€˜ ๐‘ฅ ) ) , ๐‘‡ , ( I โ†พ โ„‹ ) ) โ†’ ( โˆ€ ๐‘ฅ โˆˆ โ„‹ ( normโ„Ž โ€˜ ( ๐‘‡ โ€˜ ๐‘ฅ ) ) = ( normโ„Ž โ€˜ ๐‘ฅ ) โ†” โˆ€ ๐‘ฆ โˆˆ โ„‹ ( normโ„Ž โ€˜ ( if ( ( ๐‘‡ โˆˆ LinOp โˆง ๐‘‡ : โ„‹ โ€“ontoโ†’ โ„‹ โˆง โˆ€ ๐‘ฅ โˆˆ โ„‹ ( normโ„Ž โ€˜ ( ๐‘‡ โ€˜ ๐‘ฅ ) ) = ( normโ„Ž โ€˜ ๐‘ฅ ) ) , ๐‘‡ , ( I โ†พ โ„‹ ) ) โ€˜ ๐‘ฆ ) ) = ( normโ„Ž โ€˜ ๐‘ฆ ) ) )
18 8 9 17 3anbi123d โŠข ( ๐‘‡ = if ( ( ๐‘‡ โˆˆ LinOp โˆง ๐‘‡ : โ„‹ โ€“ontoโ†’ โ„‹ โˆง โˆ€ ๐‘ฅ โˆˆ โ„‹ ( normโ„Ž โ€˜ ( ๐‘‡ โ€˜ ๐‘ฅ ) ) = ( normโ„Ž โ€˜ ๐‘ฅ ) ) , ๐‘‡ , ( I โ†พ โ„‹ ) ) โ†’ ( ( ๐‘‡ โˆˆ LinOp โˆง ๐‘‡ : โ„‹ โ€“ontoโ†’ โ„‹ โˆง โˆ€ ๐‘ฅ โˆˆ โ„‹ ( normโ„Ž โ€˜ ( ๐‘‡ โ€˜ ๐‘ฅ ) ) = ( normโ„Ž โ€˜ ๐‘ฅ ) ) โ†” ( if ( ( ๐‘‡ โˆˆ LinOp โˆง ๐‘‡ : โ„‹ โ€“ontoโ†’ โ„‹ โˆง โˆ€ ๐‘ฅ โˆˆ โ„‹ ( normโ„Ž โ€˜ ( ๐‘‡ โ€˜ ๐‘ฅ ) ) = ( normโ„Ž โ€˜ ๐‘ฅ ) ) , ๐‘‡ , ( I โ†พ โ„‹ ) ) โˆˆ LinOp โˆง if ( ( ๐‘‡ โˆˆ LinOp โˆง ๐‘‡ : โ„‹ โ€“ontoโ†’ โ„‹ โˆง โˆ€ ๐‘ฅ โˆˆ โ„‹ ( normโ„Ž โ€˜ ( ๐‘‡ โ€˜ ๐‘ฅ ) ) = ( normโ„Ž โ€˜ ๐‘ฅ ) ) , ๐‘‡ , ( I โ†พ โ„‹ ) ) : โ„‹ โ€“ontoโ†’ โ„‹ โˆง โˆ€ ๐‘ฆ โˆˆ โ„‹ ( normโ„Ž โ€˜ ( if ( ( ๐‘‡ โˆˆ LinOp โˆง ๐‘‡ : โ„‹ โ€“ontoโ†’ โ„‹ โˆง โˆ€ ๐‘ฅ โˆˆ โ„‹ ( normโ„Ž โ€˜ ( ๐‘‡ โ€˜ ๐‘ฅ ) ) = ( normโ„Ž โ€˜ ๐‘ฅ ) ) , ๐‘‡ , ( I โ†พ โ„‹ ) ) โ€˜ ๐‘ฆ ) ) = ( normโ„Ž โ€˜ ๐‘ฆ ) ) ) )
19 eleq1 โŠข ( ( I โ†พ โ„‹ ) = if ( ( ๐‘‡ โˆˆ LinOp โˆง ๐‘‡ : โ„‹ โ€“ontoโ†’ โ„‹ โˆง โˆ€ ๐‘ฅ โˆˆ โ„‹ ( normโ„Ž โ€˜ ( ๐‘‡ โ€˜ ๐‘ฅ ) ) = ( normโ„Ž โ€˜ ๐‘ฅ ) ) , ๐‘‡ , ( I โ†พ โ„‹ ) ) โ†’ ( ( I โ†พ โ„‹ ) โˆˆ LinOp โ†” if ( ( ๐‘‡ โˆˆ LinOp โˆง ๐‘‡ : โ„‹ โ€“ontoโ†’ โ„‹ โˆง โˆ€ ๐‘ฅ โˆˆ โ„‹ ( normโ„Ž โ€˜ ( ๐‘‡ โ€˜ ๐‘ฅ ) ) = ( normโ„Ž โ€˜ ๐‘ฅ ) ) , ๐‘‡ , ( I โ†พ โ„‹ ) ) โˆˆ LinOp ) )
20 foeq1 โŠข ( ( I โ†พ โ„‹ ) = if ( ( ๐‘‡ โˆˆ LinOp โˆง ๐‘‡ : โ„‹ โ€“ontoโ†’ โ„‹ โˆง โˆ€ ๐‘ฅ โˆˆ โ„‹ ( normโ„Ž โ€˜ ( ๐‘‡ โ€˜ ๐‘ฅ ) ) = ( normโ„Ž โ€˜ ๐‘ฅ ) ) , ๐‘‡ , ( I โ†พ โ„‹ ) ) โ†’ ( ( I โ†พ โ„‹ ) : โ„‹ โ€“ontoโ†’ โ„‹ โ†” if ( ( ๐‘‡ โˆˆ LinOp โˆง ๐‘‡ : โ„‹ โ€“ontoโ†’ โ„‹ โˆง โˆ€ ๐‘ฅ โˆˆ โ„‹ ( normโ„Ž โ€˜ ( ๐‘‡ โ€˜ ๐‘ฅ ) ) = ( normโ„Ž โ€˜ ๐‘ฅ ) ) , ๐‘‡ , ( I โ†พ โ„‹ ) ) : โ„‹ โ€“ontoโ†’ โ„‹ ) )
21 fveq1 โŠข ( ( I โ†พ โ„‹ ) = if ( ( ๐‘‡ โˆˆ LinOp โˆง ๐‘‡ : โ„‹ โ€“ontoโ†’ โ„‹ โˆง โˆ€ ๐‘ฅ โˆˆ โ„‹ ( normโ„Ž โ€˜ ( ๐‘‡ โ€˜ ๐‘ฅ ) ) = ( normโ„Ž โ€˜ ๐‘ฅ ) ) , ๐‘‡ , ( I โ†พ โ„‹ ) ) โ†’ ( ( I โ†พ โ„‹ ) โ€˜ ๐‘ฆ ) = ( if ( ( ๐‘‡ โˆˆ LinOp โˆง ๐‘‡ : โ„‹ โ€“ontoโ†’ โ„‹ โˆง โˆ€ ๐‘ฅ โˆˆ โ„‹ ( normโ„Ž โ€˜ ( ๐‘‡ โ€˜ ๐‘ฅ ) ) = ( normโ„Ž โ€˜ ๐‘ฅ ) ) , ๐‘‡ , ( I โ†พ โ„‹ ) ) โ€˜ ๐‘ฆ ) )
22 21 fveqeq2d โŠข ( ( I โ†พ โ„‹ ) = if ( ( ๐‘‡ โˆˆ LinOp โˆง ๐‘‡ : โ„‹ โ€“ontoโ†’ โ„‹ โˆง โˆ€ ๐‘ฅ โˆˆ โ„‹ ( normโ„Ž โ€˜ ( ๐‘‡ โ€˜ ๐‘ฅ ) ) = ( normโ„Ž โ€˜ ๐‘ฅ ) ) , ๐‘‡ , ( I โ†พ โ„‹ ) ) โ†’ ( ( normโ„Ž โ€˜ ( ( I โ†พ โ„‹ ) โ€˜ ๐‘ฆ ) ) = ( normโ„Ž โ€˜ ๐‘ฆ ) โ†” ( normโ„Ž โ€˜ ( if ( ( ๐‘‡ โˆˆ LinOp โˆง ๐‘‡ : โ„‹ โ€“ontoโ†’ โ„‹ โˆง โˆ€ ๐‘ฅ โˆˆ โ„‹ ( normโ„Ž โ€˜ ( ๐‘‡ โ€˜ ๐‘ฅ ) ) = ( normโ„Ž โ€˜ ๐‘ฅ ) ) , ๐‘‡ , ( I โ†พ โ„‹ ) ) โ€˜ ๐‘ฆ ) ) = ( normโ„Ž โ€˜ ๐‘ฆ ) ) )
23 22 ralbidv โŠข ( ( I โ†พ โ„‹ ) = if ( ( ๐‘‡ โˆˆ LinOp โˆง ๐‘‡ : โ„‹ โ€“ontoโ†’ โ„‹ โˆง โˆ€ ๐‘ฅ โˆˆ โ„‹ ( normโ„Ž โ€˜ ( ๐‘‡ โ€˜ ๐‘ฅ ) ) = ( normโ„Ž โ€˜ ๐‘ฅ ) ) , ๐‘‡ , ( I โ†พ โ„‹ ) ) โ†’ ( โˆ€ ๐‘ฆ โˆˆ โ„‹ ( normโ„Ž โ€˜ ( ( I โ†พ โ„‹ ) โ€˜ ๐‘ฆ ) ) = ( normโ„Ž โ€˜ ๐‘ฆ ) โ†” โˆ€ ๐‘ฆ โˆˆ โ„‹ ( normโ„Ž โ€˜ ( if ( ( ๐‘‡ โˆˆ LinOp โˆง ๐‘‡ : โ„‹ โ€“ontoโ†’ โ„‹ โˆง โˆ€ ๐‘ฅ โˆˆ โ„‹ ( normโ„Ž โ€˜ ( ๐‘‡ โ€˜ ๐‘ฅ ) ) = ( normโ„Ž โ€˜ ๐‘ฅ ) ) , ๐‘‡ , ( I โ†พ โ„‹ ) ) โ€˜ ๐‘ฆ ) ) = ( normโ„Ž โ€˜ ๐‘ฆ ) ) )
24 19 20 23 3anbi123d โŠข ( ( I โ†พ โ„‹ ) = if ( ( ๐‘‡ โˆˆ LinOp โˆง ๐‘‡ : โ„‹ โ€“ontoโ†’ โ„‹ โˆง โˆ€ ๐‘ฅ โˆˆ โ„‹ ( normโ„Ž โ€˜ ( ๐‘‡ โ€˜ ๐‘ฅ ) ) = ( normโ„Ž โ€˜ ๐‘ฅ ) ) , ๐‘‡ , ( I โ†พ โ„‹ ) ) โ†’ ( ( ( I โ†พ โ„‹ ) โˆˆ LinOp โˆง ( I โ†พ โ„‹ ) : โ„‹ โ€“ontoโ†’ โ„‹ โˆง โˆ€ ๐‘ฆ โˆˆ โ„‹ ( normโ„Ž โ€˜ ( ( I โ†พ โ„‹ ) โ€˜ ๐‘ฆ ) ) = ( normโ„Ž โ€˜ ๐‘ฆ ) ) โ†” ( if ( ( ๐‘‡ โˆˆ LinOp โˆง ๐‘‡ : โ„‹ โ€“ontoโ†’ โ„‹ โˆง โˆ€ ๐‘ฅ โˆˆ โ„‹ ( normโ„Ž โ€˜ ( ๐‘‡ โ€˜ ๐‘ฅ ) ) = ( normโ„Ž โ€˜ ๐‘ฅ ) ) , ๐‘‡ , ( I โ†พ โ„‹ ) ) โˆˆ LinOp โˆง if ( ( ๐‘‡ โˆˆ LinOp โˆง ๐‘‡ : โ„‹ โ€“ontoโ†’ โ„‹ โˆง โˆ€ ๐‘ฅ โˆˆ โ„‹ ( normโ„Ž โ€˜ ( ๐‘‡ โ€˜ ๐‘ฅ ) ) = ( normโ„Ž โ€˜ ๐‘ฅ ) ) , ๐‘‡ , ( I โ†พ โ„‹ ) ) : โ„‹ โ€“ontoโ†’ โ„‹ โˆง โˆ€ ๐‘ฆ โˆˆ โ„‹ ( normโ„Ž โ€˜ ( if ( ( ๐‘‡ โˆˆ LinOp โˆง ๐‘‡ : โ„‹ โ€“ontoโ†’ โ„‹ โˆง โˆ€ ๐‘ฅ โˆˆ โ„‹ ( normโ„Ž โ€˜ ( ๐‘‡ โ€˜ ๐‘ฅ ) ) = ( normโ„Ž โ€˜ ๐‘ฅ ) ) , ๐‘‡ , ( I โ†พ โ„‹ ) ) โ€˜ ๐‘ฆ ) ) = ( normโ„Ž โ€˜ ๐‘ฆ ) ) ) )
25 idlnop โŠข ( I โ†พ โ„‹ ) โˆˆ LinOp
26 f1oi โŠข ( I โ†พ โ„‹ ) : โ„‹ โ€“1-1-ontoโ†’ โ„‹
27 f1ofo โŠข ( ( I โ†พ โ„‹ ) : โ„‹ โ€“1-1-ontoโ†’ โ„‹ โ†’ ( I โ†พ โ„‹ ) : โ„‹ โ€“ontoโ†’ โ„‹ )
28 26 27 ax-mp โŠข ( I โ†พ โ„‹ ) : โ„‹ โ€“ontoโ†’ โ„‹
29 fvresi โŠข ( ๐‘ฆ โˆˆ โ„‹ โ†’ ( ( I โ†พ โ„‹ ) โ€˜ ๐‘ฆ ) = ๐‘ฆ )
30 29 fveq2d โŠข ( ๐‘ฆ โˆˆ โ„‹ โ†’ ( normโ„Ž โ€˜ ( ( I โ†พ โ„‹ ) โ€˜ ๐‘ฆ ) ) = ( normโ„Ž โ€˜ ๐‘ฆ ) )
31 30 rgen โŠข โˆ€ ๐‘ฆ โˆˆ โ„‹ ( normโ„Ž โ€˜ ( ( I โ†พ โ„‹ ) โ€˜ ๐‘ฆ ) ) = ( normโ„Ž โ€˜ ๐‘ฆ )
32 25 28 31 3pm3.2i โŠข ( ( I โ†พ โ„‹ ) โˆˆ LinOp โˆง ( I โ†พ โ„‹ ) : โ„‹ โ€“ontoโ†’ โ„‹ โˆง โˆ€ ๐‘ฆ โˆˆ โ„‹ ( normโ„Ž โ€˜ ( ( I โ†พ โ„‹ ) โ€˜ ๐‘ฆ ) ) = ( normโ„Ž โ€˜ ๐‘ฆ ) )
33 18 24 32 elimhyp โŠข ( if ( ( ๐‘‡ โˆˆ LinOp โˆง ๐‘‡ : โ„‹ โ€“ontoโ†’ โ„‹ โˆง โˆ€ ๐‘ฅ โˆˆ โ„‹ ( normโ„Ž โ€˜ ( ๐‘‡ โ€˜ ๐‘ฅ ) ) = ( normโ„Ž โ€˜ ๐‘ฅ ) ) , ๐‘‡ , ( I โ†พ โ„‹ ) ) โˆˆ LinOp โˆง if ( ( ๐‘‡ โˆˆ LinOp โˆง ๐‘‡ : โ„‹ โ€“ontoโ†’ โ„‹ โˆง โˆ€ ๐‘ฅ โˆˆ โ„‹ ( normโ„Ž โ€˜ ( ๐‘‡ โ€˜ ๐‘ฅ ) ) = ( normโ„Ž โ€˜ ๐‘ฅ ) ) , ๐‘‡ , ( I โ†พ โ„‹ ) ) : โ„‹ โ€“ontoโ†’ โ„‹ โˆง โˆ€ ๐‘ฆ โˆˆ โ„‹ ( normโ„Ž โ€˜ ( if ( ( ๐‘‡ โˆˆ LinOp โˆง ๐‘‡ : โ„‹ โ€“ontoโ†’ โ„‹ โˆง โˆ€ ๐‘ฅ โˆˆ โ„‹ ( normโ„Ž โ€˜ ( ๐‘‡ โ€˜ ๐‘ฅ ) ) = ( normโ„Ž โ€˜ ๐‘ฅ ) ) , ๐‘‡ , ( I โ†พ โ„‹ ) ) โ€˜ ๐‘ฆ ) ) = ( normโ„Ž โ€˜ ๐‘ฆ ) )
34 33 simp1i โŠข if ( ( ๐‘‡ โˆˆ LinOp โˆง ๐‘‡ : โ„‹ โ€“ontoโ†’ โ„‹ โˆง โˆ€ ๐‘ฅ โˆˆ โ„‹ ( normโ„Ž โ€˜ ( ๐‘‡ โ€˜ ๐‘ฅ ) ) = ( normโ„Ž โ€˜ ๐‘ฅ ) ) , ๐‘‡ , ( I โ†พ โ„‹ ) ) โˆˆ LinOp
35 33 simp2i โŠข if ( ( ๐‘‡ โˆˆ LinOp โˆง ๐‘‡ : โ„‹ โ€“ontoโ†’ โ„‹ โˆง โˆ€ ๐‘ฅ โˆˆ โ„‹ ( normโ„Ž โ€˜ ( ๐‘‡ โ€˜ ๐‘ฅ ) ) = ( normโ„Ž โ€˜ ๐‘ฅ ) ) , ๐‘‡ , ( I โ†พ โ„‹ ) ) : โ„‹ โ€“ontoโ†’ โ„‹
36 33 simp3i โŠข โˆ€ ๐‘ฆ โˆˆ โ„‹ ( normโ„Ž โ€˜ ( if ( ( ๐‘‡ โˆˆ LinOp โˆง ๐‘‡ : โ„‹ โ€“ontoโ†’ โ„‹ โˆง โˆ€ ๐‘ฅ โˆˆ โ„‹ ( normโ„Ž โ€˜ ( ๐‘‡ โ€˜ ๐‘ฅ ) ) = ( normโ„Ž โ€˜ ๐‘ฅ ) ) , ๐‘‡ , ( I โ†พ โ„‹ ) ) โ€˜ ๐‘ฆ ) ) = ( normโ„Ž โ€˜ ๐‘ฆ )
37 34 35 36 lnopunii โŠข if ( ( ๐‘‡ โˆˆ LinOp โˆง ๐‘‡ : โ„‹ โ€“ontoโ†’ โ„‹ โˆง โˆ€ ๐‘ฅ โˆˆ โ„‹ ( normโ„Ž โ€˜ ( ๐‘‡ โ€˜ ๐‘ฅ ) ) = ( normโ„Ž โ€˜ ๐‘ฅ ) ) , ๐‘‡ , ( I โ†พ โ„‹ ) ) โˆˆ UniOp
38 7 37 dedth โŠข ( ( ๐‘‡ โˆˆ LinOp โˆง ๐‘‡ : โ„‹ โ€“ontoโ†’ โ„‹ โˆง โˆ€ ๐‘ฅ โˆˆ โ„‹ ( normโ„Ž โ€˜ ( ๐‘‡ โ€˜ ๐‘ฅ ) ) = ( normโ„Ž โ€˜ ๐‘ฅ ) ) โ†’ ๐‘‡ โˆˆ UniOp )
39 6 38 impbii โŠข ( ๐‘‡ โˆˆ UniOp โ†” ( ๐‘‡ โˆˆ LinOp โˆง ๐‘‡ : โ„‹ โ€“ontoโ†’ โ„‹ โˆง โˆ€ ๐‘ฅ โˆˆ โ„‹ ( normโ„Ž โ€˜ ( ๐‘‡ โ€˜ ๐‘ฅ ) ) = ( normโ„Ž โ€˜ ๐‘ฅ ) ) )