Metamath Proof Explorer

Theorem chirredlem1

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

Ref Expression
Hypothesis chirred.1 
|- A e. CH
Assertion 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 )

Proof

Step Hyp Ref Expression
1 chirred.1 
 |-  A e. CH
2 atelch 
 |-  ( r e. HAtoms -> r e. CH )
3 chsscon3 
 |-  ( ( r e. CH /\ A e. CH ) -> ( r C_ A <-> ( _|_ ` A ) C_ ( _|_ ` r ) ) )
4 1 3 mpan2 
 |-  ( r e. CH -> ( r C_ A <-> ( _|_ ` A ) C_ ( _|_ ` r ) ) )
5 4 biimpa 
 |-  ( ( r e. CH /\ r C_ A ) -> ( _|_ ` A ) C_ ( _|_ ` r ) )
6 2 5 sylan 
 |-  ( ( r e. HAtoms /\ r C_ A ) -> ( _|_ ` A ) C_ ( _|_ ` r ) )
7 sstr2 
 |-  ( q C_ ( _|_ ` A ) -> ( ( _|_ ` A ) C_ ( _|_ ` r ) -> q C_ ( _|_ ` r ) ) )
8 6 7 syl5 
 |-  ( q C_ ( _|_ ` A ) -> ( ( r e. HAtoms /\ r C_ A ) -> q C_ ( _|_ ` r ) ) )
9 atelch 
 |-  ( p e. HAtoms -> p e. CH )
10 atne0 
 |-  ( r e. HAtoms -> r =/= 0H )
11 10 neneqd 
 |-  ( r e. HAtoms -> -. r = 0H )
12 11 ad3antrrr 
 |-  ( ( ( ( r e. HAtoms /\ q C_ ( _|_ ` r ) ) /\ ( p e. CH /\ q e. CH ) ) /\ r C_ ( p vH q ) ) -> -. r = 0H )
13 simplr 
 |-  ( ( ( ( ( r e. HAtoms /\ q C_ ( _|_ ` r ) ) /\ ( p e. CH /\ q e. CH ) ) /\ r C_ ( p vH q ) ) /\ p C_ ( _|_ ` r ) ) -> r C_ ( p vH q ) )
14 choccl 
 |-  ( r e. CH -> ( _|_ ` r ) e. CH )
15 2 14 syl 
 |-  ( r e. HAtoms -> ( _|_ ` r ) e. CH )
16 chlej1 
 |-  ( ( ( p e. CH /\ ( _|_ ` r ) e. CH /\ q e. CH ) /\ p C_ ( _|_ ` r ) ) -> ( p vH q ) C_ ( ( _|_ ` r ) vH q ) )
17 16 3exp1 
 |-  ( p e. CH -> ( ( _|_ ` r ) e. CH -> ( q e. CH -> ( p C_ ( _|_ ` r ) -> ( p vH q ) C_ ( ( _|_ ` r ) vH q ) ) ) ) )
18 15 17 syl5com 
 |-  ( r e. HAtoms -> ( p e. CH -> ( q e. CH -> ( p C_ ( _|_ ` r ) -> ( p vH q ) C_ ( ( _|_ ` r ) vH q ) ) ) ) )
19 18 imp42 
 |-  ( ( ( r e. HAtoms /\ ( p e. CH /\ q e. CH ) ) /\ p C_ ( _|_ ` r ) ) -> ( p vH q ) C_ ( ( _|_ ` r ) vH q ) )
20 19 adantllr 
 |-  ( ( ( ( r e. HAtoms /\ q C_ ( _|_ ` r ) ) /\ ( p e. CH /\ q e. CH ) ) /\ p C_ ( _|_ ` r ) ) -> ( p vH q ) C_ ( ( _|_ ` r ) vH q ) )
21 20 adantlr 
 |-  ( ( ( ( ( r e. HAtoms /\ q C_ ( _|_ ` r ) ) /\ ( p e. CH /\ q e. CH ) ) /\ r C_ ( p vH q ) ) /\ p C_ ( _|_ ` r ) ) -> ( p vH q ) C_ ( ( _|_ ` r ) vH q ) )
22 13 21 sstrd 
 |-  ( ( ( ( ( r e. HAtoms /\ q C_ ( _|_ ` r ) ) /\ ( p e. CH /\ q e. CH ) ) /\ r C_ ( p vH q ) ) /\ p C_ ( _|_ ` r ) ) -> r C_ ( ( _|_ ` r ) vH q ) )
23 chlejb2 
 |-  ( ( q e. CH /\ ( _|_ ` r ) e. CH ) -> ( q C_ ( _|_ ` r ) <-> ( ( _|_ ` r ) vH q ) = ( _|_ ` r ) ) )
24 23 ancoms 
 |-  ( ( ( _|_ ` r ) e. CH /\ q e. CH ) -> ( q C_ ( _|_ ` r ) <-> ( ( _|_ ` r ) vH q ) = ( _|_ ` r ) ) )
25 24 biimpa 
 |-  ( ( ( ( _|_ ` r ) e. CH /\ q e. CH ) /\ q C_ ( _|_ ` r ) ) -> ( ( _|_ ` r ) vH q ) = ( _|_ ` r ) )
26 15 25 sylanl1 
 |-  ( ( ( r e. HAtoms /\ q e. CH ) /\ q C_ ( _|_ ` r ) ) -> ( ( _|_ ` r ) vH q ) = ( _|_ ` r ) )
27 26 an32s 
 |-  ( ( ( r e. HAtoms /\ q C_ ( _|_ ` r ) ) /\ q e. CH ) -> ( ( _|_ ` r ) vH q ) = ( _|_ ` r ) )
28 27 adantrl 
 |-  ( ( ( r e. HAtoms /\ q C_ ( _|_ ` r ) ) /\ ( p e. CH /\ q e. CH ) ) -> ( ( _|_ ` r ) vH q ) = ( _|_ ` r ) )
29 28 ad2antrr 
 |-  ( ( ( ( ( r e. HAtoms /\ q C_ ( _|_ ` r ) ) /\ ( p e. CH /\ q e. CH ) ) /\ r C_ ( p vH q ) ) /\ p C_ ( _|_ ` r ) ) -> ( ( _|_ ` r ) vH q ) = ( _|_ ` r ) )
30 22 29 sseqtrd 
 |-  ( ( ( ( ( r e. HAtoms /\ q C_ ( _|_ ` r ) ) /\ ( p e. CH /\ q e. CH ) ) /\ r C_ ( p vH q ) ) /\ p C_ ( _|_ ` r ) ) -> r C_ ( _|_ ` r ) )
31 30 ex 
 |-  ( ( ( ( r e. HAtoms /\ q C_ ( _|_ ` r ) ) /\ ( p e. CH /\ q e. CH ) ) /\ r C_ ( p vH q ) ) -> ( p C_ ( _|_ ` r ) -> r C_ ( _|_ ` r ) ) )
32 chssoc 
 |-  ( r e. CH -> ( r C_ ( _|_ ` r ) <-> r = 0H ) )
33 32 biimpd 
 |-  ( r e. CH -> ( r C_ ( _|_ ` r ) -> r = 0H ) )
34 2 33 syl 
 |-  ( r e. HAtoms -> ( r C_ ( _|_ ` r ) -> r = 0H ) )
35 34 ad3antrrr 
 |-  ( ( ( ( r e. HAtoms /\ q C_ ( _|_ ` r ) ) /\ ( p e. CH /\ q e. CH ) ) /\ r C_ ( p vH q ) ) -> ( r C_ ( _|_ ` r ) -> r = 0H ) )
36 31 35 syld 
 |-  ( ( ( ( r e. HAtoms /\ q C_ ( _|_ ` r ) ) /\ ( p e. CH /\ q e. CH ) ) /\ r C_ ( p vH q ) ) -> ( p C_ ( _|_ ` r ) -> r = 0H ) )
37 12 36 mtod 
 |-  ( ( ( ( r e. HAtoms /\ q C_ ( _|_ ` r ) ) /\ ( p e. CH /\ q e. CH ) ) /\ r C_ ( p vH q ) ) -> -. p C_ ( _|_ ` r ) )
38 37 ex 
 |-  ( ( ( r e. HAtoms /\ q C_ ( _|_ ` r ) ) /\ ( p e. CH /\ q e. CH ) ) -> ( r C_ ( p vH q ) -> -. p C_ ( _|_ ` r ) ) )
39 9 38 sylanr1 
 |-  ( ( ( r e. HAtoms /\ q C_ ( _|_ ` r ) ) /\ ( p e. HAtoms /\ q e. CH ) ) -> ( r C_ ( p vH q ) -> -. p C_ ( _|_ ` r ) ) )
40 atnssm0 
 |-  ( ( ( _|_ ` r ) e. CH /\ p e. HAtoms ) -> ( -. p C_ ( _|_ ` r ) <-> ( ( _|_ ` r ) i^i p ) = 0H ) )
41 incom 
 |-  ( ( _|_ ` r ) i^i p ) = ( p i^i ( _|_ ` r ) )
42 41 eqeq1i 
 |-  ( ( ( _|_ ` r ) i^i p ) = 0H <-> ( p i^i ( _|_ ` r ) ) = 0H )
43 40 42 bitrdi 
 |-  ( ( ( _|_ ` r ) e. CH /\ p e. HAtoms ) -> ( -. p C_ ( _|_ ` r ) <-> ( p i^i ( _|_ ` r ) ) = 0H ) )
44 15 43 sylan 
 |-  ( ( r e. HAtoms /\ p e. HAtoms ) -> ( -. p C_ ( _|_ ` r ) <-> ( p i^i ( _|_ ` r ) ) = 0H ) )
45 44 ad2ant2r 
 |-  ( ( ( r e. HAtoms /\ q C_ ( _|_ ` r ) ) /\ ( p e. HAtoms /\ q e. CH ) ) -> ( -. p C_ ( _|_ ` r ) <-> ( p i^i ( _|_ ` r ) ) = 0H ) )
46 39 45 sylibd 
 |-  ( ( ( r e. HAtoms /\ q C_ ( _|_ ` r ) ) /\ ( p e. HAtoms /\ q e. CH ) ) -> ( r C_ ( p vH q ) -> ( p i^i ( _|_ ` r ) ) = 0H ) )
47 46 exp43 
 |-  ( r e. HAtoms -> ( q C_ ( _|_ ` r ) -> ( p e. HAtoms -> ( q e. CH -> ( r C_ ( p vH q ) -> ( p i^i ( _|_ ` r ) ) = 0H ) ) ) ) )
48 47 adantr 
 |-  ( ( r e. HAtoms /\ r C_ A ) -> ( q C_ ( _|_ ` r ) -> ( p e. HAtoms -> ( q e. CH -> ( r C_ ( p vH q ) -> ( p i^i ( _|_ ` r ) ) = 0H ) ) ) ) )
49 8 48 sylcom 
 |-  ( q C_ ( _|_ ` A ) -> ( ( r e. HAtoms /\ r C_ A ) -> ( p e. HAtoms -> ( q e. CH -> ( r C_ ( p vH q ) -> ( p i^i ( _|_ ` r ) ) = 0H ) ) ) ) )
50 49 com4t 
 |-  ( 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 ) ) ) ) )
51 50 impd 
 |-  ( 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 ) ) ) )
52 51 imp43 
 |-  ( ( ( 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 )