| Mathbox for Norm Megill |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > Mathboxes > lcfrlem40 | Structured version Visualization version GIF version | ||
| Description: Lemma for lcfr 41565. Eliminate 𝐵 and 𝐼. (Contributed by NM, 11-Mar-2015.) |
| Ref | Expression |
|---|---|
| lcfrlem38.h | ⊢ 𝐻 = (LHyp‘𝐾) |
| lcfrlem38.o | ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) |
| lcfrlem38.u | ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) |
| lcfrlem38.p | ⊢ + = (+g‘𝑈) |
| lcfrlem38.f | ⊢ 𝐹 = (LFnl‘𝑈) |
| lcfrlem38.l | ⊢ 𝐿 = (LKer‘𝑈) |
| lcfrlem38.d | ⊢ 𝐷 = (LDual‘𝑈) |
| lcfrlem38.q | ⊢ 𝑄 = (LSubSp‘𝐷) |
| lcfrlem38.c | ⊢ 𝐶 = {𝑓 ∈ (LFnl‘𝑈) ∣ ( ⊥ ‘( ⊥ ‘(𝐿‘𝑓))) = (𝐿‘𝑓)} |
| lcfrlem38.e | ⊢ 𝐸 = ∪ 𝑔 ∈ 𝐺 ( ⊥ ‘(𝐿‘𝑔)) |
| lcfrlem38.k | ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
| lcfrlem38.g | ⊢ (𝜑 → 𝐺 ∈ 𝑄) |
| lcfrlem38.gs | ⊢ (𝜑 → 𝐺 ⊆ 𝐶) |
| lcfrlem38.xe | ⊢ (𝜑 → 𝑋 ∈ 𝐸) |
| lcfrlem38.ye | ⊢ (𝜑 → 𝑌 ∈ 𝐸) |
| lcfrlem38.z | ⊢ 0 = (0g‘𝑈) |
| lcfrlem38.x | ⊢ (𝜑 → 𝑋 ≠ 0 ) |
| lcfrlem38.y | ⊢ (𝜑 → 𝑌 ≠ 0 ) |
| lcfrlem38.sp | ⊢ 𝑁 = (LSpan‘𝑈) |
| lcfrlem38.ne | ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌})) |
| Ref | Expression |
|---|---|
| lcfrlem40 | ⊢ (𝜑 → (𝑋 + 𝑌) ∈ 𝐸) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | lcfrlem38.z | . . 3 ⊢ 0 = (0g‘𝑈) | |
| 2 | eqid 2736 | . . 3 ⊢ (LSAtoms‘𝑈) = (LSAtoms‘𝑈) | |
| 3 | lcfrlem38.h | . . . 4 ⊢ 𝐻 = (LHyp‘𝐾) | |
| 4 | lcfrlem38.u | . . . 4 ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) | |
| 5 | lcfrlem38.k | . . . 4 ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) | |
| 6 | 3, 4, 5 | dvhlmod 41090 | . . 3 ⊢ (𝜑 → 𝑈 ∈ LMod) |
| 7 | lcfrlem38.o | . . . 4 ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) | |
| 8 | eqid 2736 | . . . 4 ⊢ (Base‘𝑈) = (Base‘𝑈) | |
| 9 | lcfrlem38.p | . . . 4 ⊢ + = (+g‘𝑈) | |
| 10 | lcfrlem38.sp | . . . 4 ⊢ 𝑁 = (LSpan‘𝑈) | |
| 11 | lcfrlem38.l | . . . . . 6 ⊢ 𝐿 = (LKer‘𝑈) | |
| 12 | lcfrlem38.d | . . . . . 6 ⊢ 𝐷 = (LDual‘𝑈) | |
| 13 | lcfrlem38.q | . . . . . 6 ⊢ 𝑄 = (LSubSp‘𝐷) | |
| 14 | lcfrlem38.e | . . . . . 6 ⊢ 𝐸 = ∪ 𝑔 ∈ 𝐺 ( ⊥ ‘(𝐿‘𝑔)) | |
| 15 | lcfrlem38.g | . . . . . 6 ⊢ (𝜑 → 𝐺 ∈ 𝑄) | |
| 16 | lcfrlem38.xe | . . . . . 6 ⊢ (𝜑 → 𝑋 ∈ 𝐸) | |
| 17 | 3, 7, 4, 8, 11, 12, 13, 14, 5, 15, 16 | lcfrlem4 41525 | . . . . 5 ⊢ (𝜑 → 𝑋 ∈ (Base‘𝑈)) |
| 18 | lcfrlem38.x | . . . . 5 ⊢ (𝜑 → 𝑋 ≠ 0 ) | |
| 19 | eldifsn 4784 | . . . . 5 ⊢ (𝑋 ∈ ((Base‘𝑈) ∖ { 0 }) ↔ (𝑋 ∈ (Base‘𝑈) ∧ 𝑋 ≠ 0 )) | |
| 20 | 17, 18, 19 | sylanbrc 583 | . . . 4 ⊢ (𝜑 → 𝑋 ∈ ((Base‘𝑈) ∖ { 0 })) |
| 21 | lcfrlem38.ye | . . . . . 6 ⊢ (𝜑 → 𝑌 ∈ 𝐸) | |
| 22 | 3, 7, 4, 8, 11, 12, 13, 14, 5, 15, 21 | lcfrlem4 41525 | . . . . 5 ⊢ (𝜑 → 𝑌 ∈ (Base‘𝑈)) |
| 23 | lcfrlem38.y | . . . . 5 ⊢ (𝜑 → 𝑌 ≠ 0 ) | |
| 24 | eldifsn 4784 | . . . . 5 ⊢ (𝑌 ∈ ((Base‘𝑈) ∖ { 0 }) ↔ (𝑌 ∈ (Base‘𝑈) ∧ 𝑌 ≠ 0 )) | |
| 25 | 22, 23, 24 | sylanbrc 583 | . . . 4 ⊢ (𝜑 → 𝑌 ∈ ((Base‘𝑈) ∖ { 0 })) |
| 26 | lcfrlem38.ne | . . . 4 ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌})) | |
| 27 | 3, 7, 4, 8, 9, 1, 10, 2, 5, 20, 25, 26 | lcfrlem21 41543 | . . 3 ⊢ (𝜑 → ((𝑁‘{𝑋, 𝑌}) ∩ ( ⊥ ‘{(𝑋 + 𝑌)})) ∈ (LSAtoms‘𝑈)) |
| 28 | 1, 2, 6, 27 | lsateln0 38974 | . 2 ⊢ (𝜑 → ∃𝑖 ∈ ((𝑁‘{𝑋, 𝑌}) ∩ ( ⊥ ‘{(𝑋 + 𝑌)}))𝑖 ≠ 0 ) |
| 29 | lcfrlem38.f | . . . 4 ⊢ 𝐹 = (LFnl‘𝑈) | |
| 30 | lcfrlem38.c | . . . 4 ⊢ 𝐶 = {𝑓 ∈ (LFnl‘𝑈) ∣ ( ⊥ ‘( ⊥ ‘(𝐿‘𝑓))) = (𝐿‘𝑓)} | |
| 31 | 5 | 3ad2ant1 1134 | . . . 4 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝑁‘{𝑋, 𝑌}) ∩ ( ⊥ ‘{(𝑋 + 𝑌)})) ∧ 𝑖 ≠ 0 ) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
| 32 | 15 | 3ad2ant1 1134 | . . . 4 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝑁‘{𝑋, 𝑌}) ∩ ( ⊥ ‘{(𝑋 + 𝑌)})) ∧ 𝑖 ≠ 0 ) → 𝐺 ∈ 𝑄) |
| 33 | lcfrlem38.gs | . . . . 5 ⊢ (𝜑 → 𝐺 ⊆ 𝐶) | |
| 34 | 33 | 3ad2ant1 1134 | . . . 4 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝑁‘{𝑋, 𝑌}) ∩ ( ⊥ ‘{(𝑋 + 𝑌)})) ∧ 𝑖 ≠ 0 ) → 𝐺 ⊆ 𝐶) |
| 35 | 16 | 3ad2ant1 1134 | . . . 4 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝑁‘{𝑋, 𝑌}) ∩ ( ⊥ ‘{(𝑋 + 𝑌)})) ∧ 𝑖 ≠ 0 ) → 𝑋 ∈ 𝐸) |
| 36 | 21 | 3ad2ant1 1134 | . . . 4 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝑁‘{𝑋, 𝑌}) ∩ ( ⊥ ‘{(𝑋 + 𝑌)})) ∧ 𝑖 ≠ 0 ) → 𝑌 ∈ 𝐸) |
| 37 | 18 | 3ad2ant1 1134 | . . . 4 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝑁‘{𝑋, 𝑌}) ∩ ( ⊥ ‘{(𝑋 + 𝑌)})) ∧ 𝑖 ≠ 0 ) → 𝑋 ≠ 0 ) |
| 38 | 23 | 3ad2ant1 1134 | . . . 4 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝑁‘{𝑋, 𝑌}) ∩ ( ⊥ ‘{(𝑋 + 𝑌)})) ∧ 𝑖 ≠ 0 ) → 𝑌 ≠ 0 ) |
| 39 | 26 | 3ad2ant1 1134 | . . . 4 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝑁‘{𝑋, 𝑌}) ∩ ( ⊥ ‘{(𝑋 + 𝑌)})) ∧ 𝑖 ≠ 0 ) → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌})) |
| 40 | eqid 2736 | . . . 4 ⊢ ((𝑁‘{𝑋, 𝑌}) ∩ ( ⊥ ‘{(𝑋 + 𝑌)})) = ((𝑁‘{𝑋, 𝑌}) ∩ ( ⊥ ‘{(𝑋 + 𝑌)})) | |
| 41 | simp2 1138 | . . . 4 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝑁‘{𝑋, 𝑌}) ∩ ( ⊥ ‘{(𝑋 + 𝑌)})) ∧ 𝑖 ≠ 0 ) → 𝑖 ∈ ((𝑁‘{𝑋, 𝑌}) ∩ ( ⊥ ‘{(𝑋 + 𝑌)}))) | |
| 42 | simp3 1139 | . . . 4 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝑁‘{𝑋, 𝑌}) ∩ ( ⊥ ‘{(𝑋 + 𝑌)})) ∧ 𝑖 ≠ 0 ) → 𝑖 ≠ 0 ) | |
| 43 | 3, 7, 4, 9, 29, 11, 12, 13, 30, 14, 31, 32, 34, 35, 36, 1, 37, 38, 10, 39, 40, 41, 42 | lcfrlem39 41561 | . . 3 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝑁‘{𝑋, 𝑌}) ∩ ( ⊥ ‘{(𝑋 + 𝑌)})) ∧ 𝑖 ≠ 0 ) → (𝑋 + 𝑌) ∈ 𝐸) |
| 44 | 43 | rexlimdv3a 3158 | . 2 ⊢ (𝜑 → (∃𝑖 ∈ ((𝑁‘{𝑋, 𝑌}) ∩ ( ⊥ ‘{(𝑋 + 𝑌)}))𝑖 ≠ 0 → (𝑋 + 𝑌) ∈ 𝐸)) |
| 45 | 28, 44 | mpd 15 | 1 ⊢ (𝜑 → (𝑋 + 𝑌) ∈ 𝐸) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 395 ∧ w3a 1087 = wceq 1540 ∈ wcel 2108 ≠ wne 2939 ∃wrex 3069 {crab 3435 ∖ cdif 3947 ∩ cin 3949 ⊆ wss 3950 {csn 4624 {cpr 4626 ∪ ciun 4989 ‘cfv 6559 (class class class)co 7429 Basecbs 17243 +gcplusg 17293 0gc0g 17480 LSubSpclss 20921 LSpanclspn 20961 LSAtomsclsa 38953 LFnlclfn 39036 LKerclk 39064 LDualcld 39102 HLchlt 39329 LHypclh 39964 DVecHcdvh 41058 ocHcoch 41327 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2157 ax-12 2177 ax-ext 2707 ax-rep 5277 ax-sep 5294 ax-nul 5304 ax-pow 5363 ax-pr 5430 ax-un 7751 ax-cnex 11207 ax-resscn 11208 ax-1cn 11209 ax-icn 11210 ax-addcl 11211 ax-addrcl 11212 ax-mulcl 11213 ax-mulrcl 11214 ax-mulcom 11215 ax-addass 11216 ax-mulass 11217 ax-distr 11218 ax-i2m1 11219 ax-1ne0 11220 ax-1rid 11221 ax-rnegex 11222 ax-rrecex 11223 ax-cnre 11224 ax-pre-lttri 11225 ax-pre-lttrn 11226 ax-pre-ltadd 11227 ax-pre-mulgt0 11228 ax-riotaBAD 38932 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2065 df-mo 2539 df-eu 2568 df-clab 2714 df-cleq 2728 df-clel 2815 df-nfc 2891 df-ne 2940 df-nel 3046 df-ral 3061 df-rex 3070 df-rmo 3379 df-reu 3380 df-rab 3436 df-v 3481 df-sbc 3788 df-csb 3899 df-dif 3953 df-un 3955 df-in 3957 df-ss 3967 df-pss 3970 df-nul 4333 df-if 4525 df-pw 4600 df-sn 4625 df-pr 4627 df-tp 4629 df-op 4631 df-uni 4906 df-int 4945 df-iun 4991 df-iin 4992 df-br 5142 df-opab 5204 df-mpt 5224 df-tr 5258 df-id 5576 df-eprel 5582 df-po 5590 df-so 5591 df-fr 5635 df-we 5637 df-xp 5689 df-rel 5690 df-cnv 5691 df-co 5692 df-dm 5693 df-rn 5694 df-res 5695 df-ima 5696 df-pred 6319 df-ord 6385 df-on 6386 df-lim 6387 df-suc 6388 df-iota 6512 df-fun 6561 df-fn 6562 df-f 6563 df-f1 6564 df-fo 6565 df-f1o 6566 df-fv 6567 df-riota 7386 df-ov 7432 df-oprab 7433 df-mpo 7434 df-of 7694 df-om 7884 df-1st 8010 df-2nd 8011 df-tpos 8247 df-undef 8294 df-frecs 8302 df-wrecs 8333 df-recs 8407 df-rdg 8446 df-1o 8502 df-2o 8503 df-er 8741 df-map 8864 df-en 8982 df-dom 8983 df-sdom 8984 df-fin 8985 df-pnf 11293 df-mnf 11294 df-xr 11295 df-ltxr 11296 df-le 11297 df-sub 11490 df-neg 11491 df-nn 12263 df-2 12325 df-3 12326 df-4 12327 df-5 12328 df-6 12329 df-n0 12523 df-z 12610 df-uz 12875 df-fz 13544 df-struct 17180 df-sets 17197 df-slot 17215 df-ndx 17227 df-base 17244 df-ress 17271 df-plusg 17306 df-mulr 17307 df-sca 17309 df-vsca 17310 df-0g 17482 df-mre 17625 df-mrc 17626 df-acs 17628 df-proset 18336 df-poset 18355 df-plt 18371 df-lub 18387 df-glb 18388 df-join 18389 df-meet 18390 df-p0 18466 df-p1 18467 df-lat 18473 df-clat 18540 df-mgm 18649 df-sgrp 18728 df-mnd 18744 df-submnd 18793 df-grp 18950 df-minusg 18951 df-sbg 18952 df-subg 19137 df-cntz 19331 df-oppg 19360 df-lsm 19650 df-cmn 19796 df-abl 19797 df-mgp 20134 df-rng 20146 df-ur 20175 df-ring 20228 df-oppr 20326 df-dvdsr 20349 df-unit 20350 df-invr 20380 df-dvr 20393 df-nzr 20505 df-rlreg 20686 df-domn 20687 df-drng 20723 df-lmod 20852 df-lss 20922 df-lsp 20962 df-lvec 21094 df-lsatoms 38955 df-lshyp 38956 df-lcv 38998 df-lfl 39037 df-lkr 39065 df-ldual 39103 df-oposet 39155 df-ol 39157 df-oml 39158 df-covers 39245 df-ats 39246 df-atl 39277 df-cvlat 39301 df-hlat 39330 df-llines 39478 df-lplanes 39479 df-lvols 39480 df-lines 39481 df-psubsp 39483 df-pmap 39484 df-padd 39776 df-lhyp 39968 df-laut 39969 df-ldil 40084 df-ltrn 40085 df-trl 40139 df-tgrp 40723 df-tendo 40735 df-edring 40737 df-dveca 40983 df-disoa 41009 df-dvech 41059 df-dib 41119 df-dic 41153 df-dih 41209 df-doch 41328 df-djh 41375 |
| This theorem is referenced by: lcfrlem41 41563 |
| Copyright terms: Public domain | W3C validator |