dihmeetlem11N - Mathbox for Norm Megill

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

Theorem dihmeetlem11N 37092

Description: Lemma for isomorphism H of a lattice meet. (Contributed by NM, 6-Apr-2014.) (New usage is discouraged.)

**Hypotheses**
Ref	Expression
dihmeetlem9.b	⊢ 𝐵 = (Base‘𝐾)
dihmeetlem9.l	⊢ ≤ = (le‘𝐾)
dihmeetlem9.h	⊢ 𝐻 = (LHyp‘𝐾)
dihmeetlem9.j	⊢ ∨ = (join‘𝐾)
dihmeetlem9.m	⊢ ∧ = (meet‘𝐾)
dihmeetlem9.a	⊢ 𝐴 = (Atoms‘𝐾)
dihmeetlem9.u	⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)
dihmeetlem9.s	⊢ ⊕ = (LSSum‘𝑈)
dihmeetlem9.i	⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊)

**Assertion**
Ref	Expression
dihmeetlem11N	⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ((𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑊) ∧ 𝑝 ≤ 𝑋)) → ((𝐼‘((𝑋 ∧ 𝑌) ∨ 𝑝)) ∩ (𝐼‘𝑌)) = ((𝐼‘𝑋) ∩ (𝐼‘𝑌)))

**Proof of Theorem dihmeetlem11N**
Step	Hyp	Ref	Expression
1		dihmeetlem9.b	. . . 4 ⊢ 𝐵 = (Base‘𝐾)
2		dihmeetlem9.l	. . . 4 ⊢ ≤ = (le‘𝐾)
3		dihmeetlem9.h	. . . 4 ⊢ 𝐻 = (LHyp‘𝐾)
4		dihmeetlem9.j	. . . 4 ⊢ ∨ = (join‘𝐾)
5		dihmeetlem9.m	. . . 4 ⊢ ∧ = (meet‘𝐾)
6		dihmeetlem9.a	. . . 4 ⊢ 𝐴 = (Atoms‘𝐾)
7		dihmeetlem9.u	. . . 4 ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)
8		dihmeetlem9.s	. . . 4 ⊢ ⊕ = (LSSum‘𝑈)
9		dihmeetlem9.i	. . . 4 ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊)
10	1, 2, 3, 4, 5, 6, 7, 8, 9	dihmeetlem10N 37091	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ((𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑊) ∧ 𝑝 ≤ 𝑋)) → (𝐼‘((𝑋 ∧ 𝑌) ∨ 𝑝)) = ((𝐼‘𝑋) ∩ (𝐼‘(𝑌 ∨ 𝑝))))
11	10	ineq1d 4012	. 2 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ((𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑊) ∧ 𝑝 ≤ 𝑋)) → ((𝐼‘((𝑋 ∧ 𝑌) ∨ 𝑝)) ∩ (𝐼‘𝑌)) = (((𝐼‘𝑋) ∩ (𝐼‘(𝑌 ∨ 𝑝))) ∩ (𝐼‘𝑌)))
12		inass 4020	. . 3 ⊢ (((𝐼‘𝑋) ∩ (𝐼‘(𝑌 ∨ 𝑝))) ∩ (𝐼‘𝑌)) = ((𝐼‘𝑋) ∩ ((𝐼‘(𝑌 ∨ 𝑝)) ∩ (𝐼‘𝑌)))
13		simpl1l 1286	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ((𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑊) ∧ 𝑝 ≤ 𝑋)) → 𝐾 ∈ HL)
14	13	hllatd 35139	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ((𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑊) ∧ 𝑝 ≤ 𝑋)) → 𝐾 ∈ Lat)
15		simpl3 1239	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ((𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑊) ∧ 𝑝 ≤ 𝑋)) → 𝑌 ∈ 𝐵)
16		simprll 788	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ((𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑊) ∧ 𝑝 ≤ 𝑋)) → 𝑝 ∈ 𝐴)
17	1, 6	atbase 35064	. . . . . . . 8 ⊢ (𝑝 ∈ 𝐴 → 𝑝 ∈ 𝐵)
18	16, 17	syl 17	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ((𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑊) ∧ 𝑝 ≤ 𝑋)) → 𝑝 ∈ 𝐵)
19	1, 2, 4	latlej1 17261	. . . . . . 7 ⊢ ((𝐾 ∈ Lat ∧ 𝑌 ∈ 𝐵 ∧ 𝑝 ∈ 𝐵) → 𝑌 ≤ (𝑌 ∨ 𝑝))
20	14, 15, 18, 19	syl3anc 1483	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ((𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑊) ∧ 𝑝 ≤ 𝑋)) → 𝑌 ≤ (𝑌 ∨ 𝑝))
21		simpl1 1235	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ((𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑊) ∧ 𝑝 ≤ 𝑋)) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
22	1, 4	latjcl 17252	. . . . . . . 8 ⊢ ((𝐾 ∈ Lat ∧ 𝑌 ∈ 𝐵 ∧ 𝑝 ∈ 𝐵) → (𝑌 ∨ 𝑝) ∈ 𝐵)
23	14, 15, 18, 22	syl3anc 1483	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ((𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑊) ∧ 𝑝 ≤ 𝑋)) → (𝑌 ∨ 𝑝) ∈ 𝐵)
24	1, 2, 3, 9	dihord 37039	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑌 ∈ 𝐵 ∧ (𝑌 ∨ 𝑝) ∈ 𝐵) → ((𝐼‘𝑌) ⊆ (𝐼‘(𝑌 ∨ 𝑝)) ↔ 𝑌 ≤ (𝑌 ∨ 𝑝)))
25	21, 15, 23, 24	syl3anc 1483	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ((𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑊) ∧ 𝑝 ≤ 𝑋)) → ((𝐼‘𝑌) ⊆ (𝐼‘(𝑌 ∨ 𝑝)) ↔ 𝑌 ≤ (𝑌 ∨ 𝑝)))
26	20, 25	mpbird 248	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ((𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑊) ∧ 𝑝 ≤ 𝑋)) → (𝐼‘𝑌) ⊆ (𝐼‘(𝑌 ∨ 𝑝)))
27		sseqin2 4016	. . . . 5 ⊢ ((𝐼‘𝑌) ⊆ (𝐼‘(𝑌 ∨ 𝑝)) ↔ ((𝐼‘(𝑌 ∨ 𝑝)) ∩ (𝐼‘𝑌)) = (𝐼‘𝑌))
28	26, 27	sylib 209	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ((𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑊) ∧ 𝑝 ≤ 𝑋)) → ((𝐼‘(𝑌 ∨ 𝑝)) ∩ (𝐼‘𝑌)) = (𝐼‘𝑌))
29	28	ineq2d 4013	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ((𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑊) ∧ 𝑝 ≤ 𝑋)) → ((𝐼‘𝑋) ∩ ((𝐼‘(𝑌 ∨ 𝑝)) ∩ (𝐼‘𝑌))) = ((𝐼‘𝑋) ∩ (𝐼‘𝑌)))
30	12, 29	syl5eq 2852	. 2 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ((𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑊) ∧ 𝑝 ≤ 𝑋)) → (((𝐼‘𝑋) ∩ (𝐼‘(𝑌 ∨ 𝑝))) ∩ (𝐼‘𝑌)) = ((𝐼‘𝑋) ∩ (𝐼‘𝑌)))
31	11, 30	eqtrd 2840	1 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ((𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑊) ∧ 𝑝 ≤ 𝑋)) → ((𝐼‘((𝑋 ∧ 𝑌) ∨ 𝑝)) ∩ (𝐼‘𝑌)) = ((𝐼‘𝑋) ∩ (𝐼‘𝑌)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 197 ∧ wa 384 ∧ w3a 1100 = wceq 1637 ∈ wcel 2156 ∩ cin 3768 ⊆ wss 3769 class class class wbr 4844 ‘cfv 6097 (class class class)co 6870 Basecbs 16064 lecple 16156 joincjn 17145 meetcmee 17146 Latclat 17246 LSSumclsm 18246 Atomscatm 35038 HLchlt 35125 LHypclh 35759 DVecHcdvh 36853 DIsoHcdih 37003

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1877 ax-4 1894 ax-5 2001 ax-6 2068 ax-7 2104 ax-8 2158 ax-9 2165 ax-10 2185 ax-11 2201 ax-12 2214 ax-13 2420 ax-ext 2784 ax-rep 4964 ax-sep 4975 ax-nul 4983 ax-pow 5035 ax-pr 5096 ax-un 7175 ax-cnex 10273 ax-resscn 10274 ax-1cn 10275 ax-icn 10276 ax-addcl 10277 ax-addrcl 10278 ax-mulcl 10279 ax-mulrcl 10280 ax-mulcom 10281 ax-addass 10282 ax-mulass 10283 ax-distr 10284 ax-i2m1 10285 ax-1ne0 10286 ax-1rid 10287 ax-rnegex 10288 ax-rrecex 10289 ax-cnre 10290 ax-pre-lttri 10291 ax-pre-lttrn 10292 ax-pre-ltadd 10293 ax-pre-mulgt0 10294 ax-riotaBAD 34727

This theorem depends on definitions: df-bi 198 df-an 385 df-or 866 df-3or 1101 df-3an 1102 df-tru 1641 df-fal 1651 df-ex 1860 df-nf 1864 df-sb 2061 df-eu 2634 df-mo 2635 df-clab 2793 df-cleq 2799 df-clel 2802 df-nfc 2937 df-ne 2979 df-nel 3082 df-ral 3101 df-rex 3102 df-reu 3103 df-rmo 3104 df-rab 3105 df-v 3393 df-sbc 3634 df-csb 3729 df-dif 3772 df-un 3774 df-in 3776 df-ss 3783 df-pss 3785 df-nul 4117 df-if 4280 df-pw 4353 df-sn 4371 df-pr 4373 df-tp 4375 df-op 4377 df-uni 4631 df-int 4670 df-iun 4714 df-iin 4715 df-br 4845 df-opab 4907 df-mpt 4924 df-tr 4947 df-id 5219 df-eprel 5224 df-po 5232 df-so 5233 df-fr 5270 df-we 5272 df-xp 5317 df-rel 5318 df-cnv 5319 df-co 5320 df-dm 5321 df-rn 5322 df-res 5323 df-ima 5324 df-pred 5893 df-ord 5939 df-on 5940 df-lim 5941 df-suc 5942 df-iota 6060 df-fun 6099 df-fn 6100 df-f 6101 df-f1 6102 df-fo 6103 df-f1o 6104 df-fv 6105 df-riota 6831 df-ov 6873 df-oprab 6874 df-mpt2 6875 df-om 7292 df-1st 7394 df-2nd 7395 df-tpos 7583 df-undef 7630 df-wrecs 7638 df-recs 7700 df-rdg 7738 df-1o 7792 df-oadd 7796 df-er 7975 df-map 8090 df-en 8189 df-dom 8190 df-sdom 8191 df-fin 8192 df-pnf 10357 df-mnf 10358 df-xr 10359 df-ltxr 10360 df-le 10361 df-sub 10549 df-neg 10550 df-nn 11302 df-2 11360 df-3 11361 df-4 11362 df-5 11363 df-6 11364 df-n0 11556 df-z 11640 df-uz 11901 df-fz 12546 df-struct 16066 df-ndx 16067 df-slot 16068 df-base 16070 df-sets 16071 df-ress 16072 df-plusg 16162 df-mulr 16163 df-sca 16165 df-vsca 16166 df-0g 16303 df-proset 17129 df-poset 17147 df-plt 17159 df-lub 17175 df-glb 17176 df-join 17177 df-meet 17178 df-p0 17240 df-p1 17241 df-lat 17247 df-clat 17309 df-mgm 17443 df-sgrp 17485 df-mnd 17496 df-submnd 17537 df-grp 17626 df-minusg 17627 df-sbg 17628 df-subg 17789 df-cntz 17947 df-lsm 18248 df-cmn 18392 df-abl 18393 df-mgp 18688 df-ur 18700 df-ring 18747 df-oppr 18821 df-dvdsr 18839 df-unit 18840 df-invr 18870 df-dvr 18881 df-drng 18949 df-lmod 19065 df-lss 19133 df-lsp 19175 df-lvec 19306 df-oposet 34951 df-ol 34953 df-oml 34954 df-covers 35041 df-ats 35042 df-atl 35073 df-cvlat 35097 df-hlat 35126 df-llines 35273 df-lplanes 35274 df-lvols 35275 df-lines 35276 df-psubsp 35278 df-pmap 35279 df-padd 35571 df-lhyp 35763 df-laut 35764 df-ldil 35879 df-ltrn 35880 df-trl 35934 df-tendo 36530 df-edring 36532 df-disoa 36804 df-dvech 36854 df-dib 36914 df-dic 36948 df-dih 37004

This theorem is referenced by: dihmeetlem12N 37093

W3C validator