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 36729

Description: Lemma for hlhil 23122. (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	⊢ 𝐶 = (CSubSp‘𝑈)

**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 36728	. 2 ⊢ (𝜑 → 𝑈 ∈ PreHil)
20	3	adantr 481	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
21		eqid 2621	. . . . . . 7 ⊢ ((ocH‘𝐾)‘𝑊) = ((ocH‘𝐾)‘𝑊)
22		hlhilphllem.o	. . . . . . 7 ⊢ 𝑂 = (ocv‘𝑈)
23		eqid 2621	. . . . . . . . . . 11 ⊢ ((DIsoH‘𝐾)‘𝑊) = ((DIsoH‘𝐾)‘𝑊)
24		hlhilphllem.c	. . . . . . . . . . 11 ⊢ 𝐶 = (CSubSp‘𝑈)
25	1, 23, 2, 24, 3	hlhillcs 36727	. . . . . . . . . 10 ⊢ (𝜑 → 𝐶 = ran ((DIsoH‘𝐾)‘𝑊))
26	25	eleq2d 2684	. . . . . . . . 9 ⊢ (𝜑 → (𝑥 ∈ 𝐶 ↔ 𝑥 ∈ ran ((DIsoH‘𝐾)‘𝑊)))
27	26	biimpa 501	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → 𝑥 ∈ ran ((DIsoH‘𝐾)‘𝑊))
28	1, 5, 23, 6	dihrnss 36044	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑥 ∈ ran ((DIsoH‘𝐾)‘𝑊)) → 𝑥 ⊆ 𝑉)
29	3, 28	sylan 488	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ran ((DIsoH‘𝐾)‘𝑊)) → 𝑥 ⊆ 𝑉)
30	27, 29	syldan 487	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → 𝑥 ⊆ 𝑉)
31	1, 5, 2, 20, 6, 21, 22, 30	hlhilocv 36726	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → (𝑂‘𝑥) = (((ocH‘𝐾)‘𝑊)‘𝑥))
32	31	oveq2d 6620	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → (𝑥(LSSum‘𝐿)(𝑂‘𝑥)) = (𝑥(LSSum‘𝐿)(((ocH‘𝐾)‘𝑊)‘𝑥)))
33		eqid 2621	. . . . . . . 8 ⊢ (LSSum‘𝐿) = (LSSum‘𝐿)
34	1, 5, 2, 3, 33	hlhillsm 36725	. . . . . . 7 ⊢ (𝜑 → (LSSum‘𝐿) = (LSSum‘𝑈))
35	34	adantr 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → (LSSum‘𝐿) = (LSSum‘𝑈))
36	35	oveqd 6621	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → (𝑥(LSSum‘𝐿)(𝑂‘𝑥)) = (𝑥(LSSum‘𝑈)(𝑂‘𝑥)))
37		eqid 2621	. . . . . . 7 ⊢ (LSubSp‘𝐿) = (LSubSp‘𝐿)
38	3	adantr 481	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ran ((DIsoH‘𝐾)‘𝑊)) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
39	1, 5, 23, 37	dihrnlss 36043	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑥 ∈ ran ((DIsoH‘𝐾)‘𝑊)) → 𝑥 ∈ (LSubSp‘𝐿))
40	3, 39	sylan 488	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ran ((DIsoH‘𝐾)‘𝑊)) → 𝑥 ∈ (LSubSp‘𝐿))
41	1, 23, 5, 6, 21, 38, 29	dochoccl 36135	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ ran ((DIsoH‘𝐾)‘𝑊)) → (𝑥 ∈ ran ((DIsoH‘𝐾)‘𝑊) ↔ (((ocH‘𝐾)‘𝑊)‘(((ocH‘𝐾)‘𝑊)‘𝑥)) = 𝑥))
42	41	biimpd 219	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ ran ((DIsoH‘𝐾)‘𝑊)) → (𝑥 ∈ ran ((DIsoH‘𝐾)‘𝑊) → (((ocH‘𝐾)‘𝑊)‘(((ocH‘𝐾)‘𝑊)‘𝑥)) = 𝑥))
43	42	ex 450	. . . . . . . . 9 ⊢ (𝜑 → (𝑥 ∈ ran ((DIsoH‘𝐾)‘𝑊) → (𝑥 ∈ ran ((DIsoH‘𝐾)‘𝑊) → (((ocH‘𝐾)‘𝑊)‘(((ocH‘𝐾)‘𝑊)‘𝑥)) = 𝑥)))
44	43	pm2.43d 53	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ ran ((DIsoH‘𝐾)‘𝑊) → (((ocH‘𝐾)‘𝑊)‘(((ocH‘𝐾)‘𝑊)‘𝑥)) = 𝑥))
45	44	imp 445	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ran ((DIsoH‘𝐾)‘𝑊)) → (((ocH‘𝐾)‘𝑊)‘(((ocH‘𝐾)‘𝑊)‘𝑥)) = 𝑥)
46	1, 21, 5, 6, 37, 33, 38, 40, 45	dochexmid 36234	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ran ((DIsoH‘𝐾)‘𝑊)) → (𝑥(LSSum‘𝐿)(((ocH‘𝐾)‘𝑊)‘𝑥)) = 𝑉)
47	27, 46	syldan 487	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → (𝑥(LSSum‘𝐿)(((ocH‘𝐾)‘𝑊)‘𝑥)) = 𝑉)
48	32, 36, 47	3eqtr3d 2663	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → (𝑥(LSSum‘𝑈)(𝑂‘𝑥)) = 𝑉)
49	1, 2, 3, 5, 6	hlhilbase 36705	. . . . 5 ⊢ (𝜑 → 𝑉 = (Base‘𝑈))
50	49	adantr 481	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → 𝑉 = (Base‘𝑈))
51	48, 50	eqtrd 2655	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → (𝑥(LSSum‘𝑈)(𝑂‘𝑥)) = (Base‘𝑈))
52	51	ralrimiva 2960	. 2 ⊢ (𝜑 → ∀𝑥 ∈ 𝐶 (𝑥(LSSum‘𝑈)(𝑂‘𝑥)) = (Base‘𝑈))
53		eqid 2621	. . 3 ⊢ (Base‘𝑈) = (Base‘𝑈)
54		eqid 2621	. . 3 ⊢ (LSSum‘𝑈) = (LSSum‘𝑈)
55	53, 54, 22, 24	ishil2 19982	. 2 ⊢ (𝑈 ∈ Hil ↔ (𝑈 ∈ PreHil ∧ ∀𝑥 ∈ 𝐶 (𝑥(LSSum‘𝑈)(𝑂‘𝑥)) = (Base‘𝑈)))
56	19, 52, 55	sylanbrc 697	1 ⊢ (𝜑 → 𝑈 ∈ Hil)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 384 = wceq 1480 ∈ wcel 1987 ∀wral 2907 ⊆ wss 3555 ran crn 5075 ‘cfv 5847 (class class class)co 6604 ↦ cmpt2 6606 Basecbs 15781 +_gcplusg 15862 ._rcmulr 15863 Scalarcsca 15865 ·_𝑠 cvsca 15866 ·_𝑖cip 15867 0_gc0g 16021 LSSumclsm 17970 LSubSpclss 18851 PreHilcphl 19888 ocvcocv 19923 CSubSpccss 19924 Hilchs 19964 HLchlt 34114 LHypclh 34747 DVecHcdvh 35844 DIsoHcdih 35994 ocHcoch 36113 HDMapchdma 36559 HGMapchg 36652 HLHilchlh 36701

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1719 ax-4 1734 ax-5 1836 ax-6 1885 ax-7 1932 ax-8 1989 ax-9 1996 ax-10 2016 ax-11 2031 ax-12 2044 ax-13 2245 ax-ext 2601 ax-rep 4731 ax-sep 4741 ax-nul 4749 ax-pow 4803 ax-pr 4867 ax-un 6902 ax-cnex 9936 ax-resscn 9937 ax-1cn 9938 ax-icn 9939 ax-addcl 9940 ax-addrcl 9941 ax-mulcl 9942 ax-mulrcl 9943 ax-mulcom 9944 ax-addass 9945 ax-mulass 9946 ax-distr 9947 ax-i2m1 9948 ax-1ne0 9949 ax-1rid 9950 ax-rnegex 9951 ax-rrecex 9952 ax-cnre 9953 ax-pre-lttri 9954 ax-pre-lttrn 9955 ax-pre-ltadd 9956 ax-pre-mulgt0 9957 ax-riotaBAD 33716

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3or 1037 df-3an 1038 df-tru 1483 df-fal 1486 df-ex 1702 df-nf 1707 df-sb 1878 df-eu 2473 df-mo 2474 df-clab 2608 df-cleq 2614 df-clel 2617 df-nfc 2750 df-ne 2791 df-nel 2894 df-ral 2912 df-rex 2913 df-reu 2914 df-rmo 2915 df-rab 2916 df-v 3188 df-sbc 3418 df-csb 3515 df-dif 3558 df-un 3560 df-in 3562 df-ss 3569 df-pss 3571 df-nul 3892 df-if 4059 df-pw 4132 df-sn 4149 df-pr 4151 df-tp 4153 df-op 4155 df-ot 4157 df-uni 4403 df-int 4441 df-iun 4487 df-iin 4488 df-br 4614 df-opab 4674 df-mpt 4675 df-tr 4713 df-eprel 4985 df-id 4989 df-po 4995 df-so 4996 df-fr 5033 df-we 5035 df-xp 5080 df-rel 5081 df-cnv 5082 df-co 5083 df-dm 5084 df-rn 5085 df-res 5086 df-ima 5087 df-pred 5639 df-ord 5685 df-on 5686 df-lim 5687 df-suc 5688 df-iota 5810 df-fun 5849 df-fn 5850 df-f 5851 df-f1 5852 df-fo 5853 df-f1o 5854 df-fv 5855 df-riota 6565 df-ov 6607 df-oprab 6608 df-mpt2 6609 df-of 6850 df-om 7013 df-1st 7113 df-2nd 7114 df-tpos 7297 df-undef 7344 df-wrecs 7352 df-recs 7413 df-rdg 7451 df-1o 7505 df-oadd 7509 df-er 7687 df-map 7804 df-en 7900 df-dom 7901 df-sdom 7902 df-fin 7903 df-pnf 10020 df-mnf 10021 df-xr 10022 df-ltxr 10023 df-le 10024 df-sub 10212 df-neg 10213 df-nn 10965 df-2 11023 df-3 11024 df-4 11025 df-5 11026 df-6 11027 df-7 11028 df-8 11029 df-n0 11237 df-z 11322 df-uz 11632 df-fz 12269 df-struct 15783 df-ndx 15784 df-slot 15785 df-base 15786 df-sets 15787 df-ress 15788 df-plusg 15875 df-mulr 15876 df-starv 15877 df-sca 15878 df-vsca 15879 df-ip 15880 df-0g 16023 df-mre 16167 df-mrc 16168 df-acs 16170 df-preset 16849 df-poset 16867 df-plt 16879 df-lub 16895 df-glb 16896 df-join 16897 df-meet 16898 df-p0 16960 df-p1 16961 df-lat 16967 df-clat 17029 df-mgm 17163 df-sgrp 17205 df-mnd 17216 df-mhm 17256 df-submnd 17257 df-grp 17346 df-minusg 17347 df-sbg 17348 df-subg 17512 df-ghm 17579 df-cntz 17671 df-oppg 17697 df-lsm 17972 df-pj1 17973 df-cmn 18116 df-abl 18117 df-mgp 18411 df-ur 18423 df-ring 18470 df-oppr 18544 df-dvdsr 18562 df-unit 18563 df-invr 18593 df-dvr 18604 df-rnghom 18636 df-drng 18670 df-subrg 18699 df-staf 18766 df-srng 18767 df-lmod 18786 df-lss 18852 df-lsp 18891 df-lmhm 18941 df-lvec 19022 df-sra 19091 df-rgmod 19092 df-phl 19890 df-ocv 19926 df-css 19927 df-pj 19966 df-hil 19967 df-lsatoms 33740 df-lshyp 33741 df-lcv 33783 df-lfl 33822 df-lkr 33850 df-ldual 33888 df-oposet 33940 df-ol 33942 df-oml 33943 df-covers 34030 df-ats 34031 df-atl 34062 df-cvlat 34086 df-hlat 34115 df-llines 34261 df-lplanes 34262 df-lvols 34263 df-lines 34264 df-psubsp 34266 df-pmap 34267 df-padd 34559 df-lhyp 34751 df-laut 34752 df-ldil 34867 df-ltrn 34868 df-trl 34923 df-tgrp 35508 df-tendo 35520 df-edring 35522 df-dveca 35768 df-disoa 35795 df-dvech 35845 df-dib 35905 df-dic 35939 df-dih 35995 df-doch 36114 df-djh 36161 df-lcdual 36353 df-mapd 36391 df-hvmap 36523 df-hdmap1 36560 df-hdmap 36561 df-hgmap 36653 df-hlhil 36702

This theorem is referenced by: hlathil 36730

W3C validator