Step |
Hyp |
Ref |
Expression |
1 |
|
cdlemn4.b |
|- B = ( Base ` K ) |
2 |
|
cdlemn4.l |
|- .<_ = ( le ` K ) |
3 |
|
cdlemn4.a |
|- A = ( Atoms ` K ) |
4 |
|
cdlemn4.p |
|- P = ( ( oc ` K ) ` W ) |
5 |
|
cdlemn4.h |
|- H = ( LHyp ` K ) |
6 |
|
cdlemn4.t |
|- T = ( ( LTrn ` K ) ` W ) |
7 |
|
cdlemn4.o |
|- O = ( h e. T |-> ( _I |` B ) ) |
8 |
|
cdlemn4.u |
|- U = ( ( DVecH ` K ) ` W ) |
9 |
|
cdlemn4.f |
|- F = ( iota_ h e. T ( h ` P ) = Q ) |
10 |
|
cdlemn4.g |
|- G = ( iota_ h e. T ( h ` P ) = R ) |
11 |
|
cdlemn4.j |
|- J = ( iota_ h e. T ( h ` Q ) = R ) |
12 |
|
cdlemn4a.n |
|- N = ( LSpan ` U ) |
13 |
|
cdlemn4a.s |
|- .(+) = ( LSSum ` U ) |
14 |
|
eqid |
|- ( +g ` U ) = ( +g ` U ) |
15 |
1 2 3 4 5 6 7 8 9 10 11 14
|
cdlemn4 |
|- ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) -> <. G , ( _I |` T ) >. = ( <. F , ( _I |` T ) >. ( +g ` U ) <. J , O >. ) ) |
16 |
15
|
sneqd |
|- ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) -> { <. G , ( _I |` T ) >. } = { ( <. F , ( _I |` T ) >. ( +g ` U ) <. J , O >. ) } ) |
17 |
16
|
fveq2d |
|- ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) -> ( N ` { <. G , ( _I |` T ) >. } ) = ( N ` { ( <. F , ( _I |` T ) >. ( +g ` U ) <. J , O >. ) } ) ) |
18 |
|
simp1 |
|- ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) -> ( K e. HL /\ W e. H ) ) |
19 |
5 8 18
|
dvhlmod |
|- ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) -> U e. LMod ) |
20 |
2 3 5 4
|
lhpocnel2 |
|- ( ( K e. HL /\ W e. H ) -> ( P e. A /\ -. P .<_ W ) ) |
21 |
20
|
3ad2ant1 |
|- ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) -> ( P e. A /\ -. P .<_ W ) ) |
22 |
|
simp2 |
|- ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) -> ( Q e. A /\ -. Q .<_ W ) ) |
23 |
2 3 5 6 9
|
ltrniotacl |
|- ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> F e. T ) |
24 |
18 21 22 23
|
syl3anc |
|- ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) -> F e. T ) |
25 |
|
eqid |
|- ( ( TEndo ` K ) ` W ) = ( ( TEndo ` K ) ` W ) |
26 |
5 6 25
|
tendoidcl |
|- ( ( K e. HL /\ W e. H ) -> ( _I |` T ) e. ( ( TEndo ` K ) ` W ) ) |
27 |
26
|
3ad2ant1 |
|- ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) -> ( _I |` T ) e. ( ( TEndo ` K ) ` W ) ) |
28 |
|
eqid |
|- ( Base ` U ) = ( Base ` U ) |
29 |
5 6 25 8 28
|
dvhelvbasei |
|- ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ ( _I |` T ) e. ( ( TEndo ` K ) ` W ) ) ) -> <. F , ( _I |` T ) >. e. ( Base ` U ) ) |
30 |
18 24 27 29
|
syl12anc |
|- ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) -> <. F , ( _I |` T ) >. e. ( Base ` U ) ) |
31 |
2 3 5 6 11
|
ltrniotacl |
|- ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) -> J e. T ) |
32 |
1 5 6 25 7
|
tendo0cl |
|- ( ( K e. HL /\ W e. H ) -> O e. ( ( TEndo ` K ) ` W ) ) |
33 |
32
|
3ad2ant1 |
|- ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) -> O e. ( ( TEndo ` K ) ` W ) ) |
34 |
5 6 25 8 28
|
dvhelvbasei |
|- ( ( ( K e. HL /\ W e. H ) /\ ( J e. T /\ O e. ( ( TEndo ` K ) ` W ) ) ) -> <. J , O >. e. ( Base ` U ) ) |
35 |
18 31 33 34
|
syl12anc |
|- ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) -> <. J , O >. e. ( Base ` U ) ) |
36 |
28 14 12 13
|
lspsntri |
|- ( ( U e. LMod /\ <. F , ( _I |` T ) >. e. ( Base ` U ) /\ <. J , O >. e. ( Base ` U ) ) -> ( N ` { ( <. F , ( _I |` T ) >. ( +g ` U ) <. J , O >. ) } ) C_ ( ( N ` { <. F , ( _I |` T ) >. } ) .(+) ( N ` { <. J , O >. } ) ) ) |
37 |
19 30 35 36
|
syl3anc |
|- ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) -> ( N ` { ( <. F , ( _I |` T ) >. ( +g ` U ) <. J , O >. ) } ) C_ ( ( N ` { <. F , ( _I |` T ) >. } ) .(+) ( N ` { <. J , O >. } ) ) ) |
38 |
17 37
|
eqsstrd |
|- ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) -> ( N ` { <. G , ( _I |` T ) >. } ) C_ ( ( N ` { <. F , ( _I |` T ) >. } ) .(+) ( N ` { <. J , O >. } ) ) ) |