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 |
|
lclkrlem2o.h |
|- H = ( LHyp ` K ) |
18 |
|
lclkrlem2o.o |
|- ._|_ = ( ( ocH ` K ) ` W ) |
19 |
|
lclkrlem2o.u |
|- U = ( ( DVecH ` K ) ` W ) |
20 |
|
lclkrlem2o.a |
|- .(+) = ( LSSum ` U ) |
21 |
|
lclkrlem2o.k |
|- ( ph -> ( K e. HL /\ W e. H ) ) |
22 |
|
lclkrlem2o.b |
|- B = ( X .- ( ( ( ( E .+ G ) ` X ) .X. ( I ` ( ( E .+ G ) ` Y ) ) ) .x. Y ) ) |
23 |
|
lclkrlem2o.n |
|- ( ph -> ( ( E .+ G ) ` Y ) =/= .0. ) |
24 |
|
lclkrlem2p.bn |
|- ( ph -> B = ( 0g ` U ) ) |
25 |
17 19 21
|
dvhlmod |
|- ( ph -> U e. LMod ) |
26 |
|
eqid |
|- ( LSubSp ` U ) = ( LSubSp ` U ) |
27 |
1 26 15
|
lspsncl |
|- ( ( U e. LMod /\ Y e. V ) -> ( N ` { Y } ) e. ( LSubSp ` U ) ) |
28 |
25 12 27
|
syl2anc |
|- ( ph -> ( N ` { Y } ) e. ( LSubSp ` U ) ) |
29 |
1 26
|
lssss |
|- ( ( N ` { Y } ) e. ( LSubSp ` U ) -> ( N ` { Y } ) C_ V ) |
30 |
28 29
|
syl |
|- ( ph -> ( N ` { Y } ) C_ V ) |
31 |
22 24
|
eqtr3id |
|- ( ph -> ( X .- ( ( ( ( E .+ G ) ` X ) .X. ( I ` ( ( E .+ G ) ` Y ) ) ) .x. Y ) ) = ( 0g ` U ) ) |
32 |
3
|
lmodring |
|- ( U e. LMod -> S e. Ring ) |
33 |
25 32
|
syl |
|- ( ph -> S e. Ring ) |
34 |
8 9 10 25 13 14
|
ldualvaddcl |
|- ( ph -> ( E .+ G ) e. F ) |
35 |
|
eqid |
|- ( Base ` S ) = ( Base ` S ) |
36 |
3 35 1 8
|
lflcl |
|- ( ( U e. LMod /\ ( E .+ G ) e. F /\ X e. V ) -> ( ( E .+ G ) ` X ) e. ( Base ` S ) ) |
37 |
25 34 11 36
|
syl3anc |
|- ( ph -> ( ( E .+ G ) ` X ) e. ( Base ` S ) ) |
38 |
17 19 21
|
dvhlvec |
|- ( ph -> U e. LVec ) |
39 |
3
|
lvecdrng |
|- ( U e. LVec -> S e. DivRing ) |
40 |
38 39
|
syl |
|- ( ph -> S e. DivRing ) |
41 |
3 35 1 8
|
lflcl |
|- ( ( U e. LMod /\ ( E .+ G ) e. F /\ Y e. V ) -> ( ( E .+ G ) ` Y ) e. ( Base ` S ) ) |
42 |
25 34 12 41
|
syl3anc |
|- ( ph -> ( ( E .+ G ) ` Y ) e. ( Base ` S ) ) |
43 |
35 5 6
|
drnginvrcl |
|- ( ( S e. DivRing /\ ( ( E .+ G ) ` Y ) e. ( Base ` S ) /\ ( ( E .+ G ) ` Y ) =/= .0. ) -> ( I ` ( ( E .+ G ) ` Y ) ) e. ( Base ` S ) ) |
44 |
40 42 23 43
|
syl3anc |
|- ( ph -> ( I ` ( ( E .+ G ) ` Y ) ) e. ( Base ` S ) ) |
45 |
35 4
|
ringcl |
|- ( ( S e. Ring /\ ( ( E .+ G ) ` X ) e. ( Base ` S ) /\ ( I ` ( ( E .+ G ) ` Y ) ) e. ( Base ` S ) ) -> ( ( ( E .+ G ) ` X ) .X. ( I ` ( ( E .+ G ) ` Y ) ) ) e. ( Base ` S ) ) |
46 |
33 37 44 45
|
syl3anc |
|- ( ph -> ( ( ( E .+ G ) ` X ) .X. ( I ` ( ( E .+ G ) ` Y ) ) ) e. ( Base ` S ) ) |
47 |
1 3 2 35
|
lmodvscl |
|- ( ( U e. LMod /\ ( ( ( E .+ G ) ` X ) .X. ( I ` ( ( E .+ G ) ` Y ) ) ) e. ( Base ` S ) /\ Y e. V ) -> ( ( ( ( E .+ G ) ` X ) .X. ( I ` ( ( E .+ G ) ` Y ) ) ) .x. Y ) e. V ) |
48 |
25 46 12 47
|
syl3anc |
|- ( ph -> ( ( ( ( E .+ G ) ` X ) .X. ( I ` ( ( E .+ G ) ` Y ) ) ) .x. Y ) e. V ) |
49 |
|
eqid |
|- ( 0g ` U ) = ( 0g ` U ) |
50 |
1 49 7
|
lmodsubeq0 |
|- ( ( U e. LMod /\ X e. V /\ ( ( ( ( E .+ G ) ` X ) .X. ( I ` ( ( E .+ G ) ` Y ) ) ) .x. Y ) e. V ) -> ( ( X .- ( ( ( ( E .+ G ) ` X ) .X. ( I ` ( ( E .+ G ) ` Y ) ) ) .x. Y ) ) = ( 0g ` U ) <-> X = ( ( ( ( E .+ G ) ` X ) .X. ( I ` ( ( E .+ G ) ` Y ) ) ) .x. Y ) ) ) |
51 |
25 11 48 50
|
syl3anc |
|- ( ph -> ( ( X .- ( ( ( ( E .+ G ) ` X ) .X. ( I ` ( ( E .+ G ) ` Y ) ) ) .x. Y ) ) = ( 0g ` U ) <-> X = ( ( ( ( E .+ G ) ` X ) .X. ( I ` ( ( E .+ G ) ` Y ) ) ) .x. Y ) ) ) |
52 |
31 51
|
mpbid |
|- ( ph -> X = ( ( ( ( E .+ G ) ` X ) .X. ( I ` ( ( E .+ G ) ` Y ) ) ) .x. Y ) ) |
53 |
52
|
sneqd |
|- ( ph -> { X } = { ( ( ( ( E .+ G ) ` X ) .X. ( I ` ( ( E .+ G ) ` Y ) ) ) .x. Y ) } ) |
54 |
53
|
fveq2d |
|- ( ph -> ( N ` { X } ) = ( N ` { ( ( ( ( E .+ G ) ` X ) .X. ( I ` ( ( E .+ G ) ` Y ) ) ) .x. Y ) } ) ) |
55 |
3 35 1 2 15
|
lspsnvsi |
|- ( ( U e. LMod /\ ( ( ( E .+ G ) ` X ) .X. ( I ` ( ( E .+ G ) ` Y ) ) ) e. ( Base ` S ) /\ Y e. V ) -> ( N ` { ( ( ( ( E .+ G ) ` X ) .X. ( I ` ( ( E .+ G ) ` Y ) ) ) .x. Y ) } ) C_ ( N ` { Y } ) ) |
56 |
25 46 12 55
|
syl3anc |
|- ( ph -> ( N ` { ( ( ( ( E .+ G ) ` X ) .X. ( I ` ( ( E .+ G ) ` Y ) ) ) .x. Y ) } ) C_ ( N ` { Y } ) ) |
57 |
54 56
|
eqsstrd |
|- ( ph -> ( N ` { X } ) C_ ( N ` { Y } ) ) |
58 |
17 19 1 18
|
dochss |
|- ( ( ( K e. HL /\ W e. H ) /\ ( N ` { Y } ) C_ V /\ ( N ` { X } ) C_ ( N ` { Y } ) ) -> ( ._|_ ` ( N ` { Y } ) ) C_ ( ._|_ ` ( N ` { X } ) ) ) |
59 |
21 30 57 58
|
syl3anc |
|- ( ph -> ( ._|_ ` ( N ` { Y } ) ) C_ ( ._|_ ` ( N ` { X } ) ) ) |
60 |
12
|
snssd |
|- ( ph -> { Y } C_ V ) |
61 |
17 19 18 1 15 21 60
|
dochocsp |
|- ( ph -> ( ._|_ ` ( N ` { Y } ) ) = ( ._|_ ` { Y } ) ) |
62 |
11
|
snssd |
|- ( ph -> { X } C_ V ) |
63 |
17 19 18 1 15 21 62
|
dochocsp |
|- ( ph -> ( ._|_ ` ( N ` { X } ) ) = ( ._|_ ` { X } ) ) |
64 |
59 61 63
|
3sstr3d |
|- ( ph -> ( ._|_ ` { Y } ) C_ ( ._|_ ` { X } ) ) |