Mathbox for Norm Megill |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > Mathboxes > lclkrlem2a | Structured version Visualization version GIF version |
Description: Lemma for lclkr 39526. Use lshpat 37049 to show that the intersection of a hyperplane with a noncomparable sum of atoms is an atom. (Contributed by NM, 16-Jan-2015.) |
Ref | Expression |
---|---|
lclkrlem2a.h | ⊢ 𝐻 = (LHyp‘𝐾) |
lclkrlem2a.o | ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) |
lclkrlem2a.u | ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) |
lclkrlem2a.v | ⊢ 𝑉 = (Base‘𝑈) |
lclkrlem2a.z | ⊢ 0 = (0g‘𝑈) |
lclkrlem2a.p | ⊢ ⊕ = (LSSum‘𝑈) |
lclkrlem2a.n | ⊢ 𝑁 = (LSpan‘𝑈) |
lclkrlem2a.a | ⊢ 𝐴 = (LSAtoms‘𝑈) |
lclkrlem2a.k | ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
lclkrlem2a.b | ⊢ (𝜑 → 𝐵 ∈ (𝑉 ∖ { 0 })) |
lclkrlem2a.x | ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) |
lclkrlem2a.y | ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 })) |
lclkrlem2a.e | ⊢ (𝜑 → ( ⊥ ‘{𝑋}) ≠ ( ⊥ ‘{𝑌})) |
lclkrlem2a.d | ⊢ (𝜑 → ¬ 𝑋 ∈ ( ⊥ ‘{𝐵})) |
Ref | Expression |
---|---|
lclkrlem2a | ⊢ (𝜑 → (((𝑁‘{𝑋}) ⊕ (𝑁‘{𝑌})) ∩ ( ⊥ ‘{𝐵})) ∈ 𝐴) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqid 2739 | . 2 ⊢ (LSubSp‘𝑈) = (LSubSp‘𝑈) | |
2 | lclkrlem2a.p | . 2 ⊢ ⊕ = (LSSum‘𝑈) | |
3 | eqid 2739 | . 2 ⊢ (LSHyp‘𝑈) = (LSHyp‘𝑈) | |
4 | lclkrlem2a.a | . 2 ⊢ 𝐴 = (LSAtoms‘𝑈) | |
5 | lclkrlem2a.h | . . 3 ⊢ 𝐻 = (LHyp‘𝐾) | |
6 | lclkrlem2a.u | . . 3 ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) | |
7 | lclkrlem2a.k | . . 3 ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) | |
8 | 5, 6, 7 | dvhlvec 39102 | . 2 ⊢ (𝜑 → 𝑈 ∈ LVec) |
9 | lclkrlem2a.o | . . 3 ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) | |
10 | lclkrlem2a.v | . . 3 ⊢ 𝑉 = (Base‘𝑈) | |
11 | lclkrlem2a.z | . . 3 ⊢ 0 = (0g‘𝑈) | |
12 | lclkrlem2a.b | . . 3 ⊢ (𝜑 → 𝐵 ∈ (𝑉 ∖ { 0 })) | |
13 | 5, 9, 6, 10, 11, 3, 7, 12 | dochsnshp 39446 | . 2 ⊢ (𝜑 → ( ⊥ ‘{𝐵}) ∈ (LSHyp‘𝑈)) |
14 | lclkrlem2a.n | . . 3 ⊢ 𝑁 = (LSpan‘𝑈) | |
15 | 5, 6, 7 | dvhlmod 39103 | . . 3 ⊢ (𝜑 → 𝑈 ∈ LMod) |
16 | lclkrlem2a.x | . . 3 ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) | |
17 | 10, 14, 11, 4, 15, 16 | lsatlspsn 36986 | . 2 ⊢ (𝜑 → (𝑁‘{𝑋}) ∈ 𝐴) |
18 | lclkrlem2a.y | . . 3 ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 })) | |
19 | 10, 14, 11, 4, 15, 18 | lsatlspsn 36986 | . 2 ⊢ (𝜑 → (𝑁‘{𝑌}) ∈ 𝐴) |
20 | lclkrlem2a.e | . . 3 ⊢ (𝜑 → ( ⊥ ‘{𝑋}) ≠ ( ⊥ ‘{𝑌})) | |
21 | 16 | eldifad 3903 | . . . . . . . 8 ⊢ (𝜑 → 𝑋 ∈ 𝑉) |
22 | 21 | snssd 4747 | . . . . . . 7 ⊢ (𝜑 → {𝑋} ⊆ 𝑉) |
23 | 5, 6, 9, 10, 14, 7, 22 | dochocsp 39372 | . . . . . 6 ⊢ (𝜑 → ( ⊥ ‘(𝑁‘{𝑋})) = ( ⊥ ‘{𝑋})) |
24 | 18 | eldifad 3903 | . . . . . . . 8 ⊢ (𝜑 → 𝑌 ∈ 𝑉) |
25 | 24 | snssd 4747 | . . . . . . 7 ⊢ (𝜑 → {𝑌} ⊆ 𝑉) |
26 | 5, 6, 9, 10, 14, 7, 25 | dochocsp 39372 | . . . . . 6 ⊢ (𝜑 → ( ⊥ ‘(𝑁‘{𝑌})) = ( ⊥ ‘{𝑌})) |
27 | 23, 26 | eqeq12d 2755 | . . . . 5 ⊢ (𝜑 → (( ⊥ ‘(𝑁‘{𝑋})) = ( ⊥ ‘(𝑁‘{𝑌})) ↔ ( ⊥ ‘{𝑋}) = ( ⊥ ‘{𝑌}))) |
28 | eqid 2739 | . . . . . 6 ⊢ ((DIsoH‘𝐾)‘𝑊) = ((DIsoH‘𝐾)‘𝑊) | |
29 | 5, 6, 10, 14, 28 | dihlsprn 39324 | . . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝑉) → (𝑁‘{𝑋}) ∈ ran ((DIsoH‘𝐾)‘𝑊)) |
30 | 7, 21, 29 | syl2anc 583 | . . . . . 6 ⊢ (𝜑 → (𝑁‘{𝑋}) ∈ ran ((DIsoH‘𝐾)‘𝑊)) |
31 | 5, 6, 10, 14, 28 | dihlsprn 39324 | . . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑌 ∈ 𝑉) → (𝑁‘{𝑌}) ∈ ran ((DIsoH‘𝐾)‘𝑊)) |
32 | 7, 24, 31 | syl2anc 583 | . . . . . 6 ⊢ (𝜑 → (𝑁‘{𝑌}) ∈ ran ((DIsoH‘𝐾)‘𝑊)) |
33 | 5, 28, 9, 7, 30, 32 | doch11 39366 | . . . . 5 ⊢ (𝜑 → (( ⊥ ‘(𝑁‘{𝑋})) = ( ⊥ ‘(𝑁‘{𝑌})) ↔ (𝑁‘{𝑋}) = (𝑁‘{𝑌}))) |
34 | 27, 33 | bitr3d 280 | . . . 4 ⊢ (𝜑 → (( ⊥ ‘{𝑋}) = ( ⊥ ‘{𝑌}) ↔ (𝑁‘{𝑋}) = (𝑁‘{𝑌}))) |
35 | 34 | necon3bid 2989 | . . 3 ⊢ (𝜑 → (( ⊥ ‘{𝑋}) ≠ ( ⊥ ‘{𝑌}) ↔ (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌}))) |
36 | 20, 35 | mpbid 231 | . 2 ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌})) |
37 | lclkrlem2a.d | . . 3 ⊢ (𝜑 → ¬ 𝑋 ∈ ( ⊥ ‘{𝐵})) | |
38 | 12 | eldifad 3903 | . . . . . 6 ⊢ (𝜑 → 𝐵 ∈ 𝑉) |
39 | 38 | snssd 4747 | . . . . 5 ⊢ (𝜑 → {𝐵} ⊆ 𝑉) |
40 | 5, 6, 10, 1, 9 | dochlss 39347 | . . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ {𝐵} ⊆ 𝑉) → ( ⊥ ‘{𝐵}) ∈ (LSubSp‘𝑈)) |
41 | 7, 39, 40 | syl2anc 583 | . . . 4 ⊢ (𝜑 → ( ⊥ ‘{𝐵}) ∈ (LSubSp‘𝑈)) |
42 | 10, 1, 14, 15, 41, 21 | lspsnel5 20238 | . . 3 ⊢ (𝜑 → (𝑋 ∈ ( ⊥ ‘{𝐵}) ↔ (𝑁‘{𝑋}) ⊆ ( ⊥ ‘{𝐵}))) |
43 | 37, 42 | mtbid 323 | . 2 ⊢ (𝜑 → ¬ (𝑁‘{𝑋}) ⊆ ( ⊥ ‘{𝐵})) |
44 | 1, 2, 3, 4, 8, 13, 17, 19, 36, 43 | lshpat 37049 | 1 ⊢ (𝜑 → (((𝑁‘{𝑋}) ⊕ (𝑁‘{𝑌})) ∩ ( ⊥ ‘{𝐵})) ∈ 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∧ wa 395 = wceq 1541 ∈ wcel 2109 ≠ wne 2944 ∖ cdif 3888 ∩ cin 3890 ⊆ wss 3891 {csn 4566 ran crn 5589 ‘cfv 6430 (class class class)co 7268 Basecbs 16893 0gc0g 17131 LSSumclsm 19220 LSubSpclss 20174 LSpanclspn 20214 LSAtomsclsa 36967 LSHypclsh 36968 HLchlt 37343 LHypclh 37977 DVecHcdvh 39071 DIsoHcdih 39221 ocHcoch 39340 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1801 ax-4 1815 ax-5 1916 ax-6 1974 ax-7 2014 ax-8 2111 ax-9 2119 ax-10 2140 ax-11 2157 ax-12 2174 ax-ext 2710 ax-rep 5213 ax-sep 5226 ax-nul 5233 ax-pow 5291 ax-pr 5355 ax-un 7579 ax-cnex 10911 ax-resscn 10912 ax-1cn 10913 ax-icn 10914 ax-addcl 10915 ax-addrcl 10916 ax-mulcl 10917 ax-mulrcl 10918 ax-mulcom 10919 ax-addass 10920 ax-mulass 10921 ax-distr 10922 ax-i2m1 10923 ax-1ne0 10924 ax-1rid 10925 ax-rnegex 10926 ax-rrecex 10927 ax-cnre 10928 ax-pre-lttri 10929 ax-pre-lttrn 10930 ax-pre-ltadd 10931 ax-pre-mulgt0 10932 ax-riotaBAD 36946 |
This theorem depends on definitions: df-bi 206 df-an 396 df-or 844 df-3or 1086 df-3an 1087 df-tru 1544 df-fal 1554 df-ex 1786 df-nf 1790 df-sb 2071 df-mo 2541 df-eu 2570 df-clab 2717 df-cleq 2731 df-clel 2817 df-nfc 2890 df-ne 2945 df-nel 3051 df-ral 3070 df-rex 3071 df-reu 3072 df-rmo 3073 df-rab 3074 df-v 3432 df-sbc 3720 df-csb 3837 df-dif 3894 df-un 3896 df-in 3898 df-ss 3908 df-pss 3910 df-nul 4262 df-if 4465 df-pw 4540 df-sn 4567 df-pr 4569 df-tp 4571 df-op 4573 df-uni 4845 df-int 4885 df-iun 4931 df-iin 4932 df-br 5079 df-opab 5141 df-mpt 5162 df-tr 5196 df-id 5488 df-eprel 5494 df-po 5502 df-so 5503 df-fr 5543 df-we 5545 df-xp 5594 df-rel 5595 df-cnv 5596 df-co 5597 df-dm 5598 df-rn 5599 df-res 5600 df-ima 5601 df-pred 6199 df-ord 6266 df-on 6267 df-lim 6268 df-suc 6269 df-iota 6388 df-fun 6432 df-fn 6433 df-f 6434 df-f1 6435 df-fo 6436 df-f1o 6437 df-fv 6438 df-riota 7225 df-ov 7271 df-oprab 7272 df-mpo 7273 df-om 7701 df-1st 7817 df-2nd 7818 df-tpos 8026 df-undef 8073 df-frecs 8081 df-wrecs 8112 df-recs 8186 df-rdg 8225 df-1o 8281 df-er 8472 df-map 8591 df-en 8708 df-dom 8709 df-sdom 8710 df-fin 8711 df-pnf 10995 df-mnf 10996 df-xr 10997 df-ltxr 10998 df-le 10999 df-sub 11190 df-neg 11191 df-nn 11957 df-2 12019 df-3 12020 df-4 12021 df-5 12022 df-6 12023 df-n0 12217 df-z 12303 df-uz 12565 df-fz 13222 df-struct 16829 df-sets 16846 df-slot 16864 df-ndx 16876 df-base 16894 df-ress 16923 df-plusg 16956 df-mulr 16957 df-sca 16959 df-vsca 16960 df-0g 17133 df-mre 17276 df-mrc 17277 df-acs 17279 df-proset 17994 df-poset 18012 df-plt 18029 df-lub 18045 df-glb 18046 df-join 18047 df-meet 18048 df-p0 18124 df-p1 18125 df-lat 18131 df-clat 18198 df-mgm 18307 df-sgrp 18356 df-mnd 18367 df-submnd 18412 df-grp 18561 df-minusg 18562 df-sbg 18563 df-subg 18733 df-cntz 18904 df-oppg 18931 df-lsm 19222 df-cmn 19369 df-abl 19370 df-mgp 19702 df-ur 19719 df-ring 19766 df-oppr 19843 df-dvdsr 19864 df-unit 19865 df-invr 19895 df-dvr 19906 df-drng 19974 df-lmod 20106 df-lss 20175 df-lsp 20215 df-lvec 20346 df-lsatoms 36969 df-lshyp 36970 df-lcv 37012 df-oposet 37169 df-ol 37171 df-oml 37172 df-covers 37259 df-ats 37260 df-atl 37291 df-cvlat 37315 df-hlat 37344 df-llines 37491 df-lplanes 37492 df-lvols 37493 df-lines 37494 df-psubsp 37496 df-pmap 37497 df-padd 37789 df-lhyp 37981 df-laut 37982 df-ldil 38097 df-ltrn 38098 df-trl 38152 df-tgrp 38736 df-tendo 38748 df-edring 38750 df-dveca 38996 df-disoa 39022 df-dvech 39072 df-dib 39132 df-dic 39166 df-dih 39222 df-doch 39341 df-djh 39388 |
This theorem is referenced by: lclkrlem2b 39501 |
Copyright terms: Public domain | W3C validator |