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 43154

Description: Lemma for hlhil 25773. (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 43153	. 2 ⊢ (𝜑 → 𝑈 ∈ PreHil)
20	3	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
21		eqid 2760	. . . . . . 7 ⊢ ((ocH‘𝐾)‘𝑊) = ((ocH‘𝐾)‘𝑊)
22		hlhilphllem.o	. . . . . . 7 ⊢ 𝑂 = (ocv‘𝑈)
23		eqid 2760	. . . . . . . . . . 11 ⊢ ((DIsoH‘𝐾)‘𝑊) = ((DIsoH‘𝐾)‘𝑊)
24		hlhilphllem.c	. . . . . . . . . . 11 ⊢ 𝐶 = (ClSubSp‘𝑈)
25	1, 23, 2, 24, 3	hlhillcs 43152	. . . . . . . . . 10 ⊢ (𝜑 → 𝐶 = ran ((DIsoH‘𝐾)‘𝑊))
26	25	eleq2d 2846	. . . . . . . . 9 ⊢ (𝜑 → (𝑥 ∈ 𝐶 ↔ 𝑥 ∈ ran ((DIsoH‘𝐾)‘𝑊)))
27	26	biimpa 482	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → 𝑥 ∈ ran ((DIsoH‘𝐾)‘𝑊))
28	1, 5, 23, 6	dihrnss 42472	. . . . . . . . 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 43151	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → (𝑂‘𝑥) = (((ocH‘𝐾)‘𝑊)‘𝑥))
32	31	oveq2d 7440	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → (𝑥(LSSum‘𝐿)(𝑂‘𝑥)) = (𝑥(LSSum‘𝐿)(((ocH‘𝐾)‘𝑊)‘𝑥)))
33		eqid 2760	. . . . . . . 8 ⊢ (LSSum‘𝐿) = (LSSum‘𝐿)
34	1, 5, 2, 3, 33	hlhillsm 43150	. . . . . . 7 ⊢ (𝜑 → (LSSum‘𝐿) = (LSSum‘𝑈))
35	34	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → (LSSum‘𝐿) = (LSSum‘𝑈))
36	35	oveqd 7441	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → (𝑥(LSSum‘𝐿)(𝑂‘𝑥)) = (𝑥(LSSum‘𝑈)(𝑂‘𝑥)))
37		eqid 2760	. . . . . . 7 ⊢ (LSubSp‘𝐿) = (LSubSp‘𝐿)
38	3	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ran ((DIsoH‘𝐾)‘𝑊)) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
39	1, 5, 23, 37	dihrnlss 42471	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑥 ∈ ran ((DIsoH‘𝐾)‘𝑊)) → 𝑥 ∈ (LSubSp‘𝐿))
40	3, 39	sylan 592	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ran ((DIsoH‘𝐾)‘𝑊)) → 𝑥 ∈ (LSubSp‘𝐿))
41	1, 23, 5, 6, 21, 38, 29	dochoccl 42563	. . . . . . . . . . 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 42662	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ran ((DIsoH‘𝐾)‘𝑊)) → (𝑥(LSSum‘𝐿)(((ocH‘𝐾)‘𝑊)‘𝑥)) = 𝑉)
47	27, 46	syldan 603	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → (𝑥(LSSum‘𝐿)(((ocH‘𝐾)‘𝑊)‘𝑥)) = 𝑉)
48	32, 36, 47	3eqtr3d 2803	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → (𝑥(LSSum‘𝑈)(𝑂‘𝑥)) = 𝑉)
49	1, 2, 3, 5, 6	hlhilbase 43130	. . . . 5 ⊢ (𝜑 → 𝑉 = (Base‘𝑈))
50	49	adantr 486	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → 𝑉 = (Base‘𝑈))
51	48, 50	eqtrd 2795	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → (𝑥(LSSum‘𝑈)(𝑂‘𝑥)) = (Base‘𝑈))
52	51	ralrimiva 3154	. 2 ⊢ (𝜑 → ∀𝑥 ∈ 𝐶 (𝑥(LSSum‘𝑈)(𝑂‘𝑥)) = (Base‘𝑈))
53		eqid 2760	. . 3 ⊢ (Base‘𝑈) = (Base‘𝑈)
54		eqid 2760	. . 3 ⊢ (LSSum‘𝑈) = (LSSum‘𝑈)
55	53, 54, 22, 24	ishil2 22034	. 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 1569 ∈ wcel 2144 ∀wral 3076 ⊆ wss 3896 ran crn 5652 ‘cfv 6543 (class class class)co 7424 ∈ cmpo 7426 Basecbs 17396 +_gcplusg 17437 ._rcmulr 17438 Scalarcsca 17440 ·_𝑠 cvsca 17441 ·_𝑖cip 17442 0_gc0g 17619 LSSumclsm 19857 LSubSpclss 21215 PreHilcphl 21939 ocvcocv 21975 ClSubSpccss 21976 Hilchil 22016 HLchlt 40544 LHypclh 41178 DVecHcdvh 42272 DIsoHcdih 42422 ocHcoch 42541 HDMapchdma 42986 HGMapchg 43077 HLHilchlh 43126

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1827 ax-4 1841 ax-5 1942 ax-6 1999 ax-7 2040 ax-8 2146 ax-9 2154 ax-10 2177 ax-11 2193 ax-12 2212 ax-ext 2732 ax-rep 5231 ax-sep 5248 ax-nul 5259 ax-pow 5327 ax-pr 5391 ax-un 7755 ax-cnex 11263 ax-resscn 11264 ax-1cn 11265 ax-icn 11266 ax-addcl 11267 ax-addrcl 11268 ax-mulcl 11269 ax-mulrcl 11270 ax-mulcom 11271 ax-addass 11272 ax-mulass 11273 ax-distr 11274 ax-i2m1 11275 ax-1ne0 11276 ax-1rid 11277 ax-rnegex 11278 ax-rrecex 11279 ax-cnre 11280 ax-pre-lttri 11281 ax-pre-lttrn 11282 ax-pre-ltadd 11283 ax-pre-mulgt0 11284 ax-riotaBAD 40147

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1572 df-fal 1582 df-ex 1812 df-nf 1816 df-sb 2099 df-mo 2564 df-eu 2594 df-clab 2739 df-cleq 2752 df-clel 2835 df-nfc 2909 df-ne 2956 df-nel 3062 df-ral 3077 df-rex 3087 df-rmo 3365 df-reu 3366 df-rab 3413 df-v 3452 df-sbc 3739 df-csb 3848 df-ss 3897 df-pss 4013 df-dif 4046 df-in 4090 df-un 4150 df-nul 4278 df-if 4482 df-pw 4558 df-sn 4585 df-pr 4587 df-tp 4589 df-op 4835 df-ot 4858 df-uni 4867 df-int 4907 df-iun 4952 df-iin 4953 df-br 5103 df-opab 5167 df-mpt 5186 df-tr 5212 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 6307 df-ord 6368 df-on 6369 df-lim 6370 df-suc 6371 df-iota 6497 df-fun 6545 df-fn 6546 df-f 6547 df-f1 6548 df-fo 6549 df-f1o 6550 df-fv 6551 df-riota 7381 df-ov 7427 df-oprab 7428 df-mpo 7429 df-of 7697 df-om 7882 df-1st 8005 df-2nd 8006 df-tpos 8251 df-undef 8298 df-frecs 8307 df-wrecs 8338 df-recs 8387 df-rdg 8426 df-1o 8484 df-2o 8485 df-er 8725 df-map 8857 df-en 8982 df-dom 8983 df-sdom 8984 df-fin 8985 df-pnf 11352 df-mnf 11353 df-xr 11354 df-ltxr 11355 df-le 11356 df-sub 11550 df-neg 11551 df-nn 12343 df-2 12412 df-3 12413 df-4 12414 df-5 12415 df-6 12416 df-7 12417 df-8 12418 df-n0 12614 df-z 12701 df-uz 12973 df-fz 13647 df-struct 17334 df-sets 17351 df-slot 17369 df-ndx 17381 df-base 17397 df-ress 17418 df-plusg 17450 df-mulr 17451 df-starv 17452 df-sca 17453 df-vsca 17454 df-ip 17455 df-0g 17621 df-mre 17765 df-mrc 17766 df-acs 17768 df-proset 18477 df-poset 18496 df-plt 18511 df-lub 18527 df-glb 18528 df-join 18529 df-meet 18530 df-p0 18606 df-p1 18607 df-lat 18615 df-clat 18682 df-mgm 18825 df-sgrp 18917 df-mnd 18933 df-mhm 18987 df-submnd 18988 df-grp 19156 df-minusg 19157 df-sbg 19158 df-subg 19342 df-ghm 19437 df-cntz 19540 df-oppg 19569 df-lsm 19859 df-pj1 19860 df-cmn 20005 df-abl 20006 df-mgp 20370 df-rng 20384 df-ur 20417 df-ring 20470 df-oppr 20576 df-dvdsr 20596 df-unit 20597 df-invr 20627 df-dvr 20640 df-rhm 20711 df-nzr 20772 df-subrg 20831 df-rlreg 20955 df-domn 20956 df-drng 20991 df-staf 21105 df-srng 21106 df-lmod 21146 df-lss 21216 df-lsp 21256 df-lmhm 21306 df-lvec 21387 df-sra 21457 df-rgmod 21458 df-phl 21941 df-ocv 21978 df-css 21979 df-pj 22018 df-hil 22019 df-lsatoms 40170 df-lshyp 40171 df-lcv 40213 df-lfl 40252 df-lkr 40280 df-ldual 40318 df-oposet 40370 df-ol 40372 df-oml 40373 df-covers 40460 df-ats 40461 df-atl 40492 df-cvlat 40516 df-hlat 40545 df-llines 40692 df-lplanes 40693 df-lvols 40694 df-lines 40695 df-psubsp 40697 df-pmap 40698 df-padd 40990 df-lhyp 41182 df-laut 41183 df-ldil 41298 df-ltrn 41299 df-trl 41353 df-tgrp 41937 df-tendo 41949 df-edring 41951 df-dveca 42197 df-disoa 42223 df-dvech 42273 df-dib 42333 df-dic 42367 df-dih 42423 df-doch 42542 df-djh 42589 df-lcdual 42781 df-mapd 42819 df-hvmap 42951 df-hdmap1 42987 df-hdmap 42988 df-hgmap 43078 df-hlhil 43127

This theorem is used by: hlathil 43155

W3C validator