# Metamath Proof Explorer

## Theorem cdlemg2m

Description: TODO: FIX COMMENT. (Contributed by NM, 25-Apr-2013)

Ref Expression
Hypotheses cdlemg2inv.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
cdlemg2inv.t ${⊢}{T}=\mathrm{LTrn}\left({K}\right)\left({W}\right)$
cdlemg2j.l
cdlemg2j.j
cdlemg2j.a ${⊢}{A}=\mathrm{Atoms}\left({K}\right)$
cdlemg2j.m
cdlemg2j.u
Assertion cdlemg2m

### Proof

Step Hyp Ref Expression
1 cdlemg2inv.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
2 cdlemg2inv.t ${⊢}{T}=\mathrm{LTrn}\left({K}\right)\left({W}\right)$
3 cdlemg2j.l
4 cdlemg2j.j
5 cdlemg2j.a ${⊢}{A}=\mathrm{Atoms}\left({K}\right)$
6 cdlemg2j.m
7 cdlemg2j.u
8 1 2 3 4 5 6 7 cdlemg2k
9 8 oveq1d
10 simp1
11 simp3
12 simp2l
13 eqid ${⊢}\mathrm{0.}\left({K}\right)=\mathrm{0.}\left({K}\right)$
14 3 6 13 5 1 2 ltrnmw
15 10 11 12 14 syl3anc
16 15 oveq1d
17 simp1l
18 3 5 1 2 ltrnel
19 10 11 12 18 syl3anc
20 19 simpld
21 simp1r
22 simp2ll
23 simp2rl
24 eqid ${⊢}{\mathrm{Base}}_{{K}}={\mathrm{Base}}_{{K}}$
25 3 4 6 5 1 7 24 cdleme0aa ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {P}\in {A}\wedge {Q}\in {A}\right)\to {U}\in {\mathrm{Base}}_{{K}}$
26 17 21 22 23 25 syl211anc
27 24 1 lhpbase ${⊢}{W}\in {H}\to {W}\in {\mathrm{Base}}_{{K}}$
28 21 27 syl
29 17 hllatd
30 24 4 5 hlatjcl
31 17 22 23 30 syl3anc
32 24 3 6 latmle2
33 29 31 28 32 syl3anc
34 7 33 eqbrtrid
35 24 3 4 6 5 atmod4i2
36 17 20 26 28 34 35 syl131anc
37 hlol ${⊢}{K}\in \mathrm{HL}\to {K}\in \mathrm{OL}$
38 17 37 syl
39 24 4 13 olj02
40 38 26 39 syl2anc
41 16 36 40 3eqtr3d
42 9 41 eqtrd