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