Metamath Proof Explorer


Theorem osumcllem4N

Description: Lemma for osumclN . (Contributed by NM, 24-Mar-2012) (New usage is discouraged.)

Ref Expression
Hypotheses osumcllem.l ˙ = K
osumcllem.j ˙ = join K
osumcllem.a A = Atoms K
osumcllem.p + ˙ = + 𝑃 K
osumcllem.o ˙ = 𝑃 K
osumcllem.c C = PSubCl K
osumcllem.m M = X + ˙ p
osumcllem.u U = ˙ ˙ X + ˙ Y
Assertion osumcllem4N K HL Y A X ˙ Y r X q Y q r

Proof

Step Hyp Ref Expression
1 osumcllem.l ˙ = K
2 osumcllem.j ˙ = join K
3 osumcllem.a A = Atoms K
4 osumcllem.p + ˙ = + 𝑃 K
5 osumcllem.o ˙ = 𝑃 K
6 osumcllem.c C = PSubCl K
7 osumcllem.m M = X + ˙ p
8 osumcllem.u U = ˙ ˙ X + ˙ Y
9 n0i r X Y ¬ X Y =
10 incom X Y = Y X
11 sslin X ˙ Y Y X Y ˙ Y
12 11 3ad2ant3 K HL Y A X ˙ Y Y X Y ˙ Y
13 10 12 eqsstrid K HL Y A X ˙ Y X Y Y ˙ Y
14 3 5 pnonsingN K HL Y A Y ˙ Y =
15 14 3adant3 K HL Y A X ˙ Y Y ˙ Y =
16 13 15 sseqtrd K HL Y A X ˙ Y X Y
17 ss0b X Y X Y =
18 16 17 sylib K HL Y A X ˙ Y X Y =
19 18 adantr K HL Y A X ˙ Y r X q Y X Y =
20 9 19 nsyl3 K HL Y A X ˙ Y r X q Y ¬ r X Y
21 simprr K HL Y A X ˙ Y r X q Y q Y
22 eleq1w q = r q Y r Y
23 21 22 syl5ibcom K HL Y A X ˙ Y r X q Y q = r r Y
24 simprl K HL Y A X ˙ Y r X q Y r X
25 23 24 jctild K HL Y A X ˙ Y r X q Y q = r r X r Y
26 elin r X Y r X r Y
27 25 26 syl6ibr K HL Y A X ˙ Y r X q Y q = r r X Y
28 27 necon3bd K HL Y A X ˙ Y r X q Y ¬ r X Y q r
29 20 28 mpd K HL Y A X ˙ Y r X q Y q r