Metamath Proof Explorer


Theorem osumcllem9N

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 osumcllem9N K HL X C Y C X ˙ Y X p U ¬ p X + ˙ Y M = X

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 inass ˙ X U M = ˙ X U M
10 simp11 K HL X C Y C X ˙ Y X p U ¬ p X + ˙ Y K HL
11 simp13 K HL X C Y C X ˙ Y X p U ¬ p X + ˙ Y Y C
12 simp21 K HL X C Y C X ˙ Y X p U ¬ p X + ˙ Y X ˙ Y
13 1 2 3 4 5 6 7 8 osumcllem3N K HL Y C X ˙ Y ˙ X U = Y
14 10 11 12 13 syl3anc K HL X C Y C X ˙ Y X p U ¬ p X + ˙ Y ˙ X U = Y
15 14 ineq1d K HL X C Y C X ˙ Y X p U ¬ p X + ˙ Y ˙ X U M = Y M
16 9 15 eqtr3id K HL X C Y C X ˙ Y X p U ¬ p X + ˙ Y ˙ X U M = Y M
17 simp12 K HL X C Y C X ˙ Y X p U ¬ p X + ˙ Y X C
18 3 6 psubclssatN K HL X C X A
19 10 17 18 syl2anc K HL X C Y C X ˙ Y X p U ¬ p X + ˙ Y X A
20 3 6 psubclssatN K HL Y C Y A
21 10 11 20 syl2anc K HL X C Y C X ˙ Y X p U ¬ p X + ˙ Y Y A
22 simp22 K HL X C Y C X ˙ Y X p U ¬ p X + ˙ Y X
23 3 4 paddssat K HL X A Y A X + ˙ Y A
24 10 19 21 23 syl3anc K HL X C Y C X ˙ Y X p U ¬ p X + ˙ Y X + ˙ Y A
25 3 5 polssatN K HL X + ˙ Y A ˙ X + ˙ Y A
26 10 24 25 syl2anc K HL X C Y C X ˙ Y X p U ¬ p X + ˙ Y ˙ X + ˙ Y A
27 3 5 polssatN K HL ˙ X + ˙ Y A ˙ ˙ X + ˙ Y A
28 10 26 27 syl2anc K HL X C Y C X ˙ Y X p U ¬ p X + ˙ Y ˙ ˙ X + ˙ Y A
29 8 28 eqsstrid K HL X C Y C X ˙ Y X p U ¬ p X + ˙ Y U A
30 simp23 K HL X C Y C X ˙ Y X p U ¬ p X + ˙ Y p U
31 29 30 sseldd K HL X C Y C X ˙ Y X p U ¬ p X + ˙ Y p A
32 simp3 K HL X C Y C X ˙ Y X p U ¬ p X + ˙ Y ¬ p X + ˙ Y
33 1 2 3 4 5 6 7 8 osumcllem8N K HL X A Y A X ˙ Y X p A ¬ p X + ˙ Y Y M =
34 10 19 21 12 22 31 32 33 syl331anc K HL X C Y C X ˙ Y X p U ¬ p X + ˙ Y Y M =
35 16 34 eqtrd K HL X C Y C X ˙ Y X p U ¬ p X + ˙ Y ˙ X U M =
36 35 fveq2d K HL X C Y C X ˙ Y X p U ¬ p X + ˙ Y ˙ ˙ X U M = ˙
37 3 5 pol0N K HL ˙ = A
38 10 37 syl K HL X C Y C X ˙ Y X p U ¬ p X + ˙ Y ˙ = A
39 36 38 eqtrd K HL X C Y C X ˙ Y X p U ¬ p X + ˙ Y ˙ ˙ X U M = A
40 1 2 3 4 5 6 7 8 osumcllem1N K HL X A Y A p U U M = M
41 10 19 21 30 40 syl31anc K HL X C Y C X ˙ Y X p U ¬ p X + ˙ Y U M = M
42 39 41 ineq12d K HL X C Y C X ˙ Y X p U ¬ p X + ˙ Y ˙ ˙ X U M U M = A M
43 3 5 6 polsubclN K HL ˙ X + ˙ Y A ˙ ˙ X + ˙ Y C
44 10 26 43 syl2anc K HL X C Y C X ˙ Y X p U ¬ p X + ˙ Y ˙ ˙ X + ˙ Y C
45 8 44 eqeltrid K HL X C Y C X ˙ Y X p U ¬ p X + ˙ Y U C
46 3 4 6 paddatclN K HL X C p A X + ˙ p C
47 10 17 31 46 syl3anc K HL X C Y C X ˙ Y X p U ¬ p X + ˙ Y X + ˙ p C
48 7 47 eqeltrid K HL X C Y C X ˙ Y X p U ¬ p X + ˙ Y M C
49 6 psubclinN K HL U C M C U M C
50 10 45 48 49 syl3anc K HL X C Y C X ˙ Y X p U ¬ p X + ˙ Y U M C
51 1 2 3 4 5 6 7 8 osumcllem2N K HL X A Y A p U X U M
52 10 19 21 30 51 syl31anc K HL X C Y C X ˙ Y X p U ¬ p X + ˙ Y X U M
53 6 5 poml6N K HL X C U M C X U M ˙ ˙ X U M U M = X
54 10 17 50 52 53 syl31anc K HL X C Y C X ˙ Y X p U ¬ p X + ˙ Y ˙ ˙ X U M U M = X
55 31 snssd K HL X C Y C X ˙ Y X p U ¬ p X + ˙ Y p A
56 3 4 paddssat K HL X A p A X + ˙ p A
57 10 19 55 56 syl3anc K HL X C Y C X ˙ Y X p U ¬ p X + ˙ Y X + ˙ p A
58 7 57 eqsstrid K HL X C Y C X ˙ Y X p U ¬ p X + ˙ Y M A
59 sseqin2 M A A M = M
60 58 59 sylib K HL X C Y C X ˙ Y X p U ¬ p X + ˙ Y A M = M
61 42 54 60 3eqtr3rd K HL X C Y C X ˙ Y X p U ¬ p X + ˙ Y M = X