Theorem pjthlem2 25803

Description: Lemma for pjth 25804. (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 25729	. . . . 5 ⊢ (𝑊 ∈ ℂHil → 𝑊 ∈ ℂPreHil)
6	4, 5	syl 18	. . . 4 ⊢ (𝜑 → 𝑊 ∈ ℂPreHil)
7		pjthlem.2	. . . . 5 ⊢ (𝜑 → 𝑈 ∈ 𝐿)
8		pjthlem.l	. . . . 5 ⊢ 𝐿 = (LSubSp‘𝑊)
9	7, 8	eleqtrdi 2874	. . . 4 ⊢ (𝜑 → 𝑈 ∈ (LSubSp‘𝑊))
10		pjthlem.3	. . . . 5 ⊢ (𝜑 → 𝑈 ∈ (Clsd‘𝐽))
11		hlcms 25731	. . . . . . 7 ⊢ (𝑊 ∈ ℂHil → 𝑊 ∈ CMetSp)
12	4, 11	syl 18	. . . . . 6 ⊢ (𝜑 → 𝑊 ∈ CMetSp)
13	1, 8	lssss 21253	. . . . . . 7 ⊢ (𝑈 ∈ 𝐿 → 𝑈 ⊆ 𝑉)
14	7, 13	syl 18	. . . . . 6 ⊢ (𝜑 → 𝑈 ⊆ 𝑉)
15		eqid 2763	. . . . . . 7 ⊢ (𝑊 ↾s 𝑈) = (𝑊 ↾s 𝑈)
16		pjthlem.j	. . . . . . 7 ⊢ 𝐽 = (TopOpen‘𝑊)
17	15, 1, 16	cmsss 25716	. . . . . 6 ⊢ ((𝑊 ∈ CMetSp ∧ 𝑈 ⊆ 𝑉) → ((𝑊 ↾s 𝑈) ∈ CMetSp ↔ 𝑈 ∈ (Clsd‘𝐽)))
18	12, 14, 17	syl2anc 596	. . . . 5 ⊢ (𝜑 → ((𝑊 ↾s 𝑈) ∈ CMetSp ↔ 𝑈 ∈ (Clsd‘𝐽)))
19	10, 18	mpbird 260	. . . 4 ⊢ (𝜑 → (𝑊 ↾s 𝑈) ∈ CMetSp)
20		pjthlem.4	. . . 4 ⊢ (𝜑 → 𝐴 ∈ 𝑉)
21	1, 2, 3, 6, 9, 19, 20	minvec 25801	. . 3 ⊢ (𝜑 → ∃!𝑥 ∈ 𝑈 ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))
22		reurex 3373	. . 3 ⊢ (∃!𝑥 ∈ 𝑈 ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)) → ∃𝑥 ∈ 𝑈 ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))
23	21, 22	syl 18	. 2 ⊢ (𝜑 → ∃𝑥 ∈ 𝑈 ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))
24	6	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) → 𝑊 ∈ ℂPreHil)
25		cphlmod 25539	. . . . . 6 ⊢ (𝑊 ∈ ℂPreHil → 𝑊 ∈ LMod)
26	24, 25	syl 18	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) → 𝑊 ∈ LMod)
27		lmodabl 21226	. . . . 5 ⊢ (𝑊 ∈ LMod → 𝑊 ∈ Abel)
28	26, 27	syl 18	. . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) → 𝑊 ∈ Abel)
29	7	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) → 𝑈 ∈ 𝐿)
30	29, 13	syl 18	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) → 𝑈 ⊆ 𝑉)
31		simprl 783	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) → 𝑥 ∈ 𝑈)
32	30, 31	sseldd 3914	. . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) → 𝑥 ∈ 𝑉)
33	20	adantr 486	. . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) → 𝐴 ∈ 𝑉)
34		pjthlem.p	. . . . 5 ⊢ + = (+g‘𝑊)
35	1, 34, 2	ablpncan3 20072	. . . 4 ⊢ ((𝑊 ∈ Abel ∧ (𝑥 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉)) → (𝑥 + (𝐴 − 𝑥)) = 𝐴)
36	28, 32, 33, 35	syl12anc 850	. . 3 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) → (𝑥 + (𝐴 − 𝑥)) = 𝐴)
37	8	lsssssubg 21275	. . . . . 6 ⊢ (𝑊 ∈ LMod → 𝐿 ⊆ (SubGrp‘𝑊))
38	26, 37	syl 18	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) → 𝐿 ⊆ (SubGrp‘𝑊))
39	38, 29	sseldd 3914	. . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) → 𝑈 ∈ (SubGrp‘𝑊))
40		cphphl 25536	. . . . . . 7 ⊢ (𝑊 ∈ ℂPreHil → 𝑊 ∈ PreHil)
41	24, 40	syl 18	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) → 𝑊 ∈ PreHil)
42		pjthlem.o	. . . . . . 7 ⊢ 𝑂 = (ocv‘𝑊)
43	1, 42, 8	ocvlss 22022	. . . . . 6 ⊢ ((𝑊 ∈ PreHil ∧ 𝑈 ⊆ 𝑉) → (𝑂‘𝑈) ∈ 𝐿)
44	41, 30, 43	syl2anc 596	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) → (𝑂‘𝑈) ∈ 𝐿)
45	38, 44	sseldd 3914	. . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) → (𝑂‘𝑈) ∈ (SubGrp‘𝑊))
46	1, 2	lmodvsubcl 21224	. . . . . 6 ⊢ ((𝑊 ∈ LMod ∧ 𝐴 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉) → (𝐴 − 𝑥) ∈ 𝑉)
47	26, 33, 32, 46	syl3anc 1399	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) → (𝐴 − 𝑥) ∈ 𝑉)
48		pjthlem.h	. . . . . . . 8 ⊢ , = (·𝑖‘𝑊)
49	4	ad2antrr 739	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) ∧ 𝑧 ∈ 𝑈) → 𝑊 ∈ ℂHil)
50	29	adantr 486	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) ∧ 𝑧 ∈ 𝑈) → 𝑈 ∈ 𝐿)
51	47	adantr 486	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) ∧ 𝑧 ∈ 𝑈) → (𝐴 − 𝑥) ∈ 𝑉)
52		simpr 490	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) ∧ 𝑧 ∈ 𝑈) → 𝑧 ∈ 𝑈)
53		oveq2 7457	. . . . . . . . . . . . . 14 ⊢ (𝑦 = (𝑤 + 𝑥) → (𝐴 − 𝑦) = (𝐴 − (𝑤 + 𝑥)))
54	53	fveq2d 6918	. . . . . . . . . . . . 13 ⊢ (𝑦 = (𝑤 + 𝑥) → (𝑁‘(𝐴 − 𝑦)) = (𝑁‘(𝐴 − (𝑤 + 𝑥))))
55	54	breq2d 5118	. . . . . . . . . . . 12 ⊢ (𝑦 = (𝑤 + 𝑥) → ((𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)) ↔ (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − (𝑤 + 𝑥)))))
56		simplrr 790	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) ∧ 𝑤 ∈ 𝑈) → ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))
57	26	adantr 486	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) ∧ 𝑤 ∈ 𝑈) → 𝑊 ∈ LMod)
58	29	adantr 486	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) ∧ 𝑤 ∈ 𝑈) → 𝑈 ∈ 𝐿)
59		simpr 490	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) ∧ 𝑤 ∈ 𝑈) → 𝑤 ∈ 𝑈)
60	31	adantr 486	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) ∧ 𝑤 ∈ 𝑈) → 𝑥 ∈ 𝑈)
61	34, 8	lssvacl 21260	. . . . . . . . . . . . 13 ⊢ (((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝐿) ∧ (𝑤 ∈ 𝑈 ∧ 𝑥 ∈ 𝑈)) → (𝑤 + 𝑥) ∈ 𝑈)
62	57, 58, 59, 60, 61	syl22anc 852	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) ∧ 𝑤 ∈ 𝑈) → (𝑤 + 𝑥) ∈ 𝑈)
63	55, 56, 62	rspcdva 3581	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) ∧ 𝑤 ∈ 𝑈) → (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − (𝑤 + 𝑥))))
64		lmodgrp 21184	. . . . . . . . . . . . . . 15 ⊢ (𝑊 ∈ LMod → 𝑊 ∈ Grp)
65	26, 64	syl 18	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) → 𝑊 ∈ Grp)
66	65	adantr 486	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) ∧ 𝑤 ∈ 𝑈) → 𝑊 ∈ Grp)
67	33	adantr 486	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) ∧ 𝑤 ∈ 𝑈) → 𝐴 ∈ 𝑉)
68	32	adantr 486	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) ∧ 𝑤 ∈ 𝑈) → 𝑥 ∈ 𝑉)
69	30	sselda 3913	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) ∧ 𝑤 ∈ 𝑈) → 𝑤 ∈ 𝑉)
70	1, 34, 2	grpsubsub4 19284	. . . . . . . . . . . . 13 ⊢ ((𝑊 ∈ Grp ∧ (𝐴 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉 ∧ 𝑤 ∈ 𝑉)) → ((𝐴 − 𝑥) − 𝑤) = (𝐴 − (𝑤 + 𝑥)))
71	66, 67, 68, 69, 70	syl13anc 1400	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) ∧ 𝑤 ∈ 𝑈) → ((𝐴 − 𝑥) − 𝑤) = (𝐴 − (𝑤 + 𝑥)))
72	71	fveq2d 6918	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) ∧ 𝑤 ∈ 𝑈) → (𝑁‘((𝐴 − 𝑥) − 𝑤)) = (𝑁‘(𝐴 − (𝑤 + 𝑥))))
73	63, 72	breqtrrd 5137	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) ∧ 𝑤 ∈ 𝑈) → (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘((𝐴 − 𝑥) − 𝑤)))
74	73	ralrimiva 3158	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) → ∀𝑤 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘((𝐴 − 𝑥) − 𝑤)))
75	74	adantr 486	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) ∧ 𝑧 ∈ 𝑈) → ∀𝑤 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘((𝐴 − 𝑥) − 𝑤)))
76		eqid 2763	. . . . . . . 8 ⊢ (((𝐴 − 𝑥) , 𝑧) / ((𝑧 , 𝑧) + 1)) = (((𝐴 − 𝑥) , 𝑧) / ((𝑧 , 𝑧) + 1))
77	1, 3, 34, 2, 48, 8, 49, 50, 51, 52, 75, 76	pjthlem1 25802	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) ∧ 𝑧 ∈ 𝑈) → ((𝐴 − 𝑥) , 𝑧) = 0)
78	24	adantr 486	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) ∧ 𝑧 ∈ 𝑈) → 𝑊 ∈ ℂPreHil)
79		cphclm 25554	. . . . . . . . 9 ⊢ (𝑊 ∈ ℂPreHil → 𝑊 ∈ ℂMod)
80	78, 79	syl 18	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) ∧ 𝑧 ∈ 𝑈) → 𝑊 ∈ ℂMod)
81		eqid 2763	. . . . . . . . 9 ⊢ (Scalar‘𝑊) = (Scalar‘𝑊)
82	81	clm0 25437	. . . . . . . 8 ⊢ (𝑊 ∈ ℂMod → 0 = (0g‘(Scalar‘𝑊)))
83	80, 82	syl 18	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) ∧ 𝑧 ∈ 𝑈) → 0 = (0g‘(Scalar‘𝑊)))
84	77, 83	eqtrd 2798	. . . . . 6 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) ∧ 𝑧 ∈ 𝑈) → ((𝐴 − 𝑥) , 𝑧) = (0g‘(Scalar‘𝑊)))
85	84	ralrimiva 3158	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) → ∀𝑧 ∈ 𝑈 ((𝐴 − 𝑥) , 𝑧) = (0g‘(Scalar‘𝑊)))
86		eqid 2763	. . . . . 6 ⊢ (0g‘(Scalar‘𝑊)) = (0g‘(Scalar‘𝑊))
87	1, 48, 81, 86, 42	elocv 22018	. . . . 5 ⊢ ((𝐴 − 𝑥) ∈ (𝑂‘𝑈) ↔ (𝑈 ⊆ 𝑉 ∧ (𝐴 − 𝑥) ∈ 𝑉 ∧ ∀𝑧 ∈ 𝑈 ((𝐴 − 𝑥) , 𝑧) = (0g‘(Scalar‘𝑊))))
88	30, 47, 85, 87	syl3anbrc 1362	. . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) → (𝐴 − 𝑥) ∈ (𝑂‘𝑈))
89		pjthlem.s	. . . . 5 ⊢ ⊕ = (LSSum‘𝑊)
90	34, 89	lsmelvali 19906	. . . 4 ⊢ (((𝑈 ∈ (SubGrp‘𝑊) ∧ (𝑂‘𝑈) ∈ (SubGrp‘𝑊)) ∧ (𝑥 ∈ 𝑈 ∧ (𝐴 − 𝑥) ∈ (𝑂‘𝑈))) → (𝑥 + (𝐴 − 𝑥)) ∈ (𝑈 ⊕ (𝑂‘𝑈)))
91	39, 45, 31, 88, 90	syl22anc 852	. . 3 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) → (𝑥 + (𝐴 − 𝑥)) ∈ (𝑈 ⊕ (𝑂‘𝑈)))
92	36, 91	eqeltrrd 2865	. 2 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) → 𝐴 ∈ (𝑈 ⊕ (𝑂‘𝑈)))
93	23, 92	rexlimddv 3173	1 ⊢ (𝜑 → 𝐴 ∈ (𝑈 ⊕ (𝑂‘𝑈)))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1570   ∈ wcel 2147  ∀wral 3080  ∃wrex 3090  ∃!wreu 3367   ⊆ wss 3900   class class class wbr 5106  ‘cfv 6564  (class class class)co 7449  0cc0 11237  1c1 11238   + caddc 11240   ≤ cle 11381   / cdiv 12011  Basecbs 17428   ↾_s cress 17449  +_gcplusg 17469  Scalarcsca 17472  ·_𝑖cip 17474  TopOpenctopn 17633  0_gc0g 17651  Grpcgrp 19185  -_gcsg 19187  SubGrpcsubg 19371  LSSumclsm 19890  Abelcabl 20037  LModclmod 21177  LSubSpclss 21248  PreHilcphl 21974  ocvcocv 22010  Clsdccld 23378  normcnm 24939  ℂModcclm 25427  ℂPreHilccph 25531  CMetSpccms 25697  ℂHilchl 25699

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-rep 5236  ax-sep 5253  ax-nul 5264  ax-pow 5332  ax-pr 5396  ax-un 7781  ax-cnex 11293  ax-resscn 11294  ax-1cn 11295  ax-icn 11296  ax-addcl 11297  ax-addrcl 11298  ax-mulcl 11299  ax-mulrcl 11300  ax-mulcom 11301  ax-addass 11302  ax-mulass 11303  ax-distr 11304  ax-i2m1 11305  ax-1ne0 11306  ax-1rid 11307  ax-rnegex 11308  ax-rrecex 11309  ax-cnre 11310  ax-pre-lttri 11311  ax-pre-lttrn 11312  ax-pre-ltadd 11313  ax-pre-mulgt0 11314  ax-pre-sup 11315  ax-addf 11316  ax-mulf 11317

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-nel 3066  df-ral 3081  df-rex 3091  df-rmo 3369  df-reu 3370  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-pss 4017  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-tp 4593  df-op 4839  df-uni 4871  df-int 4911  df-iun 4956  df-iin 4957  df-br 5107  df-opab 5172  df-mpt 5191  df-tr 5217  df-id 5551  df-eprel 5556  df-po 5564  df-so 5565  df-fr 5609  df-se 5610  df-we 5611  df-xp 5662  df-rel 5663  df-cnv 5664  df-co 5665  df-dm 5666  df-rn 5667  df-res 5668  df-ima 5669  df-pred 6328  df-ord 6389  df-on 6390  df-lim 6391  df-suc 6392  df-iota 6518  df-fun 6566  df-fn 6567  df-f 6568  df-f1 6569  df-fo 6570  df-f1o 6571  df-fv 6572  df-isom 6573  df-riota 7406  df-ov 7452  df-oprab 7453  df-mpo 7454  df-of 7723  df-om 7910  df-1st 8033  df-2nd 8034  df-supp 8213  df-tpos 8279  df-frecs 8335  df-wrecs 8366  df-recs 8415  df-rdg 8454  df-1o 8512  df-2o 8513  df-er 8753  df-map 8885  df-ixp 8962  df-en 9010  df-dom 9011  df-sdom 9012  df-fin 9013  df-fsupp 9390  df-fi 9438  df-sup 9469  df-inf 9470  df-oi 9539  df-card 10055  df-pnf 11382  df-mnf 11383  df-xr 11384  df-ltxr 11385  df-le 11386  df-sub 11580  df-neg 11581  df-div 12012  df-nn 12374  df-2 12443  df-3 12444  df-4 12445  df-5 12446  df-6 12447  df-7 12448  df-8 12449  df-9 12450  df-n0 12645  df-z 12732  df-dec 12853  df-uz 13004  df-q 13114  df-rp 13159  df-xneg 13279  df-xadd 13280  df-xmul 13281  df-ioo 13518  df-ico 13520  df-icc 13521  df-fz 13678  df-fzo 13827  df-seq 14183  df-exp 14243  df-hash 14514  df-cj 15307  df-re 15308  df-im 15309  df-sqrt 15443  df-abs 15444  df-struct 17366  df-sets 17383  df-slot 17401  df-ndx 17413  df-base 17429  df-ress 17450  df-plusg 17482  df-mulr 17483  df-starv 17484  df-sca 17485  df-vsca 17486  df-ip 17487  df-tset 17488  df-ple 17489  df-ds 17491  df-unif 17492  df-hom 17493  df-cco 17494  df-rest 17634  df-topn 17635  df-0g 17653  df-gsum 17654  df-topgen 17655  df-pt 17656  df-prds 17659  df-xrs 17715  df-qtop 17720  df-imas 17721  df-xps 17723  df-mre 17797  df-mrc 17798  df-acs 17800  df-mgm 18857  df-sgrp 18949  df-mnd 18965  df-mhm 19019  df-submnd 19020  df-grp 19188  df-minusg 19189  df-sbg 19190  df-mulg 19319  df-subg 19374  df-ghm 19469  df-cntz 19573  df-lsm 19892  df-cmn 20038  df-abl 20039  df-mgp 20403  df-rng 20417  df-ur 20450  df-ring 20503  df-cring 20504  df-oppr 20609  df-dvdsr 20629  df-unit 20630  df-invr 20660  df-dvr 20673  df-rhm 20744  df-subrng 20840  df-subrg 20864  df-drng 21024  df-staf 21138  df-srng 21139  df-lmod 21179  df-lss 21249  df-lmhm 21339  df-lvec 21420  df-sra 21490  df-rgmod 21491  df-psmet 21712  df-xmet 21713  df-met 21714  df-bl 21715  df-mopn 21716  df-fbas 21717  df-fg 21718  df-cnfld 21721  df-phl 21976  df-ocv 22013  df-top 23256  df-topon 23273  df-topsp 23295  df-bases 23308  df-cld 23381  df-ntr 23382  df-cls 23383  df-nei 23460  df-cn 23589  df-cnp 23590  df-haus 23677  df-cmp 23749  df-tx 23925  df-hmeo 24118  df-fil 24209  df-flim 24302  df-fcls 24304  df-xms 24683  df-ms 24684  df-tms 24685  df-nm 24945  df-ngp 24946  df-nlm 24949  df-cncf 25243  df-clm 25428  df-cph 25533  df-cfil 25620  df-cmet 25622  df-cms 25700  df-bn 25701  df-hl 25702

This theorem is used by:  pjth  25804