# Metamath Proof Explorer

## Theorem dia2dimlem3

Description: Lemma for dia2dim . Define a translation D whose trace is atom V . Part of proof of Lemma M in Crawley p. 121 line 5. (Contributed by NM, 8-Sep-2014)

Ref Expression
Hypotheses dia2dimlem3.l
dia2dimlem3.j
dia2dimlem3.m
dia2dimlem3.a ${⊢}{A}=\mathrm{Atoms}\left({K}\right)$
dia2dimlem3.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
dia2dimlem3.t ${⊢}{T}=\mathrm{LTrn}\left({K}\right)\left({W}\right)$
dia2dimlem3.r ${⊢}{R}=\mathrm{trL}\left({K}\right)\left({W}\right)$
dia2dimlem3.q
dia2dimlem3.k ${⊢}{\phi }\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
dia2dimlem3.u
dia2dimlem3.v
dia2dimlem3.p
dia2dimlem3.f ${⊢}{\phi }\to \left({F}\in {T}\wedge {F}\left({P}\right)\ne {P}\right)$
dia2dimlem3.rf
dia2dimlem3.uv ${⊢}{\phi }\to {U}\ne {V}$
dia2dimlem3.ru ${⊢}{\phi }\to {R}\left({F}\right)\ne {U}$
dia2dimlem3.rv ${⊢}{\phi }\to {R}\left({F}\right)\ne {V}$
dia2dimlem3.d ${⊢}{\phi }\to {D}\in {T}$
dia2dimlem3.dv ${⊢}{\phi }\to {D}\left({Q}\right)={F}\left({P}\right)$
Assertion dia2dimlem3 ${⊢}{\phi }\to {R}\left({D}\right)={V}$

### Proof

Step Hyp Ref Expression
1 dia2dimlem3.l
2 dia2dimlem3.j
3 dia2dimlem3.m
4 dia2dimlem3.a ${⊢}{A}=\mathrm{Atoms}\left({K}\right)$
5 dia2dimlem3.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
6 dia2dimlem3.t ${⊢}{T}=\mathrm{LTrn}\left({K}\right)\left({W}\right)$
7 dia2dimlem3.r ${⊢}{R}=\mathrm{trL}\left({K}\right)\left({W}\right)$
8 dia2dimlem3.q
9 dia2dimlem3.k ${⊢}{\phi }\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
10 dia2dimlem3.u
11 dia2dimlem3.v
12 dia2dimlem3.p
13 dia2dimlem3.f ${⊢}{\phi }\to \left({F}\in {T}\wedge {F}\left({P}\right)\ne {P}\right)$
14 dia2dimlem3.rf
15 dia2dimlem3.uv ${⊢}{\phi }\to {U}\ne {V}$
16 dia2dimlem3.ru ${⊢}{\phi }\to {R}\left({F}\right)\ne {U}$
17 dia2dimlem3.rv ${⊢}{\phi }\to {R}\left({F}\right)\ne {V}$
18 dia2dimlem3.d ${⊢}{\phi }\to {D}\in {T}$
19 dia2dimlem3.dv ${⊢}{\phi }\to {D}\left({Q}\right)={F}\left({P}\right)$
20 9 simpld ${⊢}{\phi }\to {K}\in \mathrm{HL}$
21 13 simpld ${⊢}{\phi }\to {F}\in {T}$
22 1 4 5 6 ltrnel
23 9 21 12 22 syl3anc
24 23 simpld ${⊢}{\phi }\to {F}\left({P}\right)\in {A}$
25 11 simpld ${⊢}{\phi }\to {V}\in {A}$
26 1 2 4 hlatlej2
27 20 24 25 26 syl3anc
28 20 hllatd ${⊢}{\phi }\to {K}\in \mathrm{Lat}$
29 eqid ${⊢}{\mathrm{Base}}_{{K}}={\mathrm{Base}}_{{K}}$
30 29 4 atbase ${⊢}{V}\in {A}\to {V}\in {\mathrm{Base}}_{{K}}$
31 25 30 syl ${⊢}{\phi }\to {V}\in {\mathrm{Base}}_{{K}}$
32 29 2 4 hlatjcl
33 20 24 25 32 syl3anc
34 1 4 5 6 7 trlat
35 9 12 13 34 syl3anc ${⊢}{\phi }\to {R}\left({F}\right)\in {A}$
36 10 simpld ${⊢}{\phi }\to {U}\in {A}$
37 29 2 4 hlatjcl
38 20 35 36 37 syl3anc
39 29 1 3 latmlem2
40 28 31 33 38 39 syl13anc
41 27 40 mpd
42 2 4 hlatjcom
43 20 36 25 42 syl3anc
44 14 43 breqtrd
45 1 2 4 hlatexch2
46 20 35 25 36 16 45 syl131anc
47 44 46 mpd
48 29 1 3 latleeqm2
49 28 31 38 48 syl3anc
50 47 49 mpbid
51 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 dia2dimlem1
52 1 2 3 4 5 6 7 trlval2
53 9 18 51 52 syl3anc
54 8 a1i
55 54 19 oveq12d
56 12 simpld ${⊢}{\phi }\to {P}\in {A}$
57 29 2 4 hlatjcl
58 20 56 36 57 syl3anc
59 1 2 4 hlatlej1
60 20 24 25 59 syl3anc
61 29 1 2 3 4 atmod4i1
62 20 24 58 33 60 61 syl131anc
63 2 4 hlatj32
64 20 56 36 24 63 syl13anc
65 64 oveq1d
66 55 62 65 3eqtrd
67 66 oveq1d
68 hlol ${⊢}{K}\in \mathrm{HL}\to {K}\in \mathrm{OL}$
69 20 68 syl ${⊢}{\phi }\to {K}\in \mathrm{OL}$
70 29 2 4 hlatjcl
71 20 56 24 70 syl3anc
72 29 4 atbase ${⊢}{U}\in {A}\to {U}\in {\mathrm{Base}}_{{K}}$
73 36 72 syl ${⊢}{\phi }\to {U}\in {\mathrm{Base}}_{{K}}$
74 29 2 latjcl
75 28 71 73 74 syl3anc
76 9 simprd ${⊢}{\phi }\to {W}\in {H}$
77 29 5 lhpbase ${⊢}{W}\in {H}\to {W}\in {\mathrm{Base}}_{{K}}$
78 76 77 syl ${⊢}{\phi }\to {W}\in {\mathrm{Base}}_{{K}}$
79 29 3 latm32
80 69 75 33 78 79 syl13anc
81 1 2 3 4 5 6 7 trlval2
82 9 21 12 81 syl3anc
83 82 oveq1d
84 10 simprd
85 29 1 2 3 4 atmod4i1
86 20 36 71 78 84 85 syl131anc
87 83 86 eqtr2d
88 87 oveq1d
89 67 80 88 3eqtrd
90 53 89 eqtr2d
91 41 50 90 3brtr3d
92 hlatl ${⊢}{K}\in \mathrm{HL}\to {K}\in \mathrm{AtLat}$
93 20 92 syl ${⊢}{\phi }\to {K}\in \mathrm{AtLat}$
94 hlop ${⊢}{K}\in \mathrm{HL}\to {K}\in \mathrm{OP}$
95 20 94 syl ${⊢}{\phi }\to {K}\in \mathrm{OP}$
96 eqid ${⊢}\mathrm{0.}\left({K}\right)=\mathrm{0.}\left({K}\right)$
97 eqid ${⊢}{<}_{{K}}={<}_{{K}}$
98 96 97 4 0ltat ${⊢}\left({K}\in \mathrm{OP}\wedge {V}\in {A}\right)\to \mathrm{0.}\left({K}\right){<}_{{K}}{V}$
99 95 25 98 syl2anc ${⊢}{\phi }\to \mathrm{0.}\left({K}\right){<}_{{K}}{V}$
100 hlpos ${⊢}{K}\in \mathrm{HL}\to {K}\in \mathrm{Poset}$
101 20 100 syl ${⊢}{\phi }\to {K}\in \mathrm{Poset}$
102 29 96 op0cl ${⊢}{K}\in \mathrm{OP}\to \mathrm{0.}\left({K}\right)\in {\mathrm{Base}}_{{K}}$
103 95 102 syl ${⊢}{\phi }\to \mathrm{0.}\left({K}\right)\in {\mathrm{Base}}_{{K}}$
104 29 5 6 7 trlcl ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {D}\in {T}\right)\to {R}\left({D}\right)\in {\mathrm{Base}}_{{K}}$
105 9 18 104 syl2anc ${⊢}{\phi }\to {R}\left({D}\right)\in {\mathrm{Base}}_{{K}}$
106 29 1 97 pltletr
107 101 103 31 105 106 syl13anc
108 99 91 107 mp2and ${⊢}{\phi }\to \mathrm{0.}\left({K}\right){<}_{{K}}{R}\left({D}\right)$
109 29 97 96 opltn0 ${⊢}\left({K}\in \mathrm{OP}\wedge {R}\left({D}\right)\in {\mathrm{Base}}_{{K}}\right)\to \left(\mathrm{0.}\left({K}\right){<}_{{K}}{R}\left({D}\right)↔{R}\left({D}\right)\ne \mathrm{0.}\left({K}\right)\right)$
110 95 105 109 syl2anc ${⊢}{\phi }\to \left(\mathrm{0.}\left({K}\right){<}_{{K}}{R}\left({D}\right)↔{R}\left({D}\right)\ne \mathrm{0.}\left({K}\right)\right)$
111 108 110 mpbid ${⊢}{\phi }\to {R}\left({D}\right)\ne \mathrm{0.}\left({K}\right)$
112 111 neneqd ${⊢}{\phi }\to ¬{R}\left({D}\right)=\mathrm{0.}\left({K}\right)$
113 96 4 5 6 7 trlator0 ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {D}\in {T}\right)\to \left({R}\left({D}\right)\in {A}\vee {R}\left({D}\right)=\mathrm{0.}\left({K}\right)\right)$
114 9 18 113 syl2anc ${⊢}{\phi }\to \left({R}\left({D}\right)\in {A}\vee {R}\left({D}\right)=\mathrm{0.}\left({K}\right)\right)$
115 114 orcomd ${⊢}{\phi }\to \left({R}\left({D}\right)=\mathrm{0.}\left({K}\right)\vee {R}\left({D}\right)\in {A}\right)$
116 115 ord ${⊢}{\phi }\to \left(¬{R}\left({D}\right)=\mathrm{0.}\left({K}\right)\to {R}\left({D}\right)\in {A}\right)$
117 112 116 mpd ${⊢}{\phi }\to {R}\left({D}\right)\in {A}$
118 1 4 atcmp
119 93 25 117 118 syl3anc
120 91 119 mpbid ${⊢}{\phi }\to {V}={R}\left({D}\right)$
121 120 eqcomd ${⊢}{\phi }\to {R}\left({D}\right)={V}$