Description: Simplify ( A \ { Q } ) in hdmap14lem3 to provide a slightly simpler definition later. TODO: Use hdmap14lem4a if that one is also used directly elsewhere. Otherwise, merge hdmap14lem4a into this one. (Contributed by NM, 31-May-2015)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | hdmap14lem1.h | |- H = ( LHyp ` K ) |
|
| hdmap14lem1.u | |- U = ( ( DVecH ` K ) ` W ) |
||
| hdmap14lem1.v | |- V = ( Base ` U ) |
||
| hdmap14lem1.t | |- .x. = ( .s ` U ) |
||
| hdmap14lem3.o | |- .0. = ( 0g ` U ) |
||
| hdmap14lem1.r | |- R = ( Scalar ` U ) |
||
| hdmap14lem1.b | |- B = ( Base ` R ) |
||
| hdmap14lem1.z | |- Z = ( 0g ` R ) |
||
| hdmap14lem1.c | |- C = ( ( LCDual ` K ) ` W ) |
||
| hdmap14lem2.e | |- .xb = ( .s ` C ) |
||
| hdmap14lem1.l | |- L = ( LSpan ` C ) |
||
| hdmap14lem2.p | |- P = ( Scalar ` C ) |
||
| hdmap14lem2.a | |- A = ( Base ` P ) |
||
| hdmap14lem2.q | |- Q = ( 0g ` P ) |
||
| hdmap14lem1.s | |- S = ( ( HDMap ` K ) ` W ) |
||
| hdmap14lem1.k | |- ( ph -> ( K e. HL /\ W e. H ) ) |
||
| hdmap14lem3.x | |- ( ph -> X e. ( V \ { .0. } ) ) |
||
| hdmap14lem1.f | |- ( ph -> F e. ( B \ { Z } ) ) |
||
| Assertion | hdmap14lem4 | |- ( ph -> E! g e. A ( S ` ( F .x. X ) ) = ( g .xb ( S ` X ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | hdmap14lem1.h | |- H = ( LHyp ` K ) |
|
| 2 | hdmap14lem1.u | |- U = ( ( DVecH ` K ) ` W ) |
|
| 3 | hdmap14lem1.v | |- V = ( Base ` U ) |
|
| 4 | hdmap14lem1.t | |- .x. = ( .s ` U ) |
|
| 5 | hdmap14lem3.o | |- .0. = ( 0g ` U ) |
|
| 6 | hdmap14lem1.r | |- R = ( Scalar ` U ) |
|
| 7 | hdmap14lem1.b | |- B = ( Base ` R ) |
|
| 8 | hdmap14lem1.z | |- Z = ( 0g ` R ) |
|
| 9 | hdmap14lem1.c | |- C = ( ( LCDual ` K ) ` W ) |
|
| 10 | hdmap14lem2.e | |- .xb = ( .s ` C ) |
|
| 11 | hdmap14lem1.l | |- L = ( LSpan ` C ) |
|
| 12 | hdmap14lem2.p | |- P = ( Scalar ` C ) |
|
| 13 | hdmap14lem2.a | |- A = ( Base ` P ) |
|
| 14 | hdmap14lem2.q | |- Q = ( 0g ` P ) |
|
| 15 | hdmap14lem1.s | |- S = ( ( HDMap ` K ) ` W ) |
|
| 16 | hdmap14lem1.k | |- ( ph -> ( K e. HL /\ W e. H ) ) |
|
| 17 | hdmap14lem3.x | |- ( ph -> X e. ( V \ { .0. } ) ) |
|
| 18 | hdmap14lem1.f | |- ( ph -> F e. ( B \ { Z } ) ) |
|
| 19 | 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 | hdmap14lem3 | |- ( ph -> E! g e. ( A \ { Q } ) ( S ` ( F .x. X ) ) = ( g .xb ( S ` X ) ) ) |
| 20 | 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 | hdmap14lem4a | |- ( ph -> ( E! g e. ( A \ { Q } ) ( S ` ( F .x. X ) ) = ( g .xb ( S ` X ) ) <-> E! g e. A ( S ` ( F .x. X ) ) = ( g .xb ( S ` X ) ) ) ) |
| 21 | 19 20 | mpbid | |- ( ph -> E! g e. A ( S ` ( F .x. X ) ) = ( g .xb ( S ` X ) ) ) |