![]() |
Mathbox for Norm Megill |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > dochfl1 | Structured version Visualization version GIF version |
Description: The value of the explicit functional 𝐺 is 1 at the 𝑋 that determines it. (Contributed by NM, 27-Oct-2014.) |
Ref | Expression |
---|---|
dochfl1.h | ⊢ 𝐻 = (LHyp‘𝐾) |
dochfl1.o | ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) |
dochfl1.u | ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) |
dochfl1.v | ⊢ 𝑉 = (Base‘𝑈) |
dochfl1.a | ⊢ + = (+g‘𝑈) |
dochfl1.t | ⊢ · = ( ·𝑠 ‘𝑈) |
dochfl1.z | ⊢ 0 = (0g‘𝑈) |
dochfl1.d | ⊢ 𝐷 = (Scalar‘𝑈) |
dochfl1.r | ⊢ 𝑅 = (Base‘𝐷) |
dochfl1.i | ⊢ 1 = (1r‘𝐷) |
dochfl1.k | ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
dochfl1.x | ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) |
dochfl1.g | ⊢ 𝐺 = (𝑣 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝑅 ∃𝑤 ∈ ( ⊥ ‘{𝑋})𝑣 = (𝑤 + (𝑘 · 𝑋)))) |
Ref | Expression |
---|---|
dochfl1 | ⊢ (𝜑 → (𝐺‘𝑋) = 1 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dochfl1.x | . . . 4 ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) | |
2 | 1 | eldifad 3835 | . . 3 ⊢ (𝜑 → 𝑋 ∈ 𝑉) |
3 | eqeq1 2776 | . . . . . 6 ⊢ (𝑣 = 𝑋 → (𝑣 = (𝑤 + (𝑘 · 𝑋)) ↔ 𝑋 = (𝑤 + (𝑘 · 𝑋)))) | |
4 | 3 | rexbidv 3236 | . . . . 5 ⊢ (𝑣 = 𝑋 → (∃𝑤 ∈ ( ⊥ ‘{𝑋})𝑣 = (𝑤 + (𝑘 · 𝑋)) ↔ ∃𝑤 ∈ ( ⊥ ‘{𝑋})𝑋 = (𝑤 + (𝑘 · 𝑋)))) |
5 | 4 | riotabidv 6933 | . . . 4 ⊢ (𝑣 = 𝑋 → (℩𝑘 ∈ 𝑅 ∃𝑤 ∈ ( ⊥ ‘{𝑋})𝑣 = (𝑤 + (𝑘 · 𝑋))) = (℩𝑘 ∈ 𝑅 ∃𝑤 ∈ ( ⊥ ‘{𝑋})𝑋 = (𝑤 + (𝑘 · 𝑋)))) |
6 | dochfl1.g | . . . 4 ⊢ 𝐺 = (𝑣 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝑅 ∃𝑤 ∈ ( ⊥ ‘{𝑋})𝑣 = (𝑤 + (𝑘 · 𝑋)))) | |
7 | riotaex 6935 | . . . 4 ⊢ (℩𝑘 ∈ 𝑅 ∃𝑤 ∈ ( ⊥ ‘{𝑋})𝑋 = (𝑤 + (𝑘 · 𝑋))) ∈ V | |
8 | 5, 6, 7 | fvmpt 6589 | . . 3 ⊢ (𝑋 ∈ 𝑉 → (𝐺‘𝑋) = (℩𝑘 ∈ 𝑅 ∃𝑤 ∈ ( ⊥ ‘{𝑋})𝑋 = (𝑤 + (𝑘 · 𝑋)))) |
9 | 2, 8 | syl 17 | . 2 ⊢ (𝜑 → (𝐺‘𝑋) = (℩𝑘 ∈ 𝑅 ∃𝑤 ∈ ( ⊥ ‘{𝑋})𝑋 = (𝑤 + (𝑘 · 𝑋)))) |
10 | dochfl1.h | . . . . . 6 ⊢ 𝐻 = (LHyp‘𝐾) | |
11 | dochfl1.u | . . . . . 6 ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) | |
12 | dochfl1.k | . . . . . 6 ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) | |
13 | 10, 11, 12 | dvhlmod 37691 | . . . . 5 ⊢ (𝜑 → 𝑈 ∈ LMod) |
14 | 2 | snssd 4610 | . . . . . 6 ⊢ (𝜑 → {𝑋} ⊆ 𝑉) |
15 | dochfl1.v | . . . . . . 7 ⊢ 𝑉 = (Base‘𝑈) | |
16 | eqid 2772 | . . . . . . 7 ⊢ (LSubSp‘𝑈) = (LSubSp‘𝑈) | |
17 | dochfl1.o | . . . . . . 7 ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) | |
18 | 10, 11, 15, 16, 17 | dochlss 37935 | . . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ {𝑋} ⊆ 𝑉) → ( ⊥ ‘{𝑋}) ∈ (LSubSp‘𝑈)) |
19 | 12, 14, 18 | syl2anc 576 | . . . . 5 ⊢ (𝜑 → ( ⊥ ‘{𝑋}) ∈ (LSubSp‘𝑈)) |
20 | dochfl1.z | . . . . . 6 ⊢ 0 = (0g‘𝑈) | |
21 | 20, 16 | lss0cl 19434 | . . . . 5 ⊢ ((𝑈 ∈ LMod ∧ ( ⊥ ‘{𝑋}) ∈ (LSubSp‘𝑈)) → 0 ∈ ( ⊥ ‘{𝑋})) |
22 | 13, 19, 21 | syl2anc 576 | . . . 4 ⊢ (𝜑 → 0 ∈ ( ⊥ ‘{𝑋})) |
23 | dochfl1.d | . . . . . . . 8 ⊢ 𝐷 = (Scalar‘𝑈) | |
24 | dochfl1.t | . . . . . . . 8 ⊢ · = ( ·𝑠 ‘𝑈) | |
25 | dochfl1.i | . . . . . . . 8 ⊢ 1 = (1r‘𝐷) | |
26 | 15, 23, 24, 25 | lmodvs1 19378 | . . . . . . 7 ⊢ ((𝑈 ∈ LMod ∧ 𝑋 ∈ 𝑉) → ( 1 · 𝑋) = 𝑋) |
27 | 13, 2, 26 | syl2anc 576 | . . . . . 6 ⊢ (𝜑 → ( 1 · 𝑋) = 𝑋) |
28 | 27 | oveq2d 6986 | . . . . 5 ⊢ (𝜑 → ( 0 + ( 1 · 𝑋)) = ( 0 + 𝑋)) |
29 | dochfl1.a | . . . . . . 7 ⊢ + = (+g‘𝑈) | |
30 | 15, 29, 20 | lmod0vlid 19380 | . . . . . 6 ⊢ ((𝑈 ∈ LMod ∧ 𝑋 ∈ 𝑉) → ( 0 + 𝑋) = 𝑋) |
31 | 13, 2, 30 | syl2anc 576 | . . . . 5 ⊢ (𝜑 → ( 0 + 𝑋) = 𝑋) |
32 | 28, 31 | eqtr2d 2809 | . . . 4 ⊢ (𝜑 → 𝑋 = ( 0 + ( 1 · 𝑋))) |
33 | oveq1 6977 | . . . . 5 ⊢ (𝑤 = 0 → (𝑤 + ( 1 · 𝑋)) = ( 0 + ( 1 · 𝑋))) | |
34 | 33 | rspceeqv 3547 | . . . 4 ⊢ (( 0 ∈ ( ⊥ ‘{𝑋}) ∧ 𝑋 = ( 0 + ( 1 · 𝑋))) → ∃𝑤 ∈ ( ⊥ ‘{𝑋})𝑋 = (𝑤 + ( 1 · 𝑋))) |
35 | 22, 32, 34 | syl2anc 576 | . . 3 ⊢ (𝜑 → ∃𝑤 ∈ ( ⊥ ‘{𝑋})𝑋 = (𝑤 + ( 1 · 𝑋))) |
36 | 23 | lmodring 19358 | . . . . 5 ⊢ (𝑈 ∈ LMod → 𝐷 ∈ Ring) |
37 | dochfl1.r | . . . . . 6 ⊢ 𝑅 = (Base‘𝐷) | |
38 | 37, 25 | ringidcl 19035 | . . . . 5 ⊢ (𝐷 ∈ Ring → 1 ∈ 𝑅) |
39 | 13, 36, 38 | 3syl 18 | . . . 4 ⊢ (𝜑 → 1 ∈ 𝑅) |
40 | eqid 2772 | . . . . 5 ⊢ (LSpan‘𝑈) = (LSpan‘𝑈) | |
41 | eqid 2772 | . . . . 5 ⊢ (LSSum‘𝑈) = (LSSum‘𝑈) | |
42 | eqid 2772 | . . . . 5 ⊢ (LSHyp‘𝑈) = (LSHyp‘𝑈) | |
43 | 10, 11, 12 | dvhlvec 37690 | . . . . 5 ⊢ (𝜑 → 𝑈 ∈ LVec) |
44 | 10, 17, 11, 15, 20, 42, 12, 1 | dochsnshp 38034 | . . . . 5 ⊢ (𝜑 → ( ⊥ ‘{𝑋}) ∈ (LSHyp‘𝑈)) |
45 | 10, 17, 11, 15, 20, 40, 41, 12, 1 | dochexmidat 38040 | . . . . 5 ⊢ (𝜑 → (( ⊥ ‘{𝑋})(LSSum‘𝑈)((LSpan‘𝑈)‘{𝑋})) = 𝑉) |
46 | 15, 29, 40, 41, 42, 43, 44, 2, 2, 45, 23, 37, 24 | lshpsmreu 35690 | . . . 4 ⊢ (𝜑 → ∃!𝑘 ∈ 𝑅 ∃𝑤 ∈ ( ⊥ ‘{𝑋})𝑋 = (𝑤 + (𝑘 · 𝑋))) |
47 | oveq1 6977 | . . . . . . . 8 ⊢ (𝑘 = 1 → (𝑘 · 𝑋) = ( 1 · 𝑋)) | |
48 | 47 | oveq2d 6986 | . . . . . . 7 ⊢ (𝑘 = 1 → (𝑤 + (𝑘 · 𝑋)) = (𝑤 + ( 1 · 𝑋))) |
49 | 48 | eqeq2d 2782 | . . . . . 6 ⊢ (𝑘 = 1 → (𝑋 = (𝑤 + (𝑘 · 𝑋)) ↔ 𝑋 = (𝑤 + ( 1 · 𝑋)))) |
50 | 49 | rexbidv 3236 | . . . . 5 ⊢ (𝑘 = 1 → (∃𝑤 ∈ ( ⊥ ‘{𝑋})𝑋 = (𝑤 + (𝑘 · 𝑋)) ↔ ∃𝑤 ∈ ( ⊥ ‘{𝑋})𝑋 = (𝑤 + ( 1 · 𝑋)))) |
51 | 50 | riota2 6953 | . . . 4 ⊢ (( 1 ∈ 𝑅 ∧ ∃!𝑘 ∈ 𝑅 ∃𝑤 ∈ ( ⊥ ‘{𝑋})𝑋 = (𝑤 + (𝑘 · 𝑋))) → (∃𝑤 ∈ ( ⊥ ‘{𝑋})𝑋 = (𝑤 + ( 1 · 𝑋)) ↔ (℩𝑘 ∈ 𝑅 ∃𝑤 ∈ ( ⊥ ‘{𝑋})𝑋 = (𝑤 + (𝑘 · 𝑋))) = 1 )) |
52 | 39, 46, 51 | syl2anc 576 | . . 3 ⊢ (𝜑 → (∃𝑤 ∈ ( ⊥ ‘{𝑋})𝑋 = (𝑤 + ( 1 · 𝑋)) ↔ (℩𝑘 ∈ 𝑅 ∃𝑤 ∈ ( ⊥ ‘{𝑋})𝑋 = (𝑤 + (𝑘 · 𝑋))) = 1 )) |
53 | 35, 52 | mpbid 224 | . 2 ⊢ (𝜑 → (℩𝑘 ∈ 𝑅 ∃𝑤 ∈ ( ⊥ ‘{𝑋})𝑋 = (𝑤 + (𝑘 · 𝑋))) = 1 ) |
54 | 9, 53 | eqtrd 2808 | 1 ⊢ (𝜑 → (𝐺‘𝑋) = 1 ) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 198 ∧ wa 387 = wceq 1507 ∈ wcel 2050 ∃wrex 3083 ∃!wreu 3084 ∖ cdif 3820 ⊆ wss 3823 {csn 4435 ↦ cmpt 5002 ‘cfv 6182 ℩crio 6930 (class class class)co 6970 Basecbs 16333 +gcplusg 16415 Scalarcsca 16418 ·𝑠 cvsca 16419 0gc0g 16563 LSSumclsm 18514 1rcur 18968 Ringcrg 19014 LModclmod 19350 LSubSpclss 19419 LSpanclspn 19459 LSHypclsh 35556 HLchlt 35931 LHypclh 36565 DVecHcdvh 37659 ocHcoch 37928 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 ax-5 1869 ax-6 1928 ax-7 1965 ax-8 2052 ax-9 2059 ax-10 2079 ax-11 2093 ax-12 2106 ax-13 2301 ax-ext 2744 ax-rep 5043 ax-sep 5054 ax-nul 5061 ax-pow 5113 ax-pr 5180 ax-un 7273 ax-cnex 10385 ax-resscn 10386 ax-1cn 10387 ax-icn 10388 ax-addcl 10389 ax-addrcl 10390 ax-mulcl 10391 ax-mulrcl 10392 ax-mulcom 10393 ax-addass 10394 ax-mulass 10395 ax-distr 10396 ax-i2m1 10397 ax-1ne0 10398 ax-1rid 10399 ax-rnegex 10400 ax-rrecex 10401 ax-cnre 10402 ax-pre-lttri 10403 ax-pre-lttrn 10404 ax-pre-ltadd 10405 ax-pre-mulgt0 10406 ax-riotaBAD 35534 |
This theorem depends on definitions: df-bi 199 df-an 388 df-or 834 df-3or 1069 df-3an 1070 df-tru 1510 df-fal 1520 df-ex 1743 df-nf 1747 df-sb 2016 df-mo 2547 df-eu 2584 df-clab 2753 df-cleq 2765 df-clel 2840 df-nfc 2912 df-ne 2962 df-nel 3068 df-ral 3087 df-rex 3088 df-reu 3089 df-rmo 3090 df-rab 3091 df-v 3411 df-sbc 3676 df-csb 3781 df-dif 3826 df-un 3828 df-in 3830 df-ss 3837 df-pss 3839 df-nul 4173 df-if 4345 df-pw 4418 df-sn 4436 df-pr 4438 df-tp 4440 df-op 4442 df-uni 4707 df-int 4744 df-iun 4788 df-iin 4789 df-br 4924 df-opab 4986 df-mpt 5003 df-tr 5025 df-id 5306 df-eprel 5311 df-po 5320 df-so 5321 df-fr 5360 df-we 5362 df-xp 5407 df-rel 5408 df-cnv 5409 df-co 5410 df-dm 5411 df-rn 5412 df-res 5413 df-ima 5414 df-pred 5980 df-ord 6026 df-on 6027 df-lim 6028 df-suc 6029 df-iota 6146 df-fun 6184 df-fn 6185 df-f 6186 df-f1 6187 df-fo 6188 df-f1o 6189 df-fv 6190 df-riota 6931 df-ov 6973 df-oprab 6974 df-mpo 6975 df-om 7391 df-1st 7495 df-2nd 7496 df-tpos 7689 df-undef 7736 df-wrecs 7744 df-recs 7806 df-rdg 7844 df-1o 7899 df-oadd 7903 df-er 8083 df-map 8202 df-en 8301 df-dom 8302 df-sdom 8303 df-fin 8304 df-pnf 10470 df-mnf 10471 df-xr 10472 df-ltxr 10473 df-le 10474 df-sub 10666 df-neg 10667 df-nn 11434 df-2 11497 df-3 11498 df-4 11499 df-5 11500 df-6 11501 df-n0 11702 df-z 11788 df-uz 12053 df-fz 12703 df-struct 16335 df-ndx 16336 df-slot 16337 df-base 16339 df-sets 16340 df-ress 16341 df-plusg 16428 df-mulr 16429 df-sca 16431 df-vsca 16432 df-0g 16565 df-proset 17390 df-poset 17408 df-plt 17420 df-lub 17436 df-glb 17437 df-join 17438 df-meet 17439 df-p0 17501 df-p1 17502 df-lat 17508 df-clat 17570 df-mgm 17704 df-sgrp 17746 df-mnd 17757 df-submnd 17798 df-grp 17888 df-minusg 17889 df-sbg 17890 df-subg 18054 df-cntz 18212 df-lsm 18516 df-cmn 18662 df-abl 18663 df-mgp 18957 df-ur 18969 df-ring 19016 df-oppr 19090 df-dvdsr 19108 df-unit 19109 df-invr 19139 df-dvr 19150 df-drng 19221 df-lmod 19352 df-lss 19420 df-lsp 19460 df-lvec 19591 df-lsatoms 35557 df-lshyp 35558 df-oposet 35757 df-ol 35759 df-oml 35760 df-covers 35847 df-ats 35848 df-atl 35879 df-cvlat 35903 df-hlat 35932 df-llines 36079 df-lplanes 36080 df-lvols 36081 df-lines 36082 df-psubsp 36084 df-pmap 36085 df-padd 36377 df-lhyp 36569 df-laut 36570 df-ldil 36685 df-ltrn 36686 df-trl 36740 df-tgrp 37324 df-tendo 37336 df-edring 37338 df-dveca 37584 df-disoa 37610 df-dvech 37660 df-dib 37720 df-dic 37754 df-dih 37810 df-doch 37929 df-djh 37976 |
This theorem is referenced by: lcfl6lem 38079 lcfl7lem 38080 hvmapidN 38343 hdmapevec2 38417 |
Copyright terms: Public domain | W3C validator |