Metamath Proof Explorer

Theorem cdlemn4

Description: Part of proof of Lemma N of Crawley p. 121 line 31. (Contributed by NM, 21-Feb-2014) (Revised by Mario Carneiro, 24-Jun-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 )
cdlemn4.s 
|- .+ = ( +g ` U )
Assertion cdlemn4 
|- ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) -> <. G , ( _I |` T ) >. = ( <. F , ( _I |` T ) >. .+ <. 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 cdlemn4.s 
 |-  .+ = ( +g ` U )
13 simp1 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) -> ( K e. HL /\ W e. H ) )
14 2 3 5 4 lhpocnel2 
 |-  ( ( K e. HL /\ W e. H ) -> ( P e. A /\ -. P .<_ W ) )
15 13 14 syl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) -> ( P e. A /\ -. P .<_ W ) )
16 simp2 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) -> ( Q e. A /\ -. Q .<_ W ) )
17 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 )
18 13 15 16 17 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) -> F e. T )
19 eqid 
 |-  ( ( TEndo ` K ) ` W ) = ( ( TEndo ` K ) ` W )
20 5 6 19 tendoidcl 
 |-  ( ( K e. HL /\ W e. H ) -> ( _I |` T ) e. ( ( TEndo ` K ) ` W ) )
21 13 20 syl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) -> ( _I |` T ) e. ( ( TEndo ` K ) ` W ) )
22 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 )
23 1 5 6 19 7 tendo0cl 
 |-  ( ( K e. HL /\ W e. H ) -> O e. ( ( TEndo ` K ) ` W ) )
24 13 23 syl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) -> O e. ( ( TEndo ` K ) ` W ) )
25 eqid 
 |-  ( Scalar ` U ) = ( Scalar ` U )
26 eqid 
 |-  ( +g ` ( Scalar ` U ) ) = ( +g ` ( Scalar ` U ) )
27 5 6 19 8 25 12 26 dvhopvadd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ ( _I |` T ) e. ( ( TEndo ` K ) ` W ) ) /\ ( J e. T /\ O e. ( ( TEndo ` K ) ` W ) ) ) -> ( <. F , ( _I |` T ) >. .+ <. J , O >. ) = <. ( F o. J ) , ( ( _I |` T ) ( +g ` ( Scalar ` U ) ) O ) >. )
28 13 18 21 22 24 27 syl122anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) -> ( <. F , ( _I |` T ) >. .+ <. J , O >. ) = <. ( F o. J ) , ( ( _I |` T ) ( +g ` ( Scalar ` U ) ) O ) >. )
29 5 6 ltrncom 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ J e. T ) -> ( F o. J ) = ( J o. F ) )
30 13 18 22 29 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) -> ( F o. J ) = ( J o. F ) )
31 2 3 4 5 6 9 10 11 cdlemn3 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) -> ( J o. F ) = G )
32 30 31 eqtrd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) -> ( F o. J ) = G )
33 eqid 
 |-  ( ( EDRing ` K ) ` W ) = ( ( EDRing ` K ) ` W )
34 5 33 8 25 dvhsca 
 |-  ( ( K e. HL /\ W e. H ) -> ( Scalar ` U ) = ( ( EDRing ` K ) ` W ) )
35 34 fveq2d 
 |-  ( ( K e. HL /\ W e. H ) -> ( 0g ` ( Scalar ` U ) ) = ( 0g ` ( ( EDRing ` K ) ` W ) ) )
36 eqid 
 |-  ( 0g ` ( ( EDRing ` K ) ` W ) ) = ( 0g ` ( ( EDRing ` K ) ` W ) )
37 1 5 6 33 7 36 erng0g 
 |-  ( ( K e. HL /\ W e. H ) -> ( 0g ` ( ( EDRing ` K ) ` W ) ) = O )
38 35 37 eqtrd 
 |-  ( ( K e. HL /\ W e. H ) -> ( 0g ` ( Scalar ` U ) ) = O )
39 13 38 syl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) -> ( 0g ` ( Scalar ` U ) ) = O )
40 39 oveq2d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) -> ( ( _I |` T ) ( +g ` ( Scalar ` U ) ) ( 0g ` ( Scalar ` U ) ) ) = ( ( _I |` T ) ( +g ` ( Scalar ` U ) ) O ) )
41 5 33 erngdv 
 |-  ( ( K e. HL /\ W e. H ) -> ( ( EDRing ` K ) ` W ) e. DivRing )
42 drnggrp 
 |-  ( ( ( EDRing ` K ) ` W ) e. DivRing -> ( ( EDRing ` K ) ` W ) e. Grp )
43 41 42 syl 
 |-  ( ( K e. HL /\ W e. H ) -> ( ( EDRing ` K ) ` W ) e. Grp )
44 34 43 eqeltrd 
 |-  ( ( K e. HL /\ W e. H ) -> ( Scalar ` U ) e. Grp )
45 13 44 syl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) -> ( Scalar ` U ) e. Grp )
46 eqid 
 |-  ( Base ` ( Scalar ` U ) ) = ( Base ` ( Scalar ` U ) )
47 5 19 8 25 46 dvhbase 
 |-  ( ( K e. HL /\ W e. H ) -> ( Base ` ( Scalar ` U ) ) = ( ( TEndo ` K ) ` W ) )
48 13 47 syl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) -> ( Base ` ( Scalar ` U ) ) = ( ( TEndo ` K ) ` W ) )
49 21 48 eleqtrrd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) -> ( _I |` T ) e. ( Base ` ( Scalar ` U ) ) )
50 eqid 
 |-  ( 0g ` ( Scalar ` U ) ) = ( 0g ` ( Scalar ` U ) )
51 46 26 50 grprid 
 |-  ( ( ( Scalar ` U ) e. Grp /\ ( _I |` T ) e. ( Base ` ( Scalar ` U ) ) ) -> ( ( _I |` T ) ( +g ` ( Scalar ` U ) ) ( 0g ` ( Scalar ` U ) ) ) = ( _I |` T ) )
52 45 49 51 syl2anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) -> ( ( _I |` T ) ( +g ` ( Scalar ` U ) ) ( 0g ` ( Scalar ` U ) ) ) = ( _I |` T ) )
53 40 52 eqtr3d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) -> ( ( _I |` T ) ( +g ` ( Scalar ` U ) ) O ) = ( _I |` T ) )
54 32 53 opeq12d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) -> <. ( F o. J ) , ( ( _I |` T ) ( +g ` ( Scalar ` U ) ) O ) >. = <. G , ( _I |` T ) >. )
55 28 54 eqtr2d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) -> <. G , ( _I |` T ) >. = ( <. F , ( _I |` T ) >. .+ <. J , O >. ) )