![]() |
Mathbox for Norm Megill |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > dochexmidlem7 | Structured version Visualization version GIF version |
Description: Lemma for dochexmid 38160. Contradict dochexmidlem6 38157. (Contributed by NM, 15-Jan-2015.) |
Ref | Expression |
---|---|
dochexmidlem1.h | ⊢ 𝐻 = (LHyp‘𝐾) |
dochexmidlem1.o | ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) |
dochexmidlem1.u | ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) |
dochexmidlem1.v | ⊢ 𝑉 = (Base‘𝑈) |
dochexmidlem1.s | ⊢ 𝑆 = (LSubSp‘𝑈) |
dochexmidlem1.n | ⊢ 𝑁 = (LSpan‘𝑈) |
dochexmidlem1.p | ⊢ ⊕ = (LSSum‘𝑈) |
dochexmidlem1.a | ⊢ 𝐴 = (LSAtoms‘𝑈) |
dochexmidlem1.k | ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
dochexmidlem1.x | ⊢ (𝜑 → 𝑋 ∈ 𝑆) |
dochexmidlem6.pp | ⊢ (𝜑 → 𝑝 ∈ 𝐴) |
dochexmidlem6.z | ⊢ 0 = (0g‘𝑈) |
dochexmidlem6.m | ⊢ 𝑀 = (𝑋 ⊕ 𝑝) |
dochexmidlem6.xn | ⊢ (𝜑 → 𝑋 ≠ { 0 }) |
dochexmidlem6.c | ⊢ (𝜑 → ( ⊥ ‘( ⊥ ‘𝑋)) = 𝑋) |
dochexmidlem6.pl | ⊢ (𝜑 → ¬ 𝑝 ⊆ (𝑋 ⊕ ( ⊥ ‘𝑋))) |
Ref | Expression |
---|---|
dochexmidlem7 | ⊢ (𝜑 → 𝑀 ≠ 𝑋) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dochexmidlem1.h | . . . . . . 7 ⊢ 𝐻 = (LHyp‘𝐾) | |
2 | dochexmidlem1.u | . . . . . . 7 ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) | |
3 | dochexmidlem1.k | . . . . . . 7 ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) | |
4 | 1, 2, 3 | dvhlmod 37802 | . . . . . 6 ⊢ (𝜑 → 𝑈 ∈ LMod) |
5 | dochexmidlem1.s | . . . . . . 7 ⊢ 𝑆 = (LSubSp‘𝑈) | |
6 | 5 | lsssssubg 19425 | . . . . . 6 ⊢ (𝑈 ∈ LMod → 𝑆 ⊆ (SubGrp‘𝑈)) |
7 | 4, 6 | syl 17 | . . . . 5 ⊢ (𝜑 → 𝑆 ⊆ (SubGrp‘𝑈)) |
8 | dochexmidlem1.x | . . . . 5 ⊢ (𝜑 → 𝑋 ∈ 𝑆) | |
9 | 7, 8 | sseldd 3894 | . . . 4 ⊢ (𝜑 → 𝑋 ∈ (SubGrp‘𝑈)) |
10 | dochexmidlem1.a | . . . . . 6 ⊢ 𝐴 = (LSAtoms‘𝑈) | |
11 | dochexmidlem6.pp | . . . . . 6 ⊢ (𝜑 → 𝑝 ∈ 𝐴) | |
12 | 5, 10, 4, 11 | lsatlssel 35689 | . . . . 5 ⊢ (𝜑 → 𝑝 ∈ 𝑆) |
13 | 7, 12 | sseldd 3894 | . . . 4 ⊢ (𝜑 → 𝑝 ∈ (SubGrp‘𝑈)) |
14 | dochexmidlem1.p | . . . . 5 ⊢ ⊕ = (LSSum‘𝑈) | |
15 | 14 | lsmub2 18517 | . . . 4 ⊢ ((𝑋 ∈ (SubGrp‘𝑈) ∧ 𝑝 ∈ (SubGrp‘𝑈)) → 𝑝 ⊆ (𝑋 ⊕ 𝑝)) |
16 | 9, 13, 15 | syl2anc 584 | . . 3 ⊢ (𝜑 → 𝑝 ⊆ (𝑋 ⊕ 𝑝)) |
17 | dochexmidlem6.m | . . 3 ⊢ 𝑀 = (𝑋 ⊕ 𝑝) | |
18 | 16, 17 | syl6sseqr 3943 | . 2 ⊢ (𝜑 → 𝑝 ⊆ 𝑀) |
19 | dochexmidlem6.pl | . . 3 ⊢ (𝜑 → ¬ 𝑝 ⊆ (𝑋 ⊕ ( ⊥ ‘𝑋))) | |
20 | dochexmidlem1.v | . . . . . . . . 9 ⊢ 𝑉 = (Base‘𝑈) | |
21 | 20, 5 | lssss 19403 | . . . . . . . 8 ⊢ (𝑋 ∈ 𝑆 → 𝑋 ⊆ 𝑉) |
22 | 8, 21 | syl 17 | . . . . . . 7 ⊢ (𝜑 → 𝑋 ⊆ 𝑉) |
23 | dochexmidlem1.o | . . . . . . . 8 ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) | |
24 | 1, 2, 20, 5, 23 | dochlss 38046 | . . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ⊆ 𝑉) → ( ⊥ ‘𝑋) ∈ 𝑆) |
25 | 3, 22, 24 | syl2anc 584 | . . . . . 6 ⊢ (𝜑 → ( ⊥ ‘𝑋) ∈ 𝑆) |
26 | 7, 25 | sseldd 3894 | . . . . 5 ⊢ (𝜑 → ( ⊥ ‘𝑋) ∈ (SubGrp‘𝑈)) |
27 | 14 | lsmub1 18516 | . . . . 5 ⊢ ((𝑋 ∈ (SubGrp‘𝑈) ∧ ( ⊥ ‘𝑋) ∈ (SubGrp‘𝑈)) → 𝑋 ⊆ (𝑋 ⊕ ( ⊥ ‘𝑋))) |
28 | 9, 26, 27 | syl2anc 584 | . . . 4 ⊢ (𝜑 → 𝑋 ⊆ (𝑋 ⊕ ( ⊥ ‘𝑋))) |
29 | sstr2 3900 | . . . 4 ⊢ (𝑝 ⊆ 𝑋 → (𝑋 ⊆ (𝑋 ⊕ ( ⊥ ‘𝑋)) → 𝑝 ⊆ (𝑋 ⊕ ( ⊥ ‘𝑋)))) | |
30 | 28, 29 | syl5com 31 | . . 3 ⊢ (𝜑 → (𝑝 ⊆ 𝑋 → 𝑝 ⊆ (𝑋 ⊕ ( ⊥ ‘𝑋)))) |
31 | 19, 30 | mtod 199 | . 2 ⊢ (𝜑 → ¬ 𝑝 ⊆ 𝑋) |
32 | sseq2 3918 | . . . 4 ⊢ (𝑀 = 𝑋 → (𝑝 ⊆ 𝑀 ↔ 𝑝 ⊆ 𝑋)) | |
33 | 32 | biimpcd 250 | . . 3 ⊢ (𝑝 ⊆ 𝑀 → (𝑀 = 𝑋 → 𝑝 ⊆ 𝑋)) |
34 | 33 | necon3bd 2998 | . 2 ⊢ (𝑝 ⊆ 𝑀 → (¬ 𝑝 ⊆ 𝑋 → 𝑀 ≠ 𝑋)) |
35 | 18, 31, 34 | sylc 65 | 1 ⊢ (𝜑 → 𝑀 ≠ 𝑋) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∧ wa 396 = wceq 1522 ∈ wcel 2081 ≠ wne 2984 ⊆ wss 3863 {csn 4476 ‘cfv 6230 (class class class)co 7021 Basecbs 16317 0gc0g 16547 SubGrpcsubg 18032 LSSumclsm 18494 LModclmod 19329 LSubSpclss 19398 LSpanclspn 19438 LSAtomsclsa 35666 HLchlt 36042 LHypclh 36676 DVecHcdvh 37770 ocHcoch 38039 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1777 ax-4 1791 ax-5 1888 ax-6 1947 ax-7 1992 ax-8 2083 ax-9 2091 ax-10 2112 ax-11 2126 ax-12 2141 ax-13 2344 ax-ext 2769 ax-rep 5086 ax-sep 5099 ax-nul 5106 ax-pow 5162 ax-pr 5226 ax-un 7324 ax-cnex 10444 ax-resscn 10445 ax-1cn 10446 ax-icn 10447 ax-addcl 10448 ax-addrcl 10449 ax-mulcl 10450 ax-mulrcl 10451 ax-mulcom 10452 ax-addass 10453 ax-mulass 10454 ax-distr 10455 ax-i2m1 10456 ax-1ne0 10457 ax-1rid 10458 ax-rnegex 10459 ax-rrecex 10460 ax-cnre 10461 ax-pre-lttri 10462 ax-pre-lttrn 10463 ax-pre-ltadd 10464 ax-pre-mulgt0 10465 ax-riotaBAD 35645 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-3or 1081 df-3an 1082 df-tru 1525 df-fal 1535 df-ex 1762 df-nf 1766 df-sb 2043 df-mo 2576 df-eu 2612 df-clab 2776 df-cleq 2788 df-clel 2863 df-nfc 2935 df-ne 2985 df-nel 3091 df-ral 3110 df-rex 3111 df-reu 3112 df-rmo 3113 df-rab 3114 df-v 3439 df-sbc 3710 df-csb 3816 df-dif 3866 df-un 3868 df-in 3870 df-ss 3878 df-pss 3880 df-nul 4216 df-if 4386 df-pw 4459 df-sn 4477 df-pr 4479 df-tp 4481 df-op 4483 df-uni 4750 df-int 4787 df-iun 4831 df-iin 4832 df-br 4967 df-opab 5029 df-mpt 5046 df-tr 5069 df-id 5353 df-eprel 5358 df-po 5367 df-so 5368 df-fr 5407 df-we 5409 df-xp 5454 df-rel 5455 df-cnv 5456 df-co 5457 df-dm 5458 df-rn 5459 df-res 5460 df-ima 5461 df-pred 6028 df-ord 6074 df-on 6075 df-lim 6076 df-suc 6077 df-iota 6194 df-fun 6232 df-fn 6233 df-f 6234 df-f1 6235 df-fo 6236 df-f1o 6237 df-fv 6238 df-riota 6982 df-ov 7024 df-oprab 7025 df-mpo 7026 df-om 7442 df-1st 7550 df-2nd 7551 df-tpos 7748 df-undef 7795 df-wrecs 7803 df-recs 7865 df-rdg 7903 df-1o 7958 df-oadd 7962 df-er 8144 df-map 8263 df-en 8363 df-dom 8364 df-sdom 8365 df-fin 8366 df-pnf 10528 df-mnf 10529 df-xr 10530 df-ltxr 10531 df-le 10532 df-sub 10724 df-neg 10725 df-nn 11492 df-2 11553 df-3 11554 df-4 11555 df-5 11556 df-6 11557 df-n0 11751 df-z 11835 df-uz 12099 df-fz 12748 df-struct 16319 df-ndx 16320 df-slot 16321 df-base 16323 df-sets 16324 df-ress 16325 df-plusg 16412 df-mulr 16413 df-sca 16415 df-vsca 16416 df-0g 16549 df-proset 17372 df-poset 17390 df-plt 17402 df-lub 17418 df-glb 17419 df-join 17420 df-meet 17421 df-p0 17483 df-p1 17484 df-lat 17490 df-clat 17552 df-mgm 17686 df-sgrp 17728 df-mnd 17739 df-submnd 17780 df-grp 17869 df-minusg 17870 df-sbg 17871 df-subg 18035 df-cntz 18193 df-lsm 18496 df-cmn 18640 df-abl 18641 df-mgp 18935 df-ur 18947 df-ring 18994 df-oppr 19068 df-dvdsr 19086 df-unit 19087 df-invr 19117 df-dvr 19128 df-drng 19199 df-lmod 19331 df-lss 19399 df-lsp 19439 df-lvec 19570 df-lsatoms 35668 df-oposet 35868 df-ol 35870 df-oml 35871 df-covers 35958 df-ats 35959 df-atl 35990 df-cvlat 36014 df-hlat 36043 df-llines 36190 df-lplanes 36191 df-lvols 36192 df-lines 36193 df-psubsp 36195 df-pmap 36196 df-padd 36488 df-lhyp 36680 df-laut 36681 df-ldil 36796 df-ltrn 36797 df-trl 36851 df-tendo 37447 df-edring 37449 df-disoa 37721 df-dvech 37771 df-dib 37831 df-dic 37865 df-dih 37921 df-doch 38040 |
This theorem is referenced by: dochexmidlem8 38159 |
Copyright terms: Public domain | W3C validator |