![]() |
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 41529. 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 2733 | . . 3 ⊢ (LSAtoms‘𝑈) = (LSAtoms‘𝑈) | |
3 | lcfrlem38.h | . . . 4 ⊢ 𝐻 = (LHyp‘𝐾) | |
4 | lcfrlem38.u | . . . 4 ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) | |
5 | lcfrlem38.k | . . . 4 ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) | |
6 | 3, 4, 5 | dvhlmod 41054 | . . 3 ⊢ (𝜑 → 𝑈 ∈ LMod) |
7 | lcfrlem38.o | . . . 4 ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) | |
8 | eqid 2733 | . . . 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 41489 | . . . . 5 ⊢ (𝜑 → 𝑋 ∈ (Base‘𝑈)) |
18 | lcfrlem38.x | . . . . 5 ⊢ (𝜑 → 𝑋 ≠ 0 ) | |
19 | eldifsn 4793 | . . . . 5 ⊢ (𝑋 ∈ ((Base‘𝑈) ∖ { 0 }) ↔ (𝑋 ∈ (Base‘𝑈) ∧ 𝑋 ≠ 0 )) | |
20 | 17, 18, 19 | sylanbrc 582 | . . . 4 ⊢ (𝜑 → 𝑋 ∈ ((Base‘𝑈) ∖ { 0 })) |
21 | lcfrlem38.ye | . . . . . 6 ⊢ (𝜑 → 𝑌 ∈ 𝐸) | |
22 | 3, 7, 4, 8, 11, 12, 13, 14, 5, 15, 21 | lcfrlem4 41489 | . . . . 5 ⊢ (𝜑 → 𝑌 ∈ (Base‘𝑈)) |
23 | lcfrlem38.y | . . . . 5 ⊢ (𝜑 → 𝑌 ≠ 0 ) | |
24 | eldifsn 4793 | . . . . 5 ⊢ (𝑌 ∈ ((Base‘𝑈) ∖ { 0 }) ↔ (𝑌 ∈ (Base‘𝑈) ∧ 𝑌 ≠ 0 )) | |
25 | 22, 23, 24 | sylanbrc 582 | . . . 4 ⊢ (𝜑 → 𝑌 ∈ ((Base‘𝑈) ∖ { 0 })) |
26 | lcfrlem38.ne | . . . 4 ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌})) | |
27 | 3, 7, 4, 8, 9, 1, 10, 2, 5, 20, 25, 26 | lcfrlem21 41507 | . . 3 ⊢ (𝜑 → ((𝑁‘{𝑋, 𝑌}) ∩ ( ⊥ ‘{(𝑋 + 𝑌)})) ∈ (LSAtoms‘𝑈)) |
28 | 1, 2, 6, 27 | lsateln0 38938 | . 2 ⊢ (𝜑 → ∃𝑖 ∈ ((𝑁‘{𝑋, 𝑌}) ∩ ( ⊥ ‘{(𝑋 + 𝑌)}))𝑖 ≠ 0 ) |
29 | lcfrlem38.f | . . . 4 ⊢ 𝐹 = (LFnl‘𝑈) | |
30 | lcfrlem38.c | . . . 4 ⊢ 𝐶 = {𝑓 ∈ (LFnl‘𝑈) ∣ ( ⊥ ‘( ⊥ ‘(𝐿‘𝑓))) = (𝐿‘𝑓)} | |
31 | 5 | 3ad2ant1 1131 | . . . 4 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝑁‘{𝑋, 𝑌}) ∩ ( ⊥ ‘{(𝑋 + 𝑌)})) ∧ 𝑖 ≠ 0 ) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
32 | 15 | 3ad2ant1 1131 | . . . 4 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝑁‘{𝑋, 𝑌}) ∩ ( ⊥ ‘{(𝑋 + 𝑌)})) ∧ 𝑖 ≠ 0 ) → 𝐺 ∈ 𝑄) |
33 | lcfrlem38.gs | . . . . 5 ⊢ (𝜑 → 𝐺 ⊆ 𝐶) | |
34 | 33 | 3ad2ant1 1131 | . . . 4 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝑁‘{𝑋, 𝑌}) ∩ ( ⊥ ‘{(𝑋 + 𝑌)})) ∧ 𝑖 ≠ 0 ) → 𝐺 ⊆ 𝐶) |
35 | 16 | 3ad2ant1 1131 | . . . 4 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝑁‘{𝑋, 𝑌}) ∩ ( ⊥ ‘{(𝑋 + 𝑌)})) ∧ 𝑖 ≠ 0 ) → 𝑋 ∈ 𝐸) |
36 | 21 | 3ad2ant1 1131 | . . . 4 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝑁‘{𝑋, 𝑌}) ∩ ( ⊥ ‘{(𝑋 + 𝑌)})) ∧ 𝑖 ≠ 0 ) → 𝑌 ∈ 𝐸) |
37 | 18 | 3ad2ant1 1131 | . . . 4 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝑁‘{𝑋, 𝑌}) ∩ ( ⊥ ‘{(𝑋 + 𝑌)})) ∧ 𝑖 ≠ 0 ) → 𝑋 ≠ 0 ) |
38 | 23 | 3ad2ant1 1131 | . . . 4 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝑁‘{𝑋, 𝑌}) ∩ ( ⊥ ‘{(𝑋 + 𝑌)})) ∧ 𝑖 ≠ 0 ) → 𝑌 ≠ 0 ) |
39 | 26 | 3ad2ant1 1131 | . . . 4 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝑁‘{𝑋, 𝑌}) ∩ ( ⊥ ‘{(𝑋 + 𝑌)})) ∧ 𝑖 ≠ 0 ) → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌})) |
40 | eqid 2733 | . . . 4 ⊢ ((𝑁‘{𝑋, 𝑌}) ∩ ( ⊥ ‘{(𝑋 + 𝑌)})) = ((𝑁‘{𝑋, 𝑌}) ∩ ( ⊥ ‘{(𝑋 + 𝑌)})) | |
41 | simp2 1135 | . . . 4 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝑁‘{𝑋, 𝑌}) ∩ ( ⊥ ‘{(𝑋 + 𝑌)})) ∧ 𝑖 ≠ 0 ) → 𝑖 ∈ ((𝑁‘{𝑋, 𝑌}) ∩ ( ⊥ ‘{(𝑋 + 𝑌)}))) | |
42 | simp3 1136 | . . . 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 41525 | . . 3 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝑁‘{𝑋, 𝑌}) ∩ ( ⊥ ‘{(𝑋 + 𝑌)})) ∧ 𝑖 ≠ 0 ) → (𝑋 + 𝑌) ∈ 𝐸) |
44 | 43 | rexlimdv3a 3155 | . 2 ⊢ (𝜑 → (∃𝑖 ∈ ((𝑁‘{𝑋, 𝑌}) ∩ ( ⊥ ‘{(𝑋 + 𝑌)}))𝑖 ≠ 0 → (𝑋 + 𝑌) ∈ 𝐸)) |
45 | 28, 44 | mpd 15 | 1 ⊢ (𝜑 → (𝑋 + 𝑌) ∈ 𝐸) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 395 ∧ w3a 1085 = wceq 1535 ∈ wcel 2104 ≠ wne 2936 ∃wrex 3066 {crab 3432 ∖ cdif 3960 ∩ cin 3962 ⊆ wss 3963 {csn 4630 {cpr 4632 ∪ ciun 4998 ‘cfv 6558 (class class class)co 7425 Basecbs 17234 +gcplusg 17287 0gc0g 17475 LSubSpclss 20928 LSpanclspn 20968 LSAtomsclsa 38917 LFnlclfn 39000 LKerclk 39028 LDualcld 39066 HLchlt 39293 LHypclh 39928 DVecHcdvh 41022 ocHcoch 41291 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1963 ax-7 2003 ax-8 2106 ax-9 2114 ax-10 2137 ax-11 2153 ax-12 2173 ax-ext 2704 ax-rep 5286 ax-sep 5300 ax-nul 5307 ax-pow 5366 ax-pr 5430 ax-un 7747 ax-cnex 11202 ax-resscn 11203 ax-1cn 11204 ax-icn 11205 ax-addcl 11206 ax-addrcl 11207 ax-mulcl 11208 ax-mulrcl 11209 ax-mulcom 11210 ax-addass 11211 ax-mulass 11212 ax-distr 11213 ax-i2m1 11214 ax-1ne0 11215 ax-1rid 11216 ax-rnegex 11217 ax-rrecex 11218 ax-cnre 11219 ax-pre-lttri 11220 ax-pre-lttrn 11221 ax-pre-ltadd 11222 ax-pre-mulgt0 11223 ax-riotaBAD 38896 |
This theorem depends on definitions: df-bi 207 df-an 396 df-or 847 df-3or 1086 df-3an 1087 df-tru 1538 df-fal 1548 df-ex 1775 df-nf 1779 df-sb 2061 df-mo 2536 df-eu 2565 df-clab 2711 df-cleq 2725 df-clel 2812 df-nfc 2888 df-ne 2937 df-nel 3043 df-ral 3058 df-rex 3067 df-rmo 3376 df-reu 3377 df-rab 3433 df-v 3479 df-sbc 3792 df-csb 3909 df-dif 3966 df-un 3968 df-in 3970 df-ss 3980 df-pss 3983 df-nul 4340 df-if 4531 df-pw 4606 df-sn 4631 df-pr 4633 df-tp 4635 df-op 4637 df-uni 4915 df-int 4954 df-iun 5000 df-iin 5001 df-br 5150 df-opab 5212 df-mpt 5233 df-tr 5267 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 6317 df-ord 6383 df-on 6384 df-lim 6385 df-suc 6386 df-iota 6510 df-fun 6560 df-fn 6561 df-f 6562 df-f1 6563 df-fo 6564 df-f1o 6565 df-fv 6566 df-riota 7381 df-ov 7428 df-oprab 7429 df-mpo 7430 df-of 7691 df-om 7881 df-1st 8007 df-2nd 8008 df-tpos 8244 df-undef 8291 df-frecs 8299 df-wrecs 8330 df-recs 8404 df-rdg 8443 df-1o 8499 df-2o 8500 df-er 8738 df-map 8861 df-en 8979 df-dom 8980 df-sdom 8981 df-fin 8982 df-pnf 11288 df-mnf 11289 df-xr 11290 df-ltxr 11291 df-le 11292 df-sub 11485 df-neg 11486 df-nn 12258 df-2 12320 df-3 12321 df-4 12322 df-5 12323 df-6 12324 df-n0 12518 df-z 12605 df-uz 12870 df-fz 13538 df-struct 17170 df-sets 17187 df-slot 17205 df-ndx 17217 df-base 17235 df-ress 17264 df-plusg 17300 df-mulr 17301 df-sca 17303 df-vsca 17304 df-0g 17477 df-mre 17620 df-mrc 17621 df-acs 17623 df-proset 18341 df-poset 18359 df-plt 18376 df-lub 18392 df-glb 18393 df-join 18394 df-meet 18395 df-p0 18471 df-p1 18472 df-lat 18478 df-clat 18545 df-mgm 18654 df-sgrp 18733 df-mnd 18749 df-submnd 18795 df-grp 18952 df-minusg 18953 df-sbg 18954 df-subg 19139 df-cntz 19333 df-oppg 19362 df-lsm 19654 df-cmn 19800 df-abl 19801 df-mgp 20138 df-rng 20156 df-ur 20185 df-ring 20238 df-oppr 20336 df-dvdsr 20359 df-unit 20360 df-invr 20390 df-dvr 20403 df-nzr 20515 df-rlreg 20692 df-domn 20693 df-drng 20729 df-lmod 20858 df-lss 20929 df-lsp 20969 df-lvec 21101 df-lsatoms 38919 df-lshyp 38920 df-lcv 38962 df-lfl 39001 df-lkr 39029 df-ldual 39067 df-oposet 39119 df-ol 39121 df-oml 39122 df-covers 39209 df-ats 39210 df-atl 39241 df-cvlat 39265 df-hlat 39294 df-llines 39442 df-lplanes 39443 df-lvols 39444 df-lines 39445 df-psubsp 39447 df-pmap 39448 df-padd 39740 df-lhyp 39932 df-laut 39933 df-ldil 40048 df-ltrn 40049 df-trl 40103 df-tgrp 40687 df-tendo 40699 df-edring 40701 df-dveca 40947 df-disoa 40973 df-dvech 41023 df-dib 41083 df-dic 41117 df-dih 41173 df-doch 41292 df-djh 41339 |
This theorem is referenced by: lcfrlem41 41527 |
Copyright terms: Public domain | W3C validator |