Theorem strlem1

Description: Lemma for strong state theorem: if closed subspace A is not contained in B , there is a unit vector u in their difference. (Contributed by NM, 25-Oct-1999) (New usage is discouraged.)

	Ref	Expression
Hypotheses	strlem1.1	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}$$
	strlem1.2	$$⊢B\in {\mathbf{C}}_{\mathscr{H}}$$
Assertion	strlem1	$$⊢\neg A\subseteq B\to \exists u\in \left(A\setminus B\right){norm}_{ℎ}\left(u\right)=1$$

Proof

Step	Hyp	Ref	Expression
1		strlem1.1	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}$$
2		strlem1.2	$$⊢B\in {\mathbf{C}}_{\mathscr{H}}$$
3		neq0	$$⊢\neg A\setminus B=\varnothing \leftrightarrow \exists xx\in \left(A\setminus B\right)$$
4		ssdif0	$$⊢A\subseteq B\leftrightarrow A\setminus B=\varnothing$$
5	3 4	xchnxbir	$$⊢\neg A\subseteq B\leftrightarrow \exists xx\in \left(A\setminus B\right)$$
6		eldifi	$$⊢x\in \left(A\setminus B\right)\to x\in A$$
7	1	cheli	$$⊢x\in A\to x\in \mathscr{H}$$
8		normcl	$$⊢x\in \mathscr{H}\to {norm}_{ℎ}\left(x\right)\in ℝ$$
9	6 7 8	3syl	$$⊢x\in \left(A\setminus B\right)\to {norm}_{ℎ}\left(x\right)\in ℝ$$
10		ch0	$$⊢B\in {\mathbf{C}}_{\mathscr{H}}\to 0_{ℎ}\in B$$
11	2 10	ax-mp	$$⊢0_{ℎ}\in B$$
12		eldifn	$$⊢0_{ℎ}\in \left(A\setminus B\right)\to \neg 0_{ℎ}\in B$$
13	11 12	mt2	$$⊢\neg 0_{ℎ}\in \left(A\setminus B\right)$$
14		eleq1	$$⊢x=0_{ℎ}\to \left(x\in \left(A\setminus B\right)\leftrightarrow 0_{ℎ}\in \left(A\setminus B\right)\right)$$
15	13 14	mtbiri	$$⊢x=0_{ℎ}\to \neg x\in \left(A\setminus B\right)$$
16	15	con2i	$$⊢x\in \left(A\setminus B\right)\to \neg x=0_{ℎ}$$
17		norm-i	$$⊢x\in \mathscr{H}\to \left({norm}_{ℎ}\left(x\right)=0\leftrightarrow x=0_{ℎ}\right)$$
18	6 7 17	3syl	$$⊢x\in \left(A\setminus B\right)\to \left({norm}_{ℎ}\left(x\right)=0\leftrightarrow x=0_{ℎ}\right)$$
19	16 18	mtbird	$$⊢x\in \left(A\setminus B\right)\to \neg {norm}_{ℎ}\left(x\right)=0$$
20	19	neqned	$$⊢x\in \left(A\setminus B\right)\to {norm}_{ℎ}\left(x\right)\ne 0$$
21	9 20	rereccld	$$⊢x\in \left(A\setminus B\right)\to \frac{1}{{norm}_{ℎ}\left(x\right)}\in ℝ$$
22	21	recnd	$$⊢x\in \left(A\setminus B\right)\to \frac{1}{{norm}_{ℎ}\left(x\right)}\in ℂ$$
23	1	chshii	$$⊢A\in {\mathbf{S}}_{\mathscr{H}}$$
24		shmulcl	$$⊢\left(A\in {\mathbf{S}}_{\mathscr{H}}\wedge \frac{1}{{norm}_{ℎ}\left(x\right)}\in ℂ\wedge x\in A\right)\to \left(\frac{1}{{norm}_{ℎ}\left(x\right)}\right){\cdot }_{ℎ}x\in A$$
25	23 24	mp3an1	$$⊢\left(\frac{1}{{norm}_{ℎ}\left(x\right)}\in ℂ\wedge x\in A\right)\to \left(\frac{1}{{norm}_{ℎ}\left(x\right)}\right){\cdot }_{ℎ}x\in A$$
26	25	ex	$$⊢\frac{1}{{norm}_{ℎ}\left(x\right)}\in ℂ\to \left(x\in A\to \left(\frac{1}{{norm}_{ℎ}\left(x\right)}\right){\cdot }_{ℎ}x\in A\right)$$
27	22 26	syl	$$⊢x\in \left(A\setminus B\right)\to \left(x\in A\to \left(\frac{1}{{norm}_{ℎ}\left(x\right)}\right){\cdot }_{ℎ}x\in A\right)$$
28	9	recnd	$$⊢x\in \left(A\setminus B\right)\to {norm}_{ℎ}\left(x\right)\in ℂ$$
29	2	chshii	$$⊢B\in {\mathbf{S}}_{\mathscr{H}}$$
30		shmulcl	$$⊢\left(B\in {\mathbf{S}}_{\mathscr{H}}\wedge {norm}_{ℎ}\left(x\right)\in ℂ\wedge \left(\frac{1}{{norm}_{ℎ}\left(x\right)}\right){\cdot }_{ℎ}x\in B\right)\to {norm}_{ℎ}\left(x\right){\cdot }_{ℎ}\left(\left(\frac{1}{{norm}_{ℎ}\left(x\right)}\right){\cdot }_{ℎ}x\right)\in B$$
31	29 30	mp3an1	$$⊢\left({norm}_{ℎ}\left(x\right)\in ℂ\wedge \left(\frac{1}{{norm}_{ℎ}\left(x\right)}\right){\cdot }_{ℎ}x\in B\right)\to {norm}_{ℎ}\left(x\right){\cdot }_{ℎ}\left(\left(\frac{1}{{norm}_{ℎ}\left(x\right)}\right){\cdot }_{ℎ}x\right)\in B$$
32	31	ex	$$⊢{norm}_{ℎ}\left(x\right)\in ℂ\to \left(\left(\frac{1}{{norm}_{ℎ}\left(x\right)}\right){\cdot }_{ℎ}x\in B\to {norm}_{ℎ}\left(x\right){\cdot }_{ℎ}\left(\left(\frac{1}{{norm}_{ℎ}\left(x\right)}\right){\cdot }_{ℎ}x\right)\in B\right)$$
33	28 32	syl	$$⊢x\in \left(A\setminus B\right)\to \left(\left(\frac{1}{{norm}_{ℎ}\left(x\right)}\right){\cdot }_{ℎ}x\in B\to {norm}_{ℎ}\left(x\right){\cdot }_{ℎ}\left(\left(\frac{1}{{norm}_{ℎ}\left(x\right)}\right){\cdot }_{ℎ}x\right)\in B\right)$$
34	28 20	recidd	$$⊢x\in \left(A\setminus B\right)\to {norm}_{ℎ}\left(x\right)\left(\frac{1}{{norm}_{ℎ}\left(x\right)}\right)=1$$
35	34	oveq1d	$$⊢x\in \left(A\setminus B\right)\to {norm}_{ℎ}\left(x\right)\left(\frac{1}{{norm}_{ℎ}\left(x\right)}\right){\cdot }_{ℎ}x=1{\cdot }_{ℎ}x$$
36	6 7	syl	$$⊢x\in \left(A\setminus B\right)\to x\in \mathscr{H}$$
37		ax-hvmulass	$$⊢\left({norm}_{ℎ}\left(x\right)\in ℂ\wedge \frac{1}{{norm}_{ℎ}\left(x\right)}\in ℂ\wedge x\in \mathscr{H}\right)\to {norm}_{ℎ}\left(x\right)\left(\frac{1}{{norm}_{ℎ}\left(x\right)}\right){\cdot }_{ℎ}x={norm}_{ℎ}\left(x\right){\cdot }_{ℎ}\left(\left(\frac{1}{{norm}_{ℎ}\left(x\right)}\right){\cdot }_{ℎ}x\right)$$
38	28 22 36 37	syl3anc	$$⊢x\in \left(A\setminus B\right)\to {norm}_{ℎ}\left(x\right)\left(\frac{1}{{norm}_{ℎ}\left(x\right)}\right){\cdot }_{ℎ}x={norm}_{ℎ}\left(x\right){\cdot }_{ℎ}\left(\left(\frac{1}{{norm}_{ℎ}\left(x\right)}\right){\cdot }_{ℎ}x\right)$$
39		ax-hvmulid	$$⊢x\in \mathscr{H}\to 1{\cdot }_{ℎ}x=x$$
40	6 7 39	3syl	$$⊢x\in \left(A\setminus B\right)\to 1{\cdot }_{ℎ}x=x$$
41	35 38 40	3eqtr3d	$$⊢x\in \left(A\setminus B\right)\to {norm}_{ℎ}\left(x\right){\cdot }_{ℎ}\left(\left(\frac{1}{{norm}_{ℎ}\left(x\right)}\right){\cdot }_{ℎ}x\right)=x$$
42	41	eleq1d	$$⊢x\in \left(A\setminus B\right)\to \left({norm}_{ℎ}\left(x\right){\cdot }_{ℎ}\left(\left(\frac{1}{{norm}_{ℎ}\left(x\right)}\right){\cdot }_{ℎ}x\right)\in B\leftrightarrow x\in B\right)$$
43	33 42	sylibd	$$⊢x\in \left(A\setminus B\right)\to \left(\left(\frac{1}{{norm}_{ℎ}\left(x\right)}\right){\cdot }_{ℎ}x\in B\to x\in B\right)$$
44	43	con3d	$$⊢x\in \left(A\setminus B\right)\to \left(\neg x\in B\to \neg \left(\frac{1}{{norm}_{ℎ}\left(x\right)}\right){\cdot }_{ℎ}x\in B\right)$$
45	27 44	anim12d	$$⊢x\in \left(A\setminus B\right)\to \left(\left(x\in A\wedge \neg x\in B\right)\to \left(\left(\frac{1}{{norm}_{ℎ}\left(x\right)}\right){\cdot }_{ℎ}x\in A\wedge \neg \left(\frac{1}{{norm}_{ℎ}\left(x\right)}\right){\cdot }_{ℎ}x\in B\right)\right)$$
46		eldif	$$⊢x\in \left(A\setminus B\right)\leftrightarrow \left(x\in A\wedge \neg x\in B\right)$$
47		eldif	$$⊢\left(\frac{1}{{norm}_{ℎ}\left(x\right)}\right){\cdot }_{ℎ}x\in \left(A\setminus B\right)\leftrightarrow \left(\left(\frac{1}{{norm}_{ℎ}\left(x\right)}\right){\cdot }_{ℎ}x\in A\wedge \neg \left(\frac{1}{{norm}_{ℎ}\left(x\right)}\right){\cdot }_{ℎ}x\in B\right)$$
48	45 46 47	3imtr4g	$$⊢x\in \left(A\setminus B\right)\to \left(x\in \left(A\setminus B\right)\to \left(\frac{1}{{norm}_{ℎ}\left(x\right)}\right){\cdot }_{ℎ}x\in \left(A\setminus B\right)\right)$$
49	48	pm2.43i	$$⊢x\in \left(A\setminus B\right)\to \left(\frac{1}{{norm}_{ℎ}\left(x\right)}\right){\cdot }_{ℎ}x\in \left(A\setminus B\right)$$
50		norm-iii	$$⊢\left(\frac{1}{{norm}_{ℎ}\left(x\right)}\in ℂ\wedge x\in \mathscr{H}\right)\to {norm}_{ℎ}\left(\left(\frac{1}{{norm}_{ℎ}\left(x\right)}\right){\cdot }_{ℎ}x\right)=\left|\frac{1}{{norm}_{ℎ}\left(x\right)}\right|{norm}_{ℎ}\left(x\right)$$
51	22 36 50	syl2anc	$$⊢x\in \left(A\setminus B\right)\to {norm}_{ℎ}\left(\left(\frac{1}{{norm}_{ℎ}\left(x\right)}\right){\cdot }_{ℎ}x\right)=\left|\frac{1}{{norm}_{ℎ}\left(x\right)}\right|{norm}_{ℎ}\left(x\right)$$
52	15	necon2ai	$$⊢x\in \left(A\setminus B\right)\to x\ne 0_{ℎ}$$
53		normgt0	$$⊢x\in \mathscr{H}\to \left(x\ne 0_{ℎ}\leftrightarrow 0<{norm}_{ℎ}\left(x\right)\right)$$
54	6 7 53	3syl	$$⊢x\in \left(A\setminus B\right)\to \left(x\ne 0_{ℎ}\leftrightarrow 0<{norm}_{ℎ}\left(x\right)\right)$$
55	52 54	mpbid	$$⊢x\in \left(A\setminus B\right)\to 0<{norm}_{ℎ}\left(x\right)$$
56		1re	$$⊢1\in ℝ$$
57		0le1	$$⊢0\le 1$$
58		divge0	$$⊢\left(\left(1\in ℝ\wedge 0\le 1\right)\wedge \left({norm}_{ℎ}\left(x\right)\in ℝ\wedge 0<{norm}_{ℎ}\left(x\right)\right)\right)\to 0\le \frac{1}{{norm}_{ℎ}\left(x\right)}$$
59	56 57 58	mpanl12	$$⊢\left({norm}_{ℎ}\left(x\right)\in ℝ\wedge 0<{norm}_{ℎ}\left(x\right)\right)\to 0\le \frac{1}{{norm}_{ℎ}\left(x\right)}$$
60	9 55 59	syl2anc	$$⊢x\in \left(A\setminus B\right)\to 0\le \frac{1}{{norm}_{ℎ}\left(x\right)}$$
61	21 60	absidd	$$⊢x\in \left(A\setminus B\right)\to \left|\frac{1}{{norm}_{ℎ}\left(x\right)}\right|=\frac{1}{{norm}_{ℎ}\left(x\right)}$$
62	61	oveq1d	$$⊢x\in \left(A\setminus B\right)\to \left|\frac{1}{{norm}_{ℎ}\left(x\right)}\right|{norm}_{ℎ}\left(x\right)=\left(\frac{1}{{norm}_{ℎ}\left(x\right)}\right){norm}_{ℎ}\left(x\right)$$
63	28 20	recid2d	$$⊢x\in \left(A\setminus B\right)\to \left(\frac{1}{{norm}_{ℎ}\left(x\right)}\right){norm}_{ℎ}\left(x\right)=1$$
64	51 62 63	3eqtrd	$$⊢x\in \left(A\setminus B\right)\to {norm}_{ℎ}\left(\left(\frac{1}{{norm}_{ℎ}\left(x\right)}\right){\cdot }_{ℎ}x\right)=1$$
65		fveqeq2	$$⊢u=\left(\frac{1}{{norm}_{ℎ}\left(x\right)}\right){\cdot }_{ℎ}x\to \left({norm}_{ℎ}\left(u\right)=1\leftrightarrow {norm}_{ℎ}\left(\left(\frac{1}{{norm}_{ℎ}\left(x\right)}\right){\cdot }_{ℎ}x\right)=1\right)$$
66	65	rspcev	$$⊢\left(\left(\frac{1}{{norm}_{ℎ}\left(x\right)}\right){\cdot }_{ℎ}x\in \left(A\setminus B\right)\wedge {norm}_{ℎ}\left(\left(\frac{1}{{norm}_{ℎ}\left(x\right)}\right){\cdot }_{ℎ}x\right)=1\right)\to \exists u\in \left(A\setminus B\right){norm}_{ℎ}\left(u\right)=1$$
67	49 64 66	syl2anc	$$⊢x\in \left(A\setminus B\right)\to \exists u\in \left(A\setminus B\right){norm}_{ℎ}\left(u\right)=1$$
68	67	exlimiv	$$⊢\exists xx\in \left(A\setminus B\right)\to \exists u\in \left(A\setminus B\right){norm}_{ℎ}\left(u\right)=1$$
69	5 68	sylbi	$$⊢\neg A\subseteq B\to \exists u\in \left(A\setminus B\right){norm}_{ℎ}\left(u\right)=1$$