Metamath Proof Explorer

Theorem opsqrlem1

Description: Lemma for opsqri . (Contributed by NM, 9-Aug-2006) (New usage is discouraged.)

Ref Expression
Hypotheses opsqrlem1.1 
|- T e. HrmOp
opsqrlem1.2 
|- ( normop ` T ) e. RR
opsqrlem1.3 
|- 0hop <_op T
opsqrlem1.4 
|- R = ( ( 1 / ( normop ` T ) ) .op T )
opsqrlem1.5 
|- ( T =/= 0hop -> E. u e. HrmOp ( 0hop <_op u /\ ( u o. u ) = R ) )
Assertion opsqrlem1 
|- ( T =/= 0hop -> E. v e. HrmOp ( 0hop <_op v /\ ( v o. v ) = T ) )

Proof

Step Hyp Ref Expression
1 opsqrlem1.1 
 |-  T e. HrmOp
2 opsqrlem1.2 
 |-  ( normop ` T ) e. RR
3 opsqrlem1.3 
 |-  0hop <_op T
4 opsqrlem1.4 
 |-  R = ( ( 1 / ( normop ` T ) ) .op T )
5 opsqrlem1.5 
 |-  ( T =/= 0hop -> E. u e. HrmOp ( 0hop <_op u /\ ( u o. u ) = R ) )
6 hmopf 
 |-  ( T e. HrmOp -> T : ~H --> ~H )
7 1 6 ax-mp 
 |-  T : ~H --> ~H
8 nmopge0 
 |-  ( T : ~H --> ~H -> 0 <_ ( normop ` T ) )
9 7 8 ax-mp 
 |-  0 <_ ( normop ` T )
10 2 sqrtcli 
 |-  ( 0 <_ ( normop ` T ) -> ( sqrt ` ( normop ` T ) ) e. RR )
11 9 10 ax-mp 
 |-  ( sqrt ` ( normop ` T ) ) e. RR
12 hmopm 
 |-  ( ( ( sqrt ` ( normop ` T ) ) e. RR /\ u e. HrmOp ) -> ( ( sqrt ` ( normop ` T ) ) .op u ) e. HrmOp )
13 11 12 mpan 
 |-  ( u e. HrmOp -> ( ( sqrt ` ( normop ` T ) ) .op u ) e. HrmOp )
14 13 ad2antlr 
 |-  ( ( ( T =/= 0hop /\ u e. HrmOp ) /\ ( 0hop <_op u /\ ( u o. u ) = R ) ) -> ( ( sqrt ` ( normop ` T ) ) .op u ) e. HrmOp )
15 2 sqrtge0i 
 |-  ( 0 <_ ( normop ` T ) -> 0 <_ ( sqrt ` ( normop ` T ) ) )
16 9 15 ax-mp 
 |-  0 <_ ( sqrt ` ( normop ` T ) )
17 leopmuli 
 |-  ( ( ( ( sqrt ` ( normop ` T ) ) e. RR /\ u e. HrmOp ) /\ ( 0 <_ ( sqrt ` ( normop ` T ) ) /\ 0hop <_op u ) ) -> 0hop <_op ( ( sqrt ` ( normop ` T ) ) .op u ) )
18 16 17 mpanr1 
 |-  ( ( ( ( sqrt ` ( normop ` T ) ) e. RR /\ u e. HrmOp ) /\ 0hop <_op u ) -> 0hop <_op ( ( sqrt ` ( normop ` T ) ) .op u ) )
19 11 18 mpanl1 
 |-  ( ( u e. HrmOp /\ 0hop <_op u ) -> 0hop <_op ( ( sqrt ` ( normop ` T ) ) .op u ) )
20 19 ad2ant2lr 
 |-  ( ( ( T =/= 0hop /\ u e. HrmOp ) /\ ( 0hop <_op u /\ ( u o. u ) = R ) ) -> 0hop <_op ( ( sqrt ` ( normop ` T ) ) .op u ) )
21 hmopf 
 |-  ( u e. HrmOp -> u : ~H --> ~H )
22 11 recni 
 |-  ( sqrt ` ( normop ` T ) ) e. CC
23 homulcl 
 |-  ( ( ( sqrt ` ( normop ` T ) ) e. CC /\ u : ~H --> ~H ) -> ( ( sqrt ` ( normop ` T ) ) .op u ) : ~H --> ~H )
24 22 23 mpan 
 |-  ( u : ~H --> ~H -> ( ( sqrt ` ( normop ` T ) ) .op u ) : ~H --> ~H )
25 homco1 
 |-  ( ( ( sqrt ` ( normop ` T ) ) e. CC /\ u : ~H --> ~H /\ ( ( sqrt ` ( normop ` T ) ) .op u ) : ~H --> ~H ) -> ( ( ( sqrt ` ( normop ` T ) ) .op u ) o. ( ( sqrt ` ( normop ` T ) ) .op u ) ) = ( ( sqrt ` ( normop ` T ) ) .op ( u o. ( ( sqrt ` ( normop ` T ) ) .op u ) ) ) )
26 22 25 mp3an1 
 |-  ( ( u : ~H --> ~H /\ ( ( sqrt ` ( normop ` T ) ) .op u ) : ~H --> ~H ) -> ( ( ( sqrt ` ( normop ` T ) ) .op u ) o. ( ( sqrt ` ( normop ` T ) ) .op u ) ) = ( ( sqrt ` ( normop ` T ) ) .op ( u o. ( ( sqrt ` ( normop ` T ) ) .op u ) ) ) )
27 21 24 26 syl2anc2 
 |-  ( u e. HrmOp -> ( ( ( sqrt ` ( normop ` T ) ) .op u ) o. ( ( sqrt ` ( normop ` T ) ) .op u ) ) = ( ( sqrt ` ( normop ` T ) ) .op ( u o. ( ( sqrt ` ( normop ` T ) ) .op u ) ) ) )
28 hmoplin 
 |-  ( u e. HrmOp -> u e. LinOp )
29 homco2 
 |-  ( ( ( sqrt ` ( normop ` T ) ) e. CC /\ u e. LinOp /\ u : ~H --> ~H ) -> ( u o. ( ( sqrt ` ( normop ` T ) ) .op u ) ) = ( ( sqrt ` ( normop ` T ) ) .op ( u o. u ) ) )
30 22 29 mp3an1 
 |-  ( ( u e. LinOp /\ u : ~H --> ~H ) -> ( u o. ( ( sqrt ` ( normop ` T ) ) .op u ) ) = ( ( sqrt ` ( normop ` T ) ) .op ( u o. u ) ) )
31 28 21 30 syl2anc 
 |-  ( u e. HrmOp -> ( u o. ( ( sqrt ` ( normop ` T ) ) .op u ) ) = ( ( sqrt ` ( normop ` T ) ) .op ( u o. u ) ) )
32 31 oveq2d 
 |-  ( u e. HrmOp -> ( ( sqrt ` ( normop ` T ) ) .op ( u o. ( ( sqrt ` ( normop ` T ) ) .op u ) ) ) = ( ( sqrt ` ( normop ` T ) ) .op ( ( sqrt ` ( normop ` T ) ) .op ( u o. u ) ) ) )
33 fco 
 |-  ( ( u : ~H --> ~H /\ u : ~H --> ~H ) -> ( u o. u ) : ~H --> ~H )
34 21 21 33 syl2anc 
 |-  ( u e. HrmOp -> ( u o. u ) : ~H --> ~H )
35 homulass 
 |-  ( ( ( sqrt ` ( normop ` T ) ) e. CC /\ ( sqrt ` ( normop ` T ) ) e. CC /\ ( u o. u ) : ~H --> ~H ) -> ( ( ( sqrt ` ( normop ` T ) ) x. ( sqrt ` ( normop ` T ) ) ) .op ( u o. u ) ) = ( ( sqrt ` ( normop ` T ) ) .op ( ( sqrt ` ( normop ` T ) ) .op ( u o. u ) ) ) )
36 22 22 35 mp3an12 
 |-  ( ( u o. u ) : ~H --> ~H -> ( ( ( sqrt ` ( normop ` T ) ) x. ( sqrt ` ( normop ` T ) ) ) .op ( u o. u ) ) = ( ( sqrt ` ( normop ` T ) ) .op ( ( sqrt ` ( normop ` T ) ) .op ( u o. u ) ) ) )
37 34 36 syl 
 |-  ( u e. HrmOp -> ( ( ( sqrt ` ( normop ` T ) ) x. ( sqrt ` ( normop ` T ) ) ) .op ( u o. u ) ) = ( ( sqrt ` ( normop ` T ) ) .op ( ( sqrt ` ( normop ` T ) ) .op ( u o. u ) ) ) )
38 2 sqrtthi 
 |-  ( 0 <_ ( normop ` T ) -> ( ( sqrt ` ( normop ` T ) ) x. ( sqrt ` ( normop ` T ) ) ) = ( normop ` T ) )
39 9 38 ax-mp 
 |-  ( ( sqrt ` ( normop ` T ) ) x. ( sqrt ` ( normop ` T ) ) ) = ( normop ` T )
40 39 oveq1i 
 |-  ( ( ( sqrt ` ( normop ` T ) ) x. ( sqrt ` ( normop ` T ) ) ) .op ( u o. u ) ) = ( ( normop ` T ) .op ( u o. u ) )
41 37 40 eqtr3di 
 |-  ( u e. HrmOp -> ( ( sqrt ` ( normop ` T ) ) .op ( ( sqrt ` ( normop ` T ) ) .op ( u o. u ) ) ) = ( ( normop ` T ) .op ( u o. u ) ) )
42 27 32 41 3eqtrd 
 |-  ( u e. HrmOp -> ( ( ( sqrt ` ( normop ` T ) ) .op u ) o. ( ( sqrt ` ( normop ` T ) ) .op u ) ) = ( ( normop ` T ) .op ( u o. u ) ) )
43 42 ad2antlr 
 |-  ( ( ( T =/= 0hop /\ u e. HrmOp ) /\ ( u o. u ) = R ) -> ( ( ( sqrt ` ( normop ` T ) ) .op u ) o. ( ( sqrt ` ( normop ` T ) ) .op u ) ) = ( ( normop ` T ) .op ( u o. u ) ) )
44 id 
 |-  ( ( u o. u ) = R -> ( u o. u ) = R )
45 44 4 eqtrdi 
 |-  ( ( u o. u ) = R -> ( u o. u ) = ( ( 1 / ( normop ` T ) ) .op T ) )
46 45 oveq2d 
 |-  ( ( u o. u ) = R -> ( ( normop ` T ) .op ( u o. u ) ) = ( ( normop ` T ) .op ( ( 1 / ( normop ` T ) ) .op T ) ) )
47 hmoplin 
 |-  ( T e. HrmOp -> T e. LinOp )
48 1 47 ax-mp 
 |-  T e. LinOp
49 nmlnopne0 
 |-  ( T e. LinOp -> ( ( normop ` T ) =/= 0 <-> T =/= 0hop ) )
50 48 49 ax-mp 
 |-  ( ( normop ` T ) =/= 0 <-> T =/= 0hop )
51 2 recni 
 |-  ( normop ` T ) e. CC
52 51 recidzi 
 |-  ( ( normop ` T ) =/= 0 -> ( ( normop ` T ) x. ( 1 / ( normop ` T ) ) ) = 1 )
53 50 52 sylbir 
 |-  ( T =/= 0hop -> ( ( normop ` T ) x. ( 1 / ( normop ` T ) ) ) = 1 )
54 53 oveq1d 
 |-  ( T =/= 0hop -> ( ( ( normop ` T ) x. ( 1 / ( normop ` T ) ) ) .op T ) = ( 1 .op T ) )
55 2 rerecclzi 
 |-  ( ( normop ` T ) =/= 0 -> ( 1 / ( normop ` T ) ) e. RR )
56 50 55 sylbir 
 |-  ( T =/= 0hop -> ( 1 / ( normop ` T ) ) e. RR )
57 56 recnd 
 |-  ( T =/= 0hop -> ( 1 / ( normop ` T ) ) e. CC )
58 homulass 
 |-  ( ( ( normop ` T ) e. CC /\ ( 1 / ( normop ` T ) ) e. CC /\ T : ~H --> ~H ) -> ( ( ( normop ` T ) x. ( 1 / ( normop ` T ) ) ) .op T ) = ( ( normop ` T ) .op ( ( 1 / ( normop ` T ) ) .op T ) ) )
59 51 7 58 mp3an13 
 |-  ( ( 1 / ( normop ` T ) ) e. CC -> ( ( ( normop ` T ) x. ( 1 / ( normop ` T ) ) ) .op T ) = ( ( normop ` T ) .op ( ( 1 / ( normop ` T ) ) .op T ) ) )
60 57 59 syl 
 |-  ( T =/= 0hop -> ( ( ( normop ` T ) x. ( 1 / ( normop ` T ) ) ) .op T ) = ( ( normop ` T ) .op ( ( 1 / ( normop ` T ) ) .op T ) ) )
61 homulid2 
 |-  ( T : ~H --> ~H -> ( 1 .op T ) = T )
62 7 61 mp1i 
 |-  ( T =/= 0hop -> ( 1 .op T ) = T )
63 54 60 62 3eqtr3d 
 |-  ( T =/= 0hop -> ( ( normop ` T ) .op ( ( 1 / ( normop ` T ) ) .op T ) ) = T )
64 46 63 sylan9eqr 
 |-  ( ( T =/= 0hop /\ ( u o. u ) = R ) -> ( ( normop ` T ) .op ( u o. u ) ) = T )
65 64 adantlr 
 |-  ( ( ( T =/= 0hop /\ u e. HrmOp ) /\ ( u o. u ) = R ) -> ( ( normop ` T ) .op ( u o. u ) ) = T )
66 43 65 eqtrd 
 |-  ( ( ( T =/= 0hop /\ u e. HrmOp ) /\ ( u o. u ) = R ) -> ( ( ( sqrt ` ( normop ` T ) ) .op u ) o. ( ( sqrt ` ( normop ` T ) ) .op u ) ) = T )
67 66 adantrl 
 |-  ( ( ( T =/= 0hop /\ u e. HrmOp ) /\ ( 0hop <_op u /\ ( u o. u ) = R ) ) -> ( ( ( sqrt ` ( normop ` T ) ) .op u ) o. ( ( sqrt ` ( normop ` T ) ) .op u ) ) = T )
68 breq2 
 |-  ( v = ( ( sqrt ` ( normop ` T ) ) .op u ) -> ( 0hop <_op v <-> 0hop <_op ( ( sqrt ` ( normop ` T ) ) .op u ) ) )
69 coeq1 
 |-  ( v = ( ( sqrt ` ( normop ` T ) ) .op u ) -> ( v o. v ) = ( ( ( sqrt ` ( normop ` T ) ) .op u ) o. v ) )
70 coeq2 
 |-  ( v = ( ( sqrt ` ( normop ` T ) ) .op u ) -> ( ( ( sqrt ` ( normop ` T ) ) .op u ) o. v ) = ( ( ( sqrt ` ( normop ` T ) ) .op u ) o. ( ( sqrt ` ( normop ` T ) ) .op u ) ) )
71 69 70 eqtrd 
 |-  ( v = ( ( sqrt ` ( normop ` T ) ) .op u ) -> ( v o. v ) = ( ( ( sqrt ` ( normop ` T ) ) .op u ) o. ( ( sqrt ` ( normop ` T ) ) .op u ) ) )
72 71 eqeq1d 
 |-  ( v = ( ( sqrt ` ( normop ` T ) ) .op u ) -> ( ( v o. v ) = T <-> ( ( ( sqrt ` ( normop ` T ) ) .op u ) o. ( ( sqrt ` ( normop ` T ) ) .op u ) ) = T ) )
73 68 72 anbi12d 
 |-  ( v = ( ( sqrt ` ( normop ` T ) ) .op u ) -> ( ( 0hop <_op v /\ ( v o. v ) = T ) <-> ( 0hop <_op ( ( sqrt ` ( normop ` T ) ) .op u ) /\ ( ( ( sqrt ` ( normop ` T ) ) .op u ) o. ( ( sqrt ` ( normop ` T ) ) .op u ) ) = T ) ) )
74 73 rspcev 
 |-  ( ( ( ( sqrt ` ( normop ` T ) ) .op u ) e. HrmOp /\ ( 0hop <_op ( ( sqrt ` ( normop ` T ) ) .op u ) /\ ( ( ( sqrt ` ( normop ` T ) ) .op u ) o. ( ( sqrt ` ( normop ` T ) ) .op u ) ) = T ) ) -> E. v e. HrmOp ( 0hop <_op v /\ ( v o. v ) = T ) )
75 14 20 67 74 syl12anc 
 |-  ( ( ( T =/= 0hop /\ u e. HrmOp ) /\ ( 0hop <_op u /\ ( u o. u ) = R ) ) -> E. v e. HrmOp ( 0hop <_op v /\ ( v o. v ) = T ) )
76 75 5 r19.29a 
 |-  ( T =/= 0hop -> E. v e. HrmOp ( 0hop <_op v /\ ( v o. v ) = T ) )