Step | Hyp | Ref
| Expression |
1 | | riotaex 7371 |
. . 3
β’
(β©π¦
β (Baseβ((LCDualβπΎ)βπ))βπ§ β π (Β¬ π§ β (((LSpanβπ)β{β¨( I βΎ (BaseβπΎ)), ( I βΎ
((LTrnβπΎ)βπ))β©}) βͺ
((LSpanβπ)β{π‘})) β π¦ = (((HDMap1βπΎ)βπ)ββ¨π§, (((HDMap1βπΎ)βπ)ββ¨β¨( I βΎ
(BaseβπΎ)), ( I
βΎ ((LTrnβπΎ)βπ))β©, (((HVMapβπΎ)βπ)ββ¨( I βΎ (BaseβπΎ)), ( I βΎ
((LTrnβπΎ)βπ))β©), π§β©), π‘β©))) β V |
2 | | eqid 2732 |
. . 3
β’ (π‘ β π β¦ (β©π¦ β (Baseβ((LCDualβπΎ)βπ))βπ§ β π (Β¬ π§ β (((LSpanβπ)β{β¨( I βΎ (BaseβπΎ)), ( I βΎ
((LTrnβπΎ)βπ))β©}) βͺ
((LSpanβπ)β{π‘})) β π¦ = (((HDMap1βπΎ)βπ)ββ¨π§, (((HDMap1βπΎ)βπ)ββ¨β¨( I βΎ
(BaseβπΎ)), ( I
βΎ ((LTrnβπΎ)βπ))β©, (((HVMapβπΎ)βπ)ββ¨( I βΎ (BaseβπΎ)), ( I βΎ
((LTrnβπΎ)βπ))β©), π§β©), π‘β©)))) = (π‘ β π β¦ (β©π¦ β (Baseβ((LCDualβπΎ)βπ))βπ§ β π (Β¬ π§ β (((LSpanβπ)β{β¨( I βΎ (BaseβπΎ)), ( I βΎ
((LTrnβπΎ)βπ))β©}) βͺ
((LSpanβπ)β{π‘})) β π¦ = (((HDMap1βπΎ)βπ)ββ¨π§, (((HDMap1βπΎ)βπ)ββ¨β¨( I βΎ
(BaseβπΎ)), ( I
βΎ ((LTrnβπΎ)βπ))β©, (((HVMapβπΎ)βπ)ββ¨( I βΎ (BaseβπΎ)), ( I βΎ
((LTrnβπΎ)βπ))β©), π§β©), π‘β©)))) |
3 | 1, 2 | fnmpti 6693 |
. 2
β’ (π‘ β π β¦ (β©π¦ β (Baseβ((LCDualβπΎ)βπ))βπ§ β π (Β¬ π§ β (((LSpanβπ)β{β¨( I βΎ (BaseβπΎ)), ( I βΎ
((LTrnβπΎ)βπ))β©}) βͺ
((LSpanβπ)β{π‘})) β π¦ = (((HDMap1βπΎ)βπ)ββ¨π§, (((HDMap1βπΎ)βπ)ββ¨β¨( I βΎ
(BaseβπΎ)), ( I
βΎ ((LTrnβπΎ)βπ))β©, (((HVMapβπΎ)βπ)ββ¨( I βΎ (BaseβπΎ)), ( I βΎ
((LTrnβπΎ)βπ))β©), π§β©), π‘β©)))) Fn π |
4 | | hdmapfn.h |
. . . 4
β’ π» = (LHypβπΎ) |
5 | | eqid 2732 |
. . . 4
β’ β¨( I
βΎ (BaseβπΎ)), (
I βΎ ((LTrnβπΎ)βπ))β© = β¨( I βΎ
(BaseβπΎ)), ( I
βΎ ((LTrnβπΎ)βπ))β© |
6 | | hdmapfn.u |
. . . 4
β’ π = ((DVecHβπΎ)βπ) |
7 | | hdmapfn.v |
. . . 4
β’ π = (Baseβπ) |
8 | | eqid 2732 |
. . . 4
β’
(LSpanβπ) =
(LSpanβπ) |
9 | | eqid 2732 |
. . . 4
β’
((LCDualβπΎ)βπ) = ((LCDualβπΎ)βπ) |
10 | | eqid 2732 |
. . . 4
β’
(Baseβ((LCDualβπΎ)βπ)) = (Baseβ((LCDualβπΎ)βπ)) |
11 | | eqid 2732 |
. . . 4
β’
((HVMapβπΎ)βπ) = ((HVMapβπΎ)βπ) |
12 | | eqid 2732 |
. . . 4
β’
((HDMap1βπΎ)βπ) = ((HDMap1βπΎ)βπ) |
13 | | hdmapfn.s |
. . . 4
β’ π = ((HDMapβπΎ)βπ) |
14 | | hdmapfn.k |
. . . 4
β’ (π β (πΎ β HL β§ π β π»)) |
15 | 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14 | hdmapfval 41001 |
. . 3
β’ (π β π = (π‘ β π β¦ (β©π¦ β (Baseβ((LCDualβπΎ)βπ))βπ§ β π (Β¬ π§ β (((LSpanβπ)β{β¨( I βΎ (BaseβπΎ)), ( I βΎ
((LTrnβπΎ)βπ))β©}) βͺ
((LSpanβπ)β{π‘})) β π¦ = (((HDMap1βπΎ)βπ)ββ¨π§, (((HDMap1βπΎ)βπ)ββ¨β¨( I βΎ
(BaseβπΎ)), ( I
βΎ ((LTrnβπΎ)βπ))β©, (((HVMapβπΎ)βπ)ββ¨( I βΎ (BaseβπΎ)), ( I βΎ
((LTrnβπΎ)βπ))β©), π§β©), π‘β©))))) |
16 | 15 | fneq1d 6642 |
. 2
β’ (π β (π Fn π β (π‘ β π β¦ (β©π¦ β (Baseβ((LCDualβπΎ)βπ))βπ§ β π (Β¬ π§ β (((LSpanβπ)β{β¨( I βΎ (BaseβπΎ)), ( I βΎ
((LTrnβπΎ)βπ))β©}) βͺ
((LSpanβπ)β{π‘})) β π¦ = (((HDMap1βπΎ)βπ)ββ¨π§, (((HDMap1βπΎ)βπ)ββ¨β¨( I βΎ
(BaseβπΎ)), ( I
βΎ ((LTrnβπΎ)βπ))β©, (((HVMapβπΎ)βπ)ββ¨( I βΎ (BaseβπΎ)), ( I βΎ
((LTrnβπΎ)βπ))β©), π§β©), π‘β©)))) Fn π)) |
17 | 3, 16 | mpbiri 257 |
1
β’ (π β π Fn π) |