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 e. CH
Assertion chirredlem2 
|- ( ( ( ( p e. HAtoms /\ p C_ A ) /\ ( q e. CH /\ q C_ ( _|_ ` A ) ) ) /\ ( ( r e. HAtoms /\ r C_ A ) /\ r C_ ( p vH q ) ) ) -> ( ( _|_ ` r ) i^i ( p vH q ) ) = q )

Proof

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