Theorem pjthlem2 25752

Description: Lemma for pjth 25753. (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 25678	. . . . 5 ⊢ (𝑊 ∈ ℂHil → 𝑊 ∈ ℂPreHil)
6	4, 5	syl 18	. . . 4 ⊢ (𝜑 → 𝑊 ∈ ℂPreHil)
7		pjthlem.2	. . . . 5 ⊢ (𝜑 → 𝑈 ∈ 𝐿)
8		pjthlem.l	. . . . 5 ⊢ 𝐿 = (LSubSp‘𝑊)
9	7, 8	eleqtrdi 2871	. . . 4 ⊢ (𝜑 → 𝑈 ∈ (LSubSp‘𝑊))
10		pjthlem.3	. . . . 5 ⊢ (𝜑 → 𝑈 ∈ (Clsd‘𝐽))
11		hlcms 25680	. . . . . . 7 ⊢ (𝑊 ∈ ℂHil → 𝑊 ∈ CMetSp)
12	4, 11	syl 18	. . . . . 6 ⊢ (𝜑 → 𝑊 ∈ CMetSp)
13	1, 8	lssss 21204	. . . . . . 7 ⊢ (𝑈 ∈ 𝐿 → 𝑈 ⊆ 𝑉)
14	7, 13	syl 18	. . . . . 6 ⊢ (𝜑 → 𝑈 ⊆ 𝑉)
15		eqid 2761	. . . . . . 7 ⊢ (𝑊 ↾s 𝑈) = (𝑊 ↾s 𝑈)
16		pjthlem.j	. . . . . . 7 ⊢ 𝐽 = (TopOpen‘𝑊)
17	15, 1, 16	cmsss 25665	. . . . . 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 25750	. . 3 ⊢ (𝜑 → ∃!𝑥 ∈ 𝑈 ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))
22		reurex 3370	. . 3 ⊢ (∃!𝑥 ∈ 𝑈 ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)) → ∃𝑥 ∈ 𝑈 ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))
23	21, 22	syl 18	. 2 ⊢ (𝜑 → ∃𝑥 ∈ 𝑈 ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))
24	6	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) → 𝑊 ∈ ℂPreHil)
25		cphlmod 25488	. . . . . 6 ⊢ (𝑊 ∈ ℂPreHil → 𝑊 ∈ LMod)
26	24, 25	syl 18	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) → 𝑊 ∈ LMod)
27		lmodabl 21177	. . . . 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 3932	. . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) → 𝑥 ∈ 𝑉)
33	20	adantr 486	. . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) → 𝐴 ∈ 𝑉)
34		pjthlem.p	. . . . 5 ⊢ + = (+g‘𝑊)
35	1, 34, 2	ablpncan3 20023	. . . 4 ⊢ ((𝑊 ∈ Abel ∧ (𝑥 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉)) → (𝑥 + (𝐴 − 𝑥)) = 𝐴)
36	28, 32, 33, 35	syl12anc 850	. . 3 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) → (𝑥 + (𝐴 − 𝑥)) = 𝐴)
37	8	lsssssubg 21226	. . . . . 6 ⊢ (𝑊 ∈ LMod → 𝐿 ⊆ (SubGrp‘𝑊))
38	26, 37	syl 18	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) → 𝐿 ⊆ (SubGrp‘𝑊))
39	38, 29	sseldd 3932	. . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) → 𝑈 ∈ (SubGrp‘𝑊))
40		cphphl 25485	. . . . . . 7 ⊢ (𝑊 ∈ ℂPreHil → 𝑊 ∈ PreHil)
41	24, 40	syl 18	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) → 𝑊 ∈ PreHil)
42		pjthlem.o	. . . . . . 7 ⊢ 𝑂 = (ocv‘𝑊)
43	1, 42, 8	ocvlss 21971	. . . . . 6 ⊢ ((𝑊 ∈ PreHil ∧ 𝑈 ⊆ 𝑉) → (𝑂‘𝑈) ∈ 𝐿)
44	41, 30, 43	syl2anc 596	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) → (𝑂‘𝑈) ∈ 𝐿)
45	38, 44	sseldd 3932	. . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) → (𝑂‘𝑈) ∈ (SubGrp‘𝑊))
46	1, 2	lmodvsubcl 21175	. . . . . 6 ⊢ ((𝑊 ∈ LMod ∧ 𝐴 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉) → (𝐴 − 𝑥) ∈ 𝑉)
47	26, 33, 32, 46	syl3anc 1398	. . . . 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 7426	. . . . . . . . . . . . . 14 ⊢ (𝑦 = (𝑤 + 𝑥) → (𝐴 − 𝑦) = (𝐴 − (𝑤 + 𝑥)))
54	53	fveq2d 6887	. . . . . . . . . . . . 13 ⊢ (𝑦 = (𝑤 + 𝑥) → (𝑁‘(𝐴 − 𝑦)) = (𝑁‘(𝐴 − (𝑤 + 𝑥))))
55	54	breq2d 5115	. . . . . . . . . . . 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 21211	. . . . . . . . . . . . 13 ⊢ (((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝐿) ∧ (𝑤 ∈ 𝑈 ∧ 𝑥 ∈ 𝑈)) → (𝑤 + 𝑥) ∈ 𝑈)
62	57, 58, 59, 60, 61	syl22anc 852	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) ∧ 𝑤 ∈ 𝑈) → (𝑤 + 𝑥) ∈ 𝑈)
63	55, 56, 62	rspcdva 3578	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) ∧ 𝑤 ∈ 𝑈) → (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − (𝑤 + 𝑥))))
64		lmodgrp 21135	. . . . . . . . . . . . . . 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 3931	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) ∧ 𝑤 ∈ 𝑈) → 𝑤 ∈ 𝑉)
70	1, 34, 2	grpsubsub4 19236	. . . . . . . . . . . . 13 ⊢ ((𝑊 ∈ Grp ∧ (𝐴 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉 ∧ 𝑤 ∈ 𝑉)) → ((𝐴 − 𝑥) − 𝑤) = (𝐴 − (𝑤 + 𝑥)))
71	66, 67, 68, 69, 70	syl13anc 1399	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) ∧ 𝑤 ∈ 𝑈) → ((𝐴 − 𝑥) − 𝑤) = (𝐴 − (𝑤 + 𝑥)))
72	71	fveq2d 6887	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) ∧ 𝑤 ∈ 𝑈) → (𝑁‘((𝐴 − 𝑥) − 𝑤)) = (𝑁‘(𝐴 − (𝑤 + 𝑥))))
73	63, 72	breqtrrd 5133	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) ∧ 𝑤 ∈ 𝑈) → (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘((𝐴 − 𝑥) − 𝑤)))
74	73	ralrimiva 3155	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) → ∀𝑤 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘((𝐴 − 𝑥) − 𝑤)))
75	74	adantr 486	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) ∧ 𝑧 ∈ 𝑈) → ∀𝑤 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘((𝐴 − 𝑥) − 𝑤)))
76		eqid 2761	. . . . . . . 8 ⊢ (((𝐴 − 𝑥) , 𝑧) / ((𝑧 , 𝑧) + 1)) = (((𝐴 − 𝑥) , 𝑧) / ((𝑧 , 𝑧) + 1))
77	1, 3, 34, 2, 48, 8, 49, 50, 51, 52, 75, 76	pjthlem1 25751	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) ∧ 𝑧 ∈ 𝑈) → ((𝐴 − 𝑥) , 𝑧) = 0)
78	24	adantr 486	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) ∧ 𝑧 ∈ 𝑈) → 𝑊 ∈ ℂPreHil)
79		cphclm 25503	. . . . . . . . 9 ⊢ (𝑊 ∈ ℂPreHil → 𝑊 ∈ ℂMod)
80	78, 79	syl 18	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) ∧ 𝑧 ∈ 𝑈) → 𝑊 ∈ ℂMod)
81		eqid 2761	. . . . . . . . 9 ⊢ (Scalar‘𝑊) = (Scalar‘𝑊)
82	81	clm0 25386	. . . . . . . 8 ⊢ (𝑊 ∈ ℂMod → 0 = (0g‘(Scalar‘𝑊)))
83	80, 82	syl 18	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) ∧ 𝑧 ∈ 𝑈) → 0 = (0g‘(Scalar‘𝑊)))
84	77, 83	eqtrd 2796	. . . . . 6 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) ∧ 𝑧 ∈ 𝑈) → ((𝐴 − 𝑥) , 𝑧) = (0g‘(Scalar‘𝑊)))
85	84	ralrimiva 3155	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) → ∀𝑧 ∈ 𝑈 ((𝐴 − 𝑥) , 𝑧) = (0g‘(Scalar‘𝑊)))
86		eqid 2761	. . . . . 6 ⊢ (0g‘(Scalar‘𝑊)) = (0g‘(Scalar‘𝑊))
87	1, 48, 81, 86, 42	elocv 21967	. . . . 5 ⊢ ((𝐴 − 𝑥) ∈ (𝑂‘𝑈) ↔ (𝑈 ⊆ 𝑉 ∧ (𝐴 − 𝑥) ∈ 𝑉 ∧ ∀𝑧 ∈ 𝑈 ((𝐴 − 𝑥) , 𝑧) = (0g‘(Scalar‘𝑊))))
88	30, 47, 85, 87	syl3anbrc 1362	. . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) → (𝐴 − 𝑥) ∈ (𝑂‘𝑈))
89		pjthlem.s	. . . . 5 ⊢ ⊕ = (LSSum‘𝑊)
90	34, 89	lsmelvali 19857	. . . 4 ⊢ (((𝑈 ∈ (SubGrp‘𝑊) ∧ (𝑂‘𝑈) ∈ (SubGrp‘𝑊)) ∧ (𝑥 ∈ 𝑈 ∧ (𝐴 − 𝑥) ∈ (𝑂‘𝑈))) → (𝑥 + (𝐴 − 𝑥)) ∈ (𝑈 ⊕ (𝑂‘𝑈)))
91	39, 45, 31, 88, 90	syl22anc 852	. . 3 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) → (𝑥 + (𝐴 − 𝑥)) ∈ (𝑈 ⊕ (𝑂‘𝑈)))
92	36, 91	eqeltrrd 2862	. 2 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) → 𝐴 ∈ (𝑈 ⊕ (𝑂‘𝑈)))
93	23, 92	rexlimddv 3170	1 ⊢ (𝜑 → 𝐴 ∈ (𝑈 ⊕ (𝑂‘𝑈)))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1570   ∈ wcel 2145  ∀wral 3077  ∃wrex 3087  ∃!wreu 3364   ⊆ wss 3899   class class class wbr 5103  ‘cfv 6537  (class class class)co 7418  0cc0 11193  1c1 11194   + caddc 11196   ≤ cle 11337   / cdiv 11966  Basecbs 17380   ↾_s cress 17401  +_gcplusg 17421  Scalarcsca 17424  ·_𝑖cip 17426  TopOpenctopn 17585  0_gc0g 17603  Grpcgrp 19137  -_gcsg 19139  SubGrpcsubg 19323  LSSumclsm 19841  Abelcabl 19988  LModclmod 21128  LSubSpclss 21199  PreHilcphl 21923  ocvcocv 21959  Clsdccld 23327  normcnm 24888  ℂModcclm 25376  ℂPreHilccph 25480  CMetSpccms 25646  ℂHilchl 25648

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-rep 5232  ax-sep 5249  ax-nul 5260  ax-pow 5327  ax-pr 5391  ax-un 7749  ax-cnex 11249  ax-resscn 11250  ax-1cn 11251  ax-icn 11252  ax-addcl 11253  ax-addrcl 11254  ax-mulcl 11255  ax-mulrcl 11256  ax-mulcom 11257  ax-addass 11258  ax-mulass 11259  ax-distr 11260  ax-i2m1 11261  ax-1ne0 11262  ax-1rid 11263  ax-rnegex 11264  ax-rrecex 11265  ax-cnre 11266  ax-pre-lttri 11267  ax-pre-lttrn 11268  ax-pre-ltadd 11269  ax-pre-mulgt0 11270  ax-pre-sup 11271  ax-addf 11272  ax-mulf 11273

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 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-nel 3063  df-ral 3078  df-rex 3088  df-rmo 3366  df-reu 3367  df-rab 3414  df-v 3453  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-tp 4589  df-op 4591  df-uni 4868  df-int 4908  df-iun 4953  df-iin 4954  df-br 5104  df-opab 5168  df-mpt 5187  df-tr 5213  df-id 5546  df-eprel 5551  df-po 5559  df-so 5560  df-fr 5604  df-se 5605  df-we 5606  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-pred 6303  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-isom 6546  df-riota 7375  df-ov 7421  df-oprab 7422  df-mpo 7423  df-of 7691  df-om 7876  df-1st 7999  df-2nd 8000  df-supp 8171  df-tpos 8236  df-frecs 8292  df-wrecs 8323  df-recs 8372  df-rdg 8411  df-1o 8469  df-2o 8470  df-er 8710  df-map 8842  df-ixp 8919  df-en 8967  df-dom 8968  df-sdom 8969  df-fin 8970  df-fsupp 9347  df-fi 9396  df-sup 9427  df-inf 9428  df-oi 9497  df-card 10013  df-pnf 11338  df-mnf 11339  df-xr 11340  df-ltxr 11341  df-le 11342  df-sub 11536  df-neg 11537  df-div 11967  df-nn 12329  df-2 12398  df-3 12399  df-4 12400  df-5 12401  df-6 12402  df-7 12403  df-8 12404  df-9 12405  df-n0 12600  df-z 12687  df-dec 12808  df-uz 12959  df-q 13069  df-rp 13114  df-xneg 13234  df-xadd 13235  df-xmul 13236  df-ioo 13473  df-ico 13475  df-icc 13476  df-fz 13633  df-fzo 13782  df-seq 14138  df-exp 14198  df-hash 14468  df-cj 15259  df-re 15260  df-im 15261  df-sqrt 15395  df-abs 15396  df-struct 17318  df-sets 17335  df-slot 17353  df-ndx 17365  df-base 17381  df-ress 17402  df-plusg 17434  df-mulr 17435  df-starv 17436  df-sca 17437  df-vsca 17438  df-ip 17439  df-tset 17440  df-ple 17441  df-ds 17443  df-unif 17444  df-hom 17445  df-cco 17446  df-rest 17586  df-topn 17587  df-0g 17605  df-gsum 17606  df-topgen 17607  df-pt 17608  df-prds 17611  df-xrs 17667  df-qtop 17672  df-imas 17673  df-xps 17675  df-mre 17749  df-mrc 17750  df-acs 17752  df-mgm 18809  df-sgrp 18901  df-mnd 18917  df-mhm 18971  df-submnd 18972  df-grp 19140  df-minusg 19141  df-sbg 19142  df-mulg 19271  df-subg 19326  df-ghm 19421  df-cntz 19524  df-lsm 19843  df-cmn 19989  df-abl 19990  df-mgp 20354  df-rng 20368  df-ur 20401  df-ring 20454  df-cring 20455  df-oppr 20560  df-dvdsr 20580  df-unit 20581  df-invr 20611  df-dvr 20624  df-rhm 20695  df-subrng 20791  df-subrg 20815  df-drng 20975  df-staf 21089  df-srng 21090  df-lmod 21130  df-lss 21200  df-lmhm 21290  df-lvec 21371  df-sra 21441  df-rgmod 21442  df-psmet 21663  df-xmet 21664  df-met 21665  df-bl 21666  df-mopn 21667  df-fbas 21668  df-fg 21669  df-cnfld 21672  df-phl 21925  df-ocv 21962  df-top 23205  df-topon 23222  df-topsp 23244  df-bases 23257  df-cld 23330  df-ntr 23331  df-cls 23332  df-nei 23409  df-cn 23538  df-cnp 23539  df-haus 23626  df-cmp 23698  df-tx 23874  df-hmeo 24067  df-fil 24158  df-flim 24251  df-fcls 24253  df-xms 24632  df-ms 24633  df-tms 24634  df-nm 24894  df-ngp 24895  df-nlm 24898  df-cncf 25192  df-clm 25377  df-cph 25482  df-cfil 25569  df-cmet 25571  df-cms 25649  df-bn 25650  df-hl 25651

This theorem is used by:  pjth  25753