Metamath Proof Explorer


Theorem trljco

Description: Trace joined with trace of composition. (Contributed by NM, 15-Jun-2013)

Ref Expression
Hypotheses trljco.j ˙ = join K
trljco.h H = LHyp K
trljco.t T = LTrn K W
trljco.r R = trL K W
Assertion trljco K HL W H F T G T R F ˙ R F G = R F ˙ R G

Proof

Step Hyp Ref Expression
1 trljco.j ˙ = join K
2 trljco.h H = LHyp K
3 trljco.t T = LTrn K W
4 trljco.r R = trL K W
5 coeq1 F = I Base K F G = I Base K G
6 eqid Base K = Base K
7 6 2 3 ltrn1o K HL W H G T G : Base K 1-1 onto Base K
8 7 3adant2 K HL W H F T G T G : Base K 1-1 onto Base K
9 f1of G : Base K 1-1 onto Base K G : Base K Base K
10 fcoi2 G : Base K Base K I Base K G = G
11 8 9 10 3syl K HL W H F T G T I Base K G = G
12 5 11 sylan9eqr K HL W H F T G T F = I Base K F G = G
13 12 fveq2d K HL W H F T G T F = I Base K R F G = R G
14 13 oveq2d K HL W H F T G T F = I Base K R F ˙ R F G = R F ˙ R G
15 simp1l K HL W H F T G T K HL
16 15 hllatd K HL W H F T G T K Lat
17 6 2 3 4 trlcl K HL W H F T R F Base K
18 17 3adant3 K HL W H F T G T R F Base K
19 6 1 latjidm K Lat R F Base K R F ˙ R F = R F
20 16 18 19 syl2anc K HL W H F T G T R F ˙ R F = R F
21 hlol K HL K OL
22 15 21 syl K HL W H F T G T K OL
23 eqid 0. K = 0. K
24 6 1 23 olj01 K OL R F Base K R F ˙ 0. K = R F
25 22 18 24 syl2anc K HL W H F T G T R F ˙ 0. K = R F
26 20 25 eqtr4d K HL W H F T G T R F ˙ R F = R F ˙ 0. K
27 26 adantr K HL W H F T G T G = I Base K R F ˙ R F = R F ˙ 0. K
28 coeq2 G = I Base K F G = F I Base K
29 6 2 3 ltrn1o K HL W H F T F : Base K 1-1 onto Base K
30 29 3adant3 K HL W H F T G T F : Base K 1-1 onto Base K
31 f1of F : Base K 1-1 onto Base K F : Base K Base K
32 fcoi1 F : Base K Base K F I Base K = F
33 30 31 32 3syl K HL W H F T G T F I Base K = F
34 28 33 sylan9eqr K HL W H F T G T G = I Base K F G = F
35 34 fveq2d K HL W H F T G T G = I Base K R F G = R F
36 35 oveq2d K HL W H F T G T G = I Base K R F ˙ R F G = R F ˙ R F
37 6 23 2 3 4 trlid0b K HL W H G T G = I Base K R G = 0. K
38 37 3adant2 K HL W H F T G T G = I Base K R G = 0. K
39 38 biimpa K HL W H F T G T G = I Base K R G = 0. K
40 39 oveq2d K HL W H F T G T G = I Base K R F ˙ R G = R F ˙ 0. K
41 27 36 40 3eqtr4d K HL W H F T G T G = I Base K R F ˙ R F G = R F ˙ R G
42 eqid K = K
43 16 adantr K HL W H F T G T R F = R G K Lat
44 simp1 K HL W H F T G T K HL W H
45 2 3 ltrnco K HL W H F T G T F G T
46 6 2 3 4 trlcl K HL W H F G T R F G Base K
47 44 45 46 syl2anc K HL W H F T G T R F G Base K
48 6 1 latjcl K Lat R F Base K R F G Base K R F ˙ R F G Base K
49 16 18 47 48 syl3anc K HL W H F T G T R F ˙ R F G Base K
50 49 adantr K HL W H F T G T R F = R G R F ˙ R F G Base K
51 6 2 3 4 trlcl K HL W H G T R G Base K
52 51 3adant2 K HL W H F T G T R G Base K
53 6 1 latjcl K Lat R F Base K R G Base K R F ˙ R G Base K
54 16 18 52 53 syl3anc K HL W H F T G T R F ˙ R G Base K
55 54 adantr K HL W H F T G T R F = R G R F ˙ R G Base K
56 6 42 1 latlej1 K Lat R F Base K R G Base K R F K R F ˙ R G
57 16 18 52 56 syl3anc K HL W H F T G T R F K R F ˙ R G
58 42 1 2 3 4 trlco K HL W H F T G T R F G K R F ˙ R G
59 6 42 1 latjle12 K Lat R F Base K R F G Base K R F ˙ R G Base K R F K R F ˙ R G R F G K R F ˙ R G R F ˙ R F G K R F ˙ R G
60 16 18 47 54 59 syl13anc K HL W H F T G T R F K R F ˙ R G R F G K R F ˙ R G R F ˙ R F G K R F ˙ R G
61 57 58 60 mpbi2and K HL W H F T G T R F ˙ R F G K R F ˙ R G
62 61 adantr K HL W H F T G T R F = R G R F ˙ R F G K R F ˙ R G
63 simpr K HL W H F T G T R F = R G R F = R G
64 63 oveq2d K HL W H F T G T R F = R G R F ˙ R F = R F ˙ R G
65 6 42 1 latlej1 K Lat R F Base K R F G Base K R F K R F ˙ R F G
66 16 18 47 65 syl3anc K HL W H F T G T R F K R F ˙ R F G
67 20 66 eqbrtrd K HL W H F T G T R F ˙ R F K R F ˙ R F G
68 67 adantr K HL W H F T G T R F = R G R F ˙ R F K R F ˙ R F G
69 64 68 eqbrtrrd K HL W H F T G T R F = R G R F ˙ R G K R F ˙ R F G
70 6 42 43 50 55 62 69 latasymd K HL W H F T G T R F = R G R F ˙ R F G = R F ˙ R G
71 61 adantr K HL W H F T G T F I Base K G I Base K R F R G R F ˙ R F G K R F ˙ R G
72 simpl1l K HL W H F T G T F I Base K G I Base K R F R G K HL
73 simpl1 K HL W H F T G T F I Base K G I Base K R F R G K HL W H
74 simpl2 K HL W H F T G T F I Base K G I Base K R F R G F T
75 simpr1 K HL W H F T G T F I Base K G I Base K R F R G F I Base K
76 eqid Atoms K = Atoms K
77 6 76 2 3 4 trlnidat K HL W H F T F I Base K R F Atoms K
78 73 74 75 77 syl3anc K HL W H F T G T F I Base K G I Base K R F R G R F Atoms K
79 simpl3 K HL W H F T G T F I Base K G I Base K R F R G G T
80 74 79 jca K HL W H F T G T F I Base K G I Base K R F R G F T G T
81 simpr3 K HL W H F T G T F I Base K G I Base K R F R G R F R G
82 76 2 3 4 trlcoat K HL W H F T G T R F R G R F G Atoms K
83 73 80 81 82 syl3anc K HL W H F T G T F I Base K G I Base K R F R G R F G Atoms K
84 simpr2 K HL W H F T G T F I Base K G I Base K R F R G G I Base K
85 6 2 3 4 trlcone K HL W H F T G T R F R G G I Base K R F R F G
86 73 80 81 84 85 syl112anc K HL W H F T G T F I Base K G I Base K R F R G R F R F G
87 6 76 2 3 4 trlnidat K HL W H G T G I Base K R G Atoms K
88 73 79 84 87 syl3anc K HL W H F T G T F I Base K G I Base K R F R G R G Atoms K
89 42 1 76 ps-1 K HL R F Atoms K R F G Atoms K R F R F G R F Atoms K R G Atoms K R F ˙ R F G K R F ˙ R G R F ˙ R F G = R F ˙ R G
90 72 78 83 86 78 88 89 syl132anc K HL W H F T G T F I Base K G I Base K R F R G R F ˙ R F G K R F ˙ R G R F ˙ R F G = R F ˙ R G
91 71 90 mpbid K HL W H F T G T F I Base K G I Base K R F R G R F ˙ R F G = R F ˙ R G
92 14 41 70 91 pm2.61da3ne K HL W H F T G T R F ˙ R F G = R F ˙ R G