Step |
Hyp |
Ref |
Expression |
1 |
|
lkrlsp.d |
|- D = ( Scalar ` W ) |
2 |
|
lkrlsp.o |
|- .0. = ( 0g ` D ) |
3 |
|
lkrlsp.v |
|- V = ( Base ` W ) |
4 |
|
lkrlsp.n |
|- N = ( LSpan ` W ) |
5 |
|
lkrlsp.p |
|- .(+) = ( LSSum ` W ) |
6 |
|
lkrlsp.f |
|- F = ( LFnl ` W ) |
7 |
|
lkrlsp.k |
|- K = ( LKer ` W ) |
8 |
|
lveclmod |
|- ( W e. LVec -> W e. LMod ) |
9 |
8
|
3ad2ant1 |
|- ( ( W e. LVec /\ ( X e. V /\ G e. F ) /\ ( G ` X ) =/= .0. ) -> W e. LMod ) |
10 |
|
simp2r |
|- ( ( W e. LVec /\ ( X e. V /\ G e. F ) /\ ( G ` X ) =/= .0. ) -> G e. F ) |
11 |
|
eqid |
|- ( LSubSp ` W ) = ( LSubSp ` W ) |
12 |
6 7 11
|
lkrlss |
|- ( ( W e. LMod /\ G e. F ) -> ( K ` G ) e. ( LSubSp ` W ) ) |
13 |
9 10 12
|
syl2anc |
|- ( ( W e. LVec /\ ( X e. V /\ G e. F ) /\ ( G ` X ) =/= .0. ) -> ( K ` G ) e. ( LSubSp ` W ) ) |
14 |
|
simp2l |
|- ( ( W e. LVec /\ ( X e. V /\ G e. F ) /\ ( G ` X ) =/= .0. ) -> X e. V ) |
15 |
3 11 4
|
lspsncl |
|- ( ( W e. LMod /\ X e. V ) -> ( N ` { X } ) e. ( LSubSp ` W ) ) |
16 |
9 14 15
|
syl2anc |
|- ( ( W e. LVec /\ ( X e. V /\ G e. F ) /\ ( G ` X ) =/= .0. ) -> ( N ` { X } ) e. ( LSubSp ` W ) ) |
17 |
11 5
|
lsmcl |
|- ( ( W e. LMod /\ ( K ` G ) e. ( LSubSp ` W ) /\ ( N ` { X } ) e. ( LSubSp ` W ) ) -> ( ( K ` G ) .(+) ( N ` { X } ) ) e. ( LSubSp ` W ) ) |
18 |
9 13 16 17
|
syl3anc |
|- ( ( W e. LVec /\ ( X e. V /\ G e. F ) /\ ( G ` X ) =/= .0. ) -> ( ( K ` G ) .(+) ( N ` { X } ) ) e. ( LSubSp ` W ) ) |
19 |
3 11
|
lssss |
|- ( ( ( K ` G ) .(+) ( N ` { X } ) ) e. ( LSubSp ` W ) -> ( ( K ` G ) .(+) ( N ` { X } ) ) C_ V ) |
20 |
18 19
|
syl |
|- ( ( W e. LVec /\ ( X e. V /\ G e. F ) /\ ( G ` X ) =/= .0. ) -> ( ( K ` G ) .(+) ( N ` { X } ) ) C_ V ) |
21 |
|
simpl1 |
|- ( ( ( W e. LVec /\ ( X e. V /\ G e. F ) /\ ( G ` X ) =/= .0. ) /\ u e. V ) -> W e. LVec ) |
22 |
21 8
|
syl |
|- ( ( ( W e. LVec /\ ( X e. V /\ G e. F ) /\ ( G ` X ) =/= .0. ) /\ u e. V ) -> W e. LMod ) |
23 |
|
simpr |
|- ( ( ( W e. LVec /\ ( X e. V /\ G e. F ) /\ ( G ` X ) =/= .0. ) /\ u e. V ) -> u e. V ) |
24 |
1
|
lmodring |
|- ( W e. LMod -> D e. Ring ) |
25 |
22 24
|
syl |
|- ( ( ( W e. LVec /\ ( X e. V /\ G e. F ) /\ ( G ` X ) =/= .0. ) /\ u e. V ) -> D e. Ring ) |
26 |
|
simpl2r |
|- ( ( ( W e. LVec /\ ( X e. V /\ G e. F ) /\ ( G ` X ) =/= .0. ) /\ u e. V ) -> G e. F ) |
27 |
|
eqid |
|- ( Base ` D ) = ( Base ` D ) |
28 |
1 27 3 6
|
lflcl |
|- ( ( W e. LVec /\ G e. F /\ u e. V ) -> ( G ` u ) e. ( Base ` D ) ) |
29 |
21 26 23 28
|
syl3anc |
|- ( ( ( W e. LVec /\ ( X e. V /\ G e. F ) /\ ( G ` X ) =/= .0. ) /\ u e. V ) -> ( G ` u ) e. ( Base ` D ) ) |
30 |
1
|
lvecdrng |
|- ( W e. LVec -> D e. DivRing ) |
31 |
21 30
|
syl |
|- ( ( ( W e. LVec /\ ( X e. V /\ G e. F ) /\ ( G ` X ) =/= .0. ) /\ u e. V ) -> D e. DivRing ) |
32 |
|
simpl2l |
|- ( ( ( W e. LVec /\ ( X e. V /\ G e. F ) /\ ( G ` X ) =/= .0. ) /\ u e. V ) -> X e. V ) |
33 |
1 27 3 6
|
lflcl |
|- ( ( W e. LVec /\ G e. F /\ X e. V ) -> ( G ` X ) e. ( Base ` D ) ) |
34 |
21 26 32 33
|
syl3anc |
|- ( ( ( W e. LVec /\ ( X e. V /\ G e. F ) /\ ( G ` X ) =/= .0. ) /\ u e. V ) -> ( G ` X ) e. ( Base ` D ) ) |
35 |
|
simpl3 |
|- ( ( ( W e. LVec /\ ( X e. V /\ G e. F ) /\ ( G ` X ) =/= .0. ) /\ u e. V ) -> ( G ` X ) =/= .0. ) |
36 |
|
eqid |
|- ( invr ` D ) = ( invr ` D ) |
37 |
27 2 36
|
drnginvrcl |
|- ( ( D e. DivRing /\ ( G ` X ) e. ( Base ` D ) /\ ( G ` X ) =/= .0. ) -> ( ( invr ` D ) ` ( G ` X ) ) e. ( Base ` D ) ) |
38 |
31 34 35 37
|
syl3anc |
|- ( ( ( W e. LVec /\ ( X e. V /\ G e. F ) /\ ( G ` X ) =/= .0. ) /\ u e. V ) -> ( ( invr ` D ) ` ( G ` X ) ) e. ( Base ` D ) ) |
39 |
|
eqid |
|- ( .r ` D ) = ( .r ` D ) |
40 |
27 39
|
ringcl |
|- ( ( D e. Ring /\ ( G ` u ) e. ( Base ` D ) /\ ( ( invr ` D ) ` ( G ` X ) ) e. ( Base ` D ) ) -> ( ( G ` u ) ( .r ` D ) ( ( invr ` D ) ` ( G ` X ) ) ) e. ( Base ` D ) ) |
41 |
25 29 38 40
|
syl3anc |
|- ( ( ( W e. LVec /\ ( X e. V /\ G e. F ) /\ ( G ` X ) =/= .0. ) /\ u e. V ) -> ( ( G ` u ) ( .r ` D ) ( ( invr ` D ) ` ( G ` X ) ) ) e. ( Base ` D ) ) |
42 |
|
eqid |
|- ( .s ` W ) = ( .s ` W ) |
43 |
3 1 42 27
|
lmodvscl |
|- ( ( W e. LMod /\ ( ( G ` u ) ( .r ` D ) ( ( invr ` D ) ` ( G ` X ) ) ) e. ( Base ` D ) /\ X e. V ) -> ( ( ( G ` u ) ( .r ` D ) ( ( invr ` D ) ` ( G ` X ) ) ) ( .s ` W ) X ) e. V ) |
44 |
22 41 32 43
|
syl3anc |
|- ( ( ( W e. LVec /\ ( X e. V /\ G e. F ) /\ ( G ` X ) =/= .0. ) /\ u e. V ) -> ( ( ( G ` u ) ( .r ` D ) ( ( invr ` D ) ` ( G ` X ) ) ) ( .s ` W ) X ) e. V ) |
45 |
|
eqid |
|- ( +g ` W ) = ( +g ` W ) |
46 |
|
eqid |
|- ( -g ` W ) = ( -g ` W ) |
47 |
3 45 46
|
lmodvnpcan |
|- ( ( W e. LMod /\ u e. V /\ ( ( ( G ` u ) ( .r ` D ) ( ( invr ` D ) ` ( G ` X ) ) ) ( .s ` W ) X ) e. V ) -> ( ( u ( -g ` W ) ( ( ( G ` u ) ( .r ` D ) ( ( invr ` D ) ` ( G ` X ) ) ) ( .s ` W ) X ) ) ( +g ` W ) ( ( ( G ` u ) ( .r ` D ) ( ( invr ` D ) ` ( G ` X ) ) ) ( .s ` W ) X ) ) = u ) |
48 |
22 23 44 47
|
syl3anc |
|- ( ( ( W e. LVec /\ ( X e. V /\ G e. F ) /\ ( G ` X ) =/= .0. ) /\ u e. V ) -> ( ( u ( -g ` W ) ( ( ( G ` u ) ( .r ` D ) ( ( invr ` D ) ` ( G ` X ) ) ) ( .s ` W ) X ) ) ( +g ` W ) ( ( ( G ` u ) ( .r ` D ) ( ( invr ` D ) ` ( G ` X ) ) ) ( .s ` W ) X ) ) = u ) |
49 |
11
|
lsssssubg |
|- ( W e. LMod -> ( LSubSp ` W ) C_ ( SubGrp ` W ) ) |
50 |
22 49
|
syl |
|- ( ( ( W e. LVec /\ ( X e. V /\ G e. F ) /\ ( G ` X ) =/= .0. ) /\ u e. V ) -> ( LSubSp ` W ) C_ ( SubGrp ` W ) ) |
51 |
13
|
adantr |
|- ( ( ( W e. LVec /\ ( X e. V /\ G e. F ) /\ ( G ` X ) =/= .0. ) /\ u e. V ) -> ( K ` G ) e. ( LSubSp ` W ) ) |
52 |
50 51
|
sseldd |
|- ( ( ( W e. LVec /\ ( X e. V /\ G e. F ) /\ ( G ` X ) =/= .0. ) /\ u e. V ) -> ( K ` G ) e. ( SubGrp ` W ) ) |
53 |
16
|
adantr |
|- ( ( ( W e. LVec /\ ( X e. V /\ G e. F ) /\ ( G ` X ) =/= .0. ) /\ u e. V ) -> ( N ` { X } ) e. ( LSubSp ` W ) ) |
54 |
50 53
|
sseldd |
|- ( ( ( W e. LVec /\ ( X e. V /\ G e. F ) /\ ( G ` X ) =/= .0. ) /\ u e. V ) -> ( N ` { X } ) e. ( SubGrp ` W ) ) |
55 |
3 46
|
lmodvsubcl |
|- ( ( W e. LMod /\ u e. V /\ ( ( ( G ` u ) ( .r ` D ) ( ( invr ` D ) ` ( G ` X ) ) ) ( .s ` W ) X ) e. V ) -> ( u ( -g ` W ) ( ( ( G ` u ) ( .r ` D ) ( ( invr ` D ) ` ( G ` X ) ) ) ( .s ` W ) X ) ) e. V ) |
56 |
22 23 44 55
|
syl3anc |
|- ( ( ( W e. LVec /\ ( X e. V /\ G e. F ) /\ ( G ` X ) =/= .0. ) /\ u e. V ) -> ( u ( -g ` W ) ( ( ( G ` u ) ( .r ` D ) ( ( invr ` D ) ` ( G ` X ) ) ) ( .s ` W ) X ) ) e. V ) |
57 |
|
eqid |
|- ( -g ` D ) = ( -g ` D ) |
58 |
1 57 3 46 6
|
lflsub |
|- ( ( W e. LMod /\ G e. F /\ ( u e. V /\ ( ( ( G ` u ) ( .r ` D ) ( ( invr ` D ) ` ( G ` X ) ) ) ( .s ` W ) X ) e. V ) ) -> ( G ` ( u ( -g ` W ) ( ( ( G ` u ) ( .r ` D ) ( ( invr ` D ) ` ( G ` X ) ) ) ( .s ` W ) X ) ) ) = ( ( G ` u ) ( -g ` D ) ( G ` ( ( ( G ` u ) ( .r ` D ) ( ( invr ` D ) ` ( G ` X ) ) ) ( .s ` W ) X ) ) ) ) |
59 |
22 26 23 44 58
|
syl112anc |
|- ( ( ( W e. LVec /\ ( X e. V /\ G e. F ) /\ ( G ` X ) =/= .0. ) /\ u e. V ) -> ( G ` ( u ( -g ` W ) ( ( ( G ` u ) ( .r ` D ) ( ( invr ` D ) ` ( G ` X ) ) ) ( .s ` W ) X ) ) ) = ( ( G ` u ) ( -g ` D ) ( G ` ( ( ( G ` u ) ( .r ` D ) ( ( invr ` D ) ` ( G ` X ) ) ) ( .s ` W ) X ) ) ) ) |
60 |
1 27 39 3 42 6
|
lflmul |
|- ( ( W e. LMod /\ G e. F /\ ( ( ( G ` u ) ( .r ` D ) ( ( invr ` D ) ` ( G ` X ) ) ) e. ( Base ` D ) /\ X e. V ) ) -> ( G ` ( ( ( G ` u ) ( .r ` D ) ( ( invr ` D ) ` ( G ` X ) ) ) ( .s ` W ) X ) ) = ( ( ( G ` u ) ( .r ` D ) ( ( invr ` D ) ` ( G ` X ) ) ) ( .r ` D ) ( G ` X ) ) ) |
61 |
22 26 41 32 60
|
syl112anc |
|- ( ( ( W e. LVec /\ ( X e. V /\ G e. F ) /\ ( G ` X ) =/= .0. ) /\ u e. V ) -> ( G ` ( ( ( G ` u ) ( .r ` D ) ( ( invr ` D ) ` ( G ` X ) ) ) ( .s ` W ) X ) ) = ( ( ( G ` u ) ( .r ` D ) ( ( invr ` D ) ` ( G ` X ) ) ) ( .r ` D ) ( G ` X ) ) ) |
62 |
27 39
|
ringass |
|- ( ( D e. Ring /\ ( ( G ` u ) e. ( Base ` D ) /\ ( ( invr ` D ) ` ( G ` X ) ) e. ( Base ` D ) /\ ( G ` X ) e. ( Base ` D ) ) ) -> ( ( ( G ` u ) ( .r ` D ) ( ( invr ` D ) ` ( G ` X ) ) ) ( .r ` D ) ( G ` X ) ) = ( ( G ` u ) ( .r ` D ) ( ( ( invr ` D ) ` ( G ` X ) ) ( .r ` D ) ( G ` X ) ) ) ) |
63 |
25 29 38 34 62
|
syl13anc |
|- ( ( ( W e. LVec /\ ( X e. V /\ G e. F ) /\ ( G ` X ) =/= .0. ) /\ u e. V ) -> ( ( ( G ` u ) ( .r ` D ) ( ( invr ` D ) ` ( G ` X ) ) ) ( .r ` D ) ( G ` X ) ) = ( ( G ` u ) ( .r ` D ) ( ( ( invr ` D ) ` ( G ` X ) ) ( .r ` D ) ( G ` X ) ) ) ) |
64 |
|
eqid |
|- ( 1r ` D ) = ( 1r ` D ) |
65 |
27 2 39 64 36
|
drnginvrl |
|- ( ( D e. DivRing /\ ( G ` X ) e. ( Base ` D ) /\ ( G ` X ) =/= .0. ) -> ( ( ( invr ` D ) ` ( G ` X ) ) ( .r ` D ) ( G ` X ) ) = ( 1r ` D ) ) |
66 |
31 34 35 65
|
syl3anc |
|- ( ( ( W e. LVec /\ ( X e. V /\ G e. F ) /\ ( G ` X ) =/= .0. ) /\ u e. V ) -> ( ( ( invr ` D ) ` ( G ` X ) ) ( .r ` D ) ( G ` X ) ) = ( 1r ` D ) ) |
67 |
66
|
oveq2d |
|- ( ( ( W e. LVec /\ ( X e. V /\ G e. F ) /\ ( G ` X ) =/= .0. ) /\ u e. V ) -> ( ( G ` u ) ( .r ` D ) ( ( ( invr ` D ) ` ( G ` X ) ) ( .r ` D ) ( G ` X ) ) ) = ( ( G ` u ) ( .r ` D ) ( 1r ` D ) ) ) |
68 |
27 39 64
|
ringridm |
|- ( ( D e. Ring /\ ( G ` u ) e. ( Base ` D ) ) -> ( ( G ` u ) ( .r ` D ) ( 1r ` D ) ) = ( G ` u ) ) |
69 |
25 29 68
|
syl2anc |
|- ( ( ( W e. LVec /\ ( X e. V /\ G e. F ) /\ ( G ` X ) =/= .0. ) /\ u e. V ) -> ( ( G ` u ) ( .r ` D ) ( 1r ` D ) ) = ( G ` u ) ) |
70 |
67 69
|
eqtrd |
|- ( ( ( W e. LVec /\ ( X e. V /\ G e. F ) /\ ( G ` X ) =/= .0. ) /\ u e. V ) -> ( ( G ` u ) ( .r ` D ) ( ( ( invr ` D ) ` ( G ` X ) ) ( .r ` D ) ( G ` X ) ) ) = ( G ` u ) ) |
71 |
61 63 70
|
3eqtrd |
|- ( ( ( W e. LVec /\ ( X e. V /\ G e. F ) /\ ( G ` X ) =/= .0. ) /\ u e. V ) -> ( G ` ( ( ( G ` u ) ( .r ` D ) ( ( invr ` D ) ` ( G ` X ) ) ) ( .s ` W ) X ) ) = ( G ` u ) ) |
72 |
71
|
oveq2d |
|- ( ( ( W e. LVec /\ ( X e. V /\ G e. F ) /\ ( G ` X ) =/= .0. ) /\ u e. V ) -> ( ( G ` u ) ( -g ` D ) ( G ` ( ( ( G ` u ) ( .r ` D ) ( ( invr ` D ) ` ( G ` X ) ) ) ( .s ` W ) X ) ) ) = ( ( G ` u ) ( -g ` D ) ( G ` u ) ) ) |
73 |
1
|
lmodfgrp |
|- ( W e. LMod -> D e. Grp ) |
74 |
22 73
|
syl |
|- ( ( ( W e. LVec /\ ( X e. V /\ G e. F ) /\ ( G ` X ) =/= .0. ) /\ u e. V ) -> D e. Grp ) |
75 |
27 2 57
|
grpsubid |
|- ( ( D e. Grp /\ ( G ` u ) e. ( Base ` D ) ) -> ( ( G ` u ) ( -g ` D ) ( G ` u ) ) = .0. ) |
76 |
74 29 75
|
syl2anc |
|- ( ( ( W e. LVec /\ ( X e. V /\ G e. F ) /\ ( G ` X ) =/= .0. ) /\ u e. V ) -> ( ( G ` u ) ( -g ` D ) ( G ` u ) ) = .0. ) |
77 |
59 72 76
|
3eqtrd |
|- ( ( ( W e. LVec /\ ( X e. V /\ G e. F ) /\ ( G ` X ) =/= .0. ) /\ u e. V ) -> ( G ` ( u ( -g ` W ) ( ( ( G ` u ) ( .r ` D ) ( ( invr ` D ) ` ( G ` X ) ) ) ( .s ` W ) X ) ) ) = .0. ) |
78 |
3 1 2 6 7
|
ellkr |
|- ( ( W e. LVec /\ G e. F ) -> ( ( u ( -g ` W ) ( ( ( G ` u ) ( .r ` D ) ( ( invr ` D ) ` ( G ` X ) ) ) ( .s ` W ) X ) ) e. ( K ` G ) <-> ( ( u ( -g ` W ) ( ( ( G ` u ) ( .r ` D ) ( ( invr ` D ) ` ( G ` X ) ) ) ( .s ` W ) X ) ) e. V /\ ( G ` ( u ( -g ` W ) ( ( ( G ` u ) ( .r ` D ) ( ( invr ` D ) ` ( G ` X ) ) ) ( .s ` W ) X ) ) ) = .0. ) ) ) |
79 |
21 26 78
|
syl2anc |
|- ( ( ( W e. LVec /\ ( X e. V /\ G e. F ) /\ ( G ` X ) =/= .0. ) /\ u e. V ) -> ( ( u ( -g ` W ) ( ( ( G ` u ) ( .r ` D ) ( ( invr ` D ) ` ( G ` X ) ) ) ( .s ` W ) X ) ) e. ( K ` G ) <-> ( ( u ( -g ` W ) ( ( ( G ` u ) ( .r ` D ) ( ( invr ` D ) ` ( G ` X ) ) ) ( .s ` W ) X ) ) e. V /\ ( G ` ( u ( -g ` W ) ( ( ( G ` u ) ( .r ` D ) ( ( invr ` D ) ` ( G ` X ) ) ) ( .s ` W ) X ) ) ) = .0. ) ) ) |
80 |
56 77 79
|
mpbir2and |
|- ( ( ( W e. LVec /\ ( X e. V /\ G e. F ) /\ ( G ` X ) =/= .0. ) /\ u e. V ) -> ( u ( -g ` W ) ( ( ( G ` u ) ( .r ` D ) ( ( invr ` D ) ` ( G ` X ) ) ) ( .s ` W ) X ) ) e. ( K ` G ) ) |
81 |
3 42 1 27 4 22 41 32
|
lspsneli |
|- ( ( ( W e. LVec /\ ( X e. V /\ G e. F ) /\ ( G ` X ) =/= .0. ) /\ u e. V ) -> ( ( ( G ` u ) ( .r ` D ) ( ( invr ` D ) ` ( G ` X ) ) ) ( .s ` W ) X ) e. ( N ` { X } ) ) |
82 |
45 5
|
lsmelvali |
|- ( ( ( ( K ` G ) e. ( SubGrp ` W ) /\ ( N ` { X } ) e. ( SubGrp ` W ) ) /\ ( ( u ( -g ` W ) ( ( ( G ` u ) ( .r ` D ) ( ( invr ` D ) ` ( G ` X ) ) ) ( .s ` W ) X ) ) e. ( K ` G ) /\ ( ( ( G ` u ) ( .r ` D ) ( ( invr ` D ) ` ( G ` X ) ) ) ( .s ` W ) X ) e. ( N ` { X } ) ) ) -> ( ( u ( -g ` W ) ( ( ( G ` u ) ( .r ` D ) ( ( invr ` D ) ` ( G ` X ) ) ) ( .s ` W ) X ) ) ( +g ` W ) ( ( ( G ` u ) ( .r ` D ) ( ( invr ` D ) ` ( G ` X ) ) ) ( .s ` W ) X ) ) e. ( ( K ` G ) .(+) ( N ` { X } ) ) ) |
83 |
52 54 80 81 82
|
syl22anc |
|- ( ( ( W e. LVec /\ ( X e. V /\ G e. F ) /\ ( G ` X ) =/= .0. ) /\ u e. V ) -> ( ( u ( -g ` W ) ( ( ( G ` u ) ( .r ` D ) ( ( invr ` D ) ` ( G ` X ) ) ) ( .s ` W ) X ) ) ( +g ` W ) ( ( ( G ` u ) ( .r ` D ) ( ( invr ` D ) ` ( G ` X ) ) ) ( .s ` W ) X ) ) e. ( ( K ` G ) .(+) ( N ` { X } ) ) ) |
84 |
48 83
|
eqeltrrd |
|- ( ( ( W e. LVec /\ ( X e. V /\ G e. F ) /\ ( G ` X ) =/= .0. ) /\ u e. V ) -> u e. ( ( K ` G ) .(+) ( N ` { X } ) ) ) |
85 |
20 84
|
eqelssd |
|- ( ( W e. LVec /\ ( X e. V /\ G e. F ) /\ ( G ` X ) =/= .0. ) -> ( ( K ` G ) .(+) ( N ` { X } ) ) = V ) |