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 41421

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 41420	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝐼‘(𝑋 ∨ 𝑌)) = ((𝐼‘𝑋)𝐽(𝐼‘𝑌)))
10	1, 2, 3, 9	syl12anc 836	. . 3 ⊢ (𝜑 → (𝐼‘(𝑋 ∨ 𝑌)) = ((𝐼‘𝑋)𝐽(𝐼‘𝑌)))
11	4, 6, 7	dihcl 41289	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝐵) → (𝐼‘𝑋) ∈ ran 𝐼)
12	1, 2, 11	syl2anc 584	. . . . . 6 ⊢ (𝜑 → (𝐼‘𝑋) ∈ ran 𝐼)
13		eqid 2735	. . . . . . 7 ⊢ ((DVecH‘𝐾)‘𝑊) = ((DVecH‘𝐾)‘𝑊)
14		eqid 2735	. . . . . . 7 ⊢ (Base‘((DVecH‘𝐾)‘𝑊)) = (Base‘((DVecH‘𝐾)‘𝑊))
15	6, 13, 7, 14	dihrnss 41297	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐼‘𝑋) ∈ ran 𝐼) → (𝐼‘𝑋) ⊆ (Base‘((DVecH‘𝐾)‘𝑊)))
16	1, 12, 15	syl2anc 584	. . . . 5 ⊢ (𝜑 → (𝐼‘𝑋) ⊆ (Base‘((DVecH‘𝐾)‘𝑊)))
17	4, 6, 7	dihcl 41289	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑌 ∈ 𝐵) → (𝐼‘𝑌) ∈ ran 𝐼)
18	1, 3, 17	syl2anc 584	. . . . . 6 ⊢ (𝜑 → (𝐼‘𝑌) ∈ ran 𝐼)
19	6, 13, 7, 14	dihrnss 41297	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐼‘𝑌) ∈ ran 𝐼) → (𝐼‘𝑌) ⊆ (Base‘((DVecH‘𝐾)‘𝑊)))
20	1, 18, 19	syl2anc 584	. . . . 5 ⊢ (𝜑 → (𝐼‘𝑌) ⊆ (Base‘((DVecH‘𝐾)‘𝑊)))
21	6, 7, 13, 14, 8	djhcl 41419	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝐼‘𝑋) ⊆ (Base‘((DVecH‘𝐾)‘𝑊)) ∧ (𝐼‘𝑌) ⊆ (Base‘((DVecH‘𝐾)‘𝑊)))) → ((𝐼‘𝑋)𝐽(𝐼‘𝑌)) ∈ ran 𝐼)
22	1, 16, 20, 21	syl12anc 836	. . . 4 ⊢ (𝜑 → ((𝐼‘𝑋)𝐽(𝐼‘𝑌)) ∈ ran 𝐼)
23	6, 7	dihcnvid2 41292	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝐼‘𝑋)𝐽(𝐼‘𝑌)) ∈ ran 𝐼) → (𝐼‘(^◡𝐼‘((𝐼‘𝑋)𝐽(𝐼‘𝑌)))) = ((𝐼‘𝑋)𝐽(𝐼‘𝑌)))
24	1, 22, 23	syl2anc 584	. . 3 ⊢ (𝜑 → (𝐼‘(^◡𝐼‘((𝐼‘𝑋)𝐽(𝐼‘𝑌)))) = ((𝐼‘𝑋)𝐽(𝐼‘𝑌)))
25	10, 24	eqtr4d 2773	. 2 ⊢ (𝜑 → (𝐼‘(𝑋 ∨ 𝑌)) = (𝐼‘(^◡𝐼‘((𝐼‘𝑋)𝐽(𝐼‘𝑌)))))
26	1	simpld 494	. . . . 5 ⊢ (𝜑 → 𝐾 ∈ HL)
27	26	hllatd 39382	. . . 4 ⊢ (𝜑 → 𝐾 ∈ Lat)
28	4, 5	latjcl 18449	. . . 4 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ∨ 𝑌) ∈ 𝐵)
29	27, 2, 3, 28	syl3anc 1373	. . 3 ⊢ (𝜑 → (𝑋 ∨ 𝑌) ∈ 𝐵)
30	4, 6, 7	dihcnvcl 41290	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝐼‘𝑋)𝐽(𝐼‘𝑌)) ∈ ran 𝐼) → (^◡𝐼‘((𝐼‘𝑋)𝐽(𝐼‘𝑌))) ∈ 𝐵)
31	1, 22, 30	syl2anc 584	. . 3 ⊢ (𝜑 → (^◡𝐼‘((𝐼‘𝑋)𝐽(𝐼‘𝑌))) ∈ 𝐵)
32	4, 6, 7	dih11 41284	. . 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 2108 ⊆ wss 3926 ^◡ccnv 5653 ran crn 5655 ‘cfv 6531 (class class class)co 7405 Basecbs 17228 joincjn 18323 Latclat 18441 HLchlt 39368 LHypclh 40003 DVecHcdvh 41097 DIsoHcdih 41247 joinHcdjh 41413

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 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2157 ax-12 2177 ax-ext 2707 ax-rep 5249 ax-sep 5266 ax-nul 5276 ax-pow 5335 ax-pr 5402 ax-un 7729 ax-cnex 11185 ax-resscn 11186 ax-1cn 11187 ax-icn 11188 ax-addcl 11189 ax-addrcl 11190 ax-mulcl 11191 ax-mulrcl 11192 ax-mulcom 11193 ax-addass 11194 ax-mulass 11195 ax-distr 11196 ax-i2m1 11197 ax-1ne0 11198 ax-1rid 11199 ax-rnegex 11200 ax-rrecex 11201 ax-cnre 11202 ax-pre-lttri 11203 ax-pre-lttrn 11204 ax-pre-ltadd 11205 ax-pre-mulgt0 11206 ax-riotaBAD 38971

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 2065 df-mo 2539 df-eu 2568 df-clab 2714 df-cleq 2727 df-clel 2809 df-nfc 2885 df-ne 2933 df-nel 3037 df-ral 3052 df-rex 3061 df-rmo 3359 df-reu 3360 df-rab 3416 df-v 3461 df-sbc 3766 df-csb 3875 df-dif 3929 df-un 3931 df-in 3933 df-ss 3943 df-pss 3946 df-nul 4309 df-if 4501 df-pw 4577 df-sn 4602 df-pr 4604 df-tp 4606 df-op 4608 df-uni 4884 df-int 4923 df-iun 4969 df-iin 4970 df-br 5120 df-opab 5182 df-mpt 5202 df-tr 5230 df-id 5548 df-eprel 5553 df-po 5561 df-so 5562 df-fr 5606 df-we 5608 df-xp 5660 df-rel 5661 df-cnv 5662 df-co 5663 df-dm 5664 df-rn 5665 df-res 5666 df-ima 5667 df-pred 6290 df-ord 6355 df-on 6356 df-lim 6357 df-suc 6358 df-iota 6484 df-fun 6533 df-fn 6534 df-f 6535 df-f1 6536 df-fo 6537 df-f1o 6538 df-fv 6539 df-riota 7362 df-ov 7408 df-oprab 7409 df-mpo 7410 df-om 7862 df-1st 7988 df-2nd 7989 df-tpos 8225 df-undef 8272 df-frecs 8280 df-wrecs 8311 df-recs 8385 df-rdg 8424 df-1o 8480 df-er 8719 df-map 8842 df-en 8960 df-dom 8961 df-sdom 8962 df-fin 8963 df-pnf 11271 df-mnf 11272 df-xr 11273 df-ltxr 11274 df-le 11275 df-sub 11468 df-neg 11469 df-nn 12241 df-2 12303 df-3 12304 df-4 12305 df-5 12306 df-6 12307 df-n0 12502 df-z 12589 df-uz 12853 df-fz 13525 df-struct 17166 df-sets 17183 df-slot 17201 df-ndx 17213 df-base 17229 df-ress 17252 df-plusg 17284 df-mulr 17285 df-sca 17287 df-vsca 17288 df-0g 17455 df-proset 18306 df-poset 18325 df-plt 18340 df-lub 18356 df-glb 18357 df-join 18358 df-meet 18359 df-p0 18435 df-p1 18436 df-lat 18442 df-clat 18509 df-mgm 18618 df-sgrp 18697 df-mnd 18713 df-submnd 18762 df-grp 18919 df-minusg 18920 df-sbg 18921 df-subg 19106 df-cntz 19300 df-lsm 19617 df-cmn 19763 df-abl 19764 df-mgp 20101 df-rng 20113 df-ur 20142 df-ring 20195 df-oppr 20297 df-dvdsr 20317 df-unit 20318 df-invr 20348 df-dvr 20361 df-drng 20691 df-lmod 20819 df-lss 20889 df-lsp 20929 df-lvec 21061 df-lsatoms 38994 df-oposet 39194 df-ol 39196 df-oml 39197 df-covers 39284 df-ats 39285 df-atl 39316 df-cvlat 39340 df-hlat 39369 df-llines 39517 df-lplanes 39518 df-lvols 39519 df-lines 39520 df-psubsp 39522 df-pmap 39523 df-padd 39815 df-lhyp 40007 df-laut 40008 df-ldil 40123 df-ltrn 40124 df-trl 40178 df-tendo 40774 df-edring 40776 df-disoa 41048 df-dvech 41098 df-dib 41158 df-dic 41192 df-dih 41248 df-doch 41367 df-djh 41414

This theorem is referenced by: (None)

W3C validator