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 42209

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 42208	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝐼‘(𝑋 ∨ 𝑌)) = ((𝐼‘𝑋)𝐽(𝐼‘𝑌)))
10	1, 2, 3, 9	syl12anc 850	. . 3 ⊢ (𝜑 → (𝐼‘(𝑋 ∨ 𝑌)) = ((𝐼‘𝑋)𝐽(𝐼‘𝑌)))
11	4, 6, 7	dihcl 42077	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝐵) → (𝐼‘𝑋) ∈ ran 𝐼)
12	1, 2, 11	syl2anc 596	. . . . . 6 ⊢ (𝜑 → (𝐼‘𝑋) ∈ ran 𝐼)
13		eqid 2765	. . . . . . 7 ⊢ ((DVecH‘𝐾)‘𝑊) = ((DVecH‘𝐾)‘𝑊)
14		eqid 2765	. . . . . . 7 ⊢ (Base‘((DVecH‘𝐾)‘𝑊)) = (Base‘((DVecH‘𝐾)‘𝑊))
15	6, 13, 7, 14	dihrnss 42085	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐼‘𝑋) ∈ ran 𝐼) → (𝐼‘𝑋) ⊆ (Base‘((DVecH‘𝐾)‘𝑊)))
16	1, 12, 15	syl2anc 596	. . . . 5 ⊢ (𝜑 → (𝐼‘𝑋) ⊆ (Base‘((DVecH‘𝐾)‘𝑊)))
17	4, 6, 7	dihcl 42077	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑌 ∈ 𝐵) → (𝐼‘𝑌) ∈ ran 𝐼)
18	1, 3, 17	syl2anc 596	. . . . . 6 ⊢ (𝜑 → (𝐼‘𝑌) ∈ ran 𝐼)
19	6, 13, 7, 14	dihrnss 42085	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐼‘𝑌) ∈ ran 𝐼) → (𝐼‘𝑌) ⊆ (Base‘((DVecH‘𝐾)‘𝑊)))
20	1, 18, 19	syl2anc 596	. . . . 5 ⊢ (𝜑 → (𝐼‘𝑌) ⊆ (Base‘((DVecH‘𝐾)‘𝑊)))
21	6, 7, 13, 14, 8	djhcl 42207	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝐼‘𝑋) ⊆ (Base‘((DVecH‘𝐾)‘𝑊)) ∧ (𝐼‘𝑌) ⊆ (Base‘((DVecH‘𝐾)‘𝑊)))) → ((𝐼‘𝑋)𝐽(𝐼‘𝑌)) ∈ ran 𝐼)
22	1, 16, 20, 21	syl12anc 850	. . . 4 ⊢ (𝜑 → ((𝐼‘𝑋)𝐽(𝐼‘𝑌)) ∈ ran 𝐼)
23	6, 7	dihcnvid2 42080	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝐼‘𝑋)𝐽(𝐼‘𝑌)) ∈ ran 𝐼) → (𝐼‘(^◡𝐼‘((𝐼‘𝑋)𝐽(𝐼‘𝑌)))) = ((𝐼‘𝑋)𝐽(𝐼‘𝑌)))
24	1, 22, 23	syl2anc 596	. . 3 ⊢ (𝜑 → (𝐼‘(^◡𝐼‘((𝐼‘𝑋)𝐽(𝐼‘𝑌)))) = ((𝐼‘𝑋)𝐽(𝐼‘𝑌)))
25	10, 24	eqtr4d 2803	. 2 ⊢ (𝜑 → (𝐼‘(𝑋 ∨ 𝑌)) = (𝐼‘(^◡𝐼‘((𝐼‘𝑋)𝐽(𝐼‘𝑌)))))
26	1	simpld 500	. . . . 5 ⊢ (𝜑 → 𝐾 ∈ HL)
27	26	hllatd 40171	. . . 4 ⊢ (𝜑 → 𝐾 ∈ Lat)
28	4, 5	latjcl 18512	. . . 4 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ∨ 𝑌) ∈ 𝐵)
29	27, 2, 3, 28	syl3anc 1398	. . 3 ⊢ (𝜑 → (𝑋 ∨ 𝑌) ∈ 𝐵)
30	4, 6, 7	dihcnvcl 42078	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝐼‘𝑋)𝐽(𝐼‘𝑌)) ∈ ran 𝐼) → (^◡𝐼‘((𝐼‘𝑋)𝐽(𝐼‘𝑌))) ∈ 𝐵)
31	1, 22, 30	syl2anc 596	. . 3 ⊢ (𝜑 → (^◡𝐼‘((𝐼‘𝑋)𝐽(𝐼‘𝑌))) ∈ 𝐵)
32	4, 6, 7	dih11 42072	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∨ 𝑌) ∈ 𝐵 ∧ (^◡𝐼‘((𝐼‘𝑋)𝐽(𝐼‘𝑌))) ∈ 𝐵) → ((𝐼‘(𝑋 ∨ 𝑌)) = (𝐼‘(^◡𝐼‘((𝐼‘𝑋)𝐽(𝐼‘𝑌)))) ↔ (𝑋 ∨ 𝑌) = (^◡𝐼‘((𝐼‘𝑋)𝐽(𝐼‘𝑌)))))
33	1, 29, 31, 32	syl3anc 1398	. 2 ⊢ (𝜑 → ((𝐼‘(𝑋 ∨ 𝑌)) = (𝐼‘(^◡𝐼‘((𝐼‘𝑋)𝐽(𝐼‘𝑌)))) ↔ (𝑋 ∨ 𝑌) = (^◡𝐼‘((𝐼‘𝑋)𝐽(𝐼‘𝑌)))))
34	25, 33	mpbid 235	1 ⊢ (𝜑 → (𝑋 ∨ 𝑌) = (^◡𝐼‘((𝐼‘𝑋)𝐽(𝐼‘𝑌))))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ↔ wb 209 ∧ wa 401 = wceq 1570 ∈ wcel 2146 ⊆ wss 3906 ^◡ccnv 5662 ran crn 5664 ‘cfv 6540 (class class class)co 7416 Basecbs 17286 joincjn 18384 Latclat 18504 HLchlt 40157 LHypclh 40791 DVecHcdvh 41885 DIsoHcdih 42035 joinHcdjh 42201

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2148 ax-9 2156 ax-10 2179 ax-11 2195 ax-12 2216 ax-ext 2737 ax-rep 5240 ax-sep 5259 ax-nul 5271 ax-pow 5338 ax-pr 5406 ax-un 7738 ax-cnex 11167 ax-resscn 11168 ax-1cn 11169 ax-icn 11170 ax-addcl 11171 ax-addrcl 11172 ax-mulcl 11173 ax-mulrcl 11174 ax-mulcom 11175 ax-addass 11176 ax-mulass 11177 ax-distr 11178 ax-i2m1 11179 ax-1ne0 11180 ax-1rid 11181 ax-rnegex 11182 ax-rrecex 11183 ax-cnre 11184 ax-pre-lttri 11185 ax-pre-lttrn 11186 ax-pre-ltadd 11187 ax-pre-mulgt0 11188 ax-riotaBAD 39760

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2569 df-eu 2599 df-clab 2744 df-cleq 2757 df-clel 2840 df-nfc 2914 df-ne 2961 df-nel 3067 df-ral 3082 df-rex 3092 df-rmo 3371 df-reu 3372 df-rab 3419 df-v 3459 df-sbc 3747 df-csb 3855 df-dif 3909 df-un 3911 df-in 3913 df-ss 3923 df-pss 3926 df-nul 4287 df-if 4490 df-pw 4566 df-sn 4592 df-pr 4594 df-tp 4596 df-op 4598 df-uni 4875 df-int 4915 df-iun 4960 df-iin 4961 df-br 5112 df-opab 5176 df-mpt 5195 df-tr 5221 df-id 5558 df-eprel 5563 df-po 5571 df-so 5572 df-fr 5616 df-we 5618 df-xp 5669 df-rel 5670 df-cnv 5671 df-co 5672 df-dm 5673 df-rn 5674 df-res 5675 df-ima 5676 df-pred 6306 df-ord 6367 df-on 6368 df-lim 6369 df-suc 6370 df-iota 6496 df-fun 6542 df-fn 6543 df-f 6544 df-f1 6545 df-fo 6546 df-f1o 6547 df-fv 6548 df-riota 7373 df-ov 7419 df-oprab 7420 df-mpo 7421 df-om 7865 df-1st 7988 df-2nd 7989 df-tpos 8224 df-undef 8271 df-frecs 8280 df-wrecs 8311 df-recs 8360 df-rdg 8399 df-1o 8455 df-er 8696 df-map 8828 df-en 8946 df-dom 8947 df-sdom 8948 df-fin 8949 df-pnf 11256 df-mnf 11257 df-xr 11258 df-ltxr 11259 df-le 11260 df-sub 11454 df-neg 11455 df-nn 12245 df-2 12314 df-3 12315 df-4 12316 df-5 12317 df-6 12318 df-n0 12516 df-z 12603 df-uz 12874 df-fz 13547 df-struct 17224 df-sets 17241 df-slot 17259 df-ndx 17271 df-base 17287 df-ress 17308 df-plusg 17340 df-mulr 17341 df-sca 17343 df-vsca 17344 df-0g 17511 df-proset 18367 df-poset 18386 df-plt 18401 df-lub 18417 df-glb 18418 df-join 18419 df-meet 18420 df-p0 18496 df-p1 18497 df-lat 18505 df-clat 18572 df-mgm 18715 df-sgrp 18798 df-mnd 18814 df-submnd 18865 df-grp 19026 df-minusg 19027 df-sbg 19028 df-subg 19212 df-cntz 19410 df-lsm 19729 df-cmn 19875 df-abl 19876 df-mgp 20240 df-rng 20254 df-ur 20287 df-ring 20340 df-oppr 20444 df-dvdsr 20464 df-unit 20465 df-invr 20495 df-dvr 20508 df-drng 20858 df-lmod 21012 df-lss 21082 df-lsp 21122 df-lvec 21253 df-lsatoms 39783 df-oposet 39983 df-ol 39985 df-oml 39986 df-covers 40073 df-ats 40074 df-atl 40105 df-cvlat 40129 df-hlat 40158 df-llines 40305 df-lplanes 40306 df-lvols 40307 df-lines 40308 df-psubsp 40310 df-pmap 40311 df-padd 40603 df-lhyp 40795 df-laut 40796 df-ldil 40911 df-ltrn 40912 df-trl 40966 df-tendo 41562 df-edring 41564 df-disoa 41836 df-dvech 41886 df-dib 41946 df-dic 41980 df-dih 42036 df-doch 42155 df-djh 42202

This theorem is used by: (None)

W3C validator