Theorem strlem1 10172

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)(normh` u) = 1)

Distinct variable groups:   u,A   u,B

Proof of Theorem strlem1

Step	Hyp	Ref	Expression
1		ssdif0 2331	. . . 4 |- (A (_ B <-> (A \ B) = (/))
2	1	negbii 187	. . 3 |- (-. A (_ B <-> -. (A \ B) = (/))
3		n0 2293	. . 3 |- (-. (A \ B) = (/) <-> E.x x e. (A \ B))
4	2, 3	bitr 173	. 2 |- (-. A (_ B <-> E.x x e. (A \ B))
5		fveq2 3730	. . . . . 6 |- (u = ((1 / (normh` x)) .h x) -> (normh` u) = (normh` ((1 / (normh` x)) .h x)))
6	5	eqeq1d 1486	. . . . 5 |- (u = ((1 / (normh` x)) .h x) -> ((normh` u) = 1 <-> (normh` ((1 / (normh` x)) .h x)) = 1))
7	6	rcla4ev 1880	. . . 4 |- ((((1 / (normh` x)) .h x) e. (A \ B) /\ (normh` ((1 / (normh` x)) .h x)) = 1) -> E.u e. (A \ B)(normh` u) = 1)
8		rerecclt 5805	. . . . . . . . . 10 |- (((normh` x) e. RR /\ (normh` x) =/= 0) -> (1 / (normh` x)) e. RR)
9		eldifi 2165	. . . . . . . . . . 11 |- (x e. (A \ B) -> x e. A)
10		strlem1.1	. . . . . . . . . . . 12 |- A e. CH
11	10	chel 9097	. . . . . . . . . . 11 |- (x e. A -> x e. H~)
12		normclt 8986	. . . . . . . . . . 11 |- (x e. H~ -> (normh` x) e. RR)
13	9, 11, 12	3syl 20	. . . . . . . . . 10 |- (x e. (A \ B) -> (normh` x) e. RR)
14		strlem1.2	. . . . . . . . . . . . . . . 16 |- B e. CH
15		ch0 9093	. . . . . . . . . . . . . . . 16 |- (B e. CH -> 0h e. B)
16	14, 15	ax-mp 7	. . . . . . . . . . . . . . 15 |- 0h e. B
17		eldifn 2166	. . . . . . . . . . . . . . 15 |- (0h e. (A \ B) -> -. 0h e. B)
18	16, 17	mt2 109	. . . . . . . . . . . . . 14 |- -. 0h e. (A \ B)
19		eleq1 1537	. . . . . . . . . . . . . 14 |- (x = 0h -> (x e. (A \ B) <-> 0h e. (A \ B)))
20	18, 19	mtbiri 719	. . . . . . . . . . . . 13 |- (x = 0h -> -. x e. (A \ B))
21	20	con2i 97	. . . . . . . . . . . 12 |- (x e. (A \ B) -> -. x = 0h)
22		norm-it 8991	. . . . . . . . . . . . 13 |- (x e. H~ -> ((normh` x) = 0 <-> x = 0h))
23	9, 11, 22	3syl 20	. . . . . . . . . . . 12 |- (x e. (A \ B) -> ((normh` x) = 0 <-> x = 0h))
24	21, 23	mtbird 717	. . . . . . . . . . 11 |- (x e. (A \ B) -> -. (normh` x) = 0)
25		df-ne 1590	. . . . . . . . . . 11 |- ((normh` x) =/= 0 <-> -. (normh` x) = 0)
26	24, 25	sylibr 200	. . . . . . . . . 10 |- (x e. (A \ B) -> (normh` x) =/= 0)
27	8, 13, 26	sylanc 473	. . . . . . . . 9 |- (x e. (A \ B) -> (1 / (normh` x)) e. RR)
28	27	recnd 5327	. . . . . . . 8 |- (x e. (A \ B) -> (1 / (normh` x)) e. CC)
29	10	chshi 9092	. . . . . . . . . 10 |- A e. SH
30		shmulcltOLD 9083	. . . . . . . . . 10 |- (A e. SH -> (((1 / (normh` x)) e. CC /\ x e. A) -> ((1 / (normh` x)) .h x) e. A))
31	29, 30	ax-mp 7	. . . . . . . . 9 |- (((1 / (normh` x)) e. CC /\ x e. A) -> ((1 / (normh` x)) .h x) e. A)
32	31	ex 373	. . . . . . . 8 |- ((1 / (normh` x)) e. CC -> (x e. A -> ((1 / (normh` x)) .h x) e. A))
33	28, 32	syl 10	. . . . . . 7 |- (x e. (A \ B) -> (x e. A -> ((1 / (normh` x)) .h x) e. A))
34	13	recnd 5327	. . . . . . . . . 10 |- (x e. (A \ B) -> (normh` x) e. CC)
35	14	chshi 9092	. . . . . . . . . . . 12 |- B e. SH
36		shmulcltOLD 9083	. . . . . . . . . . . 12 |- (B e. SH -> (((normh` x) e. CC /\ ((1 / (normh` x)) .h x) e. B) -> ((normh` x) .h ((1 / (normh` x)) .h x)) e. B))
37	35, 36	ax-mp 7	. . . . . . . . . . 11 |- (((normh` x) e. CC /\ ((1 / (normh` x)) .h x) e. B) -> ((normh` x) .h ((1 / (normh` x)) .h x)) e. B)
38	37	ex 373	. . . . . . . . . 10 |- ((normh` x) e. CC -> (((1 / (normh` x)) .h x) e. B -> ((normh` x) .h ((1 / (normh` x)) .h x)) e. B))
39	34, 38	syl 10	. . . . . . . . 9 |- (x e. (A \ B) -> (((1 / (normh` x)) .h x) e. B -> ((normh` x) .h ((1 / (normh` x)) .h x)) e. B))
40		recidt 5742	. . . . . . . . . . . . 13 |- (((normh` x) e. CC /\ (normh` x) =/= 0) -> ((normh` x) x. (1 / (normh` x))) = 1)
41	40, 34, 26	sylanc 473	. . . . . . . . . . . 12 |- (x e. (A \ B) -> ((normh` x) x. (1 / (normh` x))) = 1)
42	41	opreq1d 3981	. . . . . . . . . . 11 |- (x e. (A \ B) -> (((normh` x) x. (1 / (normh` x))) .h x) = (1 .h x))
43		ax-hvmulass 8872	. . . . . . . . . . . 12 |- (((normh` x) e. CC /\ (1 / (normh` x)) e. CC /\ x e. H~) -> (((normh` x) x. (1 / (normh` x))) .h x) = ((normh` x) .h ((1 / (normh` x)) .h x)))
44	9, 11	syl 10	. . . . . . . . . . . 12 |- (x e. (A \ B) -> x e. H~)
45	43, 34, 28, 44	syl3anc 860	. . . . . . . . . . 11 |- (x e. (A \ B) -> (((normh` x) x. (1 / (normh` x))) .h x) = ((normh` x) .h ((1 / (normh` x)) .h x)))
46		ax-hvmulid 8871	. . . . . . . . . . . 12 |- (x e. H~ -> (1 .h x) = x)
47	9, 11, 46	3syl 20	. . . . . . . . . . 11 |- (x e. (A \ B) -> (1 .h x) = x)
48	42, 45, 47	3eqtr3d 1518	. . . . . . . . . 10 |- (x e. (A \ B) -> ((normh` x) .h ((1 / (normh` x)) .h x)) = x)
49	48	eleq1d 1543	. . . . . . . . 9 |- (x e. (A \ B) -> (((normh` x) .h ((1 / (normh` x)) .h x)) e. B <-> x e. B))
50	39, 49	sylibd 202	. . . . . . . 8 |- (x e. (A \ B) -> (((1 / (normh` x)) .h x) e. B -> x e. B))
51	50	con3d 95	. . . . . . 7 |- (x e. (A \ B) -> (-. x e. B -> -. ((1 / (normh` x)) .h x) e. B))
52	33, 51	anim12d 560	. . . . . 6 |- (x e. (A \ B) -> ((x e. A /\ -. x e. B) -> (((1 / (normh` x)) .h x) e. A /\ -. ((1 / (normh` x)) .h x) e. B)))
53		eldif 2060	. . . . . 6 |- (x e. (A \ B) <-> (x e. A /\ -. x e. B))
54		eldif 2060	. . . . . 6 |- (((1 / (normh` x)) .h x) e. (A \ B) <-> (((1 / (normh` x)) .h x) e. A /\ -. ((1 / (normh` x)) .h x) e. B))
55	52, 53, 54	3imtr4g 555	. . . . 5 |- (x e. (A \ B) -> (x e. (A \ B) -> ((1 / (normh` x)) .h x) e. (A \ B)))
56	55	pm2.43i 64	. . . 4 |- (x e. (A \ B) -> ((1 / (normh` x)) .h x) e. (A \ B))
57		norm-iiit 9002	. . . . . 6 |- (((1 / (normh` x)) e. CC /\ x e. H~) -> (normh` ((1 / (normh` x)) .h x)) = ((abs` (1 / (normh` x))) x. (normh` x)))
58	57, 28, 44	sylanc 473	. . . . 5 |- (x e. (A \ B) -> (normh` ((1 / (normh` x)) .h x)) = ((abs` (1 / (normh` x))) x. (normh` x)))
59		absidt 6862	. . . . . . 7 |- (((1 / (normh` x)) e. RR /\ 0 <_ (1 / (normh` x))) -> (abs` (1 / (normh` x))) = (1 / (normh` x)))
60		1re 5447	. . . . . . . . 9 |- 1 e. RR
61		0re 5452	. . . . . . . . . 10 |- 0 e. RR
62		lt01 5692	. . . . . . . . . 10 |- 0 < 1
63	61, 60, 62	ltlei 5593	. . . . . . . . 9 |- 0 <_ 1
64		divge0t 5858	. . . . . . . . 9 |- (((1 e. RR /\ 0 <_ 1) /\ ((normh` x) e. RR /\ 0 < (normh` x))) -> 0 <_ (1 / (normh` x)))
65	60, 63, 64	mpanl12 710	. . . . . . . 8 |- (((normh` x) e. RR /\ 0 < (normh` x)) -> 0 <_ (1 / (normh` x)))
66	20	necon2ai 1614	. . . . . . . . 9 |- (x e. (A \ B) -> x =/= 0h)
67		normgt0t 8989	. . . . . . . . . 10 |- (x e. H~ -> (x =/= 0h <-> 0 < (normh` x)))
68	44, 67	syl 10	. . . . . . . . 9 |- (x e. (A \ B) -> (x =/= 0h <-> 0 < (normh` x)))
69	66, 68	mpbid 195	. . . . . . . 8 |- (x e. (A \ B) -> 0 < (normh` x))
70	65, 13, 69	sylanc 473	. . . . . . 7 |- (x e. (A \ B) -> 0 <_ (1 / (normh` x