Metamath Proof Explorer


Theorem osumcllem11N

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

Ref Expression
Hypotheses osumcl.p + ˙ = + 𝑃 K
osumcl.o ˙ = 𝑃 K
osumcl.c C = PSubCl K
Assertion osumcllem11N K HL X C Y C X ˙ Y X X + ˙ Y = ˙ ˙ X + ˙ Y

Proof

Step Hyp Ref Expression
1 osumcl.p + ˙ = + 𝑃 K
2 osumcl.o ˙ = 𝑃 K
3 osumcl.c C = PSubCl K
4 nonconne ¬ X = X X X
5 simpl1 K HL X C Y C X ˙ Y X K HL
6 simpl2 K HL X C Y C X ˙ Y X X C
7 eqid Atoms K = Atoms K
8 7 3 psubclssatN K HL X C X Atoms K
9 5 6 8 syl2anc K HL X C Y C X ˙ Y X X Atoms K
10 simpl3 K HL X C Y C X ˙ Y X Y C
11 7 3 psubclssatN K HL Y C Y Atoms K
12 5 10 11 syl2anc K HL X C Y C X ˙ Y X Y Atoms K
13 7 1 paddssat K HL X Atoms K Y Atoms K X + ˙ Y Atoms K
14 5 9 12 13 syl3anc K HL X C Y C X ˙ Y X X + ˙ Y Atoms K
15 7 2 2polssN K HL X + ˙ Y Atoms K X + ˙ Y ˙ ˙ X + ˙ Y
16 5 14 15 syl2anc K HL X C Y C X ˙ Y X X + ˙ Y ˙ ˙ X + ˙ Y
17 df-pss X + ˙ Y ˙ ˙ X + ˙ Y X + ˙ Y ˙ ˙ X + ˙ Y X + ˙ Y ˙ ˙ X + ˙ Y
18 pssnel X + ˙ Y ˙ ˙ X + ˙ Y p p ˙ ˙ X + ˙ Y ¬ p X + ˙ Y
19 17 18 sylbir X + ˙ Y ˙ ˙ X + ˙ Y X + ˙ Y ˙ ˙ X + ˙ Y p p ˙ ˙ X + ˙ Y ¬ p X + ˙ Y
20 df-rex p ˙ ˙ X + ˙ Y ¬ p X + ˙ Y p p ˙ ˙ X + ˙ Y ¬ p X + ˙ Y
21 19 20 sylibr X + ˙ Y ˙ ˙ X + ˙ Y X + ˙ Y ˙ ˙ X + ˙ Y p ˙ ˙ X + ˙ Y ¬ p X + ˙ Y
22 eqid K = K
23 eqid join K = join K
24 eqid X + ˙ p = X + ˙ p
25 eqid ˙ ˙ X + ˙ Y = ˙ ˙ X + ˙ Y
26 22 23 7 1 2 3 24 25 osumcllem9N K HL X C Y C X ˙ Y X p ˙ ˙ X + ˙ Y ¬ p X + ˙ Y X + ˙ p = X
27 simp11 K HL X C Y C X ˙ Y X p ˙ ˙ X + ˙ Y ¬ p X + ˙ Y K HL
28 simp12 K HL X C Y C X ˙ Y X p ˙ ˙ X + ˙ Y ¬ p X + ˙ Y X C
29 27 28 8 syl2anc K HL X C Y C X ˙ Y X p ˙ ˙ X + ˙ Y ¬ p X + ˙ Y X Atoms K
30 simp13 K HL X C Y C X ˙ Y X p ˙ ˙ X + ˙ Y ¬ p X + ˙ Y Y C
31 27 30 11 syl2anc K HL X C Y C X ˙ Y X p ˙ ˙ X + ˙ Y ¬ p X + ˙ Y Y Atoms K
32 14 3adantr3 K HL X C Y C X ˙ Y X p ˙ ˙ X + ˙ Y X + ˙ Y Atoms K
33 32 3adant3 K HL X C Y C X ˙ Y X p ˙ ˙ X + ˙ Y ¬ p X + ˙ Y X + ˙ Y Atoms K
34 7 2 polssatN K HL X + ˙ Y Atoms K ˙ X + ˙ Y Atoms K
35 27 33 34 syl2anc K HL X C Y C X ˙ Y X p ˙ ˙ X + ˙ Y ¬ p X + ˙ Y ˙ X + ˙ Y Atoms K
36 7 2 polssatN K HL ˙ X + ˙ Y Atoms K ˙ ˙ X + ˙ Y Atoms K
37 27 35 36 syl2anc K HL X C Y C X ˙ Y X p ˙ ˙ X + ˙ Y ¬ p X + ˙ Y ˙ ˙ X + ˙ Y Atoms K
38 simp23 K HL X C Y C X ˙ Y X p ˙ ˙ X + ˙ Y ¬ p X + ˙ Y p ˙ ˙ X + ˙ Y
39 37 38 sseldd K HL X C Y C X ˙ Y X p ˙ ˙ X + ˙ Y ¬ p X + ˙ Y p Atoms K
40 simp3 K HL X C Y C X ˙ Y X p ˙ ˙ X + ˙ Y ¬ p X + ˙ Y ¬ p X + ˙ Y
41 22 23 7 1 2 3 24 25 osumcllem10N K HL X Atoms K Y Atoms K p Atoms K ¬ p X + ˙ Y X + ˙ p X
42 27 29 31 39 40 41 syl311anc K HL X C Y C X ˙ Y X p ˙ ˙ X + ˙ Y ¬ p X + ˙ Y X + ˙ p X
43 26 42 pm2.21ddne K HL X C Y C X ˙ Y X p ˙ ˙ X + ˙ Y ¬ p X + ˙ Y X = X X X
44 43 3exp K HL X C Y C X ˙ Y X p ˙ ˙ X + ˙ Y ¬ p X + ˙ Y X = X X X
45 44 3expd K HL X C Y C X ˙ Y X p ˙ ˙ X + ˙ Y ¬ p X + ˙ Y X = X X X
46 45 imp32 K HL X C Y C X ˙ Y X p ˙ ˙ X + ˙ Y ¬ p X + ˙ Y X = X X X
47 46 rexlimdv K HL X C Y C X ˙ Y X p ˙ ˙ X + ˙ Y ¬ p X + ˙ Y X = X X X
48 21 47 syl5 K HL X C Y C X ˙ Y X X + ˙ Y ˙ ˙ X + ˙ Y X + ˙ Y ˙ ˙ X + ˙ Y X = X X X
49 16 48 mpand K HL X C Y C X ˙ Y X X + ˙ Y ˙ ˙ X + ˙ Y X = X X X
50 49 necon1bd K HL X C Y C X ˙ Y X ¬ X = X X X X + ˙ Y = ˙ ˙ X + ˙ Y
51 4 50 mpi K HL X C Y C X ˙ Y X X + ˙ Y = ˙ ˙ X + ˙ Y