Mathbox for Norm Megill |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > Mathboxes > dihvalcq2 | Structured version Visualization version GIF version |
Description: Value of isomorphism H for a lattice 𝐾 when ¬ 𝑋 ≤ 𝑊, given auxiliary atom 𝑄. (Contributed by NM, 26-Sep-2014.) |
Ref | Expression |
---|---|
dihvalcq2.b | ⊢ 𝐵 = (Base‘𝐾) |
dihvalcq2.l | ⊢ ≤ = (le‘𝐾) |
dihvalcq2.j | ⊢ ∨ = (join‘𝐾) |
dihvalcq2.m | ⊢ ∧ = (meet‘𝐾) |
dihvalcq2.a | ⊢ 𝐴 = (Atoms‘𝐾) |
dihvalcq2.h | ⊢ 𝐻 = (LHyp‘𝐾) |
dihvalcq2.i | ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊) |
dihvalcq2.u | ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) |
dihvalcq2.p | ⊢ ⊕ = (LSSum‘𝑈) |
Ref | Expression |
---|---|
dihvalcq2 | ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑄 ≤ 𝑋)) → (𝐼‘𝑋) = ((𝐼‘𝑄) ⊕ (𝐼‘(𝑋 ∧ 𝑊)))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simp1 1135 | . . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑄 ≤ 𝑋)) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) | |
2 | simp2 1136 | . . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑄 ≤ 𝑋)) → (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊)) | |
3 | simp3l 1200 | . . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑄 ≤ 𝑋)) → (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) | |
4 | simp3r 1201 | . . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑄 ≤ 𝑋)) → 𝑄 ≤ 𝑋) | |
5 | dihvalcq2.b | . . . . . 6 ⊢ 𝐵 = (Base‘𝐾) | |
6 | dihvalcq2.l | . . . . . 6 ⊢ ≤ = (le‘𝐾) | |
7 | dihvalcq2.j | . . . . . 6 ⊢ ∨ = (join‘𝐾) | |
8 | dihvalcq2.m | . . . . . 6 ⊢ ∧ = (meet‘𝐾) | |
9 | dihvalcq2.a | . . . . . 6 ⊢ 𝐴 = (Atoms‘𝐾) | |
10 | dihvalcq2.h | . . . . . 6 ⊢ 𝐻 = (LHyp‘𝐾) | |
11 | 5, 6, 7, 8, 9, 10 | lhpmcvr3 38027 | . . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → (𝑄 ≤ 𝑋 ↔ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) |
12 | 1, 2, 3, 11 | syl3anc 1370 | . . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑄 ≤ 𝑋)) → (𝑄 ≤ 𝑋 ↔ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) |
13 | 4, 12 | mpbid 231 | . . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑄 ≤ 𝑋)) → (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋) |
14 | dihvalcq2.i | . . . 4 ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊) | |
15 | eqid 2740 | . . . 4 ⊢ ((DIsoB‘𝐾)‘𝑊) = ((DIsoB‘𝐾)‘𝑊) | |
16 | eqid 2740 | . . . 4 ⊢ ((DIsoC‘𝐾)‘𝑊) = ((DIsoC‘𝐾)‘𝑊) | |
17 | dihvalcq2.u | . . . 4 ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) | |
18 | dihvalcq2.p | . . . 4 ⊢ ⊕ = (LSSum‘𝑈) | |
19 | 5, 6, 7, 8, 9, 10, 14, 15, 16, 17, 18 | dihvalcq 39238 | . . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → (𝐼‘𝑋) = ((((DIsoC‘𝐾)‘𝑊)‘𝑄) ⊕ (((DIsoB‘𝐾)‘𝑊)‘(𝑋 ∧ 𝑊)))) |
20 | 1, 2, 3, 13, 19 | syl112anc 1373 | . 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑄 ≤ 𝑋)) → (𝐼‘𝑋) = ((((DIsoC‘𝐾)‘𝑊)‘𝑄) ⊕ (((DIsoB‘𝐾)‘𝑊)‘(𝑋 ∧ 𝑊)))) |
21 | 6, 9, 10, 16, 14 | dihvalcqat 39241 | . . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → (𝐼‘𝑄) = (((DIsoC‘𝐾)‘𝑊)‘𝑄)) |
22 | 1, 3, 21 | syl2anc 584 | . . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑄 ≤ 𝑋)) → (𝐼‘𝑄) = (((DIsoC‘𝐾)‘𝑊)‘𝑄)) |
23 | simp1l 1196 | . . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑄 ≤ 𝑋)) → 𝐾 ∈ HL) | |
24 | 23 | hllatd 37366 | . . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑄 ≤ 𝑋)) → 𝐾 ∈ Lat) |
25 | simp2l 1198 | . . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑄 ≤ 𝑋)) → 𝑋 ∈ 𝐵) | |
26 | simp1r 1197 | . . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑄 ≤ 𝑋)) → 𝑊 ∈ 𝐻) | |
27 | 5, 10 | lhpbase 38000 | . . . . . 6 ⊢ (𝑊 ∈ 𝐻 → 𝑊 ∈ 𝐵) |
28 | 26, 27 | syl 17 | . . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑄 ≤ 𝑋)) → 𝑊 ∈ 𝐵) |
29 | 5, 8 | latmcl 18148 | . . . . 5 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵) → (𝑋 ∧ 𝑊) ∈ 𝐵) |
30 | 24, 25, 28, 29 | syl3anc 1370 | . . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑄 ≤ 𝑋)) → (𝑋 ∧ 𝑊) ∈ 𝐵) |
31 | 5, 6, 8 | latmle2 18173 | . . . . 5 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵) → (𝑋 ∧ 𝑊) ≤ 𝑊) |
32 | 24, 25, 28, 31 | syl3anc 1370 | . . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑄 ≤ 𝑋)) → (𝑋 ∧ 𝑊) ≤ 𝑊) |
33 | 5, 6, 10, 14, 15 | dihvalb 39239 | . . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑋 ∧ 𝑊) ∈ 𝐵 ∧ (𝑋 ∧ 𝑊) ≤ 𝑊)) → (𝐼‘(𝑋 ∧ 𝑊)) = (((DIsoB‘𝐾)‘𝑊)‘(𝑋 ∧ 𝑊))) |
34 | 1, 30, 32, 33 | syl12anc 834 | . . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑄 ≤ 𝑋)) → (𝐼‘(𝑋 ∧ 𝑊)) = (((DIsoB‘𝐾)‘𝑊)‘(𝑋 ∧ 𝑊))) |
35 | 22, 34 | oveq12d 7287 | . 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑄 ≤ 𝑋)) → ((𝐼‘𝑄) ⊕ (𝐼‘(𝑋 ∧ 𝑊))) = ((((DIsoC‘𝐾)‘𝑊)‘𝑄) ⊕ (((DIsoB‘𝐾)‘𝑊)‘(𝑋 ∧ 𝑊)))) |
36 | 20, 35 | eqtr4d 2783 | 1 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑄 ≤ 𝑋)) → (𝐼‘𝑋) = ((𝐼‘𝑄) ⊕ (𝐼‘(𝑋 ∧ 𝑊)))) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 396 ∧ w3a 1086 = wceq 1542 ∈ wcel 2110 class class class wbr 5079 ‘cfv 6431 (class class class)co 7269 Basecbs 16902 lecple 16959 joincjn 18019 meetcmee 18020 Latclat 18139 LSSumclsm 19229 Atomscatm 37265 HLchlt 37352 LHypclh 37986 DVecHcdvh 39080 DIsoBcdib 39140 DIsoCcdic 39174 DIsoHcdih 39230 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1975 ax-7 2015 ax-8 2112 ax-9 2120 ax-10 2141 ax-11 2158 ax-12 2175 ax-ext 2711 ax-rep 5214 ax-sep 5227 ax-nul 5234 ax-pow 5292 ax-pr 5356 ax-un 7580 ax-cnex 10920 ax-resscn 10921 ax-1cn 10922 ax-icn 10923 ax-addcl 10924 ax-addrcl 10925 ax-mulcl 10926 ax-mulrcl 10927 ax-mulcom 10928 ax-addass 10929 ax-mulass 10930 ax-distr 10931 ax-i2m1 10932 ax-1ne0 10933 ax-1rid 10934 ax-rnegex 10935 ax-rrecex 10936 ax-cnre 10937 ax-pre-lttri 10938 ax-pre-lttrn 10939 ax-pre-ltadd 10940 ax-pre-mulgt0 10941 ax-riotaBAD 36955 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3or 1087 df-3an 1088 df-tru 1545 df-fal 1555 df-ex 1787 df-nf 1791 df-sb 2072 df-mo 2542 df-eu 2571 df-clab 2718 df-cleq 2732 df-clel 2818 df-nfc 2891 df-ne 2946 df-nel 3052 df-ral 3071 df-rex 3072 df-reu 3073 df-rmo 3074 df-rab 3075 df-v 3433 df-sbc 3721 df-csb 3838 df-dif 3895 df-un 3897 df-in 3899 df-ss 3909 df-pss 3911 df-nul 4263 df-if 4466 df-pw 4541 df-sn 4568 df-pr 4570 df-tp 4572 df-op 4574 df-uni 4846 df-int 4886 df-iun 4932 df-iin 4933 df-br 5080 df-opab 5142 df-mpt 5163 df-tr 5197 df-id 5489 df-eprel 5495 df-po 5503 df-so 5504 df-fr 5544 df-we 5546 df-xp 5595 df-rel 5596 df-cnv 5597 df-co 5598 df-dm 5599 df-rn 5600 df-res 5601 df-ima 5602 df-pred 6200 df-ord 6267 df-on 6268 df-lim 6269 df-suc 6270 df-iota 6389 df-fun 6433 df-fn 6434 df-f 6435 df-f1 6436 df-fo 6437 df-f1o 6438 df-fv 6439 df-riota 7226 df-ov 7272 df-oprab 7273 df-mpo 7274 df-om 7702 df-1st 7818 df-2nd 7819 df-tpos 8027 df-undef 8074 df-frecs 8082 df-wrecs 8113 df-recs 8187 df-rdg 8226 df-1o 8282 df-er 8473 df-map 8592 df-en 8709 df-dom 8710 df-sdom 8711 df-fin 8712 df-pnf 11004 df-mnf 11005 df-xr 11006 df-ltxr 11007 df-le 11008 df-sub 11199 df-neg 11200 df-nn 11966 df-2 12028 df-3 12029 df-4 12030 df-5 12031 df-6 12032 df-n0 12226 df-z 12312 df-uz 12574 df-fz 13231 df-struct 16838 df-sets 16855 df-slot 16873 df-ndx 16885 df-base 16903 df-ress 16932 df-plusg 16965 df-mulr 16966 df-sca 16968 df-vsca 16969 df-0g 17142 df-proset 18003 df-poset 18021 df-plt 18038 df-lub 18054 df-glb 18055 df-join 18056 df-meet 18057 df-p0 18133 df-p1 18134 df-lat 18140 df-clat 18207 df-mgm 18316 df-sgrp 18365 df-mnd 18376 df-submnd 18421 df-grp 18570 df-minusg 18571 df-sbg 18572 df-subg 18742 df-cntz 18913 df-lsm 19231 df-cmn 19378 df-abl 19379 df-mgp 19711 df-ur 19728 df-ring 19775 df-oppr 19852 df-dvdsr 19873 df-unit 19874 df-invr 19904 df-dvr 19915 df-drng 19983 df-lmod 20115 df-lss 20184 df-lsp 20224 df-lvec 20355 df-oposet 37178 df-ol 37180 df-oml 37181 df-covers 37268 df-ats 37269 df-atl 37300 df-cvlat 37324 df-hlat 37353 df-llines 37500 df-lplanes 37501 df-lvols 37502 df-lines 37503 df-psubsp 37505 df-pmap 37506 df-padd 37798 df-lhyp 37990 df-laut 37991 df-ldil 38106 df-ltrn 38107 df-trl 38161 df-tendo 38757 df-edring 38759 df-disoa 39031 df-dvech 39081 df-dib 39141 df-dic 39175 df-dih 39231 |
This theorem is referenced by: dihjatc1 39313 dihjatcclem1 39420 |
Copyright terms: Public domain | W3C validator |