Metamath Proof Explorer


Theorem dihord5apre

Description: Part of proof that isomorphism H is order-preserving . (Contributed by NM, 7-Mar-2014)

Ref Expression
Hypotheses dihord5apre.b B = Base K
dihord5apre.l ˙ = K
dihord5apre.h H = LHyp K
dihord5apre.j ˙ = join K
dihord5apre.m ˙ = meet K
dihord5apre.a A = Atoms K
dihord5apre.u U = DVecH K W
dihord5apre.s ˙ = LSSum U
dihord5apre.i I = DIsoH K W
Assertion dihord5apre K HL W H X B X ˙ W Y B ¬ Y ˙ W I X I Y X ˙ Y

Proof

Step Hyp Ref Expression
1 dihord5apre.b B = Base K
2 dihord5apre.l ˙ = K
3 dihord5apre.h H = LHyp K
4 dihord5apre.j ˙ = join K
5 dihord5apre.m ˙ = meet K
6 dihord5apre.a A = Atoms K
7 dihord5apre.u U = DVecH K W
8 dihord5apre.s ˙ = LSSum U
9 dihord5apre.i I = DIsoH K W
10 simpl1 K HL W H X B X ˙ W Y B ¬ Y ˙ W I X I Y K HL W H
11 simpl3 K HL W H X B X ˙ W Y B ¬ Y ˙ W I X I Y Y B ¬ Y ˙ W
12 1 2 4 5 6 3 lhpmcvr2 K HL W H Y B ¬ Y ˙ W r A ¬ r ˙ W r ˙ Y ˙ W = Y
13 10 11 12 syl2anc K HL W H X B X ˙ W Y B ¬ Y ˙ W I X I Y r A ¬ r ˙ W r ˙ Y ˙ W = Y
14 simp11l K HL W H X B X ˙ W Y B ¬ Y ˙ W I X I Y r A ¬ r ˙ W r ˙ Y ˙ W = Y K HL
15 14 hllatd K HL W H X B X ˙ W Y B ¬ Y ˙ W I X I Y r A ¬ r ˙ W r ˙ Y ˙ W = Y K Lat
16 simp12l K HL W H X B X ˙ W Y B ¬ Y ˙ W I X I Y r A ¬ r ˙ W r ˙ Y ˙ W = Y X B
17 simp3ll K HL W H X B X ˙ W Y B ¬ Y ˙ W I X I Y r A ¬ r ˙ W r ˙ Y ˙ W = Y r A
18 1 6 atbase r A r B
19 17 18 syl K HL W H X B X ˙ W Y B ¬ Y ˙ W I X I Y r A ¬ r ˙ W r ˙ Y ˙ W = Y r B
20 1 4 latjcl K Lat r B X B r ˙ X B
21 15 19 16 20 syl3anc K HL W H X B X ˙ W Y B ¬ Y ˙ W I X I Y r A ¬ r ˙ W r ˙ Y ˙ W = Y r ˙ X B
22 simp13l K HL W H X B X ˙ W Y B ¬ Y ˙ W I X I Y r A ¬ r ˙ W r ˙ Y ˙ W = Y Y B
23 1 2 4 latlej2 K Lat r B X B X ˙ r ˙ X
24 15 19 16 23 syl3anc K HL W H X B X ˙ W Y B ¬ Y ˙ W I X I Y r A ¬ r ˙ W r ˙ Y ˙ W = Y X ˙ r ˙ X
25 simp11 K HL W H X B X ˙ W Y B ¬ Y ˙ W I X I Y r A ¬ r ˙ W r ˙ Y ˙ W = Y K HL W H
26 simp3lr K HL W H X B X ˙ W Y B ¬ Y ˙ W I X I Y r A ¬ r ˙ W r ˙ Y ˙ W = Y ¬ r ˙ W
27 1 2 4 latlej1 K Lat r B X B r ˙ r ˙ X
28 15 19 16 27 syl3anc K HL W H X B X ˙ W Y B ¬ Y ˙ W I X I Y r A ¬ r ˙ W r ˙ Y ˙ W = Y r ˙ r ˙ X
29 simp11r K HL W H X B X ˙ W Y B ¬ Y ˙ W I X I Y r A ¬ r ˙ W r ˙ Y ˙ W = Y W H
30 1 3 lhpbase W H W B
31 29 30 syl K HL W H X B X ˙ W Y B ¬ Y ˙ W I X I Y r A ¬ r ˙ W r ˙ Y ˙ W = Y W B
32 1 2 lattr K Lat r B r ˙ X B W B r ˙ r ˙ X r ˙ X ˙ W r ˙ W
33 15 19 21 31 32 syl13anc K HL W H X B X ˙ W Y B ¬ Y ˙ W I X I Y r A ¬ r ˙ W r ˙ Y ˙ W = Y r ˙ r ˙ X r ˙ X ˙ W r ˙ W
34 28 33 mpand K HL W H X B X ˙ W Y B ¬ Y ˙ W I X I Y r A ¬ r ˙ W r ˙ Y ˙ W = Y r ˙ X ˙ W r ˙ W
35 26 34 mtod K HL W H X B X ˙ W Y B ¬ Y ˙ W I X I Y r A ¬ r ˙ W r ˙ Y ˙ W = Y ¬ r ˙ X ˙ W
36 simp3l K HL W H X B X ˙ W Y B ¬ Y ˙ W I X I Y r A ¬ r ˙ W r ˙ Y ˙ W = Y r A ¬ r ˙ W
37 simp12 K HL W H X B X ˙ W Y B ¬ Y ˙ W I X I Y r A ¬ r ˙ W r ˙ Y ˙ W = Y X B X ˙ W
38 1 2 4 5 6 3 lhple K HL W H r A ¬ r ˙ W X B X ˙ W r ˙ X ˙ W = X
39 25 36 37 38 syl3anc K HL W H X B X ˙ W Y B ¬ Y ˙ W I X I Y r A ¬ r ˙ W r ˙ Y ˙ W = Y r ˙ X ˙ W = X
40 39 oveq2d K HL W H X B X ˙ W Y B ¬ Y ˙ W I X I Y r A ¬ r ˙ W r ˙ Y ˙ W = Y r ˙ r ˙ X ˙ W = r ˙ X
41 eqid DIsoB K W = DIsoB K W
42 eqid DIsoC K W = DIsoC K W
43 1 2 4 5 6 3 9 41 42 7 8 dihvalcq K HL W H r ˙ X B ¬ r ˙ X ˙ W r A ¬ r ˙ W r ˙ r ˙ X ˙ W = r ˙ X I r ˙ X = DIsoC K W r ˙ DIsoB K W r ˙ X ˙ W
44 25 21 35 36 40 43 syl122anc K HL W H X B X ˙ W Y B ¬ Y ˙ W I X I Y r A ¬ r ˙ W r ˙ Y ˙ W = Y I r ˙ X = DIsoC K W r ˙ DIsoB K W r ˙ X ˙ W
45 3 7 25 dvhlmod K HL W H X B X ˙ W Y B ¬ Y ˙ W I X I Y r A ¬ r ˙ W r ˙ Y ˙ W = Y U LMod
46 eqid LSubSp U = LSubSp U
47 46 lsssssubg U LMod LSubSp U SubGrp U
48 45 47 syl K HL W H X B X ˙ W Y B ¬ Y ˙ W I X I Y r A ¬ r ˙ W r ˙ Y ˙ W = Y LSubSp U SubGrp U
49 2 6 3 7 42 46 diclss K HL W H r A ¬ r ˙ W DIsoC K W r LSubSp U
50 25 36 49 syl2anc K HL W H X B X ˙ W Y B ¬ Y ˙ W I X I Y r A ¬ r ˙ W r ˙ Y ˙ W = Y DIsoC K W r LSubSp U
51 48 50 sseldd K HL W H X B X ˙ W Y B ¬ Y ˙ W I X I Y r A ¬ r ˙ W r ˙ Y ˙ W = Y DIsoC K W r SubGrp U
52 1 5 latmcl K Lat Y B W B Y ˙ W B
53 15 22 31 52 syl3anc K HL W H X B X ˙ W Y B ¬ Y ˙ W I X I Y r A ¬ r ˙ W r ˙ Y ˙ W = Y Y ˙ W B
54 1 2 5 latmle2 K Lat Y B W B Y ˙ W ˙ W
55 15 22 31 54 syl3anc K HL W H X B X ˙ W Y B ¬ Y ˙ W I X I Y r A ¬ r ˙ W r ˙ Y ˙ W = Y Y ˙ W ˙ W
56 1 2 3 7 41 46 diblss K HL W H Y ˙ W B Y ˙ W ˙ W DIsoB K W Y ˙ W LSubSp U
57 25 53 55 56 syl12anc K HL W H X B X ˙ W Y B ¬ Y ˙ W I X I Y r A ¬ r ˙ W r ˙ Y ˙ W = Y DIsoB K W Y ˙ W LSubSp U
58 48 57 sseldd K HL W H X B X ˙ W Y B ¬ Y ˙ W I X I Y r A ¬ r ˙ W r ˙ Y ˙ W = Y DIsoB K W Y ˙ W SubGrp U
59 8 lsmub1 DIsoC K W r SubGrp U DIsoB K W Y ˙ W SubGrp U DIsoC K W r DIsoC K W r ˙ DIsoB K W Y ˙ W
60 51 58 59 syl2anc K HL W H X B X ˙ W Y B ¬ Y ˙ W I X I Y r A ¬ r ˙ W r ˙ Y ˙ W = Y DIsoC K W r DIsoC K W r ˙ DIsoB K W Y ˙ W
61 simp13 K HL W H X B X ˙ W Y B ¬ Y ˙ W I X I Y r A ¬ r ˙ W r ˙ Y ˙ W = Y Y B ¬ Y ˙ W
62 simp3r K HL W H X B X ˙ W Y B ¬ Y ˙ W I X I Y r A ¬ r ˙ W r ˙ Y ˙ W = Y r ˙ Y ˙ W = Y
63 1 2 4 5 6 3 9 41 42 7 8 dihvalcq K HL W H Y B ¬ Y ˙ W r A ¬ r ˙ W r ˙ Y ˙ W = Y I Y = DIsoC K W r ˙ DIsoB K W Y ˙ W
64 25 61 36 62 63 syl112anc K HL W H X B X ˙ W Y B ¬ Y ˙ W I X I Y r A ¬ r ˙ W r ˙ Y ˙ W = Y I Y = DIsoC K W r ˙ DIsoB K W Y ˙ W
65 60 64 sseqtrrd K HL W H X B X ˙ W Y B ¬ Y ˙ W I X I Y r A ¬ r ˙ W r ˙ Y ˙ W = Y DIsoC K W r I Y
66 39 fveq2d K HL W H X B X ˙ W Y B ¬ Y ˙ W I X I Y r A ¬ r ˙ W r ˙ Y ˙ W = Y DIsoB K W r ˙ X ˙ W = DIsoB K W X
67 1 2 3 9 41 dihvalb K HL W H X B X ˙ W I X = DIsoB K W X
68 25 37 67 syl2anc K HL W H X B X ˙ W Y B ¬ Y ˙ W I X I Y r A ¬ r ˙ W r ˙ Y ˙ W = Y I X = DIsoB K W X
69 66 68 eqtr4d K HL W H X B X ˙ W Y B ¬ Y ˙ W I X I Y r A ¬ r ˙ W r ˙ Y ˙ W = Y DIsoB K W r ˙ X ˙ W = I X
70 simp2 K HL W H X B X ˙ W Y B ¬ Y ˙ W I X I Y r A ¬ r ˙ W r ˙ Y ˙ W = Y I X I Y
71 69 70 eqsstrd K HL W H X B X ˙ W Y B ¬ Y ˙ W I X I Y r A ¬ r ˙ W r ˙ Y ˙ W = Y DIsoB K W r ˙ X ˙ W I Y
72 1 5 latmcl K Lat r ˙ X B W B r ˙ X ˙ W B
73 15 21 31 72 syl3anc K HL W H X B X ˙ W Y B ¬ Y ˙ W I X I Y r A ¬ r ˙ W r ˙ Y ˙ W = Y r ˙ X ˙ W B
74 1 2 5 latmle2 K Lat r ˙ X B W B r ˙ X ˙ W ˙ W
75 15 21 31 74 syl3anc K HL W H X B X ˙ W Y B ¬ Y ˙ W I X I Y r A ¬ r ˙ W r ˙ Y ˙ W = Y r ˙ X ˙ W ˙ W
76 1 2 3 7 41 46 diblss K HL W H r ˙ X ˙ W B r ˙ X ˙ W ˙ W DIsoB K W r ˙ X ˙ W LSubSp U
77 25 73 75 76 syl12anc K HL W H X B X ˙ W Y B ¬ Y ˙ W I X I Y r A ¬ r ˙ W r ˙ Y ˙ W = Y DIsoB K W r ˙ X ˙ W LSubSp U
78 48 77 sseldd K HL W H X B X ˙ W Y B ¬ Y ˙ W I X I Y r A ¬ r ˙ W r ˙ Y ˙ W = Y DIsoB K W r ˙ X ˙ W SubGrp U
79 1 3 9 7 46 dihlss K HL W H Y B I Y LSubSp U
80 25 22 79 syl2anc K HL W H X B X ˙ W Y B ¬ Y ˙ W I X I Y r A ¬ r ˙ W r ˙ Y ˙ W = Y I Y LSubSp U
81 48 80 sseldd K HL W H X B X ˙ W Y B ¬ Y ˙ W I X I Y r A ¬ r ˙ W r ˙ Y ˙ W = Y I Y SubGrp U
82 8 lsmlub DIsoC K W r SubGrp U DIsoB K W r ˙ X ˙ W SubGrp U I Y SubGrp U DIsoC K W r I Y DIsoB K W r ˙ X ˙ W I Y DIsoC K W r ˙ DIsoB K W r ˙ X ˙ W I Y
83 51 78 81 82 syl3anc K HL W H X B X ˙ W Y B ¬ Y ˙ W I X I Y r A ¬ r ˙ W r ˙ Y ˙ W = Y DIsoC K W r I Y DIsoB K W r ˙ X ˙ W I Y DIsoC K W r ˙ DIsoB K W r ˙ X ˙ W I Y
84 65 71 83 mpbi2and K HL W H X B X ˙ W Y B ¬ Y ˙ W I X I Y r A ¬ r ˙ W r ˙ Y ˙ W = Y DIsoC K W r ˙ DIsoB K W r ˙ X ˙ W I Y
85 44 84 eqsstrd K HL W H X B X ˙ W Y B ¬ Y ˙ W I X I Y r A ¬ r ˙ W r ˙ Y ˙ W = Y I r ˙ X I Y
86 1 2 3 9 dihord4 K HL W H r ˙ X B ¬ r ˙ X ˙ W Y B ¬ Y ˙ W I r ˙ X I Y r ˙ X ˙ Y
87 25 21 35 61 86 syl121anc K HL W H X B X ˙ W Y B ¬ Y ˙ W I X I Y r A ¬ r ˙ W r ˙ Y ˙ W = Y I r ˙ X I Y r ˙ X ˙ Y
88 85 87 mpbid K HL W H X B X ˙ W Y B ¬ Y ˙ W I X I Y r A ¬ r ˙ W r ˙ Y ˙ W = Y r ˙ X ˙ Y
89 1 2 15 16 21 22 24 88 lattrd K HL W H X B X ˙ W Y B ¬ Y ˙ W I X I Y r A ¬ r ˙ W r ˙ Y ˙ W = Y X ˙ Y
90 89 3expia K HL W H X B X ˙ W Y B ¬ Y ˙ W I X I Y r A ¬ r ˙ W r ˙ Y ˙ W = Y X ˙ Y
91 90 exp4c K HL W H X B X ˙ W Y B ¬ Y ˙ W I X I Y r A ¬ r ˙ W r ˙ Y ˙ W = Y X ˙ Y
92 91 imp4a K HL W H X B X ˙ W Y B ¬ Y ˙ W I X I Y r A ¬ r ˙ W r ˙ Y ˙ W = Y X ˙ Y
93 92 rexlimdv K HL W H X B X ˙ W Y B ¬ Y ˙ W I X I Y r A ¬ r ˙ W r ˙ Y ˙ W = Y X ˙ Y
94 13 93 mpd K HL W H X B X ˙ W Y B ¬ Y ˙ W I X I Y X ˙ Y