djhljjN - Mathbox for Norm Megill

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

Theorem djhljjN 41391

Description: Lattice join in terms of DVecH vector space closed subspace join. (Contributed by NM, 17-Aug-2014.) (New usage is discouraged.)

**Hypotheses**
Ref	Expression
djhlj.b	⊢ 𝐵 = (Base‘𝐾)
djhlj.k	⊢ ∨ = (join‘𝐾)
djhlj.h	⊢ 𝐻 = (LHyp‘𝐾)
djhlj.i	⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊)
djhlj.j	⊢ 𝐽 = ((joinH‘𝐾)‘𝑊)
djhljj.w	⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
djhljj.x	⊢ (𝜑 → 𝑋 ∈ 𝐵)
djhljj.y	⊢ (𝜑 → 𝑌 ∈ 𝐵)

**Assertion**
Ref	Expression
djhljjN	⊢ (𝜑 → (𝑋 ∨ 𝑌) = (^◡𝐼‘((𝐼‘𝑋)𝐽(𝐼‘𝑌))))

**Proof of Theorem djhljjN**
Step	Hyp	Ref	Expression
1		djhljj.w	. . . 4 ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
2		djhljj.x	. . . 4 ⊢ (𝜑 → 𝑋 ∈ 𝐵)
3		djhljj.y	. . . 4 ⊢ (𝜑 → 𝑌 ∈ 𝐵)
4		djhlj.b	. . . . 5 ⊢ 𝐵 = (Base‘𝐾)
5		djhlj.k	. . . . 5 ⊢ ∨ = (join‘𝐾)
6		djhlj.h	. . . . 5 ⊢ 𝐻 = (LHyp‘𝐾)
7		djhlj.i	. . . . 5 ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊)
8		djhlj.j	. . . . 5 ⊢ 𝐽 = ((joinH‘𝐾)‘𝑊)
9	4, 5, 6, 7, 8	djhlj 41390	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝐼‘(𝑋 ∨ 𝑌)) = ((𝐼‘𝑋)𝐽(𝐼‘𝑌)))
10	1, 2, 3, 9	syl12anc 836	. . 3 ⊢ (𝜑 → (𝐼‘(𝑋 ∨ 𝑌)) = ((𝐼‘𝑋)𝐽(𝐼‘𝑌)))
11	4, 6, 7	dihcl 41259	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝐵) → (𝐼‘𝑋) ∈ ran 𝐼)
12	1, 2, 11	syl2anc 584	. . . . . 6 ⊢ (𝜑 → (𝐼‘𝑋) ∈ ran 𝐼)
13		eqid 2729	. . . . . . 7 ⊢ ((DVecH‘𝐾)‘𝑊) = ((DVecH‘𝐾)‘𝑊)
14		eqid 2729	. . . . . . 7 ⊢ (Base‘((DVecH‘𝐾)‘𝑊)) = (Base‘((DVecH‘𝐾)‘𝑊))
15	6, 13, 7, 14	dihrnss 41267	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐼‘𝑋) ∈ ran 𝐼) → (𝐼‘𝑋) ⊆ (Base‘((DVecH‘𝐾)‘𝑊)))
16	1, 12, 15	syl2anc 584	. . . . 5 ⊢ (𝜑 → (𝐼‘𝑋) ⊆ (Base‘((DVecH‘𝐾)‘𝑊)))
17	4, 6, 7	dihcl 41259	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑌 ∈ 𝐵) → (𝐼‘𝑌) ∈ ran 𝐼)
18	1, 3, 17	syl2anc 584	. . . . . 6 ⊢ (𝜑 → (𝐼‘𝑌) ∈ ran 𝐼)
19	6, 13, 7, 14	dihrnss 41267	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐼‘𝑌) ∈ ran 𝐼) → (𝐼‘𝑌) ⊆ (Base‘((DVecH‘𝐾)‘𝑊)))
20	1, 18, 19	syl2anc 584	. . . . 5 ⊢ (𝜑 → (𝐼‘𝑌) ⊆ (Base‘((DVecH‘𝐾)‘𝑊)))
21	6, 7, 13, 14, 8	djhcl 41389	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝐼‘𝑋) ⊆ (Base‘((DVecH‘𝐾)‘𝑊)) ∧ (𝐼‘𝑌) ⊆ (Base‘((DVecH‘𝐾)‘𝑊)))) → ((𝐼‘𝑋)𝐽(𝐼‘𝑌)) ∈ ran 𝐼)
22	1, 16, 20, 21	syl12anc 836	. . . 4 ⊢ (𝜑 → ((𝐼‘𝑋)𝐽(𝐼‘𝑌)) ∈ ran 𝐼)
23	6, 7	dihcnvid2 41262	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝐼‘𝑋)𝐽(𝐼‘𝑌)) ∈ ran 𝐼) → (𝐼‘(^◡𝐼‘((𝐼‘𝑋)𝐽(𝐼‘𝑌)))) = ((𝐼‘𝑋)𝐽(𝐼‘𝑌)))
24	1, 22, 23	syl2anc 584	. . 3 ⊢ (𝜑 → (𝐼‘(^◡𝐼‘((𝐼‘𝑋)𝐽(𝐼‘𝑌)))) = ((𝐼‘𝑋)𝐽(𝐼‘𝑌)))
25	10, 24	eqtr4d 2767	. 2 ⊢ (𝜑 → (𝐼‘(𝑋 ∨ 𝑌)) = (𝐼‘(^◡𝐼‘((𝐼‘𝑋)𝐽(𝐼‘𝑌)))))
26	1	simpld 494	. . . . 5 ⊢ (𝜑 → 𝐾 ∈ HL)
27	26	hllatd 39352	. . . 4 ⊢ (𝜑 → 𝐾 ∈ Lat)
28	4, 5	latjcl 18382	. . . 4 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ∨ 𝑌) ∈ 𝐵)
29	27, 2, 3, 28	syl3anc 1373	. . 3 ⊢ (𝜑 → (𝑋 ∨ 𝑌) ∈ 𝐵)
30	4, 6, 7	dihcnvcl 41260	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝐼‘𝑋)𝐽(𝐼‘𝑌)) ∈ ran 𝐼) → (^◡𝐼‘((𝐼‘𝑋)𝐽(𝐼‘𝑌))) ∈ 𝐵)
31	1, 22, 30	syl2anc 584	. . 3 ⊢ (𝜑 → (^◡𝐼‘((𝐼‘𝑋)𝐽(𝐼‘𝑌))) ∈ 𝐵)
32	4, 6, 7	dih11 41254	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∨ 𝑌) ∈ 𝐵 ∧ (^◡𝐼‘((𝐼‘𝑋)𝐽(𝐼‘𝑌))) ∈ 𝐵) → ((𝐼‘(𝑋 ∨ 𝑌)) = (𝐼‘(^◡𝐼‘((𝐼‘𝑋)𝐽(𝐼‘𝑌)))) ↔ (𝑋 ∨ 𝑌) = (^◡𝐼‘((𝐼‘𝑋)𝐽(𝐼‘𝑌)))))
33	1, 29, 31, 32	syl3anc 1373	. 2 ⊢ (𝜑 → ((𝐼‘(𝑋 ∨ 𝑌)) = (𝐼‘(^◡𝐼‘((𝐼‘𝑋)𝐽(𝐼‘𝑌)))) ↔ (𝑋 ∨ 𝑌) = (^◡𝐼‘((𝐼‘𝑋)𝐽(𝐼‘𝑌)))))
34	25, 33	mpbid 232	1 ⊢ (𝜑 → (𝑋 ∨ 𝑌) = (^◡𝐼‘((𝐼‘𝑋)𝐽(𝐼‘𝑌))))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 = wceq 1540 ∈ wcel 2109 ⊆ wss 3911 ^◡ccnv 5630 ran crn 5632 ‘cfv 6500 (class class class)co 7370 Basecbs 17157 joincjn 18254 Latclat 18374 HLchlt 39338 LHypclh 39973 DVecHcdvh 41067 DIsoHcdih 41217 joinHcdjh 41383

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2701 ax-rep 5229 ax-sep 5246 ax-nul 5256 ax-pow 5315 ax-pr 5382 ax-un 7692 ax-cnex 11103 ax-resscn 11104 ax-1cn 11105 ax-icn 11106 ax-addcl 11107 ax-addrcl 11108 ax-mulcl 11109 ax-mulrcl 11110 ax-mulcom 11111 ax-addass 11112 ax-mulass 11113 ax-distr 11114 ax-i2m1 11115 ax-1ne0 11116 ax-1rid 11117 ax-rnegex 11118 ax-rrecex 11119 ax-cnre 11120 ax-pre-lttri 11121 ax-pre-lttrn 11122 ax-pre-ltadd 11123 ax-pre-mulgt0 11124 ax-riotaBAD 38941

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2533 df-eu 2562 df-clab 2708 df-cleq 2721 df-clel 2803 df-nfc 2878 df-ne 2926 df-nel 3030 df-ral 3045 df-rex 3054 df-rmo 3351 df-reu 3352 df-rab 3403 df-v 3446 df-sbc 3751 df-csb 3860 df-dif 3914 df-un 3916 df-in 3918 df-ss 3928 df-pss 3931 df-nul 4293 df-if 4485 df-pw 4561 df-sn 4586 df-pr 4588 df-tp 4590 df-op 4592 df-uni 4868 df-int 4907 df-iun 4953 df-iin 4954 df-br 5103 df-opab 5165 df-mpt 5184 df-tr 5210 df-id 5526 df-eprel 5531 df-po 5539 df-so 5540 df-fr 5584 df-we 5586 df-xp 5637 df-rel 5638 df-cnv 5639 df-co 5640 df-dm 5641 df-rn 5642 df-res 5643 df-ima 5644 df-pred 6263 df-ord 6324 df-on 6325 df-lim 6326 df-suc 6327 df-iota 6453 df-fun 6502 df-fn 6503 df-f 6504 df-f1 6505 df-fo 6506 df-f1o 6507 df-fv 6508 df-riota 7327 df-ov 7373 df-oprab 7374 df-mpo 7375 df-om 7824 df-1st 7948 df-2nd 7949 df-tpos 8183 df-undef 8230 df-frecs 8238 df-wrecs 8269 df-recs 8318 df-rdg 8356 df-1o 8412 df-er 8649 df-map 8779 df-en 8897 df-dom 8898 df-sdom 8899 df-fin 8900 df-pnf 11189 df-mnf 11190 df-xr 11191 df-ltxr 11192 df-le 11193 df-sub 11386 df-neg 11387 df-nn 12166 df-2 12228 df-3 12229 df-4 12230 df-5 12231 df-6 12232 df-n0 12422 df-z 12509 df-uz 12773 df-fz 13448 df-struct 17095 df-sets 17112 df-slot 17130 df-ndx 17142 df-base 17158 df-ress 17179 df-plusg 17211 df-mulr 17212 df-sca 17214 df-vsca 17215 df-0g 17382 df-proset 18237 df-poset 18256 df-plt 18271 df-lub 18287 df-glb 18288 df-join 18289 df-meet 18290 df-p0 18366 df-p1 18367 df-lat 18375 df-clat 18442 df-mgm 18551 df-sgrp 18630 df-mnd 18646 df-submnd 18695 df-grp 18852 df-minusg 18853 df-sbg 18854 df-subg 19039 df-cntz 19233 df-lsm 19552 df-cmn 19698 df-abl 19699 df-mgp 20063 df-rng 20075 df-ur 20104 df-ring 20157 df-oppr 20259 df-dvdsr 20279 df-unit 20280 df-invr 20310 df-dvr 20323 df-drng 20653 df-lmod 20802 df-lss 20872 df-lsp 20912 df-lvec 21044 df-lsatoms 38964 df-oposet 39164 df-ol 39166 df-oml 39167 df-covers 39254 df-ats 39255 df-atl 39286 df-cvlat 39310 df-hlat 39339 df-llines 39487 df-lplanes 39488 df-lvols 39489 df-lines 39490 df-psubsp 39492 df-pmap 39493 df-padd 39785 df-lhyp 39977 df-laut 39978 df-ldil 40093 df-ltrn 40094 df-trl 40148 df-tendo 40744 df-edring 40746 df-disoa 41018 df-dvech 41068 df-dib 41128 df-dic 41162 df-dih 41218 df-doch 41337 df-djh 41384

This theorem is referenced by: (None)

W3C validator