Description: Part (6) of Baer p. 47 line 6. Note that we use -. X e. ( N{ Y , Z } ) which is equivalent to Baer's "Fx i^i (Fy + Fz)" by lspdisjb . TODO: If disjoint variable conditions with I and ph become a problem later, use cbv* theorems on I variables here to get rid of them. Maybe reorder hypotheses in lemmas to the more consistent order of this theorem, so they can be shared with this theorem. TODO: may be deleted (with its lemmas), if not needed, in view of hdmap1l6 . (Contributed by NM, 1-May-2015) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | mapdh6.h | |- H = ( LHyp ` K ) |
|
| mapdh6.u | |- U = ( ( DVecH ` K ) ` W ) |
||
| mapdh6.v | |- V = ( Base ` U ) |
||
| mapdh6.p | |- .+ = ( +g ` U ) |
||
| mapdh6.s | |- .- = ( -g ` U ) |
||
| mapdh6.o | |- .0. = ( 0g ` U ) |
||
| mapdh6.n | |- N = ( LSpan ` U ) |
||
| mapdh6.c | |- C = ( ( LCDual ` K ) ` W ) |
||
| mapdh6.d | |- D = ( Base ` C ) |
||
| mapdh6.a | |- .+b = ( +g ` C ) |
||
| mapdh6.r | |- R = ( -g ` C ) |
||
| mapdh6.q | |- Q = ( 0g ` C ) |
||
| mapdh6.j | |- J = ( LSpan ` C ) |
||
| mapdh6.m | |- M = ( ( mapd ` K ) ` W ) |
||
| mapdh6.i | |- I = ( x e. _V |-> if ( ( 2nd ` x ) = .0. , Q , ( iota_ h e. D ( ( M ` ( N ` { ( 2nd ` x ) } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( ( 1st ` ( 1st ` x ) ) .- ( 2nd ` x ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` x ) ) R h ) } ) ) ) ) ) |
||
| mapdh6.k | |- ( ph -> ( K e. HL /\ W e. H ) ) |
||
| mapdh6.f | |- ( ph -> F e. D ) |
||
| mapdh6.x | |- ( ph -> X e. ( V \ { .0. } ) ) |
||
| mapdh6.y | |- ( ph -> Y e. V ) |
||
| mapdh6.z | |- ( ph -> Z e. V ) |
||
| mapdh6.xn | |- ( ph -> -. X e. ( N ` { Y , Z } ) ) |
||
| mapdh6.mn | |- ( ph -> ( M ` ( N ` { X } ) ) = ( J ` { F } ) ) |
||
| Assertion | mapdh6N | |- ( ph -> ( I ` <. X , F , ( Y .+ Z ) >. ) = ( ( I ` <. X , F , Y >. ) .+b ( I ` <. X , F , Z >. ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | mapdh6.h | |- H = ( LHyp ` K ) |
|
| 2 | mapdh6.u | |- U = ( ( DVecH ` K ) ` W ) |
|
| 3 | mapdh6.v | |- V = ( Base ` U ) |
|
| 4 | mapdh6.p | |- .+ = ( +g ` U ) |
|
| 5 | mapdh6.s | |- .- = ( -g ` U ) |
|
| 6 | mapdh6.o | |- .0. = ( 0g ` U ) |
|
| 7 | mapdh6.n | |- N = ( LSpan ` U ) |
|
| 8 | mapdh6.c | |- C = ( ( LCDual ` K ) ` W ) |
|
| 9 | mapdh6.d | |- D = ( Base ` C ) |
|
| 10 | mapdh6.a | |- .+b = ( +g ` C ) |
|
| 11 | mapdh6.r | |- R = ( -g ` C ) |
|
| 12 | mapdh6.q | |- Q = ( 0g ` C ) |
|
| 13 | mapdh6.j | |- J = ( LSpan ` C ) |
|
| 14 | mapdh6.m | |- M = ( ( mapd ` K ) ` W ) |
|
| 15 | mapdh6.i | |- I = ( x e. _V |-> if ( ( 2nd ` x ) = .0. , Q , ( iota_ h e. D ( ( M ` ( N ` { ( 2nd ` x ) } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( ( 1st ` ( 1st ` x ) ) .- ( 2nd ` x ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` x ) ) R h ) } ) ) ) ) ) |
|
| 16 | mapdh6.k | |- ( ph -> ( K e. HL /\ W e. H ) ) |
|
| 17 | mapdh6.f | |- ( ph -> F e. D ) |
|
| 18 | mapdh6.x | |- ( ph -> X e. ( V \ { .0. } ) ) |
|
| 19 | mapdh6.y | |- ( ph -> Y e. V ) |
|
| 20 | mapdh6.z | |- ( ph -> Z e. V ) |
|
| 21 | mapdh6.xn | |- ( ph -> -. X e. ( N ` { Y , Z } ) ) |
|
| 22 | mapdh6.mn | |- ( ph -> ( M ` ( N ` { X } ) ) = ( J ` { F } ) ) |
|
| 23 | 12 15 1 14 2 3 5 6 7 8 9 11 13 16 17 22 18 4 10 19 20 21 | mapdh6kN | |- ( ph -> ( I ` <. X , F , ( Y .+ Z ) >. ) = ( ( I ` <. X , F , Y >. ) .+b ( I ` <. X , F , Z >. ) ) ) |