Metamath Proof Explorer


Theorem cdlemn4a

Description: Part of proof of Lemma N of Crawley p. 121 line 32. (Contributed by NM, 24-Feb-2014)

Ref Expression
Hypotheses cdlemn4.b
|- B = ( Base ` K )
cdlemn4.l
|- .<_ = ( le ` K )
cdlemn4.a
|- A = ( Atoms ` K )
cdlemn4.p
|- P = ( ( oc ` K ) ` W )
cdlemn4.h
|- H = ( LHyp ` K )
cdlemn4.t
|- T = ( ( LTrn ` K ) ` W )
cdlemn4.o
|- O = ( h e. T |-> ( _I |` B ) )
cdlemn4.u
|- U = ( ( DVecH ` K ) ` W )
cdlemn4.f
|- F = ( iota_ h e. T ( h ` P ) = Q )
cdlemn4.g
|- G = ( iota_ h e. T ( h ` P ) = R )
cdlemn4.j
|- J = ( iota_ h e. T ( h ` Q ) = R )
cdlemn4a.n
|- N = ( LSpan ` U )
cdlemn4a.s
|- .(+) = ( LSSum ` U )
Assertion cdlemn4a
|- ( ( ( 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 >. } ) ) )

Proof

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 >. } ) ) )