Theorem strlem1 5691

Description: Lemma for strong state theorem: if closed subspace A is not contained in B, there is a unit vector u in their difference.

Hypotheses

Ref	Expression
strlem1.1	|- A e. CH
strlem1.2	|- B e. CH

Assertion

Ref	Expression
strlem1	|- (-. A (_ B -> E.u e. (A \ B)(norm` u) = 1)

Distinct variable group(s):   u,A   u,B

Proof of Theorem strlem1

Step	Hyp	Ref	Expression
1		ssdif0 1748	. . . 4 |- (A (_ B <-> (A \ B) = (/))
2	1	negbii 162	. . 3 |- (-. A (_ B <-> -. (A \ B) = (/))
3		n0 1714	. . 3 |- (-. (A \ B) = (/) <-> E.x x e. (A \ B))
4	2, 3	bitr 151	. 2 |- (-. A (_ B <-> E.x x e. (A \ B))
5		fveq2 2832	. . . . . 6 |- (u = ((1 / (norm` x)) .s x) -> (norm` u) = (norm` ((1 / (norm` x)) .s x)))
6	5	cleq1d 1109	. . . . 5 |- (u = ((1 / (norm` x)) .s x) -> ((norm` u) = 1 <-> (norm` ((1 / (norm` x)) .s x)) = 1))
7	6	rcla4ev 1403	. . . 4 |- ((((1 / (norm` x)) .s x) e. (A \ B) /\ (norm` ((1 / (norm` x)) .s x)) = 1) -> E.u e. (A \ B)(norm` u) = 1)
8		ax1re 4064	. . . . . . . . . . 11 |- 1 e. RR
9		redivclt 4276	. . . . . . . . . . 11 |- (((1 e. RR /\ (norm` x) e. RR) /\ (norm` x) =/= 0) -> (1 / (norm` x)) e. RR)
10	8, 9	mpan11 529	. . . . . . . . . 10 |- (((norm` x) e. RR /\ (norm` x) =/= 0) -> (1 / (norm` x)) e. RR)
11		eldifi 1591	. . . . . . . . . . 11 |- (x e. (A \ B) -> x e. A)
12		strlem1.1	. . . . . . . . . . . 12 |- A e. CH
13	12	chel 5137	. . . . . . . . . . 11 |- (x e. A -> x e. H~)
14		normclt 5076	. . . . . . . . . . 11 |- (x e. H~ -> (norm` x) e. RR)
15	11, 13, 14	3syl 21	. . . . . . . . . 10 |- (x e. (A \ B) -> (norm` x) e. RR)
16		strlem1.2	. . . . . . . . . . . . . . . 16 |- B e. CH
17		ch0 5133	. . . . . . . . . . . . . . . 16 |- (B e. CH -> 0v e. B)
18	16, 17	ax-mp 6	. . . . . . . . . . . . . . 15 |- 0v e. B
19		eldifn 1592	. . . . . . . . . . . . . . 15 |- (0v e. (A \ B) -> -. 0v e. B)
20	18, 19	mt2 96	. . . . . . . . . . . . . 14 |- -. 0v e. (A \ B)
21		eleq1 1149	. . . . . . . . . . . . . 14 |- (x = 0v -> (x e. (A \ B) <-> 0v e. (A \ B)))
22	20, 21	mtbiri 539	. . . . . . . . . . . . 13 |- (x = 0v -> -. x e. (A \ B))
23	22	con2i 89	. . . . . . . . . . . 12 |- (x e. (A \ B) -> -. x = 0v)
24		norm-it 5080	. . . . . . . . . . . . 13 |- (x e. H~ -> ((norm` x) = 0 <-> x = 0v))
25	11, 13, 24	3syl 21	. . . . . . . . . . . 12 |- (x e. (A \ B) -> ((norm` x) = 0 <-> x = 0v))
26	23, 25	mtbird 537	. . . . . . . . . . 11 |- (x e. (A \ B) -> -. (norm` x) = 0)
27		df-ne 1192	. . . . . . . . . . 11 |- ((norm` x) =/= 0 <-> -. (norm` x) = 0)
28	26, 27	sylibr 175	. . . . . . . . . 10 |- (x e. (A \ B) -> (norm` x) =/= 0)
29	10, 15, 28	sylanc 361	. . . . . . . . 9 |- (x e. (A \ B) -> (1 / (norm` x)) e. RR)
30	29	recnd 4099	. . . . . . . 8 |- (x e. (A \ B) -> (1 / (norm` x)) e. CC)
31	12	chshi 5132	. . . . . . . . . 10 |- A e. SH
32		shmulclt 5124	. . . . . . . . . 10 |- (A e. SH -> (((1 / (norm` x)) e. CC /\ x e. A) -> ((1 / (norm` x)) .s x) e. A))
33	31, 32	ax-mp 6	. . . . . . . . 9 |- (((1 / (norm` x)) e. CC /\ x e. A) -> ((1 / (norm` x)) .s x) e. A)
34	33	exp 291	. . . . . . . 8 |- ((1 / (norm` x)) e. CC -> (x e. A -> ((1 / (norm` x)) .s x) e. A))
35	30, 34	syl 12	. . . . . . 7 |- (x e. (A \ B) -> (x e. A -> ((1 / (norm` x)) .s x) e. A))
36	15	recnd 4099	. . . . . . . . . 10 |- (x e. (A \ B) -> (norm` x) e. CC)
37	16	chshi 5132	. . . . . . . . . . . 12 |- B e. SH
38		shmulclt 5124	. . . . . . . . . . . 12 |- (B e. SH -> (((norm` x) e. CC /\ ((1 / (norm` x)) .s x) e. B) -> ((norm` x) .s ((1 / (norm` x)) .s x)) e. B))
39	37, 38	ax-mp 6	. . . . . . . . . . 11 |- (((norm` x) e. CC /\ ((1 / (norm` x)) .s x) e. B) -> ((norm` x) .s ((1 / (norm` x)) .s x)) e. B)
40	39	exp 291	. . . . . . . . . 10 |- ((norm` x) e. CC -> (((1 / (norm` x)) .s x) e. B -> ((norm` x) .s ((1 / (norm` x)) .s x)) e. B))
41	36, 40	syl 12	. . . . . . . . 9 |- (x e. (A \ B) -> (((1 / (norm` x)) .s x) e. B -> ((norm` x) .s ((1 / (norm` x)) .s x)) e. B))
42		recidt 4235	. . . . . . . . . . . . 13 |- (((norm` x) e. CC /\ (norm` x) =/= 0) -> ((norm` x) x. (1 / (norm` x))) = 1)
43	42, 36, 28	sylanc 361	. . . . . . . . . . . 12 |- (x e. (A \ B) -> ((norm` x) x. (1 / (norm` x))) = 1)
44	43	opreq1d 3012	. . . . . . . . . . 11 |- (x e. (A \ B) -> (((norm` x) x. (1 / (norm` x))) .s x) = (1 .s x))
45		ax-hvmulass 4992	. . . . . . . . . . . 12 |- (((norm` x) e. CC /\ (1 / (norm` x)) e. CC /\ x e. H~) -> (((norm` x) x. (1 / (norm` x))) .s x) = ((norm` x) .s ((1 / (norm` x)) .s x)))
46	11, 13	syl 12	. . . . . . . . . . . 12 |- (x e. (A \ B) -> x e. H~)
47	45, 36, 30, 46	syl3anc 629	. . . . . . . . . . 11 |- (x e. (A \ B) -> (((norm` x) x. (1 / (norm` x))) .s x) = ((norm` x) .s ((1 / (norm` x)) .s x)))
48		ax-hvmulid 4991	. . . . . . . . . . . 12 |- (x e. H~ -> (1 .s x) = x)
49	11, 13, 48	3syl 21	. . . . . . . . . . 11 |- (x e. (A \ B) -> (1 .s x) = x)
50	44, 47, 49	3eqtr3d 1133	. . . . . . . . . 10 |- (x e. (A \ B) -> ((norm` x) .s ((1 / (norm` x)) .s x)) = x)
51	50	eleq1d 1155	. . . . . . . . 9 |- (x e. (A \ B) -> (((norm` x) .s ((1 / (norm` x)) .s x)) e. B <-> x e. B))
52	41, 51	sylibd 177	. . . . . . . 8 |- (x e. (A \ B) -> (((1 / (norm` x)) .s x) e. B -> x e. B))
53	52	con3d 87	. . . . . . 7 |- (x e. (A \ B) -> (-. x e. B -> -. ((1 / (norm` x)) .s x) e. B))
54	35, 53	anim12d 431	. . . . . 6 |- (x e. (A \ B) -> ((x e. A /\ -. x e. B) -> (((1 / (norm` x)) .s x) e. A /\ -. ((1 / (norm` x)) .s x) e. B)))
55		eldif 1496	. . . . . 6 |- (x e. (A \ B) <-> (x e. A /\ -. x e. B))
56		eldif 1496	. . . . . 6 |- (((1 / (norm` x)) .s x) e. (A \ B) <-> (((1 / (norm` x)) .s x) e. A /\ -. ((1 / (norm` x)) .s x) e. B))
57	54, 55, 56	3imtr4g 426	. . . . 5 |- (x e. (A \ B) -> (x e. (A \ B) -> ((1 / (norm` x)) .s x) e. (A \ B)))
58	57	pm2.43i 58	. . . 4 |- (x e. (A \ B) -> ((1 / (norm` x)) .s x) e. (A \ B))
59		norm-iiit 5088	. . . . . 6 |- (((1 / (norm` x)) e. CC /\ x e. H~) -> (norm` ((1 / (norm` x)) .s x)) = ((abs` (1 / (norm` x))) x. (norm` x)))
60	59, 30, 46	sylanc 361	. . . . 5 |- (x e. (A \ B) -> (norm` ((1 / (norm` x)) .s x)) = ((abs` (1 / (norm` x))) x. (norm` x)))
61		absidt 4862	. . . . . . 7 |- ((1 / (norm` x)) e. RR -> (0 <_ (1 / (norm` x)) -> (abs` (1 / (norm` x))) = (1 / (norm` x))))
62		divge0t 4403	. . . . . . . 8 |- ((1 e. RR /\ (norm` x) e. RR) -> ((0 <_ 1 /\ 0 < (norm` x)) -> 0 <_ (1 / (norm` x))))
63	15, 8	jctil 240	. . . . . . . 8 |- (x e. (A \ B) -> (1 e. RR /\ (norm` x) e. RR))
64		normgt0t 5078	. . . . . . . . . . 11 |- (x e. H~ -> (-. x = 0v <-> 0 < (norm` x)))
65	11, 13, 64	3syl 21	. . . . . . . . . 10 |- (x e. (A \ B) -> (-. x = 0v <-> 0 < (norm` x)))
66	23, 65	mpbid 170	. . . . . . . . 9 |- (x e. (A \ B) -> 0 < (norm` x))
67		ax0re 4063	. . . . . . . . . 10 |- 0 e. RR
68		lt01 4377	. . . . . . . . . 10 |- 0 < 1
69	67, 8, 68	ltlei 4303	. . . . . . . . 9 |- 0 <_ 1
70	66, 69	jctil 240	. . . . . . . 8 |- (x e. (A \ B) -> (0 <_ 1 /\ 0 < (norm` x)))
71	62, 63, 70	sylc 62	. . . . . . 7 |- (x e. (A \ B) -> 0 <_ (1 / (norm` x)))
72	61, 29, 71	sylc 62	. . . . . 6 |- (x e. (A \ B) -> (abs` (1 / (norm` x))) = (1 / (norm