Step |
Hyp |
Ref |
Expression |
1 |
|
hdmapglem7.h |
|- H = ( LHyp ` K ) |
2 |
|
hdmapglem7.e |
|- E = <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >. |
3 |
|
hdmapglem7.o |
|- O = ( ( ocH ` K ) ` W ) |
4 |
|
hdmapglem7.u |
|- U = ( ( DVecH ` K ) ` W ) |
5 |
|
hdmapglem7.v |
|- V = ( Base ` U ) |
6 |
|
hdmapglem7.p |
|- .+ = ( +g ` U ) |
7 |
|
hdmapglem7.q |
|- .x. = ( .s ` U ) |
8 |
|
hdmapglem7.r |
|- R = ( Scalar ` U ) |
9 |
|
hdmapglem7.b |
|- B = ( Base ` R ) |
10 |
|
hdmapglem7.a |
|- .(+) = ( LSSum ` U ) |
11 |
|
hdmapglem7.n |
|- N = ( LSpan ` U ) |
12 |
|
hdmapglem7.k |
|- ( ph -> ( K e. HL /\ W e. H ) ) |
13 |
|
hdmapglem7.x |
|- ( ph -> X e. V ) |
14 |
|
eqid |
|- ( LSubSp ` U ) = ( LSubSp ` U ) |
15 |
1 4 12
|
dvhlmod |
|- ( ph -> U e. LMod ) |
16 |
|
eqid |
|- ( Base ` K ) = ( Base ` K ) |
17 |
|
eqid |
|- ( ( LTrn ` K ) ` W ) = ( ( LTrn ` K ) ` W ) |
18 |
|
eqid |
|- ( 0g ` U ) = ( 0g ` U ) |
19 |
1 16 17 4 5 18 2 12
|
dvheveccl |
|- ( ph -> E e. ( V \ { ( 0g ` U ) } ) ) |
20 |
19
|
eldifad |
|- ( ph -> E e. V ) |
21 |
5 14 11
|
lspsncl |
|- ( ( U e. LMod /\ E e. V ) -> ( N ` { E } ) e. ( LSubSp ` U ) ) |
22 |
15 20 21
|
syl2anc |
|- ( ph -> ( N ` { E } ) e. ( LSubSp ` U ) ) |
23 |
20
|
snssd |
|- ( ph -> { E } C_ V ) |
24 |
1 4 3 5 11 12 23
|
dochocsp |
|- ( ph -> ( O ` ( N ` { E } ) ) = ( O ` { E } ) ) |
25 |
24
|
fveq2d |
|- ( ph -> ( O ` ( O ` ( N ` { E } ) ) ) = ( O ` ( O ` { E } ) ) ) |
26 |
1 4 3 5 11 12 20
|
dochocsn |
|- ( ph -> ( O ` ( O ` { E } ) ) = ( N ` { E } ) ) |
27 |
25 26
|
eqtrd |
|- ( ph -> ( O ` ( O ` ( N ` { E } ) ) ) = ( N ` { E } ) ) |
28 |
1 3 4 5 14 10 12 22 27
|
dochexmid |
|- ( ph -> ( ( N ` { E } ) .(+) ( O ` ( N ` { E } ) ) ) = V ) |
29 |
24
|
oveq2d |
|- ( ph -> ( ( N ` { E } ) .(+) ( O ` ( N ` { E } ) ) ) = ( ( N ` { E } ) .(+) ( O ` { E } ) ) ) |
30 |
28 29
|
eqtr3d |
|- ( ph -> V = ( ( N ` { E } ) .(+) ( O ` { E } ) ) ) |
31 |
13 30
|
eleqtrd |
|- ( ph -> X e. ( ( N ` { E } ) .(+) ( O ` { E } ) ) ) |
32 |
14
|
lsssssubg |
|- ( U e. LMod -> ( LSubSp ` U ) C_ ( SubGrp ` U ) ) |
33 |
15 32
|
syl |
|- ( ph -> ( LSubSp ` U ) C_ ( SubGrp ` U ) ) |
34 |
33 22
|
sseldd |
|- ( ph -> ( N ` { E } ) e. ( SubGrp ` U ) ) |
35 |
1 4 5 14 3
|
dochlss |
|- ( ( ( K e. HL /\ W e. H ) /\ { E } C_ V ) -> ( O ` { E } ) e. ( LSubSp ` U ) ) |
36 |
12 23 35
|
syl2anc |
|- ( ph -> ( O ` { E } ) e. ( LSubSp ` U ) ) |
37 |
33 36
|
sseldd |
|- ( ph -> ( O ` { E } ) e. ( SubGrp ` U ) ) |
38 |
6 10
|
lsmelval |
|- ( ( ( N ` { E } ) e. ( SubGrp ` U ) /\ ( O ` { E } ) e. ( SubGrp ` U ) ) -> ( X e. ( ( N ` { E } ) .(+) ( O ` { E } ) ) <-> E. a e. ( N ` { E } ) E. u e. ( O ` { E } ) X = ( a .+ u ) ) ) |
39 |
34 37 38
|
syl2anc |
|- ( ph -> ( X e. ( ( N ` { E } ) .(+) ( O ` { E } ) ) <-> E. a e. ( N ` { E } ) E. u e. ( O ` { E } ) X = ( a .+ u ) ) ) |
40 |
31 39
|
mpbid |
|- ( ph -> E. a e. ( N ` { E } ) E. u e. ( O ` { E } ) X = ( a .+ u ) ) |
41 |
|
rexcom |
|- ( E. a e. ( N ` { E } ) E. u e. ( O ` { E } ) X = ( a .+ u ) <-> E. u e. ( O ` { E } ) E. a e. ( N ` { E } ) X = ( a .+ u ) ) |
42 |
|
df-rex |
|- ( E. a e. ( N ` { E } ) X = ( a .+ u ) <-> E. a ( a e. ( N ` { E } ) /\ X = ( a .+ u ) ) ) |
43 |
8 9 5 7 11
|
lspsnel |
|- ( ( U e. LMod /\ E e. V ) -> ( a e. ( N ` { E } ) <-> E. k e. B a = ( k .x. E ) ) ) |
44 |
15 20 43
|
syl2anc |
|- ( ph -> ( a e. ( N ` { E } ) <-> E. k e. B a = ( k .x. E ) ) ) |
45 |
44
|
anbi1d |
|- ( ph -> ( ( a e. ( N ` { E } ) /\ X = ( a .+ u ) ) <-> ( E. k e. B a = ( k .x. E ) /\ X = ( a .+ u ) ) ) ) |
46 |
|
r19.41v |
|- ( E. k e. B ( a = ( k .x. E ) /\ X = ( a .+ u ) ) <-> ( E. k e. B a = ( k .x. E ) /\ X = ( a .+ u ) ) ) |
47 |
45 46
|
bitr4di |
|- ( ph -> ( ( a e. ( N ` { E } ) /\ X = ( a .+ u ) ) <-> E. k e. B ( a = ( k .x. E ) /\ X = ( a .+ u ) ) ) ) |
48 |
47
|
exbidv |
|- ( ph -> ( E. a ( a e. ( N ` { E } ) /\ X = ( a .+ u ) ) <-> E. a E. k e. B ( a = ( k .x. E ) /\ X = ( a .+ u ) ) ) ) |
49 |
|
rexcom4 |
|- ( E. k e. B E. a ( a = ( k .x. E ) /\ X = ( a .+ u ) ) <-> E. a E. k e. B ( a = ( k .x. E ) /\ X = ( a .+ u ) ) ) |
50 |
|
ovex |
|- ( k .x. E ) e. _V |
51 |
|
oveq1 |
|- ( a = ( k .x. E ) -> ( a .+ u ) = ( ( k .x. E ) .+ u ) ) |
52 |
51
|
eqeq2d |
|- ( a = ( k .x. E ) -> ( X = ( a .+ u ) <-> X = ( ( k .x. E ) .+ u ) ) ) |
53 |
50 52
|
ceqsexv |
|- ( E. a ( a = ( k .x. E ) /\ X = ( a .+ u ) ) <-> X = ( ( k .x. E ) .+ u ) ) |
54 |
53
|
rexbii |
|- ( E. k e. B E. a ( a = ( k .x. E ) /\ X = ( a .+ u ) ) <-> E. k e. B X = ( ( k .x. E ) .+ u ) ) |
55 |
49 54
|
bitr3i |
|- ( E. a E. k e. B ( a = ( k .x. E ) /\ X = ( a .+ u ) ) <-> E. k e. B X = ( ( k .x. E ) .+ u ) ) |
56 |
48 55
|
bitrdi |
|- ( ph -> ( E. a ( a e. ( N ` { E } ) /\ X = ( a .+ u ) ) <-> E. k e. B X = ( ( k .x. E ) .+ u ) ) ) |
57 |
42 56
|
syl5bb |
|- ( ph -> ( E. a e. ( N ` { E } ) X = ( a .+ u ) <-> E. k e. B X = ( ( k .x. E ) .+ u ) ) ) |
58 |
57
|
rexbidv |
|- ( ph -> ( E. u e. ( O ` { E } ) E. a e. ( N ` { E } ) X = ( a .+ u ) <-> E. u e. ( O ` { E } ) E. k e. B X = ( ( k .x. E ) .+ u ) ) ) |
59 |
41 58
|
syl5bb |
|- ( ph -> ( E. a e. ( N ` { E } ) E. u e. ( O ` { E } ) X = ( a .+ u ) <-> E. u e. ( O ` { E } ) E. k e. B X = ( ( k .x. E ) .+ u ) ) ) |
60 |
40 59
|
mpbid |
|- ( ph -> E. u e. ( O ` { E } ) E. k e. B X = ( ( k .x. E ) .+ u ) ) |