# Metamath Proof Explorer

## Theorem cdlemg10

Description: TODO: FIX COMMENT. (Contributed by NM, 4-May-2013)

Ref Expression
Hypotheses cdlemg8.l
cdlemg8.j
cdlemg8.m
cdlemg8.a $⊢ A = Atoms ⁡ K$
cdlemg8.h $⊢ H = LHyp ⁡ K$
cdlemg8.t $⊢ T = LTrn ⁡ K ⁡ W$
cdlemg10.r $⊢ R = trL ⁡ K ⁡ W$
Assertion cdlemg10

### Proof

Step Hyp Ref Expression
1 cdlemg8.l
2 cdlemg8.j
3 cdlemg8.m
4 cdlemg8.a $⊢ A = Atoms ⁡ K$
5 cdlemg8.h $⊢ H = LHyp ⁡ K$
6 cdlemg8.t $⊢ T = LTrn ⁡ K ⁡ W$
7 cdlemg10.r $⊢ R = trL ⁡ K ⁡ W$
8 eqid $⊢ Base K = Base K$
9 simp11l
10 9 hllatd
11 simp12l
12 simp11
13 simp21
14 simp22
15 1 4 5 6 ltrnat $⊢ K ∈ HL ∧ W ∈ H ∧ G ∈ T ∧ P ∈ A → G ⁡ P ∈ A$
16 12 14 11 15 syl3anc
17 1 4 5 6 ltrnat $⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ G ⁡ P ∈ A → F ⁡ G ⁡ P ∈ A$
18 12 13 16 17 syl3anc
19 8 2 4 hlatjcl
20 9 11 18 19 syl3anc
21 simp13l
22 1 4 5 6 ltrnat $⊢ K ∈ HL ∧ W ∈ H ∧ G ∈ T ∧ Q ∈ A → G ⁡ Q ∈ A$
23 12 14 21 22 syl3anc
24 1 4 5 6 ltrnat $⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ G ⁡ Q ∈ A → F ⁡ G ⁡ Q ∈ A$
25 12 13 23 24 syl3anc
26 8 2 4 hlatjcl
27 9 21 25 26 syl3anc
28 8 3 latmcl
29 10 20 27 28 syl3anc
30 8 5 6 7 trlcl $⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T → R ⁡ F ∈ Base K$
31 12 13 30 syl2anc
32 8 5 6 7 trlcl $⊢ K ∈ HL ∧ W ∈ H ∧ G ∈ T → R ⁡ G ∈ Base K$
33 12 14 32 syl2anc
34 8 2 latjcl
35 10 31 33 34 syl3anc
36 simp11r
37 8 5 lhpbase $⊢ W ∈ H → W ∈ Base K$
38 36 37 syl
39 1 2 3 4 5 6 7 cdlemg10a
40 1 5 6 7 trlle
41 12 13 40 syl2anc
42 1 5 6 7 trlle
43 12 14 42 syl2anc
44 8 1 2 latjle12
45 10 31 33 38 44 syl13anc
46 41 43 45 mpbi2and
47 8 1 10 29 35 38 39 46 lattrd