Mathbox for Norm Megill |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > Mathboxes > cdlemn5 | Structured version Visualization version GIF version |
Description: Part of proof of Lemma N of [Crawley] p. 121 line 32. (Contributed by NM, 25-Feb-2014.) |
Ref | Expression |
---|---|
cdlemn5.b | ⊢ 𝐵 = (Base‘𝐾) |
cdlemn5.l | ⊢ ≤ = (le‘𝐾) |
cdlemn5.j | ⊢ ∨ = (join‘𝐾) |
cdlemn5.a | ⊢ 𝐴 = (Atoms‘𝐾) |
cdlemn5.h | ⊢ 𝐻 = (LHyp‘𝐾) |
cdlemn5.u | ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) |
cdlemn5.s | ⊢ ⊕ = (LSSum‘𝑈) |
cdlemn5.i | ⊢ 𝐼 = ((DIsoB‘𝐾)‘𝑊) |
cdlemn5.J | ⊢ 𝐽 = ((DIsoC‘𝐾)‘𝑊) |
Ref | Expression |
---|---|
cdlemn5 | ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ 𝑅 ≤ (𝑄 ∨ 𝑋)) → (𝐽‘𝑅) ⊆ ((𝐽‘𝑄) ⊕ (𝐼‘𝑋))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cdlemn5.b | . 2 ⊢ 𝐵 = (Base‘𝐾) | |
2 | cdlemn5.l | . 2 ⊢ ≤ = (le‘𝐾) | |
3 | cdlemn5.j | . 2 ⊢ ∨ = (join‘𝐾) | |
4 | cdlemn5.a | . 2 ⊢ 𝐴 = (Atoms‘𝐾) | |
5 | cdlemn5.h | . 2 ⊢ 𝐻 = (LHyp‘𝐾) | |
6 | cdlemn5.u | . 2 ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) | |
7 | cdlemn5.s | . 2 ⊢ ⊕ = (LSSum‘𝑈) | |
8 | cdlemn5.i | . 2 ⊢ 𝐼 = ((DIsoB‘𝐾)‘𝑊) | |
9 | cdlemn5.J | . 2 ⊢ 𝐽 = ((DIsoC‘𝐾)‘𝑊) | |
10 | eqid 2738 | . 2 ⊢ ((oc‘𝐾)‘𝑊) = ((oc‘𝐾)‘𝑊) | |
11 | eqid 2738 | . 2 ⊢ (ℎ ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ 𝐵)) = (ℎ ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ 𝐵)) | |
12 | eqid 2738 | . 2 ⊢ ((LTrn‘𝐾)‘𝑊) = ((LTrn‘𝐾)‘𝑊) | |
13 | eqid 2738 | . 2 ⊢ ((TEndo‘𝐾)‘𝑊) = ((TEndo‘𝐾)‘𝑊) | |
14 | eqid 2738 | . 2 ⊢ (LSpan‘𝑈) = (LSpan‘𝑈) | |
15 | eqid 2738 | . 2 ⊢ (℩ℎ ∈ ((LTrn‘𝐾)‘𝑊)(ℎ‘((oc‘𝐾)‘𝑊)) = 𝑄) = (℩ℎ ∈ ((LTrn‘𝐾)‘𝑊)(ℎ‘((oc‘𝐾)‘𝑊)) = 𝑄) | |
16 | eqid 2738 | . 2 ⊢ (℩ℎ ∈ ((LTrn‘𝐾)‘𝑊)(ℎ‘((oc‘𝐾)‘𝑊)) = 𝑅) = (℩ℎ ∈ ((LTrn‘𝐾)‘𝑊)(ℎ‘((oc‘𝐾)‘𝑊)) = 𝑅) | |
17 | eqid 2738 | . 2 ⊢ (℩ℎ ∈ ((LTrn‘𝐾)‘𝑊)(ℎ‘𝑄) = 𝑅) = (℩ℎ ∈ ((LTrn‘𝐾)‘𝑊)(ℎ‘𝑄) = 𝑅) | |
18 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17 | cdlemn5pre 39200 | 1 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ 𝑅 ≤ (𝑄 ∨ 𝑋)) → (𝐽‘𝑅) ⊆ ((𝐽‘𝑄) ⊕ (𝐼‘𝑋))) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∧ wa 396 ∧ w3a 1086 = wceq 1539 ∈ wcel 2106 ⊆ wss 3887 class class class wbr 5074 ↦ cmpt 5157 I cid 5484 ↾ cres 5587 ‘cfv 6427 ℩crio 7224 (class class class)co 7268 Basecbs 16900 lecple 16957 occoc 16958 joincjn 18017 LSSumclsm 19227 LSpanclspn 20221 Atomscatm 37263 HLchlt 37350 LHypclh 37984 LTrncltrn 38101 TEndoctendo 38752 DVecHcdvh 39078 DIsoBcdib 39138 DIsoCcdic 39172 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2709 ax-rep 5209 ax-sep 5222 ax-nul 5229 ax-pow 5287 ax-pr 5351 ax-un 7579 ax-cnex 10915 ax-resscn 10916 ax-1cn 10917 ax-icn 10918 ax-addcl 10919 ax-addrcl 10920 ax-mulcl 10921 ax-mulrcl 10922 ax-mulcom 10923 ax-addass 10924 ax-mulass 10925 ax-distr 10926 ax-i2m1 10927 ax-1ne0 10928 ax-1rid 10929 ax-rnegex 10930 ax-rrecex 10931 ax-cnre 10932 ax-pre-lttri 10933 ax-pre-lttrn 10934 ax-pre-ltadd 10935 ax-pre-mulgt0 10936 ax-riotaBAD 36953 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3or 1087 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1783 df-nf 1787 df-sb 2068 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2816 df-nfc 2889 df-ne 2944 df-nel 3050 df-ral 3069 df-rex 3070 df-reu 3071 df-rmo 3072 df-rab 3073 df-v 3432 df-sbc 3717 df-csb 3833 df-dif 3890 df-un 3892 df-in 3894 df-ss 3904 df-pss 3906 df-nul 4258 df-if 4461 df-pw 4536 df-sn 4563 df-pr 4565 df-tp 4567 df-op 4569 df-uni 4841 df-int 4881 df-iun 4927 df-iin 4928 df-br 5075 df-opab 5137 df-mpt 5158 df-tr 5192 df-id 5485 df-eprel 5491 df-po 5499 df-so 5500 df-fr 5540 df-we 5542 df-xp 5591 df-rel 5592 df-cnv 5593 df-co 5594 df-dm 5595 df-rn 5596 df-res 5597 df-ima 5598 df-pred 6196 df-ord 6263 df-on 6264 df-lim 6265 df-suc 6266 df-iota 6385 df-fun 6429 df-fn 6430 df-f 6431 df-f1 6432 df-fo 6433 df-f1o 6434 df-fv 6435 df-riota 7225 df-ov 7271 df-oprab 7272 df-mpo 7273 df-om 7704 df-1st 7821 df-2nd 7822 df-tpos 8030 df-undef 8077 df-frecs 8085 df-wrecs 8116 df-recs 8190 df-rdg 8229 df-1o 8285 df-er 8486 df-map 8605 df-en 8722 df-dom 8723 df-sdom 8724 df-fin 8725 df-pnf 10999 df-mnf 11000 df-xr 11001 df-ltxr 11002 df-le 11003 df-sub 11195 df-neg 11196 df-nn 11962 df-2 12024 df-3 12025 df-4 12026 df-5 12027 df-6 12028 df-n0 12222 df-z 12308 df-uz 12571 df-fz 13228 df-struct 16836 df-sets 16853 df-slot 16871 df-ndx 16883 df-base 16901 df-ress 16930 df-plusg 16963 df-mulr 16964 df-sca 16966 df-vsca 16967 df-0g 17140 df-proset 18001 df-poset 18019 df-plt 18036 df-lub 18052 df-glb 18053 df-join 18054 df-meet 18055 df-p0 18131 df-p1 18132 df-lat 18138 df-clat 18205 df-mgm 18314 df-sgrp 18363 df-mnd 18374 df-submnd 18419 df-grp 18568 df-minusg 18569 df-sbg 18570 df-subg 18740 df-cntz 18911 df-lsm 19229 df-cmn 19376 df-abl 19377 df-mgp 19709 df-ur 19726 df-ring 19773 df-oppr 19850 df-dvdsr 19871 df-unit 19872 df-invr 19902 df-dvr 19913 df-drng 19981 df-lmod 20113 df-lss 20182 df-lsp 20222 df-lvec 20353 df-oposet 37176 df-ol 37178 df-oml 37179 df-covers 37266 df-ats 37267 df-atl 37298 df-cvlat 37322 df-hlat 37351 df-llines 37498 df-lplanes 37499 df-lvols 37500 df-lines 37501 df-psubsp 37503 df-pmap 37504 df-padd 37796 df-lhyp 37988 df-laut 37989 df-ldil 38104 df-ltrn 38105 df-trl 38159 df-tendo 38755 df-edring 38757 df-disoa 39029 df-dvech 39079 df-dib 39139 df-dic 39173 |
This theorem is referenced by: cdlemn 39212 dihord1 39218 |
Copyright terms: Public domain | W3C validator |