opsqrlem1

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

	Ref	Expression
Hypotheses	opsqrlem1.1	$⊢ T \in HrmOp$
	opsqrlem1.2	$⊢ {norm}_{op} (T) \in ℝ$
	opsqrlem1.3	$⊢ 0_{hop} \leq_{op} T$
	opsqrlem1.4	$⊢ R = (\frac{1}{{norm}_{op} (T)}) \cdot_{op} T$
	opsqrlem1.5	$⊢ T \neq 0_{hop} \to \exists u \in HrmOp (0_{hop} \leq_{op} u \land u \circ u = R)$
Assertion	opsqrlem1	$⊢ T \neq 0_{hop} \to \exists v \in HrmOp (0_{hop} \leq_{op} v \land v \circ v = T)$

Proof

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

Metamath Proof Explorer

Theorem opsqrlem1

Proof