pjthlem2 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > pjthlem2		Structured version Visualization version GIF version

Theorem pjthlem2 25368

Description: Lemma for pjth 25369. (Contributed by NM, 10-Oct-1999.) (Revised by Mario Carneiro, 15-May-2014.)

**Hypotheses**
Ref	Expression
pjthlem.v	⊢ 𝑉 = (Base‘𝑊)
pjthlem.n	⊢ 𝑁 = (norm‘𝑊)
pjthlem.p	⊢ + = (+_g‘𝑊)
pjthlem.m	⊢ − = (-_g‘𝑊)
pjthlem.h	⊢ , = (·_𝑖‘𝑊)
pjthlem.l	⊢ 𝐿 = (LSubSp‘𝑊)
pjthlem.1	⊢ (𝜑 → 𝑊 ∈ ℂHil)
pjthlem.2	⊢ (𝜑 → 𝑈 ∈ 𝐿)
pjthlem.4	⊢ (𝜑 → 𝐴 ∈ 𝑉)
pjthlem.j	⊢ 𝐽 = (TopOpen‘𝑊)
pjthlem.s	⊢ ⊕ = (LSSum‘𝑊)
pjthlem.o	⊢ 𝑂 = (ocv‘𝑊)
pjthlem.3	⊢ (𝜑 → 𝑈 ∈ (Clsd‘𝐽))

**Assertion**
Ref	Expression
pjthlem2	⊢ (𝜑 → 𝐴 ∈ (𝑈 ⊕ (𝑂‘𝑈)))

Proof of Theorem pjthlem2 Dummy variables 𝑥 𝑤 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		pjthlem.v	. . . 4 ⊢ 𝑉 = (Base‘𝑊)
2		pjthlem.m	. . . 4 ⊢ − = (-_g‘𝑊)
3		pjthlem.n	. . . 4 ⊢ 𝑁 = (norm‘𝑊)
4		pjthlem.1	. . . . 5 ⊢ (𝜑 → 𝑊 ∈ ℂHil)
5		hlcph 25294	. . . . 5 ⊢ (𝑊 ∈ ℂHil → 𝑊 ∈ ℂPreHil)
6	4, 5	syl 17	. . . 4 ⊢ (𝜑 → 𝑊 ∈ ℂPreHil)
7		pjthlem.2	. . . . 5 ⊢ (𝜑 → 𝑈 ∈ 𝐿)
8		pjthlem.l	. . . . 5 ⊢ 𝐿 = (LSubSp‘𝑊)
9	7, 8	eleqtrdi 2843	. . . 4 ⊢ (𝜑 → 𝑈 ∈ (LSubSp‘𝑊))
10		pjthlem.3	. . . . 5 ⊢ (𝜑 → 𝑈 ∈ (Clsd‘𝐽))
11		hlcms 25296	. . . . . . 7 ⊢ (𝑊 ∈ ℂHil → 𝑊 ∈ CMetSp)
12	4, 11	syl 17	. . . . . 6 ⊢ (𝜑 → 𝑊 ∈ CMetSp)
13	1, 8	lssss 20873	. . . . . . 7 ⊢ (𝑈 ∈ 𝐿 → 𝑈 ⊆ 𝑉)
14	7, 13	syl 17	. . . . . 6 ⊢ (𝜑 → 𝑈 ⊆ 𝑉)
15		eqid 2733	. . . . . . 7 ⊢ (𝑊 ↾_s 𝑈) = (𝑊 ↾_s 𝑈)
16		pjthlem.j	. . . . . . 7 ⊢ 𝐽 = (TopOpen‘𝑊)
17	15, 1, 16	cmsss 25281	. . . . . 6 ⊢ ((𝑊 ∈ CMetSp ∧ 𝑈 ⊆ 𝑉) → ((𝑊 ↾_s 𝑈) ∈ CMetSp ↔ 𝑈 ∈ (Clsd‘𝐽)))
18	12, 14, 17	syl2anc 584	. . . . 5 ⊢ (𝜑 → ((𝑊 ↾_s 𝑈) ∈ CMetSp ↔ 𝑈 ∈ (Clsd‘𝐽)))
19	10, 18	mpbird 257	. . . 4 ⊢ (𝜑 → (𝑊 ↾_s 𝑈) ∈ CMetSp)
20		pjthlem.4	. . . 4 ⊢ (𝜑 → 𝐴 ∈ 𝑉)
21	1, 2, 3, 6, 9, 19, 20	minvec 25366	. . 3 ⊢ (𝜑 → ∃!𝑥 ∈ 𝑈 ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))
22		reurex 3351	. . 3 ⊢ (∃!𝑥 ∈ 𝑈 ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)) → ∃𝑥 ∈ 𝑈 ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))
23	21, 22	syl 17	. 2 ⊢ (𝜑 → ∃𝑥 ∈ 𝑈 ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))
24	6	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) → 𝑊 ∈ ℂPreHil)
25		cphlmod 25104	. . . . . 6 ⊢ (𝑊 ∈ ℂPreHil → 𝑊 ∈ LMod)
26	24, 25	syl 17	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) → 𝑊 ∈ LMod)
27		lmodabl 20846	. . . . 5 ⊢ (𝑊 ∈ LMod → 𝑊 ∈ Abel)
28	26, 27	syl 17	. . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) → 𝑊 ∈ Abel)
29	7	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) → 𝑈 ∈ 𝐿)
30	29, 13	syl 17	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) → 𝑈 ⊆ 𝑉)
31		simprl 770	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) → 𝑥 ∈ 𝑈)
32	30, 31	sseldd 3931	. . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) → 𝑥 ∈ 𝑉)
33	20	adantr 480	. . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) → 𝐴 ∈ 𝑉)
34		pjthlem.p	. . . . 5 ⊢ + = (+_g‘𝑊)
35	1, 34, 2	ablpncan3 19732	. . . 4 ⊢ ((𝑊 ∈ Abel ∧ (𝑥 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉)) → (𝑥 + (𝐴 − 𝑥)) = 𝐴)
36	28, 32, 33, 35	syl12anc 836	. . 3 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) → (𝑥 + (𝐴 − 𝑥)) = 𝐴)
37	8	lsssssubg 20895	. . . . . 6 ⊢ (𝑊 ∈ LMod → 𝐿 ⊆ (SubGrp‘𝑊))
38	26, 37	syl 17	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) → 𝐿 ⊆ (SubGrp‘𝑊))
39	38, 29	sseldd 3931	. . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) → 𝑈 ∈ (SubGrp‘𝑊))
40		cphphl 25101	. . . . . . 7 ⊢ (𝑊 ∈ ℂPreHil → 𝑊 ∈ PreHil)
41	24, 40	syl 17	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) → 𝑊 ∈ PreHil)
42		pjthlem.o	. . . . . . 7 ⊢ 𝑂 = (ocv‘𝑊)
43	1, 42, 8	ocvlss 21613	. . . . . 6 ⊢ ((𝑊 ∈ PreHil ∧ 𝑈 ⊆ 𝑉) → (𝑂‘𝑈) ∈ 𝐿)
44	41, 30, 43	syl2anc 584	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) → (𝑂‘𝑈) ∈ 𝐿)
45	38, 44	sseldd 3931	. . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) → (𝑂‘𝑈) ∈ (SubGrp‘𝑊))
46	1, 2	lmodvsubcl 20844	. . . . . 6 ⊢ ((𝑊 ∈ LMod ∧ 𝐴 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉) → (𝐴 − 𝑥) ∈ 𝑉)
47	26, 33, 32, 46	syl3anc 1373	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) → (𝐴 − 𝑥) ∈ 𝑉)
48		pjthlem.h	. . . . . . . 8 ⊢ , = (·_𝑖‘𝑊)
49	4	ad2antrr 726	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) ∧ 𝑧 ∈ 𝑈) → 𝑊 ∈ ℂHil)
50	29	adantr 480	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) ∧ 𝑧 ∈ 𝑈) → 𝑈 ∈ 𝐿)
51	47	adantr 480	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) ∧ 𝑧 ∈ 𝑈) → (𝐴 − 𝑥) ∈ 𝑉)
52		simpr 484	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) ∧ 𝑧 ∈ 𝑈) → 𝑧 ∈ 𝑈)
53		oveq2 7362	. . . . . . . . . . . . . 14 ⊢ (𝑦 = (𝑤 + 𝑥) → (𝐴 − 𝑦) = (𝐴 − (𝑤 + 𝑥)))
54	53	fveq2d 6834	. . . . . . . . . . . . 13 ⊢ (𝑦 = (𝑤 + 𝑥) → (𝑁‘(𝐴 − 𝑦)) = (𝑁‘(𝐴 − (𝑤 + 𝑥))))
55	54	breq2d 5107	. . . . . . . . . . . 12 ⊢ (𝑦 = (𝑤 + 𝑥) → ((𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)) ↔ (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − (𝑤 + 𝑥)))))
56		simplrr 777	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) ∧ 𝑤 ∈ 𝑈) → ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))
57	26	adantr 480	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) ∧ 𝑤 ∈ 𝑈) → 𝑊 ∈ LMod)
58	29	adantr 480	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) ∧ 𝑤 ∈ 𝑈) → 𝑈 ∈ 𝐿)
59		simpr 484	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) ∧ 𝑤 ∈ 𝑈) → 𝑤 ∈ 𝑈)
60	31	adantr 480	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) ∧ 𝑤 ∈ 𝑈) → 𝑥 ∈ 𝑈)
61	34, 8	lssvacl 20880	. . . . . . . . . . . . 13 ⊢ (((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝐿) ∧ (𝑤 ∈ 𝑈 ∧ 𝑥 ∈ 𝑈)) → (𝑤 + 𝑥) ∈ 𝑈)
62	57, 58, 59, 60, 61	syl22anc 838	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) ∧ 𝑤 ∈ 𝑈) → (𝑤 + 𝑥) ∈ 𝑈)
63	55, 56, 62	rspcdva 3574	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) ∧ 𝑤 ∈ 𝑈) → (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − (𝑤 + 𝑥))))
64		lmodgrp 20804	. . . . . . . . . . . . . . 15 ⊢ (𝑊 ∈ LMod → 𝑊 ∈ Grp)
65	26, 64	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) → 𝑊 ∈ Grp)
66	65	adantr 480	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) ∧ 𝑤 ∈ 𝑈) → 𝑊 ∈ Grp)
67	33	adantr 480	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) ∧ 𝑤 ∈ 𝑈) → 𝐴 ∈ 𝑉)
68	32	adantr 480	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) ∧ 𝑤 ∈ 𝑈) → 𝑥 ∈ 𝑉)
69	30	sselda 3930	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) ∧ 𝑤 ∈ 𝑈) → 𝑤 ∈ 𝑉)
70	1, 34, 2	grpsubsub4 18950	. . . . . . . . . . . . 13 ⊢ ((𝑊 ∈ Grp ∧ (𝐴 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉 ∧ 𝑤 ∈ 𝑉)) → ((𝐴 − 𝑥) − 𝑤) = (𝐴 − (𝑤 + 𝑥)))
71	66, 67, 68, 69, 70	syl13anc 1374	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) ∧ 𝑤 ∈ 𝑈) → ((𝐴 − 𝑥) − 𝑤) = (𝐴 − (𝑤 + 𝑥)))
72	71	fveq2d 6834	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) ∧ 𝑤 ∈ 𝑈) → (𝑁‘((𝐴 − 𝑥) − 𝑤)) = (𝑁‘(𝐴 − (𝑤 + 𝑥))))
73	63, 72	breqtrrd 5123	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) ∧ 𝑤 ∈ 𝑈) → (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘((𝐴 − 𝑥) − 𝑤)))
74	73	ralrimiva 3125	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) → ∀𝑤 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘((𝐴 − 𝑥) − 𝑤)))
75	74	adantr 480	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) ∧ 𝑧 ∈ 𝑈) → ∀𝑤 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘((𝐴 − 𝑥) − 𝑤)))
76		eqid 2733	. . . . . . . 8 ⊢ (((𝐴 − 𝑥) , 𝑧) / ((𝑧 , 𝑧) + 1)) = (((𝐴 − 𝑥) , 𝑧) / ((𝑧 , 𝑧) + 1))
77	1, 3, 34, 2, 48, 8, 49, 50, 51, 52, 75, 76	pjthlem1 25367	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) ∧ 𝑧 ∈ 𝑈) → ((𝐴 − 𝑥) , 𝑧) = 0)
78	24	adantr 480	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) ∧ 𝑧 ∈ 𝑈) → 𝑊 ∈ ℂPreHil)
79		cphclm 25119	. . . . . . . . 9 ⊢ (𝑊 ∈ ℂPreHil → 𝑊 ∈ ℂMod)
80	78, 79	syl 17	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) ∧ 𝑧 ∈ 𝑈) → 𝑊 ∈ ℂMod)
81		eqid 2733	. . . . . . . . 9 ⊢ (Scalar‘𝑊) = (Scalar‘𝑊)
82	81	clm0 25002	. . . . . . . 8 ⊢ (𝑊 ∈ ℂMod → 0 = (0_g‘(Scalar‘𝑊)))
83	80, 82	syl 17	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) ∧ 𝑧 ∈ 𝑈) → 0 = (0_g‘(Scalar‘𝑊)))
84	77, 83	eqtrd 2768	. . . . . 6 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) ∧ 𝑧 ∈ 𝑈) → ((𝐴 − 𝑥) , 𝑧) = (0_g‘(Scalar‘𝑊)))
85	84	ralrimiva 3125	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) → ∀𝑧 ∈ 𝑈 ((𝐴 − 𝑥) , 𝑧) = (0_g‘(Scalar‘𝑊)))
86		eqid 2733	. . . . . 6 ⊢ (0_g‘(Scalar‘𝑊)) = (0_g‘(Scalar‘𝑊))
87	1, 48, 81, 86, 42	elocv 21609	. . . . 5 ⊢ ((𝐴 − 𝑥) ∈ (𝑂‘𝑈) ↔ (𝑈 ⊆ 𝑉 ∧ (𝐴 − 𝑥) ∈ 𝑉 ∧ ∀𝑧 ∈ 𝑈 ((𝐴 − 𝑥) , 𝑧) = (0_g‘(Scalar‘𝑊))))
88	30, 47, 85, 87	syl3anbrc 1344	. . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) → (𝐴 − 𝑥) ∈ (𝑂‘𝑈))
89		pjthlem.s	. . . . 5 ⊢ ⊕ = (LSSum‘𝑊)
90	34, 89	lsmelvali 19566	. . . 4 ⊢ (((𝑈 ∈ (SubGrp‘𝑊) ∧ (𝑂‘𝑈) ∈ (SubGrp‘𝑊)) ∧ (𝑥 ∈ 𝑈 ∧ (𝐴 − 𝑥) ∈ (𝑂‘𝑈))) → (𝑥 + (𝐴 − 𝑥)) ∈ (𝑈 ⊕ (𝑂‘𝑈)))
91	39, 45, 31, 88, 90	syl22anc 838	. . 3 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) → (𝑥 + (𝐴 − 𝑥)) ∈ (𝑈 ⊕ (𝑂‘𝑈)))
92	36, 91	eqeltrrd 2834	. 2 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) → 𝐴 ∈ (𝑈 ⊕ (𝑂‘𝑈)))
93	23, 92	rexlimddv 3140	1 ⊢ (𝜑 → 𝐴 ∈ (𝑈 ⊕ (𝑂‘𝑈)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 = wceq 1541 ∈ wcel 2113 ∀wral 3048 ∃wrex 3057 ∃!wreu 3345 ⊆ wss 3898 class class class wbr 5095 ‘cfv 6488 (class class class)co 7354 0cc0 11015 1c1 11016 + caddc 11018 ≤ cle 11156 / cdiv 11783 Basecbs 17124 ↾_s cress 17145 +_gcplusg 17165 Scalarcsca 17168 ·_𝑖cip 17170 TopOpenctopn 17329 0_gc0g 17347 Grpcgrp 18850 -_gcsg 18852 SubGrpcsubg 19037 LSSumclsm 19550 Abelcabl 19697 LModclmod 20797 LSubSpclss 20868 PreHilcphl 21565 ocvcocv 21601 Clsdccld 22934 normcnm 24494 ℂModcclm 24992 ℂPreHilccph 25096 CMetSpccms 25262 ℂHilchl 25264

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2115 ax-9 2123 ax-10 2146 ax-11 2162 ax-12 2182 ax-ext 2705 ax-rep 5221 ax-sep 5238 ax-nul 5248 ax-pow 5307 ax-pr 5374 ax-un 7676 ax-cnex 11071 ax-resscn 11072 ax-1cn 11073 ax-icn 11074 ax-addcl 11075 ax-addrcl 11076 ax-mulcl 11077 ax-mulrcl 11078 ax-mulcom 11079 ax-addass 11080 ax-mulass 11081 ax-distr 11082 ax-i2m1 11083 ax-1ne0 11084 ax-1rid 11085 ax-rnegex 11086 ax-rrecex 11087 ax-cnre 11088 ax-pre-lttri 11089 ax-pre-lttrn 11090 ax-pre-ltadd 11091 ax-pre-mulgt0 11092 ax-pre-sup 11093 ax-addf 11094 ax-mulf 11095

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2068 df-mo 2537 df-eu 2566 df-clab 2712 df-cleq 2725 df-clel 2808 df-nfc 2882 df-ne 2930 df-nel 3034 df-ral 3049 df-rex 3058 df-rmo 3347 df-reu 3348 df-rab 3397 df-v 3439 df-sbc 3738 df-csb 3847 df-dif 3901 df-un 3903 df-in 3905 df-ss 3915 df-pss 3918 df-nul 4283 df-if 4477 df-pw 4553 df-sn 4578 df-pr 4580 df-tp 4582 df-op 4584 df-uni 4861 df-int 4900 df-iun 4945 df-iin 4946 df-br 5096 df-opab 5158 df-mpt 5177 df-tr 5203 df-id 5516 df-eprel 5521 df-po 5529 df-so 5530 df-fr 5574 df-se 5575 df-we 5576 df-xp 5627 df-rel 5628 df-cnv 5629 df-co 5630 df-dm 5631 df-rn 5632 df-res 5633 df-ima 5634 df-pred 6255 df-ord 6316 df-on 6317 df-lim 6318 df-suc 6319 df-iota 6444 df-fun 6490 df-fn 6491 df-f 6492 df-f1 6493 df-fo 6494 df-f1o 6495 df-fv 6496 df-isom 6497 df-riota 7311 df-ov 7357 df-oprab 7358 df-mpo 7359 df-of 7618 df-om 7805 df-1st 7929 df-2nd 7930 df-supp 8099 df-tpos 8164 df-frecs 8219 df-wrecs 8250 df-recs 8299 df-rdg 8337 df-1o 8393 df-2o 8394 df-er 8630 df-map 8760 df-ixp 8830 df-en 8878 df-dom 8879 df-sdom 8880 df-fin 8881 df-fsupp 9255 df-fi 9304 df-sup 9335 df-inf 9336 df-oi 9405 df-card 9841 df-pnf 11157 df-mnf 11158 df-xr 11159 df-ltxr 11160 df-le 11161 df-sub 11355 df-neg 11356 df-div 11784 df-nn 12135 df-2 12197 df-3 12198 df-4 12199 df-5 12200 df-6 12201 df-7 12202 df-8 12203 df-9 12204 df-n0 12391 df-z 12478 df-dec 12597 df-uz 12741 df-q 12851 df-rp 12895 df-xneg 13015 df-xadd 13016 df-xmul 13017 df-ioo 13253 df-ico 13255 df-icc 13256 df-fz 13412 df-fzo 13559 df-seq 13913 df-exp 13973 df-hash 14242 df-cj 15010 df-re 15011 df-im 15012 df-sqrt 15146 df-abs 15147 df-struct 17062 df-sets 17079 df-slot 17097 df-ndx 17109 df-base 17125 df-ress 17146 df-plusg 17178 df-mulr 17179 df-starv 17180 df-sca 17181 df-vsca 17182 df-ip 17183 df-tset 17184 df-ple 17185 df-ds 17187 df-unif 17188 df-hom 17189 df-cco 17190 df-rest 17330 df-topn 17331 df-0g 17349 df-gsum 17350 df-topgen 17351 df-pt 17352 df-prds 17355 df-xrs 17410 df-qtop 17415 df-imas 17416 df-xps 17418 df-mre 17492 df-mrc 17493 df-acs 17495 df-mgm 18552 df-sgrp 18631 df-mnd 18647 df-mhm 18695 df-submnd 18696 df-grp 18853 df-minusg 18854 df-sbg 18855 df-mulg 18985 df-subg 19040 df-ghm 19129 df-cntz 19233 df-lsm 19552 df-cmn 19698 df-abl 19699 df-mgp 20063 df-rng 20075 df-ur 20104 df-ring 20157 df-cring 20158 df-oppr 20259 df-dvdsr 20279 df-unit 20280 df-invr 20310 df-dvr 20323 df-rhm 20394 df-subrng 20465 df-subrg 20489 df-drng 20650 df-staf 20758 df-srng 20759 df-lmod 20799 df-lss 20869 df-lmhm 20960 df-lvec 21041 df-sra 21111 df-rgmod 21112 df-psmet 21287 df-xmet 21288 df-met 21289 df-bl 21290 df-mopn 21291 df-fbas 21292 df-fg 21293 df-cnfld 21296 df-phl 21567 df-ocv 21604 df-top 22812 df-topon 22829 df-topsp 22851 df-bases 22864 df-cld 22937 df-ntr 22938 df-cls 22939 df-nei 23016 df-cn 23145 df-cnp 23146 df-haus 23233 df-cmp 23305 df-tx 23480 df-hmeo 23673 df-fil 23764 df-flim 23857 df-fcls 23859 df-xms 24238 df-ms 24239 df-tms 24240 df-nm 24500 df-ngp 24501 df-nlm 24504 df-cncf 24801 df-clm 24993 df-cph 25098 df-cfil 25185 df-cmet 25187 df-cms 25265 df-bn 25266 df-hl 25267

This theorem is referenced by: pjth 25369

W3C validator