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	⊢ 𝐴 ∈ Cℋ
	strlem1.2	⊢ 𝐵 ∈ Cℋ
Assertion	strlem1	⊢ ( ¬ 𝐴 ⊆ 𝐵 → ∃ 𝑢 ∈ ( 𝐴 ∖ 𝐵 ) ( normℎ ‘ 𝑢 ) = 1 )

Proof

Step	Hyp	Ref	Expression
1		strlem1.1	⊢ 𝐴 ∈ Cℋ
2		strlem1.2	⊢ 𝐵 ∈ Cℋ
3		neq0	⊢ ( ¬ ( 𝐴 ∖ 𝐵 ) = ∅ ↔ ∃ 𝑥 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) )
4		ssdif0	⊢ ( 𝐴 ⊆ 𝐵 ↔ ( 𝐴 ∖ 𝐵 ) = ∅ )
5	3 4	xchnxbir	⊢ ( ¬ 𝐴 ⊆ 𝐵 ↔ ∃ 𝑥 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) )
6		eldifi	⊢ ( 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) → 𝑥 ∈ 𝐴 )
7	1	cheli	⊢ ( 𝑥 ∈ 𝐴 → 𝑥 ∈ ℋ )
8		normcl	⊢ ( 𝑥 ∈ ℋ → ( normℎ ‘ 𝑥 ) ∈ ℝ )
9	6 7 8	3syl	⊢ ( 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) → ( normℎ ‘ 𝑥 ) ∈ ℝ )
10		ch0	⊢ ( 𝐵 ∈ Cℋ → 0ℎ ∈ 𝐵 )
11	2 10	ax-mp	⊢ 0ℎ ∈ 𝐵
12		eldifn	⊢ ( 0ℎ ∈ ( 𝐴 ∖ 𝐵 ) → ¬ 0ℎ ∈ 𝐵 )
13	11 12	mt2	⊢ ¬ 0ℎ ∈ ( 𝐴 ∖ 𝐵 )
14		eleq1	⊢ ( 𝑥 = 0ℎ → ( 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) ↔ 0ℎ ∈ ( 𝐴 ∖ 𝐵 ) ) )
15	13 14	mtbiri	⊢ ( 𝑥 = 0ℎ → ¬ 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) )
16	15	con2i	⊢ ( 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) → ¬ 𝑥 = 0ℎ )
17		norm-i	⊢ ( 𝑥 ∈ ℋ → ( ( normℎ ‘ 𝑥 ) = 0 ↔ 𝑥 = 0ℎ ) )
18	6 7 17	3syl	⊢ ( 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) → ( ( normℎ ‘ 𝑥 ) = 0 ↔ 𝑥 = 0ℎ ) )
19	16 18	mtbird	⊢ ( 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) → ¬ ( normℎ ‘ 𝑥 ) = 0 )
20	19	neqned	⊢ ( 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) → ( normℎ ‘ 𝑥 ) ≠ 0 )
21	9 20	rereccld	⊢ ( 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) → ( 1 / ( normℎ ‘ 𝑥 ) ) ∈ ℝ )
22	21	recnd	⊢ ( 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) → ( 1 / ( normℎ ‘ 𝑥 ) ) ∈ ℂ )
23	1	chshii	⊢ 𝐴 ∈ Sℋ
24		shmulcl	⊢ ( ( 𝐴 ∈ Sℋ ∧ ( 1 / ( normℎ ‘ 𝑥 ) ) ∈ ℂ ∧ 𝑥 ∈ 𝐴 ) → ( ( 1 / ( normℎ ‘ 𝑥 ) ) ·ℎ 𝑥 ) ∈ 𝐴 )
25	23 24	mp3an1	⊢ ( ( ( 1 / ( normℎ ‘ 𝑥 ) ) ∈ ℂ ∧ 𝑥 ∈ 𝐴 ) → ( ( 1 / ( normℎ ‘ 𝑥 ) ) ·ℎ 𝑥 ) ∈ 𝐴 )
26	25	ex	⊢ ( ( 1 / ( normℎ ‘ 𝑥 ) ) ∈ ℂ → ( 𝑥 ∈ 𝐴 → ( ( 1 / ( normℎ ‘ 𝑥 ) ) ·ℎ 𝑥 ) ∈ 𝐴 ) )
27	22 26	syl	⊢ ( 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) → ( 𝑥 ∈ 𝐴 → ( ( 1 / ( normℎ ‘ 𝑥 ) ) ·ℎ 𝑥 ) ∈ 𝐴 ) )
28	9	recnd	⊢ ( 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) → ( normℎ ‘ 𝑥 ) ∈ ℂ )
29	2	chshii	⊢ 𝐵 ∈ Sℋ
30		shmulcl	⊢ ( ( 𝐵 ∈ Sℋ ∧ ( normℎ ‘ 𝑥 ) ∈ ℂ ∧ ( ( 1 / ( normℎ ‘ 𝑥 ) ) ·ℎ 𝑥 ) ∈ 𝐵 ) → ( ( normℎ ‘ 𝑥 ) ·ℎ ( ( 1 / ( normℎ ‘ 𝑥 ) ) ·ℎ 𝑥 ) ) ∈ 𝐵 )
31	29 30	mp3an1	⊢ ( ( ( normℎ ‘ 𝑥 ) ∈ ℂ ∧ ( ( 1 / ( normℎ ‘ 𝑥 ) ) ·ℎ 𝑥 ) ∈ 𝐵 ) → ( ( normℎ ‘ 𝑥 ) ·ℎ ( ( 1 / ( normℎ ‘ 𝑥 ) ) ·ℎ 𝑥 ) ) ∈ 𝐵 )
32	31	ex	⊢ ( ( normℎ ‘ 𝑥 ) ∈ ℂ → ( ( ( 1 / ( normℎ ‘ 𝑥 ) ) ·ℎ 𝑥 ) ∈ 𝐵 → ( ( normℎ ‘ 𝑥 ) ·ℎ ( ( 1 / ( normℎ ‘ 𝑥 ) ) ·ℎ 𝑥 ) ) ∈ 𝐵 ) )
33	28 32	syl	⊢ ( 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) → ( ( ( 1 / ( normℎ ‘ 𝑥 ) ) ·ℎ 𝑥 ) ∈ 𝐵 → ( ( normℎ ‘ 𝑥 ) ·ℎ ( ( 1 / ( normℎ ‘ 𝑥 ) ) ·ℎ 𝑥 ) ) ∈ 𝐵 ) )
34	28 20	recidd	⊢ ( 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) → ( ( normℎ ‘ 𝑥 ) · ( 1 / ( normℎ ‘ 𝑥 ) ) ) = 1 )
35	34	oveq1d	⊢ ( 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) → ( ( ( normℎ ‘ 𝑥 ) · ( 1 / ( normℎ ‘ 𝑥 ) ) ) ·ℎ 𝑥 ) = ( 1 ·ℎ 𝑥 ) )
36	6 7	syl	⊢ ( 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) → 𝑥 ∈ ℋ )
37		ax-hvmulass	⊢ ( ( ( normℎ ‘ 𝑥 ) ∈ ℂ ∧ ( 1 / ( normℎ ‘ 𝑥 ) ) ∈ ℂ ∧ 𝑥 ∈ ℋ ) → ( ( ( normℎ ‘ 𝑥 ) · ( 1 / ( normℎ ‘ 𝑥 ) ) ) ·ℎ 𝑥 ) = ( ( normℎ ‘ 𝑥 ) ·ℎ ( ( 1 / ( normℎ ‘ 𝑥 ) ) ·ℎ 𝑥 ) ) )
38	28 22 36 37	syl3anc	⊢ ( 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) → ( ( ( normℎ ‘ 𝑥 ) · ( 1 / ( normℎ ‘ 𝑥 ) ) ) ·ℎ 𝑥 ) = ( ( normℎ ‘ 𝑥 ) ·ℎ ( ( 1 / ( normℎ ‘ 𝑥 ) ) ·ℎ 𝑥 ) ) )
39		ax-hvmulid	⊢ ( 𝑥 ∈ ℋ → ( 1 ·ℎ 𝑥 ) = 𝑥 )
40	6 7 39	3syl	⊢ ( 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) → ( 1 ·ℎ 𝑥 ) = 𝑥 )
41	35 38 40	3eqtr3d	⊢ ( 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) → ( ( normℎ ‘ 𝑥 ) ·ℎ ( ( 1 / ( normℎ ‘ 𝑥 ) ) ·ℎ 𝑥 ) ) = 𝑥 )
42	41	eleq1d	⊢ ( 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) → ( ( ( normℎ ‘ 𝑥 ) ·ℎ ( ( 1 / ( normℎ ‘ 𝑥 ) ) ·ℎ 𝑥 ) ) ∈ 𝐵 ↔ 𝑥 ∈ 𝐵 ) )
43	33 42	sylibd	⊢ ( 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) → ( ( ( 1 / ( normℎ ‘ 𝑥 ) ) ·ℎ 𝑥 ) ∈ 𝐵 → 𝑥 ∈ 𝐵 ) )
44	43	con3d	⊢ ( 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) → ( ¬ 𝑥 ∈ 𝐵 → ¬ ( ( 1 / ( normℎ ‘ 𝑥 ) ) ·ℎ 𝑥 ) ∈ 𝐵 ) )
45	27 44	anim12d	⊢ ( 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) → ( ( 𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵 ) → ( ( ( 1 / ( normℎ ‘ 𝑥 ) ) ·ℎ 𝑥 ) ∈ 𝐴 ∧ ¬ ( ( 1 / ( normℎ ‘ 𝑥 ) ) ·ℎ 𝑥 ) ∈ 𝐵 ) ) )
46		eldif	⊢ ( 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) ↔ ( 𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵 ) )
47		eldif	⊢ ( ( ( 1 / ( normℎ ‘ 𝑥 ) ) ·ℎ 𝑥 ) ∈ ( 𝐴 ∖ 𝐵 ) ↔ ( ( ( 1 / ( normℎ ‘ 𝑥 ) ) ·ℎ 𝑥 ) ∈ 𝐴 ∧ ¬ ( ( 1 / ( normℎ ‘ 𝑥 ) ) ·ℎ 𝑥 ) ∈ 𝐵 ) )
48	45 46 47	3imtr4g	⊢ ( 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) → ( 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) → ( ( 1 / ( normℎ ‘ 𝑥 ) ) ·ℎ 𝑥 ) ∈ ( 𝐴 ∖ 𝐵 ) ) )
49	48	pm2.43i	⊢ ( 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) → ( ( 1 / ( normℎ ‘ 𝑥 ) ) ·ℎ 𝑥 ) ∈ ( 𝐴 ∖ 𝐵 ) )
50		norm-iii	⊢ ( ( ( 1 / ( normℎ ‘ 𝑥 ) ) ∈ ℂ ∧ 𝑥 ∈ ℋ ) → ( normℎ ‘ ( ( 1 / ( normℎ ‘ 𝑥 ) ) ·ℎ 𝑥 ) ) = ( ( abs ‘ ( 1 / ( normℎ ‘ 𝑥 ) ) ) · ( normℎ ‘ 𝑥 ) ) )
51	22 36 50	syl2anc	⊢ ( 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) → ( normℎ ‘ ( ( 1 / ( normℎ ‘ 𝑥 ) ) ·ℎ 𝑥 ) ) = ( ( abs ‘ ( 1 / ( normℎ ‘ 𝑥 ) ) ) · ( normℎ ‘ 𝑥 ) ) )
52	15	necon2ai	⊢ ( 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) → 𝑥 ≠ 0ℎ )
53		normgt0	⊢ ( 𝑥 ∈ ℋ → ( 𝑥 ≠ 0ℎ ↔ 0 < ( normℎ ‘ 𝑥 ) ) )
54	6 7 53	3syl	⊢ ( 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) → ( 𝑥 ≠ 0ℎ ↔ 0 < ( normℎ ‘ 𝑥 ) ) )
55	52 54	mpbid	⊢ ( 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) → 0 < ( normℎ ‘ 𝑥 ) )
56		1re	⊢ 1 ∈ ℝ
57		0le1	⊢ 0 ≤ 1
58		divge0	⊢ ( ( ( 1 ∈ ℝ ∧ 0 ≤ 1 ) ∧ ( ( normℎ ‘ 𝑥 ) ∈ ℝ ∧ 0 < ( normℎ ‘ 𝑥 ) ) ) → 0 ≤ ( 1 / ( normℎ ‘ 𝑥 ) ) )
59	56 57 58	mpanl12	⊢ ( ( ( normℎ ‘ 𝑥 ) ∈ ℝ ∧ 0 < ( normℎ ‘ 𝑥 ) ) → 0 ≤ ( 1 / ( normℎ ‘ 𝑥 ) ) )
60	9 55 59	syl2anc	⊢ ( 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) → 0 ≤ ( 1 / ( normℎ ‘ 𝑥 ) ) )
61	21 60	absidd	⊢ ( 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) → ( abs ‘ ( 1 / ( normℎ ‘ 𝑥 ) ) ) = ( 1 / ( normℎ ‘ 𝑥 ) ) )
62	61	oveq1d	⊢ ( 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) → ( ( abs ‘ ( 1 / ( normℎ ‘ 𝑥 ) ) ) · ( normℎ ‘ 𝑥 ) ) = ( ( 1 / ( normℎ ‘ 𝑥 ) ) · ( normℎ ‘ 𝑥 ) ) )
63	28 20	recid2d	⊢ ( 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) → ( ( 1 / ( normℎ ‘ 𝑥 ) ) · ( normℎ ‘ 𝑥 ) ) = 1 )
64	51 62 63	3eqtrd	⊢ ( 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) → ( normℎ ‘ ( ( 1 / ( normℎ ‘ 𝑥 ) ) ·ℎ 𝑥 ) ) = 1 )
65		fveqeq2	⊢ ( 𝑢 = ( ( 1 / ( normℎ ‘ 𝑥 ) ) ·ℎ 𝑥 ) → ( ( normℎ ‘ 𝑢 ) = 1 ↔ ( normℎ ‘ ( ( 1 / ( normℎ ‘ 𝑥 ) ) ·ℎ 𝑥 ) ) = 1 ) )
66	65	rspcev	⊢ ( ( ( ( 1 / ( normℎ ‘ 𝑥 ) ) ·ℎ 𝑥 ) ∈ ( 𝐴 ∖ 𝐵 ) ∧ ( normℎ ‘ ( ( 1 / ( normℎ ‘ 𝑥 ) ) ·ℎ 𝑥 ) ) = 1 ) → ∃ 𝑢 ∈ ( 𝐴 ∖ 𝐵 ) ( normℎ ‘ 𝑢 ) = 1 )
67	49 64 66	syl2anc	⊢ ( 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) → ∃ 𝑢 ∈ ( 𝐴 ∖ 𝐵 ) ( normℎ ‘ 𝑢 ) = 1 )
68	67	exlimiv	⊢ ( ∃ 𝑥 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) → ∃ 𝑢 ∈ ( 𝐴 ∖ 𝐵 ) ( normℎ ‘ 𝑢 ) = 1 )
69	5 68	sylbi	⊢ ( ¬ 𝐴 ⊆ 𝐵 → ∃ 𝑢 ∈ ( 𝐴 ∖ 𝐵 ) ( normℎ ‘ 𝑢 ) = 1 )