Metamath Proof Explorer

Theorem trlcoabs2N

Description: Absorption of the trace of a composition. (Contributed by NM, 29-Jul-2013) (New usage is discouraged.)

Ref Expression
Hypotheses trlcoabs.l 
|- .<_ = ( le ` K )
trlcoabs.j 
|- .\/ = ( join ` K )
trlcoabs.a 
|- A = ( Atoms ` K )
trlcoabs.h 
|- H = ( LHyp ` K )
trlcoabs.t 
|- T = ( ( LTrn ` K ) ` W )
trlcoabs.r 
|- R = ( ( trL ` K ) ` W )
Assertion trlcoabs2N 
|- ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( P e. A /\ -. P .<_ W ) ) -> ( ( F ` P ) .\/ ( R ` ( G o. `' F ) ) ) = ( ( F ` P ) .\/ ( G ` P ) ) )

Proof

Step Hyp Ref Expression
1 trlcoabs.l 
 |-  .<_ = ( le ` K )
2 trlcoabs.j 
 |-  .\/ = ( join ` K )
3 trlcoabs.a 
 |-  A = ( Atoms ` K )
4 trlcoabs.h 
 |-  H = ( LHyp ` K )
5 trlcoabs.t 
 |-  T = ( ( LTrn ` K ) ` W )
6 trlcoabs.r 
 |-  R = ( ( trL ` K ) ` W )
7 simp1 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( P e. A /\ -. P .<_ W ) ) -> ( K e. HL /\ W e. H ) )
8 simp2r 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( P e. A /\ -. P .<_ W ) ) -> G e. T )
9 simp2l 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( P e. A /\ -. P .<_ W ) ) -> F e. T )
10 4 5 ltrncnv 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> `' F e. T )
11 7 9 10 syl2anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( P e. A /\ -. P .<_ W ) ) -> `' F e. T )
12 4 5 ltrnco 
 |-  ( ( ( K e. HL /\ W e. H ) /\ G e. T /\ `' F e. T ) -> ( G o. `' F ) e. T )
13 7 8 11 12 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( P e. A /\ -. P .<_ W ) ) -> ( G o. `' F ) e. T )
14 1 3 4 5 ltrnel 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ ( P e. A /\ -. P .<_ W ) ) -> ( ( F ` P ) e. A /\ -. ( F ` P ) .<_ W ) )
15 14 3adant2r 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( P e. A /\ -. P .<_ W ) ) -> ( ( F ` P ) e. A /\ -. ( F ` P ) .<_ W ) )
16 eqid 
 |-  ( meet ` K ) = ( meet ` K )
17 1 2 16 3 4 5 6 trlval2 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( G o. `' F ) e. T /\ ( ( F ` P ) e. A /\ -. ( F ` P ) .<_ W ) ) -> ( R ` ( G o. `' F ) ) = ( ( ( F ` P ) .\/ ( ( G o. `' F ) ` ( F ` P ) ) ) ( meet ` K ) W ) )
18 7 13 15 17 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( P e. A /\ -. P .<_ W ) ) -> ( R ` ( G o. `' F ) ) = ( ( ( F ` P ) .\/ ( ( G o. `' F ) ` ( F ` P ) ) ) ( meet ` K ) W ) )
19 18 oveq2d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( P e. A /\ -. P .<_ W ) ) -> ( ( F ` P ) .\/ ( R ` ( G o. `' F ) ) ) = ( ( F ` P ) .\/ ( ( ( F ` P ) .\/ ( ( G o. `' F ) ` ( F ` P ) ) ) ( meet ` K ) W ) ) )
20 simp1l 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( P e. A /\ -. P .<_ W ) ) -> K e. HL )
21 simp3l 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( P e. A /\ -. P .<_ W ) ) -> P e. A )
22 1 3 4 5 ltrnat 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ P e. A ) -> ( F ` P ) e. A )
23 7 9 21 22 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( P e. A /\ -. P .<_ W ) ) -> ( F ` P ) e. A )
24 1 3 4 5 ltrnat 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( G o. `' F ) e. T /\ ( F ` P ) e. A ) -> ( ( G o. `' F ) ` ( F ` P ) ) e. A )
25 7 13 23 24 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( P e. A /\ -. P .<_ W ) ) -> ( ( G o. `' F ) ` ( F ` P ) ) e. A )
26 eqid 
 |-  ( Base ` K ) = ( Base ` K )
27 26 2 3 hlatjcl 
 |-  ( ( K e. HL /\ ( F ` P ) e. A /\ ( ( G o. `' F ) ` ( F ` P ) ) e. A ) -> ( ( F ` P ) .\/ ( ( G o. `' F ) ` ( F ` P ) ) ) e. ( Base ` K ) )
28 20 23 25 27 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( P e. A /\ -. P .<_ W ) ) -> ( ( F ` P ) .\/ ( ( G o. `' F ) ` ( F ` P ) ) ) e. ( Base ` K ) )
29 simp1r 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( P e. A /\ -. P .<_ W ) ) -> W e. H )
30 26 4 lhpbase 
 |-  ( W e. H -> W e. ( Base ` K ) )
31 29 30 syl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( P e. A /\ -. P .<_ W ) ) -> W e. ( Base ` K ) )
32 1 2 3 hlatlej1 
 |-  ( ( K e. HL /\ ( F ` P ) e. A /\ ( ( G o. `' F ) ` ( F ` P ) ) e. A ) -> ( F ` P ) .<_ ( ( F ` P ) .\/ ( ( G o. `' F ) ` ( F ` P ) ) ) )
33 20 23 25 32 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( P e. A /\ -. P .<_ W ) ) -> ( F ` P ) .<_ ( ( F ` P ) .\/ ( ( G o. `' F ) ` ( F ` P ) ) ) )
34 26 1 2 16 3 atmod3i1 
 |-  ( ( K e. HL /\ ( ( F ` P ) e. A /\ ( ( F ` P ) .\/ ( ( G o. `' F ) ` ( F ` P ) ) ) e. ( Base ` K ) /\ W e. ( Base ` K ) ) /\ ( F ` P ) .<_ ( ( F ` P ) .\/ ( ( G o. `' F ) ` ( F ` P ) ) ) ) -> ( ( F ` P ) .\/ ( ( ( F ` P ) .\/ ( ( G o. `' F ) ` ( F ` P ) ) ) ( meet ` K ) W ) ) = ( ( ( F ` P ) .\/ ( ( G o. `' F ) ` ( F ` P ) ) ) ( meet ` K ) ( ( F ` P ) .\/ W ) ) )
35 20 23 28 31 33 34 syl131anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( P e. A /\ -. P .<_ W ) ) -> ( ( F ` P ) .\/ ( ( ( F ` P ) .\/ ( ( G o. `' F ) ` ( F ` P ) ) ) ( meet ` K ) W ) ) = ( ( ( F ` P ) .\/ ( ( G o. `' F ) ` ( F ` P ) ) ) ( meet ` K ) ( ( F ` P ) .\/ W ) ) )
36 1 3 4 5 ltrncoval 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( G o. `' F ) e. T /\ F e. T ) /\ P e. A ) -> ( ( ( G o. `' F ) o. F ) ` P ) = ( ( G o. `' F ) ` ( F ` P ) ) )
37 7 13 9 21 36 syl121anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( P e. A /\ -. P .<_ W ) ) -> ( ( ( G o. `' F ) o. F ) ` P ) = ( ( G o. `' F ) ` ( F ` P ) ) )
38 coass 
 |-  ( ( G o. `' F ) o. F ) = ( G o. ( `' F o. F ) )
39 26 4 5 ltrn1o 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> F : ( Base ` K ) -1-1-onto-> ( Base ` K ) )
40 7 9 39 syl2anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( P e. A /\ -. P .<_ W ) ) -> F : ( Base ` K ) -1-1-onto-> ( Base ` K ) )
41 f1ococnv1 
 |-  ( F : ( Base ` K ) -1-1-onto-> ( Base ` K ) -> ( `' F o. F ) = ( _I |` ( Base ` K ) ) )
42 40 41 syl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( P e. A /\ -. P .<_ W ) ) -> ( `' F o. F ) = ( _I |` ( Base ` K ) ) )
43 42 coeq2d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( P e. A /\ -. P .<_ W ) ) -> ( G o. ( `' F o. F ) ) = ( G o. ( _I |` ( Base ` K ) ) ) )
44 26 4 5 ltrn1o 
 |-  ( ( ( K e. HL /\ W e. H ) /\ G e. T ) -> G : ( Base ` K ) -1-1-onto-> ( Base ` K ) )
45 7 8 44 syl2anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( P e. A /\ -. P .<_ W ) ) -> G : ( Base ` K ) -1-1-onto-> ( Base ` K ) )
46 f1of 
 |-  ( G : ( Base ` K ) -1-1-onto-> ( Base ` K ) -> G : ( Base ` K ) --> ( Base ` K ) )
47 fcoi1 
 |-  ( G : ( Base ` K ) --> ( Base ` K ) -> ( G o. ( _I |` ( Base ` K ) ) ) = G )
48 45 46 47 3syl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( P e. A /\ -. P .<_ W ) ) -> ( G o. ( _I |` ( Base ` K ) ) ) = G )
49 43 48 eqtrd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( P e. A /\ -. P .<_ W ) ) -> ( G o. ( `' F o. F ) ) = G )
50 38 49 syl5eq 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( P e. A /\ -. P .<_ W ) ) -> ( ( G o. `' F ) o. F ) = G )
51 50 fveq1d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( P e. A /\ -. P .<_ W ) ) -> ( ( ( G o. `' F ) o. F ) ` P ) = ( G ` P ) )
52 37 51 eqtr3d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( P e. A /\ -. P .<_ W ) ) -> ( ( G o. `' F ) ` ( F ` P ) ) = ( G ` P ) )
53 52 oveq2d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( P e. A /\ -. P .<_ W ) ) -> ( ( F ` P ) .\/ ( ( G o. `' F ) ` ( F ` P ) ) ) = ( ( F ` P ) .\/ ( G ` P ) ) )
54 eqid 
 |-  ( 1. ` K ) = ( 1. ` K )
55 1 2 54 3 4 lhpjat2 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( F ` P ) e. A /\ -. ( F ` P ) .<_ W ) ) -> ( ( F ` P ) .\/ W ) = ( 1. ` K ) )
56 7 15 55 syl2anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( P e. A /\ -. P .<_ W ) ) -> ( ( F ` P ) .\/ W ) = ( 1. ` K ) )
57 53 56 oveq12d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( P e. A /\ -. P .<_ W ) ) -> ( ( ( F ` P ) .\/ ( ( G o. `' F ) ` ( F ` P ) ) ) ( meet ` K ) ( ( F ` P ) .\/ W ) ) = ( ( ( F ` P ) .\/ ( G ` P ) ) ( meet ` K ) ( 1. ` K ) ) )
58 hlol 
 |-  ( K e. HL -> K e. OL )
59 20 58 syl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( P e. A /\ -. P .<_ W ) ) -> K e. OL )
60 1 3 4 5 ltrnat 
 |-  ( ( ( K e. HL /\ W e. H ) /\ G e. T /\ P e. A ) -> ( G ` P ) e. A )
61 7 8 21 60 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( P e. A /\ -. P .<_ W ) ) -> ( G ` P ) e. A )
62 26 2 3 hlatjcl 
 |-  ( ( K e. HL /\ ( F ` P ) e. A /\ ( G ` P ) e. A ) -> ( ( F ` P ) .\/ ( G ` P ) ) e. ( Base ` K ) )
63 20 23 61 62 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( P e. A /\ -. P .<_ W ) ) -> ( ( F ` P ) .\/ ( G ` P ) ) e. ( Base ` K ) )
64 26 16 54 olm11 
 |-  ( ( K e. OL /\ ( ( F ` P ) .\/ ( G ` P ) ) e. ( Base ` K ) ) -> ( ( ( F ` P ) .\/ ( G ` P ) ) ( meet ` K ) ( 1. ` K ) ) = ( ( F ` P ) .\/ ( G ` P ) ) )
65 59 63 64 syl2anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( P e. A /\ -. P .<_ W ) ) -> ( ( ( F ` P ) .\/ ( G ` P ) ) ( meet ` K ) ( 1. ` K ) ) = ( ( F ` P ) .\/ ( G ` P ) ) )
66 57 65 eqtrd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( P e. A /\ -. P .<_ W ) ) -> ( ( ( F ` P ) .\/ ( ( G o. `' F ) ` ( F ` P ) ) ) ( meet ` K ) ( ( F ` P ) .\/ W ) ) = ( ( F ` P ) .\/ ( G ` P ) ) )
67 19 35 66 3eqtrd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( P e. A /\ -. P .<_ W ) ) -> ( ( F ` P ) .\/ ( R ` ( G o. `' F ) ) ) = ( ( F ` P ) .\/ ( G ` P ) ) )