dihmeetlem9N - Mathbox for Norm Megill

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

Theorem dihmeetlem9N 41946

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
dihmeetlem9N	⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑝 ∈ 𝐴) → (((𝐼‘𝑝) ⊕ (𝐼‘(𝑋 ∧ 𝑌))) ∩ (𝐼‘𝑌)) = ((𝐼‘(𝑋 ∧ 𝑌)) ⊕ ((𝐼‘𝑝) ∩ (𝐼‘𝑌))))

**Proof of Theorem dihmeetlem9N**
Step	Hyp	Ref	Expression
1		dihmeetlem9.h	. . . . . 6 ⊢ 𝐻 = (LHyp‘𝐾)
2		dihmeetlem9.u	. . . . . 6 ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)
3		simp1 1152	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑝 ∈ 𝐴) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
4	1, 2, 3	dvhlmod 41741	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑝 ∈ 𝐴) → 𝑈 ∈ LMod)
5		eqid 2765	. . . . . 6 ⊢ (LSubSp‘𝑈) = (LSubSp‘𝑈)
6	5	lsssssubg 21045	. . . . 5 ⊢ (𝑈 ∈ LMod → (LSubSp‘𝑈) ⊆ (SubGrp‘𝑈))
7	4, 6	syl 18	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑝 ∈ 𝐴) → (LSubSp‘𝑈) ⊆ (SubGrp‘𝑈))
8		simp1l 1214	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑝 ∈ 𝐴) → 𝐾 ∈ HL)
9	8	hllatd 39995	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑝 ∈ 𝐴) → 𝐾 ∈ Lat)
10		simp2l 1216	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑝 ∈ 𝐴) → 𝑋 ∈ 𝐵)
11		simp2r 1217	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑝 ∈ 𝐴) → 𝑌 ∈ 𝐵)
12		dihmeetlem9.b	. . . . . . 7 ⊢ 𝐵 = (Base‘𝐾)
13		dihmeetlem9.m	. . . . . . 7 ⊢ ∧ = (meet‘𝐾)
14	12, 13	latmcl 18484	. . . . . 6 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ∧ 𝑌) ∈ 𝐵)
15	9, 10, 11, 14	syl3anc 1394	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑝 ∈ 𝐴) → (𝑋 ∧ 𝑌) ∈ 𝐵)
16		dihmeetlem9.i	. . . . . 6 ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊)
17	12, 1, 16, 2, 5	dihlss 41881	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∧ 𝑌) ∈ 𝐵) → (𝐼‘(𝑋 ∧ 𝑌)) ∈ (LSubSp‘𝑈))
18	3, 15, 17	syl2anc 595	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑝 ∈ 𝐴) → (𝐼‘(𝑋 ∧ 𝑌)) ∈ (LSubSp‘𝑈))
19	7, 18	sseldd 3940	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑝 ∈ 𝐴) → (𝐼‘(𝑋 ∧ 𝑌)) ∈ (SubGrp‘𝑈))
20		dihmeetlem9.a	. . . . . . 7 ⊢ 𝐴 = (Atoms‘𝐾)
21	12, 20	atbase 39920	. . . . . 6 ⊢ (𝑝 ∈ 𝐴 → 𝑝 ∈ 𝐵)
22	21	3ad2ant3 1151	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑝 ∈ 𝐴) → 𝑝 ∈ 𝐵)
23	12, 1, 16, 2, 5	dihlss 41881	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑝 ∈ 𝐵) → (𝐼‘𝑝) ∈ (LSubSp‘𝑈))
24	3, 22, 23	syl2anc 595	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑝 ∈ 𝐴) → (𝐼‘𝑝) ∈ (LSubSp‘𝑈))
25	7, 24	sseldd 3940	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑝 ∈ 𝐴) → (𝐼‘𝑝) ∈ (SubGrp‘𝑈))
26	12, 1, 16, 2, 5	dihlss 41881	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑌 ∈ 𝐵) → (𝐼‘𝑌) ∈ (LSubSp‘𝑈))
27	3, 11, 26	syl2anc 595	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑝 ∈ 𝐴) → (𝐼‘𝑌) ∈ (LSubSp‘𝑈))
28	7, 27	sseldd 3940	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑝 ∈ 𝐴) → (𝐼‘𝑌) ∈ (SubGrp‘𝑈))
29		dihmeetlem9.l	. . . . . 6 ⊢ ≤ = (le‘𝐾)
30	12, 29, 13	latmle2 18509	. . . . 5 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ∧ 𝑌) ≤ 𝑌)
31	9, 10, 11, 30	syl3anc 1394	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑝 ∈ 𝐴) → (𝑋 ∧ 𝑌) ≤ 𝑌)
32	12, 29, 1, 16	dihord 41895	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∧ 𝑌) ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((𝐼‘(𝑋 ∧ 𝑌)) ⊆ (𝐼‘𝑌) ↔ (𝑋 ∧ 𝑌) ≤ 𝑌))
33	3, 15, 11, 32	syl3anc 1394	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑝 ∈ 𝐴) → ((𝐼‘(𝑋 ∧ 𝑌)) ⊆ (𝐼‘𝑌) ↔ (𝑋 ∧ 𝑌) ≤ 𝑌))
34	31, 33	mpbird 260	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑝 ∈ 𝐴) → (𝐼‘(𝑋 ∧ 𝑌)) ⊆ (𝐼‘𝑌))
35		dihmeetlem9.s	. . . 4 ⊢ ⊕ = (LSSum‘𝑈)
36	35	lsmmod 19733	. . 3 ⊢ ((((𝐼‘(𝑋 ∧ 𝑌)) ∈ (SubGrp‘𝑈) ∧ (𝐼‘𝑝) ∈ (SubGrp‘𝑈) ∧ (𝐼‘𝑌) ∈ (SubGrp‘𝑈)) ∧ (𝐼‘(𝑋 ∧ 𝑌)) ⊆ (𝐼‘𝑌)) → ((𝐼‘(𝑋 ∧ 𝑌)) ⊕ ((𝐼‘𝑝) ∩ (𝐼‘𝑌))) = (((𝐼‘(𝑋 ∧ 𝑌)) ⊕ (𝐼‘𝑝)) ∩ (𝐼‘𝑌)))
37	19, 25, 28, 34, 36	syl31anc 1396	. 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑝 ∈ 𝐴) → ((𝐼‘(𝑋 ∧ 𝑌)) ⊕ ((𝐼‘𝑝) ∩ (𝐼‘𝑌))) = (((𝐼‘(𝑋 ∧ 𝑌)) ⊕ (𝐼‘𝑝)) ∩ (𝐼‘𝑌)))
38		lmodabl 20996	. . . . 5 ⊢ (𝑈 ∈ LMod → 𝑈 ∈ Abel)
39	4, 38	syl 18	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑝 ∈ 𝐴) → 𝑈 ∈ Abel)
40	35	lsmcom 19916	. . . 4 ⊢ ((𝑈 ∈ Abel ∧ (𝐼‘(𝑋 ∧ 𝑌)) ∈ (SubGrp‘𝑈) ∧ (𝐼‘𝑝) ∈ (SubGrp‘𝑈)) → ((𝐼‘(𝑋 ∧ 𝑌)) ⊕ (𝐼‘𝑝)) = ((𝐼‘𝑝) ⊕ (𝐼‘(𝑋 ∧ 𝑌))))
41	39, 19, 25, 40	syl3anc 1394	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑝 ∈ 𝐴) → ((𝐼‘(𝑋 ∧ 𝑌)) ⊕ (𝐼‘𝑝)) = ((𝐼‘𝑝) ⊕ (𝐼‘(𝑋 ∧ 𝑌))))
42	41	ineq1d 4174	. 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑝 ∈ 𝐴) → (((𝐼‘(𝑋 ∧ 𝑌)) ⊕ (𝐼‘𝑝)) ∩ (𝐼‘𝑌)) = (((𝐼‘𝑝) ⊕ (𝐼‘(𝑋 ∧ 𝑌))) ∩ (𝐼‘𝑌)))
43	37, 42	eqtr2d 2801	1 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑝 ∈ 𝐴) → (((𝐼‘𝑝) ⊕ (𝐼‘(𝑋 ∧ 𝑌))) ∩ (𝐼‘𝑌)) = ((𝐼‘(𝑋 ∧ 𝑌)) ⊕ ((𝐼‘𝑝) ∩ (𝐼‘𝑌))))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 209 ∧ wa 400 ∧ w3a 1101 = wceq 1563 ∈ wcel 2145 ∩ cin 3906 ⊆ wss 3907 class class class wbr 5104 ‘cfv 6525 (class class class)co 7400 Basecbs 17257 lecple 17305 joincjn 18355 meetcmee 18356 Latclat 18475 SubGrpcsubg 19174 LSSumclsm 19692 Abelcabl 19839 LModclmod 20947 LSubSpclss 21018 Atomscatm 39894 HLchlt 39981 LHypclh 40615 DVecHcdvh 41709 DIsoHcdih 41859

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1818 ax-4 1832 ax-5 1933 ax-6 1990 ax-7 2031 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2215 ax-ext 2737 ax-rep 5231 ax-sep 5250 ax-nul 5260 ax-pow 5326 ax-pr 5394 ax-un 7722 ax-cnex 11144 ax-resscn 11145 ax-1cn 11146 ax-icn 11147 ax-addcl 11148 ax-addrcl 11149 ax-mulcl 11150 ax-mulrcl 11151 ax-mulcom 11152 ax-addass 11153 ax-mulass 11154 ax-distr 11155 ax-i2m1 11156 ax-1ne0 11157 ax-1rid 11158 ax-rnegex 11159 ax-rrecex 11160 ax-cnre 11161 ax-pre-lttri 11162 ax-pre-lttrn 11163 ax-pre-ltadd 11164 ax-pre-mulgt0 11165 ax-riotaBAD 39584

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1102 df-3an 1103 df-tru 1566 df-fal 1576 df-ex 1803 df-nf 1807 df-sb 2094 df-mo 2569 df-eu 2599 df-clab 2744 df-cleq 2757 df-clel 2840 df-nfc 2914 df-ne 2961 df-nel 3065 df-ral 3080 df-rex 3090 df-rmo 3370 df-reu 3371 df-rab 3418 df-v 3459 df-sbc 3748 df-csb 3856 df-dif 3910 df-un 3912 df-in 3914 df-ss 3924 df-pss 3927 df-nul 4289 df-if 4484 df-pw 4560 df-sn 4586 df-pr 4588 df-tp 4590 df-op 4592 df-uni 4868 df-int 4908 df-iun 4953 df-iin 4954 df-br 5105 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 6291 df-ord 6352 df-on 6353 df-lim 6354 df-suc 6355 df-iota 6481 df-fun 6527 df-fn 6528 df-f 6529 df-f1 6530 df-fo 6531 df-f1o 6532 df-fv 6533 df-riota 7357 df-ov 7403 df-oprab 7404 df-mpo 7405 df-om 7851 df-1st 7974 df-2nd 7975 df-tpos 8210 df-undef 8257 df-frecs 8266 df-wrecs 8297 df-recs 8346 df-rdg 8385 df-1o 8441 df-2o 8442 df-er 8682 df-map 8814 df-en 8932 df-dom 8933 df-sdom 8934 df-fin 8935 df-pnf 11233 df-mnf 11234 df-xr 11235 df-ltxr 11236 df-le 11237 df-sub 11431 df-neg 11432 df-nn 12222 df-2 12291 df-3 12292 df-4 12293 df-5 12294 df-6 12295 df-n0 12493 df-z 12580 df-uz 12851 df-fz 13524 df-struct 17195 df-sets 17212 df-slot 17230 df-ndx 17242 df-base 17258 df-ress 17279 df-plusg 17311 df-mulr 17312 df-sca 17314 df-vsca 17315 df-0g 17482 df-mre 17626 df-mrc 17627 df-acs 17629 df-proset 18338 df-poset 18357 df-plt 18372 df-lub 18388 df-glb 18389 df-join 18390 df-meet 18391 df-p0 18467 df-p1 18468 df-lat 18476 df-clat 18543 df-mgm 18686 df-sgrp 18765 df-mnd 18781 df-submnd 18830 df-grp 18991 df-minusg 18992 df-sbg 18993 df-subg 19177 df-cntz 19375 df-lsm 19694 df-cmn 19840 df-abl 19841 df-mgp 20205 df-rng 20219 df-ur 20252 df-ring 20305 df-oppr 20407 df-dvdsr 20427 df-unit 20428 df-invr 20458 df-dvr 20471 df-drng 20803 df-lmod 20949 df-lss 21019 df-lsp 21059 df-lvec 21190 df-oposet 39807 df-ol 39809 df-oml 39810 df-covers 39897 df-ats 39898 df-atl 39929 df-cvlat 39953 df-hlat 39982 df-llines 40129 df-lplanes 40130 df-lvols 40131 df-lines 40132 df-psubsp 40134 df-pmap 40135 df-padd 40427 df-lhyp 40619 df-laut 40620 df-ldil 40735 df-ltrn 40736 df-trl 40790 df-tendo 41386 df-edring 41388 df-disoa 41660 df-dvech 41710 df-dib 41770 df-dic 41804 df-dih 41860

This theorem is referenced by: dihmeetlem12N 41949

W3C validator