| Step |
Hyp |
Ref |
Expression |
| 1 |
|
lclkrlem2m.v |
|- V = ( Base ` U ) |
| 2 |
|
lclkrlem2m.t |
|- .x. = ( .s ` U ) |
| 3 |
|
lclkrlem2m.s |
|- S = ( Scalar ` U ) |
| 4 |
|
lclkrlem2m.q |
|- .X. = ( .r ` S ) |
| 5 |
|
lclkrlem2m.z |
|- .0. = ( 0g ` S ) |
| 6 |
|
lclkrlem2m.i |
|- I = ( invr ` S ) |
| 7 |
|
lclkrlem2m.m |
|- .- = ( -g ` U ) |
| 8 |
|
lclkrlem2m.f |
|- F = ( LFnl ` U ) |
| 9 |
|
lclkrlem2m.d |
|- D = ( LDual ` U ) |
| 10 |
|
lclkrlem2m.p |
|- .+ = ( +g ` D ) |
| 11 |
|
lclkrlem2m.x |
|- ( ph -> X e. V ) |
| 12 |
|
lclkrlem2m.y |
|- ( ph -> Y e. V ) |
| 13 |
|
lclkrlem2m.e |
|- ( ph -> E e. F ) |
| 14 |
|
lclkrlem2m.g |
|- ( ph -> G e. F ) |
| 15 |
|
lclkrlem2n.n |
|- N = ( LSpan ` U ) |
| 16 |
|
lclkrlem2n.l |
|- L = ( LKer ` U ) |
| 17 |
|
lclkrlem2n.w |
|- ( ph -> U e. LVec ) |
| 18 |
|
lclkrlem2n.j |
|- ( ph -> ( ( E .+ G ) ` X ) = .0. ) |
| 19 |
|
lclkrlem2n.k |
|- ( ph -> ( ( E .+ G ) ` Y ) = .0. ) |
| 20 |
|
eqid |
|- ( LSubSp ` U ) = ( LSubSp ` U ) |
| 21 |
|
lveclmod |
|- ( U e. LVec -> U e. LMod ) |
| 22 |
17 21
|
syl |
|- ( ph -> U e. LMod ) |
| 23 |
8 9 10 22 13 14
|
ldualvaddcl |
|- ( ph -> ( E .+ G ) e. F ) |
| 24 |
8 16 20
|
lkrlss |
|- ( ( U e. LMod /\ ( E .+ G ) e. F ) -> ( L ` ( E .+ G ) ) e. ( LSubSp ` U ) ) |
| 25 |
22 23 24
|
syl2anc |
|- ( ph -> ( L ` ( E .+ G ) ) e. ( LSubSp ` U ) ) |
| 26 |
1 3 5 8 16 17 23 11
|
ellkr2 |
|- ( ph -> ( X e. ( L ` ( E .+ G ) ) <-> ( ( E .+ G ) ` X ) = .0. ) ) |
| 27 |
18 26
|
mpbird |
|- ( ph -> X e. ( L ` ( E .+ G ) ) ) |
| 28 |
1 3 5 8 16 17 23 12
|
ellkr2 |
|- ( ph -> ( Y e. ( L ` ( E .+ G ) ) <-> ( ( E .+ G ) ` Y ) = .0. ) ) |
| 29 |
19 28
|
mpbird |
|- ( ph -> Y e. ( L ` ( E .+ G ) ) ) |
| 30 |
20 15 22 25 27 29
|
lspprss |
|- ( ph -> ( N ` { X , Y } ) C_ ( L ` ( E .+ G ) ) ) |