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 38893

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 38892	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ((𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑊) ∧ 𝑝 ≤ 𝑋)) → (𝐼‘((𝑋 ∧ 𝑌) ∨ 𝑝)) = ((𝐼‘𝑋) ∩ (𝐼‘(𝑌 ∨ 𝑝))))
11	10	ineq1d 4116	. 2 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ((𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑊) ∧ 𝑝 ≤ 𝑋)) → ((𝐼‘((𝑋 ∧ 𝑌) ∨ 𝑝)) ∩ (𝐼‘𝑌)) = (((𝐼‘𝑋) ∩ (𝐼‘(𝑌 ∨ 𝑝))) ∩ (𝐼‘𝑌)))
12		inass 4124	. . 3 ⊢ (((𝐼‘𝑋) ∩ (𝐼‘(𝑌 ∨ 𝑝))) ∩ (𝐼‘𝑌)) = ((𝐼‘𝑋) ∩ ((𝐼‘(𝑌 ∨ 𝑝)) ∩ (𝐼‘𝑌)))
13		simpl1l 1221	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ((𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑊) ∧ 𝑝 ≤ 𝑋)) → 𝐾 ∈ HL)
14	13	hllatd 36940	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ((𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑊) ∧ 𝑝 ≤ 𝑋)) → 𝐾 ∈ Lat)
15		simpl3 1190	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ((𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑊) ∧ 𝑝 ≤ 𝑋)) → 𝑌 ∈ 𝐵)
16		simprll 778	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ((𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑊) ∧ 𝑝 ≤ 𝑋)) → 𝑝 ∈ 𝐴)
17	1, 6	atbase 36865	. . . . . . . 8 ⊢ (𝑝 ∈ 𝐴 → 𝑝 ∈ 𝐵)
18	16, 17	syl 17	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ((𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑊) ∧ 𝑝 ≤ 𝑋)) → 𝑝 ∈ 𝐵)
19	1, 2, 4	latlej1 17736	. . . . . . 7 ⊢ ((𝐾 ∈ Lat ∧ 𝑌 ∈ 𝐵 ∧ 𝑝 ∈ 𝐵) → 𝑌 ≤ (𝑌 ∨ 𝑝))
20	14, 15, 18, 19	syl3anc 1368	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ((𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑊) ∧ 𝑝 ≤ 𝑋)) → 𝑌 ≤ (𝑌 ∨ 𝑝))
21		simpl1 1188	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ((𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑊) ∧ 𝑝 ≤ 𝑋)) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
22	1, 4	latjcl 17727	. . . . . . . 8 ⊢ ((𝐾 ∈ Lat ∧ 𝑌 ∈ 𝐵 ∧ 𝑝 ∈ 𝐵) → (𝑌 ∨ 𝑝) ∈ 𝐵)
23	14, 15, 18, 22	syl3anc 1368	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ((𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑊) ∧ 𝑝 ≤ 𝑋)) → (𝑌 ∨ 𝑝) ∈ 𝐵)
24	1, 2, 3, 9	dihord 38840	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑌 ∈ 𝐵 ∧ (𝑌 ∨ 𝑝) ∈ 𝐵) → ((𝐼‘𝑌) ⊆ (𝐼‘(𝑌 ∨ 𝑝)) ↔ 𝑌 ≤ (𝑌 ∨ 𝑝)))
25	21, 15, 23, 24	syl3anc 1368	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ((𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑊) ∧ 𝑝 ≤ 𝑋)) → ((𝐼‘𝑌) ⊆ (𝐼‘(𝑌 ∨ 𝑝)) ↔ 𝑌 ≤ (𝑌 ∨ 𝑝)))
26	20, 25	mpbird 260	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ((𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑊) ∧ 𝑝 ≤ 𝑋)) → (𝐼‘𝑌) ⊆ (𝐼‘(𝑌 ∨ 𝑝)))
27		sseqin2 4120	. . . . 5 ⊢ ((𝐼‘𝑌) ⊆ (𝐼‘(𝑌 ∨ 𝑝)) ↔ ((𝐼‘(𝑌 ∨ 𝑝)) ∩ (𝐼‘𝑌)) = (𝐼‘𝑌))
28	26, 27	sylib 221	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ((𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑊) ∧ 𝑝 ≤ 𝑋)) → ((𝐼‘(𝑌 ∨ 𝑝)) ∩ (𝐼‘𝑌)) = (𝐼‘𝑌))
29	28	ineq2d 4117	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ((𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑊) ∧ 𝑝 ≤ 𝑋)) → ((𝐼‘𝑋) ∩ ((𝐼‘(𝑌 ∨ 𝑝)) ∩ (𝐼‘𝑌))) = ((𝐼‘𝑋) ∩ (𝐼‘𝑌)))
30	12, 29	syl5eq 2805	. 2 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ((𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑊) ∧ 𝑝 ≤ 𝑋)) → (((𝐼‘𝑋) ∩ (𝐼‘(𝑌 ∨ 𝑝))) ∩ (𝐼‘𝑌)) = ((𝐼‘𝑋) ∩ (𝐼‘𝑌)))
31	11, 30	eqtrd 2793	1 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ((𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑊) ∧ 𝑝 ≤ 𝑋)) → ((𝐼‘((𝑋 ∧ 𝑌) ∨ 𝑝)) ∩ (𝐼‘𝑌)) = ((𝐼‘𝑋) ∩ (𝐼‘𝑌)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 399 ∧ w3a 1084 = wceq 1538 ∈ wcel 2111 ∩ cin 3857 ⊆ wss 3858 class class class wbr 5032 ‘cfv 6335 (class class class)co 7150 Basecbs 16541 lecple 16630 joincjn 17620 meetcmee 17621 Latclat 17721 LSSumclsm 18826 Atomscatm 36839 HLchlt 36926 LHypclh 37560 DVecHcdvh 38654 DIsoHcdih 38804

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-10 2142 ax-11 2158 ax-12 2175 ax-ext 2729 ax-rep 5156 ax-sep 5169 ax-nul 5176 ax-pow 5234 ax-pr 5298 ax-un 7459 ax-cnex 10631 ax-resscn 10632 ax-1cn 10633 ax-icn 10634 ax-addcl 10635 ax-addrcl 10636 ax-mulcl 10637 ax-mulrcl 10638 ax-mulcom 10639 ax-addass 10640 ax-mulass 10641 ax-distr 10642 ax-i2m1 10643 ax-1ne0 10644 ax-1rid 10645 ax-rnegex 10646 ax-rrecex 10647 ax-cnre 10648 ax-pre-lttri 10649 ax-pre-lttrn 10650 ax-pre-ltadd 10651 ax-pre-mulgt0 10652 ax-riotaBAD 36529

This theorem depends on definitions: df-bi 210 df-an 400 df-or 845 df-3or 1085 df-3an 1086 df-tru 1541 df-fal 1551 df-ex 1782 df-nf 1786 df-sb 2070 df-mo 2557 df-eu 2588 df-clab 2736 df-cleq 2750 df-clel 2830 df-nfc 2901 df-ne 2952 df-nel 3056 df-ral 3075 df-rex 3076 df-reu 3077 df-rmo 3078 df-rab 3079 df-v 3411 df-sbc 3697 df-csb 3806 df-dif 3861 df-un 3863 df-in 3865 df-ss 3875 df-pss 3877 df-nul 4226 df-if 4421 df-pw 4496 df-sn 4523 df-pr 4525 df-tp 4527 df-op 4529 df-uni 4799 df-int 4839 df-iun 4885 df-iin 4886 df-br 5033 df-opab 5095 df-mpt 5113 df-tr 5139 df-id 5430 df-eprel 5435 df-po 5443 df-so 5444 df-fr 5483 df-we 5485 df-xp 5530 df-rel 5531 df-cnv 5532 df-co 5533 df-dm 5534 df-rn 5535 df-res 5536 df-ima 5537 df-pred 6126 df-ord 6172 df-on 6173 df-lim 6174 df-suc 6175 df-iota 6294 df-fun 6337 df-fn 6338 df-f 6339 df-f1 6340 df-fo 6341 df-f1o 6342 df-fv 6343 df-riota 7108 df-ov 7153 df-oprab 7154 df-mpo 7155 df-om 7580 df-1st 7693 df-2nd 7694 df-tpos 7902 df-undef 7949 df-wrecs 7957 df-recs 8018 df-rdg 8056 df-1o 8112 df-er 8299 df-map 8418 df-en 8528 df-dom 8529 df-sdom 8530 df-fin 8531 df-pnf 10715 df-mnf 10716 df-xr 10717 df-ltxr 10718 df-le 10719 df-sub 10910 df-neg 10911 df-nn 11675 df-2 11737 df-3 11738 df-4 11739 df-5 11740 df-6 11741 df-n0 11935 df-z 12021 df-uz 12283 df-fz 12940 df-struct 16543 df-ndx 16544 df-slot 16545 df-base 16547 df-sets 16548 df-ress 16549 df-plusg 16636 df-mulr 16637 df-sca 16639 df-vsca 16640 df-0g 16773 df-proset 17604 df-poset 17622 df-plt 17634 df-lub 17650 df-glb 17651 df-join 17652 df-meet 17653 df-p0 17715 df-p1 17716 df-lat 17722 df-clat 17784 df-mgm 17918 df-sgrp 17967 df-mnd 17978 df-submnd 18023 df-grp 18172 df-minusg 18173 df-sbg 18174 df-subg 18343 df-cntz 18514 df-lsm 18828 df-cmn 18975 df-abl 18976 df-mgp 19308 df-ur 19320 df-ring 19367 df-oppr 19444 df-dvdsr 19462 df-unit 19463 df-invr 19493 df-dvr 19504 df-drng 19572 df-lmod 19704 df-lss 19772 df-lsp 19812 df-lvec 19943 df-oposet 36752 df-ol 36754 df-oml 36755 df-covers 36842 df-ats 36843 df-atl 36874 df-cvlat 36898 df-hlat 36927 df-llines 37074 df-lplanes 37075 df-lvols 37076 df-lines 37077 df-psubsp 37079 df-pmap 37080 df-padd 37372 df-lhyp 37564 df-laut 37565 df-ldil 37680 df-ltrn 37681 df-trl 37735 df-tendo 38331 df-edring 38333 df-disoa 38605 df-dvech 38655 df-dib 38715 df-dic 38749 df-dih 38805

This theorem is referenced by: dihmeetlem12N 38894

W3C validator