Metamath Proof Explorer

Theorem opsqrlem1

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

Ref Expression
Hypotheses opsqrlem1.1 ⊢ 𝑇 ∈ HrmOp
opsqrlem1.2 ⊢ ( normop ‘ 𝑇 ) ∈ ℝ
opsqrlem1.3 ⊢ 0hop ≤op 𝑇
opsqrlem1.4 ⊢ 𝑅 = ( ( 1 / ( normop ‘ 𝑇 ) ) ·op 𝑇 )
opsqrlem1.5 ⊢ ( 𝑇 ≠ 0hop → ∃ 𝑢 ∈ HrmOp ( 0hop ≤op 𝑢 ∧ ( 𝑢 ∘ 𝑢 ) = 𝑅 ) )
Assertion opsqrlem1 ( 𝑇 ≠ 0hop → ∃ 𝑣 ∈ HrmOp ( 0hop ≤op 𝑣 ∧ ( 𝑣 ∘ 𝑣 ) = 𝑇 ) )

Proof

Step Hyp Ref Expression
1 opsqrlem1.1 ⊢ 𝑇 ∈ HrmOp
2 opsqrlem1.2 ⊢ ( normop ‘ 𝑇 ) ∈ ℝ
3 opsqrlem1.3 ⊢ 0hop ≤op 𝑇
4 opsqrlem1.4 ⊢ 𝑅 = ( ( 1 / ( normop ‘ 𝑇 ) ) ·op 𝑇 )
5 opsqrlem1.5 ⊢ ( 𝑇 ≠ 0hop → ∃ 𝑢 ∈ HrmOp ( 0hop ≤op 𝑢 ∧ ( 𝑢 ∘ 𝑢 ) = 𝑅 ) )
6 hmopf ⊢ ( 𝑇 ∈ HrmOp → 𝑇 : ℋ ⟶ ℋ )
7 1 6 ax-mp ⊢ 𝑇 : ℋ ⟶ ℋ
8 nmopge0 ⊢ ( 𝑇 : ℋ ⟶ ℋ → 0 ≤ ( normop ‘ 𝑇 ) )
9 7 8 ax-mp ⊢ 0 ≤ ( normop ‘ 𝑇 )
10 2 sqrtcli ⊢ ( 0 ≤ ( normop ‘ 𝑇 ) → ( √ ‘ ( normop ‘ 𝑇 ) ) ∈ ℝ )
11 9 10 ax-mp ⊢ ( √ ‘ ( normop ‘ 𝑇 ) ) ∈ ℝ
12 hmopm ⊢ ( ( ( √ ‘ ( normop ‘ 𝑇 ) ) ∈ ℝ ∧ 𝑢 ∈ HrmOp ) → ( ( √ ‘ ( normop ‘ 𝑇 ) ) ·op 𝑢 ) ∈ HrmOp )
13 11 12 mpan ⊢ ( 𝑢 ∈ HrmOp → ( ( √ ‘ ( normop ‘ 𝑇 ) ) ·op 𝑢 ) ∈ HrmOp )
14 13 ad2antlr ⊢ ( ( ( 𝑇 ≠ 0hop ∧ 𝑢 ∈ HrmOp ) ∧ ( 0hop ≤op 𝑢 ∧ ( 𝑢 ∘ 𝑢 ) = 𝑅 ) ) → ( ( √ ‘ ( normop ‘ 𝑇 ) ) ·op 𝑢 ) ∈ HrmOp )
15 2 sqrtge0i ⊢ ( 0 ≤ ( normop ‘ 𝑇 ) → 0 ≤ ( √ ‘ ( normop ‘ 𝑇 ) ) )
16 9 15 ax-mp ⊢ 0 ≤ ( √ ‘ ( normop ‘ 𝑇 ) )
17 leopmuli ⊢ ( ( ( ( √ ‘ ( normop ‘ 𝑇 ) ) ∈ ℝ ∧ 𝑢 ∈ HrmOp ) ∧ ( 0 ≤ ( √ ‘ ( normop ‘ 𝑇 ) ) ∧ 0hop ≤op 𝑢 ) ) → 0hop ≤op ( ( √ ‘ ( normop ‘ 𝑇 ) ) ·op 𝑢 ) )
18 16 17 mpanr1 ⊢ ( ( ( ( √ ‘ ( normop ‘ 𝑇 ) ) ∈ ℝ ∧ 𝑢 ∈ HrmOp ) ∧ 0hop ≤op 𝑢 ) → 0hop ≤op ( ( √ ‘ ( normop ‘ 𝑇 ) ) ·op 𝑢 ) )
19 11 18 mpanl1 ⊢ ( ( 𝑢 ∈ HrmOp ∧ 0hop ≤op 𝑢 ) → 0hop ≤op ( ( √ ‘ ( normop ‘ 𝑇 ) ) ·op 𝑢 ) )
20 19 ad2ant2lr ⊢ ( ( ( 𝑇 ≠ 0hop ∧ 𝑢 ∈ HrmOp ) ∧ ( 0hop ≤op 𝑢 ∧ ( 𝑢 ∘ 𝑢 ) = 𝑅 ) ) → 0hop ≤op ( ( √ ‘ ( normop ‘ 𝑇 ) ) ·op 𝑢 ) )
21 hmopf ⊢ ( 𝑢 ∈ HrmOp → 𝑢 : ℋ ⟶ ℋ )
22 11 recni ⊢ ( √ ‘ ( normop ‘ 𝑇 ) ) ∈ ℂ
23 homulcl ⊢ ( ( ( √ ‘ ( normop ‘ 𝑇 ) ) ∈ ℂ ∧ 𝑢 : ℋ ⟶ ℋ ) → ( ( √ ‘ ( normop ‘ 𝑇 ) ) ·op 𝑢 ) : ℋ ⟶ ℋ )
24 22 23 mpan ⊢ ( 𝑢 : ℋ ⟶ ℋ → ( ( √ ‘ ( normop ‘ 𝑇 ) ) ·op 𝑢 ) : ℋ ⟶ ℋ )
25 homco1 ⊢ ( ( ( √ ‘ ( normop ‘ 𝑇 ) ) ∈ ℂ ∧ 𝑢 : ℋ ⟶ ℋ ∧ ( ( √ ‘ ( normop ‘ 𝑇 ) ) ·op 𝑢 ) : ℋ ⟶ ℋ ) → ( ( ( √ ‘ ( normop ‘ 𝑇 ) ) ·op 𝑢 ) ∘ ( ( √ ‘ ( normop ‘ 𝑇 ) ) ·op 𝑢 ) ) = ( ( √ ‘ ( normop ‘ 𝑇 ) ) ·op ( 𝑢 ∘ ( ( √ ‘ ( normop ‘ 𝑇 ) ) ·op 𝑢 ) ) ) )
26 22 25 mp3an1 ⊢ ( ( 𝑢 : ℋ ⟶ ℋ ∧ ( ( √ ‘ ( normop ‘ 𝑇 ) ) ·op 𝑢 ) : ℋ ⟶ ℋ ) → ( ( ( √ ‘ ( normop ‘ 𝑇 ) ) ·op 𝑢 ) ∘ ( ( √ ‘ ( normop ‘ 𝑇 ) ) ·op 𝑢 ) ) = ( ( √ ‘ ( normop ‘ 𝑇 ) ) ·op ( 𝑢 ∘ ( ( √ ‘ ( normop ‘ 𝑇 ) ) ·op 𝑢 ) ) ) )
27 21 24 26 syl2anc2 ⊢ ( 𝑢 ∈ HrmOp → ( ( ( √ ‘ ( normop ‘ 𝑇 ) ) ·op 𝑢 ) ∘ ( ( √ ‘ ( normop ‘ 𝑇 ) ) ·op 𝑢 ) ) = ( ( √ ‘ ( normop ‘ 𝑇 ) ) ·op ( 𝑢 ∘ ( ( √ ‘ ( normop ‘ 𝑇 ) ) ·op 𝑢 ) ) ) )
28 hmoplin ⊢ ( 𝑢 ∈ HrmOp → 𝑢 ∈ LinOp )
29 homco2 ⊢ ( ( ( √ ‘ ( normop ‘ 𝑇 ) ) ∈ ℂ ∧ 𝑢 ∈ LinOp ∧ 𝑢 : ℋ ⟶ ℋ ) → ( 𝑢 ∘ ( ( √ ‘ ( normop ‘ 𝑇 ) ) ·op 𝑢 ) ) = ( ( √ ‘ ( normop ‘ 𝑇 ) ) ·op ( 𝑢 ∘ 𝑢 ) ) )
30 22 29 mp3an1 ⊢ ( ( 𝑢 ∈ LinOp ∧ 𝑢 : ℋ ⟶ ℋ ) → ( 𝑢 ∘ ( ( √ ‘ ( normop ‘ 𝑇 ) ) ·op 𝑢 ) ) = ( ( √ ‘ ( normop ‘ 𝑇 ) ) ·op ( 𝑢 ∘ 𝑢 ) ) )
31 28 21 30 syl2anc ⊢ ( 𝑢 ∈ HrmOp → ( 𝑢 ∘ ( ( √ ‘ ( normop ‘ 𝑇 ) ) ·op 𝑢 ) ) = ( ( √ ‘ ( normop ‘ 𝑇 ) ) ·op ( 𝑢 ∘ 𝑢 ) ) )
32 31 oveq2d ⊢ ( 𝑢 ∈ HrmOp → ( ( √ ‘ ( normop ‘ 𝑇 ) ) ·op ( 𝑢 ∘ ( ( √ ‘ ( normop ‘ 𝑇 ) ) ·op 𝑢 ) ) ) = ( ( √ ‘ ( normop ‘ 𝑇 ) ) ·op ( ( √ ‘ ( normop ‘ 𝑇 ) ) ·op ( 𝑢 ∘ 𝑢 ) ) ) )
33 fco ⊢ ( ( 𝑢 : ℋ ⟶ ℋ ∧ 𝑢 : ℋ ⟶ ℋ ) → ( 𝑢 ∘ 𝑢 ) : ℋ ⟶ ℋ )
34 21 21 33 syl2anc ⊢ ( 𝑢 ∈ HrmOp → ( 𝑢 ∘ 𝑢 ) : ℋ ⟶ ℋ )
35 homulass ⊢ ( ( ( √ ‘ ( normop ‘ 𝑇 ) ) ∈ ℂ ∧ ( √ ‘ ( normop ‘ 𝑇 ) ) ∈ ℂ ∧ ( 𝑢 ∘ 𝑢 ) : ℋ ⟶ ℋ ) → ( ( ( √ ‘ ( normop ‘ 𝑇 ) ) · ( √ ‘ ( normop ‘ 𝑇 ) ) ) ·op ( 𝑢 ∘ 𝑢 ) ) = ( ( √ ‘ ( normop ‘ 𝑇 ) ) ·op ( ( √ ‘ ( normop ‘ 𝑇 ) ) ·op ( 𝑢 ∘ 𝑢 ) ) ) )
36 22 22 35 mp3an12 ⊢ ( ( 𝑢 ∘ 𝑢 ) : ℋ ⟶ ℋ → ( ( ( √ ‘ ( normop ‘ 𝑇 ) ) · ( √ ‘ ( normop ‘ 𝑇 ) ) ) ·op ( 𝑢 ∘ 𝑢 ) ) = ( ( √ ‘ ( normop ‘ 𝑇 ) ) ·op ( ( √ ‘ ( normop ‘ 𝑇 ) ) ·op ( 𝑢 ∘ 𝑢 ) ) ) )
37 34 36 syl ⊢ ( 𝑢 ∈ HrmOp → ( ( ( √ ‘ ( normop ‘ 𝑇 ) ) · ( √ ‘ ( normop ‘ 𝑇 ) ) ) ·op ( 𝑢 ∘ 𝑢 ) ) = ( ( √ ‘ ( normop ‘ 𝑇 ) ) ·op ( ( √ ‘ ( normop ‘ 𝑇 ) ) ·op ( 𝑢 ∘ 𝑢 ) ) ) )
38 2 sqrtthi ⊢ ( 0 ≤ ( normop ‘ 𝑇 ) → ( ( √ ‘ ( normop ‘ 𝑇 ) ) · ( √ ‘ ( normop ‘ 𝑇 ) ) ) = ( normop ‘ 𝑇 ) )
39 9 38 ax-mp ⊢ ( ( √ ‘ ( normop ‘ 𝑇 ) ) · ( √ ‘ ( normop ‘ 𝑇 ) ) ) = ( normop ‘ 𝑇 )
40 39 oveq1i ⊢ ( ( ( √ ‘ ( normop ‘ 𝑇 ) ) · ( √ ‘ ( normop ‘ 𝑇 ) ) ) ·op ( 𝑢 ∘ 𝑢 ) ) = ( ( normop ‘ 𝑇 ) ·op ( 𝑢 ∘ 𝑢 ) )
41 37 40 eqtr3di ⊢ ( 𝑢 ∈ HrmOp → ( ( √ ‘ ( normop ‘ 𝑇 ) ) ·op ( ( √ ‘ ( normop ‘ 𝑇 ) ) ·op ( 𝑢 ∘ 𝑢 ) ) ) = ( ( normop ‘ 𝑇 ) ·op ( 𝑢 ∘ 𝑢 ) ) )
42 27 32 41 3eqtrd ⊢ ( 𝑢 ∈ HrmOp → ( ( ( √ ‘ ( normop ‘ 𝑇 ) ) ·op 𝑢 ) ∘ ( ( √ ‘ ( normop ‘ 𝑇 ) ) ·op 𝑢 ) ) = ( ( normop ‘ 𝑇 ) ·op ( 𝑢 ∘ 𝑢 ) ) )
43 42 ad2antlr ⊢ ( ( ( 𝑇 ≠ 0hop ∧ 𝑢 ∈ HrmOp ) ∧ ( 𝑢 ∘ 𝑢 ) = 𝑅 ) → ( ( ( √ ‘ ( normop ‘ 𝑇 ) ) ·op 𝑢 ) ∘ ( ( √ ‘ ( normop ‘ 𝑇 ) ) ·op 𝑢 ) ) = ( ( normop ‘ 𝑇 ) ·op ( 𝑢 ∘ 𝑢 ) ) )
44 id ⊢ ( ( 𝑢 ∘ 𝑢 ) = 𝑅 → ( 𝑢 ∘ 𝑢 ) = 𝑅 )
45 44 4 eqtrdi ⊢ ( ( 𝑢 ∘ 𝑢 ) = 𝑅 → ( 𝑢 ∘ 𝑢 ) = ( ( 1 / ( normop ‘ 𝑇 ) ) ·op 𝑇 ) )
46 45 oveq2d ⊢ ( ( 𝑢 ∘ 𝑢 ) = 𝑅 → ( ( normop ‘ 𝑇 ) ·op ( 𝑢 ∘ 𝑢 ) ) = ( ( normop ‘ 𝑇 ) ·op ( ( 1 / ( normop ‘ 𝑇 ) ) ·op 𝑇 ) ) )
47 hmoplin ⊢ ( 𝑇 ∈ HrmOp → 𝑇 ∈ LinOp )
48 1 47 ax-mp ⊢ 𝑇 ∈ LinOp
49 nmlnopne0 ⊢ ( 𝑇 ∈ LinOp → ( ( normop ‘ 𝑇 ) ≠ 0 ↔ 𝑇 ≠ 0hop ) )
50 48 49 ax-mp ⊢ ( ( normop ‘ 𝑇 ) ≠ 0 ↔ 𝑇 ≠ 0hop )
51 2 recni ⊢ ( normop ‘ 𝑇 ) ∈ ℂ
52 51 recidzi ⊢ ( ( normop ‘ 𝑇 ) ≠ 0 → ( ( normop ‘ 𝑇 ) · ( 1 / ( normop ‘ 𝑇 ) ) ) = 1 )
53 50 52 sylbir ⊢ ( 𝑇 ≠ 0hop → ( ( normop ‘ 𝑇 ) · ( 1 / ( normop ‘ 𝑇 ) ) ) = 1 )
54 53 oveq1d ⊢ ( 𝑇 ≠ 0hop → ( ( ( normop ‘ 𝑇 ) · ( 1 / ( normop ‘ 𝑇 ) ) ) ·op 𝑇 ) = ( 1 ·op 𝑇 ) )
55 2 rerecclzi ⊢ ( ( normop ‘ 𝑇 ) ≠ 0 → ( 1 / ( normop ‘ 𝑇 ) ) ∈ ℝ )
56 50 55 sylbir ⊢ ( 𝑇 ≠ 0hop → ( 1 / ( normop ‘ 𝑇 ) ) ∈ ℝ )
57 56 recnd ⊢ ( 𝑇 ≠ 0hop → ( 1 / ( normop ‘ 𝑇 ) ) ∈ ℂ )
58 homulass ⊢ ( ( ( normop ‘ 𝑇 ) ∈ ℂ ∧ ( 1 / ( normop ‘ 𝑇 ) ) ∈ ℂ ∧ 𝑇 : ℋ ⟶ ℋ ) → ( ( ( normop ‘ 𝑇 ) · ( 1 / ( normop ‘ 𝑇 ) ) ) ·op 𝑇 ) = ( ( normop ‘ 𝑇 ) ·op ( ( 1 / ( normop ‘ 𝑇 ) ) ·op 𝑇 ) ) )
59 51 7 58 mp3an13 ⊢ ( ( 1 / ( normop ‘ 𝑇 ) ) ∈ ℂ → ( ( ( normop ‘ 𝑇 ) · ( 1 / ( normop ‘ 𝑇 ) ) ) ·op 𝑇 ) = ( ( normop ‘ 𝑇 ) ·op ( ( 1 / ( normop ‘ 𝑇 ) ) ·op 𝑇 ) ) )
60 57 59 syl ⊢ ( 𝑇 ≠ 0hop → ( ( ( normop ‘ 𝑇 ) · ( 1 / ( normop ‘ 𝑇 ) ) ) ·op 𝑇 ) = ( ( normop ‘ 𝑇 ) ·op ( ( 1 / ( normop ‘ 𝑇 ) ) ·op 𝑇 ) ) )
61 homullid ⊢ ( 𝑇 : ℋ ⟶ ℋ → ( 1 ·op 𝑇 ) = 𝑇 )
62 7 61 mp1i ⊢ ( 𝑇 ≠ 0hop → ( 1 ·op 𝑇 ) = 𝑇 )
63 54 60 62 3eqtr3d ⊢ ( 𝑇 ≠ 0hop → ( ( normop ‘ 𝑇 ) ·op ( ( 1 / ( normop ‘ 𝑇 ) ) ·op 𝑇 ) ) = 𝑇 )
64 46 63 sylan9eqr ⊢ ( ( 𝑇 ≠ 0hop ∧ ( 𝑢 ∘ 𝑢 ) = 𝑅 ) → ( ( normop ‘ 𝑇 ) ·op ( 𝑢 ∘ 𝑢 ) ) = 𝑇 )
65 64 adantlr ⊢ ( ( ( 𝑇 ≠ 0hop ∧ 𝑢 ∈ HrmOp ) ∧ ( 𝑢 ∘ 𝑢 ) = 𝑅 ) → ( ( normop ‘ 𝑇 ) ·op ( 𝑢 ∘ 𝑢 ) ) = 𝑇 )
66 43 65 eqtrd ⊢ ( ( ( 𝑇 ≠ 0hop ∧ 𝑢 ∈ HrmOp ) ∧ ( 𝑢 ∘ 𝑢 ) = 𝑅 ) → ( ( ( √ ‘ ( normop ‘ 𝑇 ) ) ·op 𝑢 ) ∘ ( ( √ ‘ ( normop ‘ 𝑇 ) ) ·op 𝑢 ) ) = 𝑇 )
67 66 adantrl ⊢ ( ( ( 𝑇 ≠ 0hop ∧ 𝑢 ∈ HrmOp ) ∧ ( 0hop ≤op 𝑢 ∧ ( 𝑢 ∘ 𝑢 ) = 𝑅 ) ) → ( ( ( √ ‘ ( normop ‘ 𝑇 ) ) ·op 𝑢 ) ∘ ( ( √ ‘ ( normop ‘ 𝑇 ) ) ·op 𝑢 ) ) = 𝑇 )
68 breq2 ⊢ ( 𝑣 = ( ( √ ‘ ( normop ‘ 𝑇 ) ) ·op 𝑢 ) → ( 0hop ≤op 𝑣 ↔ 0hop ≤op ( ( √ ‘ ( normop ‘ 𝑇 ) ) ·op 𝑢 ) ) )
69 coeq1 ⊢ ( 𝑣 = ( ( √ ‘ ( normop ‘ 𝑇 ) ) ·op 𝑢 ) → ( 𝑣 ∘ 𝑣 ) = ( ( ( √ ‘ ( normop ‘ 𝑇 ) ) ·op 𝑢 ) ∘ 𝑣 ) )
70 coeq2 ⊢ ( 𝑣 = ( ( √ ‘ ( normop ‘ 𝑇 ) ) ·op 𝑢 ) → ( ( ( √ ‘ ( normop ‘ 𝑇 ) ) ·op 𝑢 ) ∘ 𝑣 ) = ( ( ( √ ‘ ( normop ‘ 𝑇 ) ) ·op 𝑢 ) ∘ ( ( √ ‘ ( normop ‘ 𝑇 ) ) ·op 𝑢 ) ) )
71 69 70 eqtrd ⊢ ( 𝑣 = ( ( √ ‘ ( normop ‘ 𝑇 ) ) ·op 𝑢 ) → ( 𝑣 ∘ 𝑣 ) = ( ( ( √ ‘ ( normop ‘ 𝑇 ) ) ·op 𝑢 ) ∘ ( ( √ ‘ ( normop ‘ 𝑇 ) ) ·op 𝑢 ) ) )
72 71 eqeq1d ⊢ ( 𝑣 = ( ( √ ‘ ( normop ‘ 𝑇 ) ) ·op 𝑢 ) → ( ( 𝑣 ∘ 𝑣 ) = 𝑇 ↔ ( ( ( √ ‘ ( normop ‘ 𝑇 ) ) ·op 𝑢 ) ∘ ( ( √ ‘ ( normop ‘ 𝑇 ) ) ·op 𝑢 ) ) = 𝑇 ) )
73 68 72 anbi12d ⊢ ( 𝑣 = ( ( √ ‘ ( normop ‘ 𝑇 ) ) ·op 𝑢 ) → ( ( 0hop ≤op 𝑣 ∧ ( 𝑣 ∘ 𝑣 ) = 𝑇 ) ↔ ( 0hop ≤op ( ( √ ‘ ( normop ‘ 𝑇 ) ) ·op 𝑢 ) ∧ ( ( ( √ ‘ ( normop ‘ 𝑇 ) ) ·op 𝑢 ) ∘ ( ( √ ‘ ( normop ‘ 𝑇 ) ) ·op 𝑢 ) ) = 𝑇 ) ) )
74 73 rspcev ⊢ ( ( ( ( √ ‘ ( normop ‘ 𝑇 ) ) ·op 𝑢 ) ∈ HrmOp ∧ ( 0hop ≤op ( ( √ ‘ ( normop ‘ 𝑇 ) ) ·op 𝑢 ) ∧ ( ( ( √ ‘ ( normop ‘ 𝑇 ) ) ·op 𝑢 ) ∘ ( ( √ ‘ ( normop ‘ 𝑇 ) ) ·op 𝑢 ) ) = 𝑇 ) ) → ∃ 𝑣 ∈ HrmOp ( 0hop ≤op 𝑣 ∧ ( 𝑣 ∘ 𝑣 ) = 𝑇 ) )
75 14 20 67 74 syl12anc ⊢ ( ( ( 𝑇 ≠ 0hop ∧ 𝑢 ∈ HrmOp ) ∧ ( 0hop ≤op 𝑢 ∧ ( 𝑢 ∘ 𝑢 ) = 𝑅 ) ) → ∃ 𝑣 ∈ HrmOp ( 0hop ≤op 𝑣 ∧ ( 𝑣 ∘ 𝑣 ) = 𝑇 ) )
76 75 5 r19.29a ⊢ ( 𝑇 ≠ 0hop → ∃ 𝑣 ∈ HrmOp ( 0hop ≤op 𝑣 ∧ ( 𝑣 ∘ 𝑣 ) = 𝑇 ) )