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 23724

Description: Lemma for pjth 23725. (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 23650	. . . . 5 ⊢ (𝑊 ∈ ℂHil → 𝑊 ∈ ℂPreHil)
6	4, 5	syl 17	. . . 4 ⊢ (𝜑 → 𝑊 ∈ ℂPreHil)
7		pjthlem.2	. . . . 5 ⊢ (𝜑 → 𝑈 ∈ 𝐿)
8		pjthlem.l	. . . . 5 ⊢ 𝐿 = (LSubSp‘𝑊)
9	7, 8	syl6eleq 2893	. . . 4 ⊢ (𝜑 → 𝑈 ∈ (LSubSp‘𝑊))
10		pjthlem.3	. . . . 5 ⊢ (𝜑 → 𝑈 ∈ (Clsd‘𝐽))
11		hlcms 23652	. . . . . . 7 ⊢ (𝑊 ∈ ℂHil → 𝑊 ∈ CMetSp)
12	4, 11	syl 17	. . . . . 6 ⊢ (𝜑 → 𝑊 ∈ CMetSp)
13	1, 8	lssss 19398	. . . . . . 7 ⊢ (𝑈 ∈ 𝐿 → 𝑈 ⊆ 𝑉)
14	7, 13	syl 17	. . . . . 6 ⊢ (𝜑 → 𝑈 ⊆ 𝑉)
15		eqid 2795	. . . . . . 7 ⊢ (𝑊 ↾_s 𝑈) = (𝑊 ↾_s 𝑈)
16		pjthlem.j	. . . . . . 7 ⊢ 𝐽 = (TopOpen‘𝑊)
17	15, 1, 16	cmsss 23637	. . . . . 6 ⊢ ((𝑊 ∈ CMetSp ∧ 𝑈 ⊆ 𝑉) → ((𝑊 ↾_s 𝑈) ∈ CMetSp ↔ 𝑈 ∈ (Clsd‘𝐽)))
18	12, 14, 17	syl2anc 584	. . . . 5 ⊢ (𝜑 → ((𝑊 ↾_s 𝑈) ∈ CMetSp ↔ 𝑈 ∈ (Clsd‘𝐽)))
19	10, 18	mpbird 258	. . . 4 ⊢ (𝜑 → (𝑊 ↾_s 𝑈) ∈ CMetSp)
20		pjthlem.4	. . . 4 ⊢ (𝜑 → 𝐴 ∈ 𝑉)
21	1, 2, 3, 6, 9, 19, 20	minvec 23722	. . 3 ⊢ (𝜑 → ∃!𝑥 ∈ 𝑈 ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))
22		reurex 3391	. . 3 ⊢ (∃!𝑥 ∈ 𝑈 ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)) → ∃𝑥 ∈ 𝑈 ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))
23	21, 22	syl 17	. 2 ⊢ (𝜑 → ∃𝑥 ∈ 𝑈 ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))
24	6	adantr 481	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) → 𝑊 ∈ ℂPreHil)
25		cphlmod 23461	. . . . . 6 ⊢ (𝑊 ∈ ℂPreHil → 𝑊 ∈ LMod)
26	24, 25	syl 17	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) → 𝑊 ∈ LMod)
27		lmodabl 19371	. . . . 5 ⊢ (𝑊 ∈ LMod → 𝑊 ∈ Abel)
28	26, 27	syl 17	. . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) → 𝑊 ∈ Abel)
29	7	adantr 481	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) → 𝑈 ∈ 𝐿)
30	29, 13	syl 17	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) → 𝑈 ⊆ 𝑉)
31		simprl 767	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) → 𝑥 ∈ 𝑈)
32	30, 31	sseldd 3890	. . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) → 𝑥 ∈ 𝑉)
33	20	adantr 481	. . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) → 𝐴 ∈ 𝑉)
34		pjthlem.p	. . . . 5 ⊢ + = (+_g‘𝑊)
35	1, 34, 2	ablpncan3 18662	. . . 4 ⊢ ((𝑊 ∈ Abel ∧ (𝑥 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉)) → (𝑥 + (𝐴 − 𝑥)) = 𝐴)
36	28, 32, 33, 35	syl12anc 833	. . 3 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) → (𝑥 + (𝐴 − 𝑥)) = 𝐴)
37	8	lsssssubg 19420	. . . . . 6 ⊢ (𝑊 ∈ LMod → 𝐿 ⊆ (SubGrp‘𝑊))
38	26, 37	syl 17	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) → 𝐿 ⊆ (SubGrp‘𝑊))
39	38, 29	sseldd 3890	. . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) → 𝑈 ∈ (SubGrp‘𝑊))
40		cphphl 23458	. . . . . . 7 ⊢ (𝑊 ∈ ℂPreHil → 𝑊 ∈ PreHil)
41	24, 40	syl 17	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) → 𝑊 ∈ PreHil)
42		pjthlem.o	. . . . . . 7 ⊢ 𝑂 = (ocv‘𝑊)
43	1, 42, 8	ocvlss 20498	. . . . . 6 ⊢ ((𝑊 ∈ PreHil ∧ 𝑈 ⊆ 𝑉) → (𝑂‘𝑈) ∈ 𝐿)
44	41, 30, 43	syl2anc 584	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) → (𝑂‘𝑈) ∈ 𝐿)
45	38, 44	sseldd 3890	. . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) → (𝑂‘𝑈) ∈ (SubGrp‘𝑊))
46	1, 2	lmodvsubcl 19369	. . . . . 6 ⊢ ((𝑊 ∈ LMod ∧ 𝐴 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉) → (𝐴 − 𝑥) ∈ 𝑉)
47	26, 33, 32, 46	syl3anc 1364	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) → (𝐴 − 𝑥) ∈ 𝑉)
48		pjthlem.h	. . . . . . . 8 ⊢ , = (·_𝑖‘𝑊)
49	4	ad2antrr 722	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) ∧ 𝑧 ∈ 𝑈) → 𝑊 ∈ ℂHil)
50	29	adantr 481	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) ∧ 𝑧 ∈ 𝑈) → 𝑈 ∈ 𝐿)
51	47	adantr 481	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) ∧ 𝑧 ∈ 𝑈) → (𝐴 − 𝑥) ∈ 𝑉)
52		simpr 485	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) ∧ 𝑧 ∈ 𝑈) → 𝑧 ∈ 𝑈)
53		oveq2 7024	. . . . . . . . . . . . . 14 ⊢ (𝑦 = (𝑤 + 𝑥) → (𝐴 − 𝑦) = (𝐴 − (𝑤 + 𝑥)))
54	53	fveq2d 6542	. . . . . . . . . . . . 13 ⊢ (𝑦 = (𝑤 + 𝑥) → (𝑁‘(𝐴 − 𝑦)) = (𝑁‘(𝐴 − (𝑤 + 𝑥))))
55	54	breq2d 4974	. . . . . . . . . . . 12 ⊢ (𝑦 = (𝑤 + 𝑥) → ((𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)) ↔ (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − (𝑤 + 𝑥)))))
56		simplrr 774	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) ∧ 𝑤 ∈ 𝑈) → ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))
57	26	adantr 481	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) ∧ 𝑤 ∈ 𝑈) → 𝑊 ∈ LMod)
58	29	adantr 481	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) ∧ 𝑤 ∈ 𝑈) → 𝑈 ∈ 𝐿)
59		simpr 485	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) ∧ 𝑤 ∈ 𝑈) → 𝑤 ∈ 𝑈)
60	31	adantr 481	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) ∧ 𝑤 ∈ 𝑈) → 𝑥 ∈ 𝑈)
61	34, 8	lssvacl 19416	. . . . . . . . . . . . 13 ⊢ (((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝐿) ∧ (𝑤 ∈ 𝑈 ∧ 𝑥 ∈ 𝑈)) → (𝑤 + 𝑥) ∈ 𝑈)
62	57, 58, 59, 60, 61	syl22anc 835	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) ∧ 𝑤 ∈ 𝑈) → (𝑤 + 𝑥) ∈ 𝑈)
63	55, 56, 62	rspcdva 3565	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) ∧ 𝑤 ∈ 𝑈) → (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − (𝑤 + 𝑥))))
64		lmodgrp 19331	. . . . . . . . . . . . . . 15 ⊢ (𝑊 ∈ LMod → 𝑊 ∈ Grp)
65	26, 64	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) → 𝑊 ∈ Grp)
66	65	adantr 481	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) ∧ 𝑤 ∈ 𝑈) → 𝑊 ∈ Grp)
67	33	adantr 481	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) ∧ 𝑤 ∈ 𝑈) → 𝐴 ∈ 𝑉)
68	32	adantr 481	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) ∧ 𝑤 ∈ 𝑈) → 𝑥 ∈ 𝑉)
69	30	sselda 3889	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) ∧ 𝑤 ∈ 𝑈) → 𝑤 ∈ 𝑉)
70	1, 34, 2	grpsubsub4 17949	. . . . . . . . . . . . 13 ⊢ ((𝑊 ∈ Grp ∧ (𝐴 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉 ∧ 𝑤 ∈ 𝑉)) → ((𝐴 − 𝑥) − 𝑤) = (𝐴 − (𝑤 + 𝑥)))
71	66, 67, 68, 69, 70	syl13anc 1365	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) ∧ 𝑤 ∈ 𝑈) → ((𝐴 − 𝑥) − 𝑤) = (𝐴 − (𝑤 + 𝑥)))
72	71	fveq2d 6542	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) ∧ 𝑤 ∈ 𝑈) → (𝑁‘((𝐴 − 𝑥) − 𝑤)) = (𝑁‘(𝐴 − (𝑤 + 𝑥))))
73	63, 72	breqtrrd 4990	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) ∧ 𝑤 ∈ 𝑈) → (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘((𝐴 − 𝑥) − 𝑤)))
74	73	ralrimiva 3149	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) → ∀𝑤 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘((𝐴 − 𝑥) − 𝑤)))
75	74	adantr 481	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) ∧ 𝑧 ∈ 𝑈) → ∀𝑤 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘((𝐴 − 𝑥) − 𝑤)))
76		eqid 2795	. . . . . . . 8 ⊢ (((𝐴 − 𝑥) , 𝑧) / ((𝑧 , 𝑧) + 1)) = (((𝐴 − 𝑥) , 𝑧) / ((𝑧 , 𝑧) + 1))
77	1, 3, 34, 2, 48, 8, 49, 50, 51, 52, 75, 76	pjthlem1 23723	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) ∧ 𝑧 ∈ 𝑈) → ((𝐴 − 𝑥) , 𝑧) = 0)
78	24	adantr 481	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) ∧ 𝑧 ∈ 𝑈) → 𝑊 ∈ ℂPreHil)
79		cphclm 23476	. . . . . . . . 9 ⊢ (𝑊 ∈ ℂPreHil → 𝑊 ∈ ℂMod)
80	78, 79	syl 17	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) ∧ 𝑧 ∈ 𝑈) → 𝑊 ∈ ℂMod)
81		eqid 2795	. . . . . . . . 9 ⊢ (Scalar‘𝑊) = (Scalar‘𝑊)
82	81	clm0 23359	. . . . . . . 8 ⊢ (𝑊 ∈ ℂMod → 0 = (0_g‘(Scalar‘𝑊)))
83	80, 82	syl 17	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) ∧ 𝑧 ∈ 𝑈) → 0 = (0_g‘(Scalar‘𝑊)))
84	77, 83	eqtrd 2831	. . . . . 6 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) ∧ 𝑧 ∈ 𝑈) → ((𝐴 − 𝑥) , 𝑧) = (0_g‘(Scalar‘𝑊)))
85	84	ralrimiva 3149	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) → ∀𝑧 ∈ 𝑈 ((𝐴 − 𝑥) , 𝑧) = (0_g‘(Scalar‘𝑊)))
86		eqid 2795	. . . . . 6 ⊢ (0_g‘(Scalar‘𝑊)) = (0_g‘(Scalar‘𝑊))
87	1, 48, 81, 86, 42	elocv 20494	. . . . 5 ⊢ ((𝐴 − 𝑥) ∈ (𝑂‘𝑈) ↔ (𝑈 ⊆ 𝑉 ∧ (𝐴 − 𝑥) ∈ 𝑉 ∧ ∀𝑧 ∈ 𝑈 ((𝐴 − 𝑥) , 𝑧) = (0_g‘(Scalar‘𝑊))))
88	30, 47, 85, 87	syl3anbrc 1336	. . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) → (𝐴 − 𝑥) ∈ (𝑂‘𝑈))
89		pjthlem.s	. . . . 5 ⊢ ⊕ = (LSSum‘𝑊)
90	34, 89	lsmelvali 18505	. . . 4 ⊢ (((𝑈 ∈ (SubGrp‘𝑊) ∧ (𝑂‘𝑈) ∈ (SubGrp‘𝑊)) ∧ (𝑥 ∈ 𝑈 ∧ (𝐴 − 𝑥) ∈ (𝑂‘𝑈))) → (𝑥 + (𝐴 − 𝑥)) ∈ (𝑈 ⊕ (𝑂‘𝑈)))
91	39, 45, 31, 88, 90	syl22anc 835	. . 3 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) → (𝑥 + (𝐴 − 𝑥)) ∈ (𝑈 ⊕ (𝑂‘𝑈)))
92	36, 91	eqeltrrd 2884	. 2 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) → 𝐴 ∈ (𝑈 ⊕ (𝑂‘𝑈)))
93	23, 92	rexlimddv 3254	1 ⊢ (𝜑 → 𝐴 ∈ (𝑈 ⊕ (𝑂‘𝑈)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 207 ∧ wa 396 = wceq 1522 ∈ wcel 2081 ∀wral 3105 ∃wrex 3106 ∃!wreu 3107 ⊆ wss 3859 class class class wbr 4962 ‘cfv 6225 (class class class)co 7016 0cc0 10383 1c1 10384 + caddc 10386 ≤ cle 10522 / cdiv 11145 Basecbs 16312 ↾_s cress 16313 +_gcplusg 16394 Scalarcsca 16397 ·_𝑖cip 16399 TopOpenctopn 16524 0_gc0g 16542 Grpcgrp 17861 -_gcsg 17863 SubGrpcsubg 18027 LSSumclsm 18489 Abelcabl 18634 LModclmod 19324 LSubSpclss 19393 PreHilcphl 20450 ocvcocv 20486 Clsdccld 21308 normcnm 22869 ℂModcclm 23349 ℂPreHilccph 23453 CMetSpccms 23618 ℂHilchl 23620

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1777 ax-4 1791 ax-5 1888 ax-6 1947 ax-7 1992 ax-8 2083 ax-9 2091 ax-10 2112 ax-11 2126 ax-12 2141 ax-13 2344 ax-ext 2769 ax-rep 5081 ax-sep 5094 ax-nul 5101 ax-pow 5157 ax-pr 5221 ax-un 7319 ax-cnex 10439 ax-resscn 10440 ax-1cn 10441 ax-icn 10442 ax-addcl 10443 ax-addrcl 10444 ax-mulcl 10445 ax-mulrcl 10446 ax-mulcom 10447 ax-addass 10448 ax-mulass 10449 ax-distr 10450 ax-i2m1 10451 ax-1ne0 10452 ax-1rid 10453 ax-rnegex 10454 ax-rrecex 10455 ax-cnre 10456 ax-pre-lttri 10457 ax-pre-lttrn 10458 ax-pre-ltadd 10459 ax-pre-mulgt0 10460 ax-pre-sup 10461 ax-addf 10462 ax-mulf 10463

This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-3or 1081 df-3an 1082 df-tru 1525 df-ex 1762 df-nf 1766 df-sb 2043 df-mo 2576 df-eu 2612 df-clab 2776 df-cleq 2788 df-clel 2863 df-nfc 2935 df-ne 2985 df-nel 3091 df-ral 3110 df-rex 3111 df-reu 3112 df-rmo 3113 df-rab 3114 df-v 3439 df-sbc 3707 df-csb 3812 df-dif 3862 df-un 3864 df-in 3866 df-ss 3874 df-pss 3876 df-nul 4212 df-if 4382 df-pw 4455 df-sn 4473 df-pr 4475 df-tp 4477 df-op 4479 df-uni 4746 df-int 4783 df-iun 4827 df-iin 4828 df-br 4963 df-opab 5025 df-mpt 5042 df-tr 5064 df-id 5348 df-eprel 5353 df-po 5362 df-so 5363 df-fr 5402 df-se 5403 df-we 5404 df-xp 5449 df-rel 5450 df-cnv 5451 df-co 5452 df-dm 5453 df-rn 5454 df-res 5455 df-ima 5456 df-pred 6023 df-ord 6069 df-on 6070 df-lim 6071 df-suc 6072 df-iota 6189 df-fun 6227 df-fn 6228 df-f 6229 df-f1 6230 df-fo 6231 df-f1o 6232 df-fv 6233 df-isom 6234 df-riota 6977 df-ov 7019 df-oprab 7020 df-mpo 7021 df-of 7267 df-om 7437 df-1st 7545 df-2nd 7546 df-supp 7682 df-tpos 7743 df-wrecs 7798 df-recs 7860 df-rdg 7898 df-1o 7953 df-2o 7954 df-oadd 7957 df-er 8139 df-map 8258 df-ixp 8311 df-en 8358 df-dom 8359 df-sdom 8360 df-fin 8361 df-fsupp 8680 df-fi 8721 df-sup 8752 df-inf 8753 df-oi 8820 df-card 9214 df-pnf 10523 df-mnf 10524 df-xr 10525 df-ltxr 10526 df-le 10527 df-sub 10719 df-neg 10720 df-div 11146 df-nn 11487 df-2 11548 df-3 11549 df-4 11550 df-5 11551 df-6 11552 df-7 11553 df-8 11554 df-9 11555 df-n0 11746 df-z 11830 df-dec 11948 df-uz 12094 df-q 12198 df-rp 12240 df-xneg 12357 df-xadd 12358 df-xmul 12359 df-ioo 12592 df-ico 12594 df-icc 12595 df-fz 12743 df-fzo 12884 df-seq 13220 df-exp 13280 df-hash 13541 df-cj 14292 df-re 14293 df-im 14294 df-sqrt 14428 df-abs 14429 df-struct 16314 df-ndx 16315 df-slot 16316 df-base 16318 df-sets 16319 df-ress 16320 df-plusg 16407 df-mulr 16408 df-starv 16409 df-sca 16410 df-vsca 16411 df-ip 16412 df-tset 16413 df-ple 16414 df-ds 16416 df-unif 16417 df-hom 16418 df-cco 16419 df-rest 16525 df-topn 16526 df-0g 16544 df-gsum 16545 df-topgen 16546 df-pt 16547 df-prds 16550 df-xrs 16604 df-qtop 16609 df-imas 16610 df-xps 16612 df-mre 16686 df-mrc 16687 df-acs 16689 df-mgm 17681 df-sgrp 17723 df-mnd 17734 df-mhm 17774 df-submnd 17775 df-grp 17864 df-minusg 17865 df-sbg 17866 df-mulg 17982 df-subg 18030 df-ghm 18097 df-cntz 18188 df-lsm 18491 df-cmn 18635 df-abl 18636 df-mgp 18930 df-ur 18942 df-ring 18989 df-cring 18990 df-oppr 19063 df-dvdsr 19081 df-unit 19082 df-invr 19112 df-dvr 19123 df-rnghom 19157 df-drng 19194 df-subrg 19223 df-staf 19306 df-srng 19307 df-lmod 19326 df-lss 19394 df-lmhm 19484 df-lvec 19565 df-sra 19634 df-rgmod 19635 df-psmet 20219 df-xmet 20220 df-met 20221 df-bl 20222 df-mopn 20223 df-fbas 20224 df-fg 20225 df-cnfld 20228 df-phl 20452 df-ocv 20489 df-top 21186 df-topon 21203 df-topsp 21225 df-bases 21238 df-cld 21311 df-ntr 21312 df-cls 21313 df-nei 21390 df-cn 21519 df-cnp 21520 df-haus 21607 df-cmp 21679 df-tx 21854 df-hmeo 22047 df-fil 22138 df-flim 22231 df-fcls 22233 df-xms 22613 df-ms 22614 df-tms 22615 df-nm 22875 df-ngp 22876 df-nlm 22879 df-cncf 23169 df-clm 23350 df-cph 23455 df-cfil 23541 df-cmet 23543 df-cms 23621 df-bn 23622 df-hl 23623

This theorem is referenced by: pjth 23725

W3C validator