dochfl1 - Mathbox for Norm Megill

	Mathbox for Norm Megill		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > dochfl1		Structured version Visualization version GIF version

Theorem dochfl1 38057

Description: The value of the explicit functional 𝐺 is 1 at the 𝑋 that determines it. (Contributed by NM, 27-Oct-2014.)

**Hypotheses**
Ref	Expression
dochfl1.h	⊢ 𝐻 = (LHyp‘𝐾)
dochfl1.o	⊢ ⊥ = ((ocH‘𝐾)‘𝑊)
dochfl1.u	⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)
dochfl1.v	⊢ 𝑉 = (Base‘𝑈)
dochfl1.a	⊢ + = (+_g‘𝑈)
dochfl1.t	⊢ · = ( ·_𝑠 ‘𝑈)
dochfl1.z	⊢ 0 = (0_g‘𝑈)
dochfl1.d	⊢ 𝐷 = (Scalar‘𝑈)
dochfl1.r	⊢ 𝑅 = (Base‘𝐷)
dochfl1.i	⊢ 1 = (1_r‘𝐷)
dochfl1.k	⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
dochfl1.x	⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))
dochfl1.g	⊢ 𝐺 = (𝑣 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝑅 ∃𝑤 ∈ ( ⊥ ‘{𝑋})𝑣 = (𝑤 + (𝑘 · 𝑋))))

**Assertion**
Ref	Expression
dochfl1	⊢ (𝜑 → (𝐺‘𝑋) = 1 )

Distinct variable groups: 𝑣,𝑘,𝑤, + 1 ,𝑘,𝑤 ⊥ ,𝑘,𝑣,𝑤 𝑅,𝑘,𝑣 · ,𝑘,𝑣,𝑤 𝑣,𝑉 𝑘,𝑋,𝑣,𝑤 𝑤, 0 Allowed substitution hints: 𝜑(𝑤,𝑣,𝑘) 𝐷(𝑤,𝑣,𝑘) 𝑅(𝑤) 𝑈(𝑤,𝑣,𝑘) 1 (𝑣) 𝐺(𝑤,𝑣,𝑘) 𝐻(𝑤,𝑣,𝑘) 𝐾(𝑤,𝑣,𝑘) 𝑉(𝑤,𝑘) 𝑊(𝑤,𝑣,𝑘) 0 (𝑣,𝑘)

**Proof of Theorem dochfl1**
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 = (0_g‘𝑈)
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 = (1_r‘𝐷)
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 0_gc0g 16563 LSSumclsm 18514 1_rcur 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

W3C validator