# Metamath Proof Explorer

## Theorem cdlemg6c

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

Ref Expression
Hypotheses cdlemg4.l
cdlemg4.a ${⊢}{A}=\mathrm{Atoms}\left({K}\right)$
cdlemg4.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
cdlemg4.t ${⊢}{T}=\mathrm{LTrn}\left({K}\right)\left({W}\right)$
cdlemg4.r ${⊢}{R}=\mathrm{trL}\left({K}\right)\left({W}\right)$
cdlemg4.j
cdlemg4b.v ${⊢}{V}={R}\left({G}\right)$
Assertion cdlemg6c

### Proof

Step Hyp Ref Expression
1 cdlemg4.l
2 cdlemg4.a ${⊢}{A}=\mathrm{Atoms}\left({K}\right)$
3 cdlemg4.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
4 cdlemg4.t ${⊢}{T}=\mathrm{LTrn}\left({K}\right)\left({W}\right)$
5 cdlemg4.r ${⊢}{R}=\mathrm{trL}\left({K}\right)\left({W}\right)$
6 cdlemg4.j
7 cdlemg4b.v ${⊢}{V}={R}\left({G}\right)$
8 simpl1
9 simprl
10 simpl22
11 simpl23
12 simpl31
13 simprr
14 simpl1l
15 simp22l
17 simprll
18 eqid ${⊢}{\mathrm{Base}}_{{K}}={\mathrm{Base}}_{{K}}$
19 18 3 4 5 trlcl ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {G}\in {T}\right)\to {R}\left({G}\right)\in {\mathrm{Base}}_{{K}}$
20 8 12 19 syl2anc
21 7 20 eqeltrid
22 simp22r
24 1 3 4 5 trlle
25 8 12 24 syl2anc
26 7 25 eqbrtrid
27 simp1l
28 27 hllatd
30 18 2 atbase ${⊢}{Q}\in {A}\to {Q}\in {\mathrm{Base}}_{{K}}$
31 15 30 syl
33 simp1r
34 18 3 lhpbase ${⊢}{W}\in {H}\to {W}\in {\mathrm{Base}}_{{K}}$
35 33 34 syl
37 18 1 lattr
38 29 32 21 36 37 syl13anc
39 26 38 mpan2d
40 23 39 mtod
41 18 1 6 2 hlexch2
42 14 16 17 21 40 41 syl131anc
43 simpl32
44 simp21l
46 18 2 atbase ${⊢}{P}\in {A}\to {P}\in {\mathrm{Base}}_{{K}}$
47 45 46 syl
48 18 1 6 latlej2
49 29 47 21 48 syl3anc
50 18 6 latjcl
51 29 47 21 50 syl3anc
52 18 1 6 latjle12
53 29 32 21 51 52 syl13anc
54 43 49 53 mpbi2and
55 18 2 atbase ${⊢}{r}\in {A}\to {r}\in {\mathrm{Base}}_{{K}}$
56 17 55 syl
57 18 6 latjcl
58 29 32 21 57 syl3anc
59 18 1 lattr
60 29 56 58 51 59 syl13anc
61 54 60 mpan2d
62 42 61 syld
63 13 62 mtod
64 simpl21
65 simpl33
66 1 2 3 4 5 6 7 cdlemg6a
67 8 64 9 11 12 13 65 66 syl133anc
68 1 2 3 4 5 6 7 cdlemg6b
69 8 9 10 11 12 63 67 68 syl133anc
70 69 ex