hlhilhillem - Mathbox for Norm Megill

	Mathbox for Norm Megill		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > hlhilhillem		Structured version Visualization version GIF version

Theorem hlhilhillem 43017

Description: Lemma for hlhil 25764. (Contributed by NM, 23-Jun-2015.)

**Hypotheses**
Ref	Expression
hlhilphl.h	⊢ 𝐻 = (LHyp‘𝐾)
hlhilphllem.u	⊢ 𝑈 = ((HLHil‘𝐾)‘𝑊)
hlhilphl.k	⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
hlhilphllem.f	⊢ 𝐹 = (Scalar‘𝑈)
hlhilphllem.l	⊢ 𝐿 = ((DVecH‘𝐾)‘𝑊)
hlhilphllem.v	⊢ 𝑉 = (Base‘𝐿)
hlhilphllem.a	⊢ + = (+_g‘𝐿)
hlhilphllem.s	⊢ · = ( ·_𝑠 ‘𝐿)
hlhilphllem.r	⊢ 𝑅 = (Scalar‘𝐿)
hlhilphllem.b	⊢ 𝐵 = (Base‘𝑅)
hlhilphllem.p	⊢ ⨣ = (+_g‘𝑅)
hlhilphllem.t	⊢ × = (._r‘𝑅)
hlhilphllem.q	⊢ 𝑄 = (0_g‘𝑅)
hlhilphllem.z	⊢ 0 = (0_g‘𝐿)
hlhilphllem.i	⊢ , = (·_𝑖‘𝑈)
hlhilphllem.j	⊢ 𝐽 = ((HDMap‘𝐾)‘𝑊)
hlhilphllem.g	⊢ 𝐺 = ((HGMap‘𝐾)‘𝑊)
hlhilphllem.e	⊢ 𝐸 = (𝑥 ∈ 𝑉, 𝑦 ∈ 𝑉 ↦ ((𝐽‘𝑦)‘𝑥))
hlhilphllem.o	⊢ 𝑂 = (ocv‘𝑈)
hlhilphllem.c	⊢ 𝐶 = (ClSubSp‘𝑈)

**Assertion**
Ref	Expression
hlhilhillem	⊢ (𝜑 → 𝑈 ∈ Hil)

Distinct variable groups: 𝑥,𝑦,𝐾 𝑥,𝑈 𝑥,𝑊,𝑦 𝜑,𝑥 𝑥,𝐽,𝑦 𝑥,𝑉,𝑦 𝑥,𝐶 Allowed substitution hints: 𝜑(𝑦) 𝐵(𝑥, 𝑦) 𝐶(𝑦) + (𝑥, 𝑦) ⨣ (𝑥, 𝑦) 𝑄(𝑥, 𝑦) 𝑅(𝑥, 𝑦) · (𝑥, 𝑦) × (𝑥, 𝑦) 𝑈(𝑦) 𝐸(𝑥, 𝑦) 𝐹(𝑥, 𝑦) 𝐺(𝑥, 𝑦) 𝐻(𝑥, 𝑦) , (𝑥, 𝑦) 𝐿(𝑥, 𝑦) 𝑂(𝑥, 𝑦) 0 (𝑥, 𝑦)

**Proof of Theorem hlhilhillem**
Step	Hyp	Ref	Expression
1		hlhilphl.h	. . 3 ⊢ 𝐻 = (LHyp‘𝐾)
2		hlhilphllem.u	. . 3 ⊢ 𝑈 = ((HLHil‘𝐾)‘𝑊)
3		hlhilphl.k	. . 3 ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
4		hlhilphllem.f	. . 3 ⊢ 𝐹 = (Scalar‘𝑈)
5		hlhilphllem.l	. . 3 ⊢ 𝐿 = ((DVecH‘𝐾)‘𝑊)
6		hlhilphllem.v	. . 3 ⊢ 𝑉 = (Base‘𝐿)
7		hlhilphllem.a	. . 3 ⊢ + = (+_g‘𝐿)
8		hlhilphllem.s	. . 3 ⊢ · = ( ·_𝑠 ‘𝐿)
9		hlhilphllem.r	. . 3 ⊢ 𝑅 = (Scalar‘𝐿)
10		hlhilphllem.b	. . 3 ⊢ 𝐵 = (Base‘𝑅)
11		hlhilphllem.p	. . 3 ⊢ ⨣ = (+_g‘𝑅)
12		hlhilphllem.t	. . 3 ⊢ × = (._r‘𝑅)
13		hlhilphllem.q	. . 3 ⊢ 𝑄 = (0_g‘𝑅)
14		hlhilphllem.z	. . 3 ⊢ 0 = (0_g‘𝐿)
15		hlhilphllem.i	. . 3 ⊢ , = (·_𝑖‘𝑈)
16		hlhilphllem.j	. . 3 ⊢ 𝐽 = ((HDMap‘𝐾)‘𝑊)
17		hlhilphllem.g	. . 3 ⊢ 𝐺 = ((HGMap‘𝐾)‘𝑊)
18		hlhilphllem.e	. . 3 ⊢ 𝐸 = (𝑥 ∈ 𝑉, 𝑦 ∈ 𝑉 ↦ ((𝐽‘𝑦)‘𝑥))
19	1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18	hlhilphllem 43016	. 2 ⊢ (𝜑 → 𝑈 ∈ PreHil)
20	3	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
21		eqid 2761	. . . . . . 7 ⊢ ((ocH‘𝐾)‘𝑊) = ((ocH‘𝐾)‘𝑊)
22		hlhilphllem.o	. . . . . . 7 ⊢ 𝑂 = (ocv‘𝑈)
23		eqid 2761	. . . . . . . . . . 11 ⊢ ((DIsoH‘𝐾)‘𝑊) = ((DIsoH‘𝐾)‘𝑊)
24		hlhilphllem.c	. . . . . . . . . . 11 ⊢ 𝐶 = (ClSubSp‘𝑈)
25	1, 23, 2, 24, 3	hlhillcs 43015	. . . . . . . . . 10 ⊢ (𝜑 → 𝐶 = ran ((DIsoH‘𝐾)‘𝑊))
26	25	eleq2d 2847	. . . . . . . . 9 ⊢ (𝜑 → (𝑥 ∈ 𝐶 ↔ 𝑥 ∈ ran ((DIsoH‘𝐾)‘𝑊)))
27	26	biimpa 482	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → 𝑥 ∈ ran ((DIsoH‘𝐾)‘𝑊))
28	1, 5, 23, 6	dihrnss 42335	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑥 ∈ ran ((DIsoH‘𝐾)‘𝑊)) → 𝑥 ⊆ 𝑉)
29	3, 28	sylan 592	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ran ((DIsoH‘𝐾)‘𝑊)) → 𝑥 ⊆ 𝑉)
30	27, 29	syldan 603	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → 𝑥 ⊆ 𝑉)
31	1, 5, 2, 20, 6, 21, 22, 30	hlhilocv 43014	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → (𝑂‘𝑥) = (((ocH‘𝐾)‘𝑊)‘𝑥))
32	31	oveq2d 7436	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → (𝑥(LSSum‘𝐿)(𝑂‘𝑥)) = (𝑥(LSSum‘𝐿)(((ocH‘𝐾)‘𝑊)‘𝑥)))
33		eqid 2761	. . . . . . . 8 ⊢ (LSSum‘𝐿) = (LSSum‘𝐿)
34	1, 5, 2, 3, 33	hlhillsm 43013	. . . . . . 7 ⊢ (𝜑 → (LSSum‘𝐿) = (LSSum‘𝑈))
35	34	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → (LSSum‘𝐿) = (LSSum‘𝑈))
36	35	oveqd 7437	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → (𝑥(LSSum‘𝐿)(𝑂‘𝑥)) = (𝑥(LSSum‘𝑈)(𝑂‘𝑥)))
37		eqid 2761	. . . . . . 7 ⊢ (LSubSp‘𝐿) = (LSubSp‘𝐿)
38	3	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ran ((DIsoH‘𝐾)‘𝑊)) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
39	1, 5, 23, 37	dihrnlss 42334	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑥 ∈ ran ((DIsoH‘𝐾)‘𝑊)) → 𝑥 ∈ (LSubSp‘𝐿))
40	3, 39	sylan 592	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ran ((DIsoH‘𝐾)‘𝑊)) → 𝑥 ∈ (LSubSp‘𝐿))
41	1, 23, 5, 6, 21, 38, 29	dochoccl 42426	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ ran ((DIsoH‘𝐾)‘𝑊)) → (𝑥 ∈ ran ((DIsoH‘𝐾)‘𝑊) ↔ (((ocH‘𝐾)‘𝑊)‘(((ocH‘𝐾)‘𝑊)‘𝑥)) = 𝑥))
42	41	biimpd 232	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ ran ((DIsoH‘𝐾)‘𝑊)) → (𝑥 ∈ ran ((DIsoH‘𝐾)‘𝑊) → (((ocH‘𝐾)‘𝑊)‘(((ocH‘𝐾)‘𝑊)‘𝑥)) = 𝑥))
43	42	ex 418	. . . . . . . . 9 ⊢ (𝜑 → (𝑥 ∈ ran ((DIsoH‘𝐾)‘𝑊) → (𝑥 ∈ ran ((DIsoH‘𝐾)‘𝑊) → (((ocH‘𝐾)‘𝑊)‘(((ocH‘𝐾)‘𝑊)‘𝑥)) = 𝑥)))
44	43	pm2.43d 54	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ ran ((DIsoH‘𝐾)‘𝑊) → (((ocH‘𝐾)‘𝑊)‘(((ocH‘𝐾)‘𝑊)‘𝑥)) = 𝑥))
45	44	imp 412	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ran ((DIsoH‘𝐾)‘𝑊)) → (((ocH‘𝐾)‘𝑊)‘(((ocH‘𝐾)‘𝑊)‘𝑥)) = 𝑥)
46	1, 21, 5, 6, 37, 33, 38, 40, 45	dochexmid 42525	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ran ((DIsoH‘𝐾)‘𝑊)) → (𝑥(LSSum‘𝐿)(((ocH‘𝐾)‘𝑊)‘𝑥)) = 𝑉)
47	27, 46	syldan 603	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → (𝑥(LSSum‘𝐿)(((ocH‘𝐾)‘𝑊)‘𝑥)) = 𝑉)
48	32, 36, 47	3eqtr3d 2804	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → (𝑥(LSSum‘𝑈)(𝑂‘𝑥)) = 𝑉)
49	1, 2, 3, 5, 6	hlhilbase 42993	. . . . 5 ⊢ (𝜑 → 𝑉 = (Base‘𝑈))
50	49	adantr 486	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → 𝑉 = (Base‘𝑈))
51	48, 50	eqtrd 2796	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → (𝑥(LSSum‘𝑈)(𝑂‘𝑥)) = (Base‘𝑈))
52	51	ralrimiva 3155	. 2 ⊢ (𝜑 → ∀𝑥 ∈ 𝐶 (𝑥(LSSum‘𝑈)(𝑂‘𝑥)) = (Base‘𝑈))
53		eqid 2761	. . 3 ⊢ (Base‘𝑈) = (Base‘𝑈)
54		eqid 2761	. . 3 ⊢ (LSSum‘𝑈) = (LSSum‘𝑈)
55	53, 54, 22, 24	ishil2 22025	. 2 ⊢ (𝑈 ∈ Hil ↔ (𝑈 ∈ PreHil ∧ ∀𝑥 ∈ 𝐶 (𝑥(LSSum‘𝑈)(𝑂‘𝑥)) = (Base‘𝑈)))
56	19, 52, 55	sylanbrc 595	1 ⊢ (𝜑 → 𝑈 ∈ Hil)

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ∧ wa 401 = wceq 1570 ∈ wcel 2145 ∀wral 3077 ⊆ wss 3899 ran crn 5652 ‘cfv 6538 (class class class)co 7420 ∈ cmpo 7422 Basecbs 17387 +_gcplusg 17428 ._rcmulr 17429 Scalarcsca 17431 ·_𝑠 cvsca 17432 ·_𝑖cip 17433 0_gc0g 17610 LSSumclsm 19848 LSubSpclss 21206 PreHilcphl 21930 ocvcocv 21966 ClSubSpccss 21967 Hilchil 22007 HLchlt 40407 LHypclh 41041 DVecHcdvh 42135 DIsoHcdih 42285 ocHcoch 42404 HDMapchdma 42849 HGMapchg 42940 HLHilchlh 42989

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 7751 ax-cnex 11256 ax-resscn 11257 ax-1cn 11258 ax-icn 11259 ax-addcl 11260 ax-addrcl 11261 ax-mulcl 11262 ax-mulrcl 11263 ax-mulcom 11264 ax-addass 11265 ax-mulass 11266 ax-distr 11267 ax-i2m1 11268 ax-1ne0 11269 ax-1rid 11270 ax-rnegex 11271 ax-rrecex 11272 ax-cnre 11273 ax-pre-lttri 11274 ax-pre-lttrn 11275 ax-pre-ltadd 11276 ax-pre-mulgt0 11277 ax-riotaBAD 40010

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-ot 4593 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-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 6304 df-ord 6365 df-on 6366 df-lim 6367 df-suc 6368 df-iota 6494 df-fun 6540 df-fn 6541 df-f 6542 df-f1 6543 df-fo 6544 df-f1o 6545 df-fv 6546 df-riota 7377 df-ov 7423 df-oprab 7424 df-mpo 7425 df-of 7693 df-om 7878 df-1st 8001 df-2nd 8002 df-tpos 8243 df-undef 8290 df-frecs 8299 df-wrecs 8330 df-recs 8379 df-rdg 8418 df-1o 8476 df-2o 8477 df-er 8717 df-map 8849 df-en 8974 df-dom 8975 df-sdom 8976 df-fin 8977 df-pnf 11345 df-mnf 11346 df-xr 11347 df-ltxr 11348 df-le 11349 df-sub 11543 df-neg 11544 df-nn 12336 df-2 12405 df-3 12406 df-4 12407 df-5 12408 df-6 12409 df-7 12410 df-8 12411 df-n0 12607 df-z 12694 df-uz 12966 df-fz 13640 df-struct 17325 df-sets 17342 df-slot 17360 df-ndx 17372 df-base 17388 df-ress 17409 df-plusg 17441 df-mulr 17442 df-starv 17443 df-sca 17444 df-vsca 17445 df-ip 17446 df-0g 17612 df-mre 17756 df-mrc 17757 df-acs 17759 df-proset 18468 df-poset 18487 df-plt 18502 df-lub 18518 df-glb 18519 df-join 18520 df-meet 18521 df-p0 18597 df-p1 18598 df-lat 18606 df-clat 18673 df-mgm 18816 df-sgrp 18908 df-mnd 18924 df-mhm 18978 df-submnd 18979 df-grp 19147 df-minusg 19148 df-sbg 19149 df-subg 19333 df-ghm 19428 df-cntz 19531 df-oppg 19560 df-lsm 19850 df-pj1 19851 df-cmn 19996 df-abl 19997 df-mgp 20361 df-rng 20375 df-ur 20408 df-ring 20461 df-oppr 20567 df-dvdsr 20587 df-unit 20588 df-invr 20618 df-dvr 20631 df-rhm 20702 df-nzr 20763 df-subrg 20822 df-rlreg 20946 df-domn 20947 df-drng 20982 df-staf 21096 df-srng 21097 df-lmod 21137 df-lss 21207 df-lsp 21247 df-lmhm 21297 df-lvec 21378 df-sra 21448 df-rgmod 21449 df-phl 21932 df-ocv 21969 df-css 21970 df-pj 22009 df-hil 22010 df-lsatoms 40033 df-lshyp 40034 df-lcv 40076 df-lfl 40115 df-lkr 40143 df-ldual 40181 df-oposet 40233 df-ol 40235 df-oml 40236 df-covers 40323 df-ats 40324 df-atl 40355 df-cvlat 40379 df-hlat 40408 df-llines 40555 df-lplanes 40556 df-lvols 40557 df-lines 40558 df-psubsp 40560 df-pmap 40561 df-padd 40853 df-lhyp 41045 df-laut 41046 df-ldil 41161 df-ltrn 41162 df-trl 41216 df-tgrp 41800 df-tendo 41812 df-edring 41814 df-dveca 42060 df-disoa 42086 df-dvech 42136 df-dib 42196 df-dic 42230 df-dih 42286 df-doch 42405 df-djh 42452 df-lcdual 42644 df-mapd 42682 df-hvmap 42814 df-hdmap1 42850 df-hdmap 42851 df-hgmap 42941 df-hlhil 42990

This theorem is used by: hlathil 43018

W3C validator