dihoml4 - Mathbox for Norm Megill

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

Theorem dihoml4 42076

Description: Orthomodular law for constructed vector space H. Lemma 3.3(1) in [Holland95] p. 215. (poml4N 40652 analog.) (Contributed by NM, 15-Jan-2015.)

**Hypotheses**
Ref	Expression
dihoml4.h	⊢ 𝐻 = (LHyp‘𝐾)
dihoml4.u	⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)
dihoml4.s	⊢ 𝑆 = (LSubSp‘𝑈)
dihoml4.o	⊢ ⊥ = ((ocH‘𝐾)‘𝑊)
dihoml4.k	⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
dihoml4.x	⊢ (𝜑 → 𝑋 ∈ 𝑆)
dihoml4.y	⊢ (𝜑 → 𝑌 ∈ 𝑆)
dihoml4.c	⊢ (𝜑 → ( ⊥ ‘( ⊥ ‘𝑌)) = 𝑌)
dihoml4.l	⊢ (𝜑 → 𝑋 ⊆ 𝑌)

**Assertion**
Ref	Expression
dihoml4	⊢ (𝜑 → (( ⊥ ‘(( ⊥ ‘𝑋) ∩ 𝑌)) ∩ 𝑌) = ( ⊥ ‘( ⊥ ‘𝑋)))

**Proof of Theorem dihoml4**
Step	Hyp	Ref	Expression
1		dihoml4.k	. . . . . 6 ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
2		dihoml4.x	. . . . . . . 8 ⊢ (𝜑 → 𝑋 ∈ 𝑆)
3		eqid 2769	. . . . . . . . 9 ⊢ (Base‘𝑈) = (Base‘𝑈)
4		dihoml4.s	. . . . . . . . 9 ⊢ 𝑆 = (LSubSp‘𝑈)
5	3, 4	lssss 21035	. . . . . . . 8 ⊢ (𝑋 ∈ 𝑆 → 𝑋 ⊆ (Base‘𝑈))
6	2, 5	syl 18	. . . . . . 7 ⊢ (𝜑 → 𝑋 ⊆ (Base‘𝑈))
7		dihoml4.h	. . . . . . . 8 ⊢ 𝐻 = (LHyp‘𝐾)
8		eqid 2769	. . . . . . . 8 ⊢ ((DIsoH‘𝐾)‘𝑊) = ((DIsoH‘𝐾)‘𝑊)
9		dihoml4.u	. . . . . . . 8 ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)
10		dihoml4.o	. . . . . . . 8 ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)
11	7, 8, 9, 3, 10	dochcl 42052	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ⊆ (Base‘𝑈)) → ( ⊥ ‘𝑋) ∈ ran ((DIsoH‘𝐾)‘𝑊))
12	1, 6, 11	syl2anc 595	. . . . . 6 ⊢ (𝜑 → ( ⊥ ‘𝑋) ∈ ran ((DIsoH‘𝐾)‘𝑊))
13	7, 8, 10	dochoc 42066	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ( ⊥ ‘𝑋) ∈ ran ((DIsoH‘𝐾)‘𝑊)) → ( ⊥ ‘( ⊥ ‘( ⊥ ‘𝑋))) = ( ⊥ ‘𝑋))
14	1, 12, 13	syl2anc 595	. . . . 5 ⊢ (𝜑 → ( ⊥ ‘( ⊥ ‘( ⊥ ‘𝑋))) = ( ⊥ ‘𝑋))
15	14	ineq1d 4178	. . . 4 ⊢ (𝜑 → (( ⊥ ‘( ⊥ ‘( ⊥ ‘𝑋))) ∩ 𝑌) = (( ⊥ ‘𝑋) ∩ 𝑌))
16	15	fveq2d 6886	. . 3 ⊢ (𝜑 → ( ⊥ ‘(( ⊥ ‘( ⊥ ‘( ⊥ ‘𝑋))) ∩ 𝑌)) = ( ⊥ ‘(( ⊥ ‘𝑋) ∩ 𝑌)))
17	16	ineq1d 4178	. 2 ⊢ (𝜑 → (( ⊥ ‘(( ⊥ ‘( ⊥ ‘( ⊥ ‘𝑋))) ∩ 𝑌)) ∩ 𝑌) = (( ⊥ ‘(( ⊥ ‘𝑋) ∩ 𝑌)) ∩ 𝑌))
18	7, 9, 3, 10	dochssv 42054	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ⊆ (Base‘𝑈)) → ( ⊥ ‘𝑋) ⊆ (Base‘𝑈))
19	1, 6, 18	syl2anc 595	. . . 4 ⊢ (𝜑 → ( ⊥ ‘𝑋) ⊆ (Base‘𝑈))
20	7, 8, 9, 3, 10	dochcl 42052	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ( ⊥ ‘𝑋) ⊆ (Base‘𝑈)) → ( ⊥ ‘( ⊥ ‘𝑋)) ∈ ran ((DIsoH‘𝐾)‘𝑊))
21	1, 19, 20	syl2anc 595	. . 3 ⊢ (𝜑 → ( ⊥ ‘( ⊥ ‘𝑋)) ∈ ran ((DIsoH‘𝐾)‘𝑊))
22		dihoml4.c	. . . 4 ⊢ (𝜑 → ( ⊥ ‘( ⊥ ‘𝑌)) = 𝑌)
23		dihoml4.y	. . . . . 6 ⊢ (𝜑 → 𝑌 ∈ 𝑆)
24	3, 4	lssss 21035	. . . . . 6 ⊢ (𝑌 ∈ 𝑆 → 𝑌 ⊆ (Base‘𝑈))
25	23, 24	syl 18	. . . . 5 ⊢ (𝜑 → 𝑌 ⊆ (Base‘𝑈))
26	7, 8, 9, 3, 10, 1, 25	dochoccl 42068	. . . 4 ⊢ (𝜑 → (𝑌 ∈ ran ((DIsoH‘𝐾)‘𝑊) ↔ ( ⊥ ‘( ⊥ ‘𝑌)) = 𝑌))
27	22, 26	mpbird 260	. . 3 ⊢ (𝜑 → 𝑌 ∈ ran ((DIsoH‘𝐾)‘𝑊))
28		dihoml4.l	. . . . . 6 ⊢ (𝜑 → 𝑋 ⊆ 𝑌)
29	7, 9, 3, 10	dochss 42064	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑌 ⊆ (Base‘𝑈) ∧ 𝑋 ⊆ 𝑌) → ( ⊥ ‘𝑌) ⊆ ( ⊥ ‘𝑋))
30	1, 25, 28, 29	syl3anc 1396	. . . . 5 ⊢ (𝜑 → ( ⊥ ‘𝑌) ⊆ ( ⊥ ‘𝑋))
31	7, 9, 3, 10	dochss 42064	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ( ⊥ ‘𝑋) ⊆ (Base‘𝑈) ∧ ( ⊥ ‘𝑌) ⊆ ( ⊥ ‘𝑋)) → ( ⊥ ‘( ⊥ ‘𝑋)) ⊆ ( ⊥ ‘( ⊥ ‘𝑌)))
32	1, 19, 30, 31	syl3anc 1396	. . . 4 ⊢ (𝜑 → ( ⊥ ‘( ⊥ ‘𝑋)) ⊆ ( ⊥ ‘( ⊥ ‘𝑌)))
33	32, 22	sseqtrd 3979	. . 3 ⊢ (𝜑 → ( ⊥ ‘( ⊥ ‘𝑋)) ⊆ 𝑌)
34	7, 8, 10, 1, 21, 27, 33	dihoml4c 42075	. 2 ⊢ (𝜑 → (( ⊥ ‘(( ⊥ ‘( ⊥ ‘( ⊥ ‘𝑋))) ∩ 𝑌)) ∩ 𝑌) = ( ⊥ ‘( ⊥ ‘𝑋)))
35	17, 34	eqtr3d 2806	1 ⊢ (𝜑 → (( ⊥ ‘(( ⊥ ‘𝑋) ∩ 𝑌)) ∩ 𝑌) = ( ⊥ ‘( ⊥ ‘𝑋)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 400 = wceq 1567 ∈ wcel 2149 ∩ cin 3910 ⊆ wss 3911 ran crn 5663 ‘cfv 6537 Basecbs 17269 LSubSpclss 21030 HLchlt 40049 LHypclh 40683 DVecHcdvh 41777 DIsoHcdih 41927 ocHcoch 42046

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1822 ax-4 1836 ax-5 1937 ax-6 1994 ax-7 2035 ax-8 2151 ax-9 2159 ax-10 2182 ax-11 2198 ax-12 2219 ax-ext 2741 ax-rep 5240 ax-sep 5259 ax-nul 5271 ax-pow 5337 ax-pr 5405 ax-un 7733 ax-cnex 11156 ax-resscn 11157 ax-1cn 11158 ax-icn 11159 ax-addcl 11160 ax-addrcl 11161 ax-mulcl 11162 ax-mulrcl 11163 ax-mulcom 11164 ax-addass 11165 ax-mulass 11166 ax-distr 11167 ax-i2m1 11168 ax-1ne0 11169 ax-1rid 11170 ax-rnegex 11171 ax-rrecex 11172 ax-cnre 11173 ax-pre-lttri 11174 ax-pre-lttrn 11175 ax-pre-ltadd 11176 ax-pre-mulgt0 11177 ax-riotaBAD 39652

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1102 df-3an 1103 df-tru 1570 df-fal 1580 df-ex 1807 df-nf 1811 df-sb 2098 df-mo 2573 df-eu 2603 df-clab 2748 df-cleq 2761 df-clel 2844 df-nfc 2918 df-ne 2965 df-nel 3071 df-ral 3086 df-rex 3096 df-rmo 3375 df-reu 3376 df-rab 3423 df-v 3463 df-sbc 3752 df-csb 3860 df-dif 3914 df-un 3916 df-in 3918 df-ss 3928 df-pss 3931 df-nul 4293 df-if 4491 df-pw 4567 df-sn 4593 df-pr 4595 df-tp 4597 df-op 4599 df-uni 4875 df-int 4915 df-iun 4960 df-iin 4961 df-br 5112 df-opab 5176 df-mpt 5195 df-tr 5221 df-id 5557 df-eprel 5562 df-po 5570 df-so 5571 df-fr 5615 df-we 5617 df-xp 5668 df-rel 5669 df-cnv 5670 df-co 5671 df-dm 5672 df-rn 5673 df-res 5674 df-ima 5675 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-riota 7368 df-ov 7414 df-oprab 7415 df-mpo 7416 df-om 7863 df-1st 7986 df-2nd 7987 df-tpos 8222 df-undef 8269 df-frecs 8278 df-wrecs 8309 df-recs 8358 df-rdg 8397 df-1o 8453 df-er 8694 df-map 8826 df-en 8944 df-dom 8945 df-sdom 8946 df-fin 8947 df-pnf 11245 df-mnf 11246 df-xr 11247 df-ltxr 11248 df-le 11249 df-sub 11443 df-neg 11444 df-nn 12234 df-2 12303 df-3 12304 df-4 12305 df-5 12306 df-6 12307 df-n0 12505 df-z 12592 df-uz 12863 df-fz 13536 df-struct 17207 df-sets 17224 df-slot 17242 df-ndx 17254 df-base 17270 df-ress 17291 df-plusg 17323 df-mulr 17324 df-sca 17326 df-vsca 17327 df-0g 17494 df-proset 18350 df-poset 18369 df-plt 18384 df-lub 18400 df-glb 18401 df-join 18402 df-meet 18403 df-p0 18479 df-p1 18480 df-lat 18488 df-clat 18555 df-mgm 18698 df-sgrp 18777 df-mnd 18793 df-submnd 18842 df-grp 19003 df-minusg 19004 df-sbg 19005 df-subg 19189 df-cntz 19387 df-lsm 19706 df-cmn 19852 df-abl 19853 df-mgp 20217 df-rng 20231 df-ur 20264 df-ring 20317 df-oppr 20419 df-dvdsr 20439 df-unit 20440 df-invr 20470 df-dvr 20483 df-drng 20815 df-lmod 20961 df-lss 21031 df-lsp 21071 df-lvec 21202 df-lsatoms 39675 df-oposet 39875 df-ol 39877 df-oml 39878 df-covers 39965 df-ats 39966 df-atl 39997 df-cvlat 40021 df-hlat 40050 df-llines 40197 df-lplanes 40198 df-lvols 40199 df-lines 40200 df-psubsp 40202 df-pmap 40203 df-padd 40495 df-lhyp 40687 df-laut 40688 df-ldil 40803 df-ltrn 40804 df-trl 40858 df-tendo 41454 df-edring 41456 df-disoa 41728 df-dvech 41778 df-dib 41838 df-dic 41872 df-dih 41928 df-doch 42047

This theorem is referenced by: dochexmidlem6 42164

W3C validator