# Metamath Proof Explorer

Description: Lemma for paddass . The case when x = y . (Contributed by NM, 11-Jan-2012)

Ref Expression
paddasslem.a ${⊢}{A}=\mathrm{Atoms}\left({K}\right)$

### Proof

Step Hyp Ref Expression
3 paddasslem.a ${⊢}{A}=\mathrm{Atoms}\left({K}\right)$
5 simpl1l
6 simpl21
7 simpl22
9 5 6 7 8 syl3anc
10 simpl23
11 5 9 10 3jca
13 5 7 6 12 syl3anc
15 11 13 14 sylc
16 5 hllatd
17 simprll
18 simprlr
19 simpl3l
20 eqid ${⊢}{\mathrm{Base}}_{{K}}={\mathrm{Base}}_{{K}}$
21 20 3 atbase ${⊢}{p}\in {A}\to {p}\in {\mathrm{Base}}_{{K}}$
22 19 21 syl
23 7 17 sseldd
24 20 3 atbase ${⊢}{y}\in {A}\to {y}\in {\mathrm{Base}}_{{K}}$
25 23 24 syl
26 simpl3r
27 20 3 atbase ${⊢}{r}\in {A}\to {r}\in {\mathrm{Base}}_{{K}}$
28 26 27 syl
29 20 2 latjcl
30 16 25 28 29 syl3anc
31 10 18 sseldd
32 20 3 atbase ${⊢}{z}\in {A}\to {z}\in {\mathrm{Base}}_{{K}}$
33 31 32 syl
34 20 2 latjcl
35 16 25 33 34 syl3anc
36 simpl1r
37 simprrl
38 oveq1
39 38 breq2d
40 39 biimpa
41 36 37 40 syl2anc
42 20 1 2 latlej1
43 16 25 33 42 syl3anc
44 simprrr
45 20 1 2 latjle12
46 16 25 28 35 45 syl13anc
47 43 44 46 mpbi2and
48 20 1 16 22 30 35 41 47 lattrd
49 1 2 3 4 elpaddri
50 16 7 10 17 18 19 48 49 syl322anc
51 15 50 sseldd