Metamath Proof Explorer


Theorem chirredlem2

Description: Lemma for chirredi . (Contributed by NM, 15-Jun-2006) (New usage is discouraged.)

Ref Expression
Hypothesis chirred.1 A C
Assertion chirredlem2 p HAtoms p A q C q A r HAtoms r A r p q r p q = q

Proof

Step Hyp Ref Expression
1 chirred.1 A C
2 atelch p HAtoms p C
3 chjcom p C q C p q = q p
4 2 3 sylan p HAtoms q C p q = q p
5 4 ad2ant2r p HAtoms p A q C q A p q = q p
6 5 adantr p HAtoms p A q C q A r HAtoms r A r p q p q = q p
7 6 ineq2d p HAtoms p A q C q A r HAtoms r A r p q r p q = r q p
8 atelch r HAtoms r C
9 choccl r C r C
10 8 9 syl r HAtoms r C
11 id q C q C
12 10 11 2 3anim123i r HAtoms q C p HAtoms r C q C p C
13 12 3com13 p HAtoms q C r HAtoms r C q C p C
14 13 3expa p HAtoms q C r HAtoms r C q C p C
15 14 adantllr p HAtoms p A q C r HAtoms r C q C p C
16 15 adantlrr p HAtoms p A q C q A r HAtoms r C q C p C
17 16 adantrr p HAtoms p A q C q A r HAtoms r A r C q C p C
18 17 adantrr p HAtoms p A q C q A r HAtoms r A r p q r C q C p C
19 simpll q C q A r HAtoms r A q C
20 10 ad2antrl q C q A r HAtoms r A r C
21 chsscon3 r C A C r A A r
22 8 1 21 sylancl r HAtoms r A A r
23 22 biimpa r HAtoms r A A r
24 sstr q A A r q r
25 23 24 sylan2 q A r HAtoms r A q r
26 25 adantll q C q A r HAtoms r A q r
27 lecm q C r C q r q 𝐶 r
28 19 20 26 27 syl3anc q C q A r HAtoms r A q 𝐶 r
29 28 ad2ant2lr p HAtoms p A q C q A r HAtoms r A r p q q 𝐶 r
30 chsscon3 p C A C p A A p
31 1 30 mpan2 p C p A A p
32 31 biimpa p C p A A p
33 sstr q A A p q p
34 32 33 sylan2 q A p C p A q p
35 34 an12s p C q A p A q p
36 35 ancom2s p C p A q A q p
37 36 adantll q C p C p A q A q p
38 choccl p C p C
39 lecm q C p C q p q 𝐶 p
40 38 39 syl3an2 q C p C q p q 𝐶 p
41 40 3expia q C p C q p q 𝐶 p
42 cmcm2 q C p C q 𝐶 p q 𝐶 p
43 41 42 sylibrd q C p C q p q 𝐶 p
44 43 adantr q C p C p A q A q p q 𝐶 p
45 37 44 mpd q C p C p A q A q 𝐶 p
46 2 45 sylanl2 q C p HAtoms p A q A q 𝐶 p
47 46 ancom1s p HAtoms q C p A q A q 𝐶 p
48 47 an4s p HAtoms p A q C q A q 𝐶 p
49 48 adantr p HAtoms p A q C q A r HAtoms r A r p q q 𝐶 p
50 fh2 r C q C p C q 𝐶 r q 𝐶 p r q p = r q r p
51 18 29 49 50 syl12anc p HAtoms p A q C q A r HAtoms r A r p q r q p = r q r p
52 sseqin2 q r r q = q
53 26 52 sylib q C q A r HAtoms r A r q = q
54 53 ad2ant2lr p HAtoms p A q C q A r HAtoms r A r p q r q = q
55 incom r p = p r
56 1 chirredlem1 p HAtoms q C q A r HAtoms r A r p q p r = 0
57 56 adantllr p HAtoms p A q C q A r HAtoms r A r p q p r = 0
58 55 57 syl5eq p HAtoms p A q C q A r HAtoms r A r p q r p = 0
59 54 58 oveq12d p HAtoms p A q C q A r HAtoms r A r p q r q r p = q 0
60 chj0 q C q 0 = q
61 60 adantr q C q A q 0 = q
62 61 ad2antlr p HAtoms p A q C q A r HAtoms r A r p q q 0 = q
63 59 62 eqtrd p HAtoms p A q C q A r HAtoms r A r p q r q r p = q
64 7 51 63 3eqtrd p HAtoms p A q C q A r HAtoms r A r p q r p q = q