Metamath Proof Explorer

Theorem mdsymlem3

Description: Lemma for mdsymi . (Contributed by NM, 2-Jul-2004) (New usage is discouraged.)

Ref Expression
Hypotheses mdsymlem1.1 
|- A e. CH
mdsymlem1.2 
|- B e. CH
mdsymlem1.3 
|- C = ( A vH p )
Assertion mdsymlem3 
|- ( ( ( ( p e. HAtoms /\ -. ( B i^i C ) C_ A ) /\ p C_ ( A vH B ) ) /\ A =/= 0H ) -> E. r e. HAtoms E. q e. HAtoms ( p C_ ( q vH r ) /\ ( q C_ A /\ r C_ B ) ) )

Proof

Step Hyp Ref Expression
1 mdsymlem1.1 
 |-  A e. CH
2 mdsymlem1.2 
 |-  B e. CH
3 mdsymlem1.3 
 |-  C = ( A vH p )
4 ssin 
 |-  ( ( r C_ B /\ r C_ C ) <-> r C_ ( B i^i C ) )
5 3 sseq2i 
 |-  ( r C_ C <-> r C_ ( A vH p ) )
6 5 biimpi 
 |-  ( r C_ C -> r C_ ( A vH p ) )
7 6 adantl 
 |-  ( ( r C_ B /\ r C_ C ) -> r C_ ( A vH p ) )
8 4 7 sylbir 
 |-  ( r C_ ( B i^i C ) -> r C_ ( A vH p ) )
9 1 atcvat4i 
 |-  ( ( r e. HAtoms /\ p e. HAtoms ) -> ( ( A =/= 0H /\ r C_ ( A vH p ) ) -> E. q e. HAtoms ( q C_ A /\ r C_ ( p vH q ) ) ) )
10 9 exp4b 
 |-  ( r e. HAtoms -> ( p e. HAtoms -> ( A =/= 0H -> ( r C_ ( A vH p ) -> E. q e. HAtoms ( q C_ A /\ r C_ ( p vH q ) ) ) ) ) )
11 10 com34 
 |-  ( r e. HAtoms -> ( p e. HAtoms -> ( r C_ ( A vH p ) -> ( A =/= 0H -> E. q e. HAtoms ( q C_ A /\ r C_ ( p vH q ) ) ) ) ) )
12 11 com23 
 |-  ( r e. HAtoms -> ( r C_ ( A vH p ) -> ( p e. HAtoms -> ( A =/= 0H -> E. q e. HAtoms ( q C_ A /\ r C_ ( p vH q ) ) ) ) ) )
13 12 imp4b 
 |-  ( ( r e. HAtoms /\ r C_ ( A vH p ) ) -> ( ( p e. HAtoms /\ A =/= 0H ) -> E. q e. HAtoms ( q C_ A /\ r C_ ( p vH q ) ) ) )
14 8 13 sylan2 
 |-  ( ( r e. HAtoms /\ r C_ ( B i^i C ) ) -> ( ( p e. HAtoms /\ A =/= 0H ) -> E. q e. HAtoms ( q C_ A /\ r C_ ( p vH q ) ) ) )
15 14 adantrr 
 |-  ( ( r e. HAtoms /\ ( r C_ ( B i^i C ) /\ -. r C_ A ) ) -> ( ( p e. HAtoms /\ A =/= 0H ) -> E. q e. HAtoms ( q C_ A /\ r C_ ( p vH q ) ) ) )
16 15 com12 
 |-  ( ( p e. HAtoms /\ A =/= 0H ) -> ( ( r e. HAtoms /\ ( r C_ ( B i^i C ) /\ -. r C_ A ) ) -> E. q e. HAtoms ( q C_ A /\ r C_ ( p vH q ) ) ) )
17 16 adantlr 
 |-  ( ( ( p e. HAtoms /\ -. ( B i^i C ) C_ A ) /\ A =/= 0H ) -> ( ( r e. HAtoms /\ ( r C_ ( B i^i C ) /\ -. r C_ A ) ) -> E. q e. HAtoms ( q C_ A /\ r C_ ( p vH q ) ) ) )
18 17 adantlr 
 |-  ( ( ( ( p e. HAtoms /\ -. ( B i^i C ) C_ A ) /\ p C_ ( A vH B ) ) /\ A =/= 0H ) -> ( ( r e. HAtoms /\ ( r C_ ( B i^i C ) /\ -. r C_ A ) ) -> E. q e. HAtoms ( q C_ A /\ r C_ ( p vH q ) ) ) )
19 18 imp 
 |-  ( ( ( ( ( p e. HAtoms /\ -. ( B i^i C ) C_ A ) /\ p C_ ( A vH B ) ) /\ A =/= 0H ) /\ ( r e. HAtoms /\ ( r C_ ( B i^i C ) /\ -. r C_ A ) ) ) -> E. q e. HAtoms ( q C_ A /\ r C_ ( p vH q ) ) )
20 nssne2 
 |-  ( ( q C_ A /\ -. r C_ A ) -> q =/= r )
21 20 adantrl 
 |-  ( ( q C_ A /\ ( r C_ ( B i^i C ) /\ -. r C_ A ) ) -> q =/= r )
22 atnemeq0 
 |-  ( ( q e. HAtoms /\ r e. HAtoms ) -> ( q =/= r <-> ( q i^i r ) = 0H ) )
23 22 ancoms 
 |-  ( ( r e. HAtoms /\ q e. HAtoms ) -> ( q =/= r <-> ( q i^i r ) = 0H ) )
24 21 23 syl5ib 
 |-  ( ( r e. HAtoms /\ q e. HAtoms ) -> ( ( q C_ A /\ ( r C_ ( B i^i C ) /\ -. r C_ A ) ) -> ( q i^i r ) = 0H ) )
25 24 adantll 
 |-  ( ( ( p e. HAtoms /\ r e. HAtoms ) /\ q e. HAtoms ) -> ( ( q C_ A /\ ( r C_ ( B i^i C ) /\ -. r C_ A ) ) -> ( q i^i r ) = 0H ) )
26 25 adantr 
 |-  ( ( ( ( p e. HAtoms /\ r e. HAtoms ) /\ q e. HAtoms ) /\ r C_ ( p vH q ) ) -> ( ( q C_ A /\ ( r C_ ( B i^i C ) /\ -. r C_ A ) ) -> ( q i^i r ) = 0H ) )
27 atelch 
 |-  ( p e. HAtoms -> p e. CH )
28 atelch 
 |-  ( q e. HAtoms -> q e. CH )
29 chjcom 
 |-  ( ( p e. CH /\ q e. CH ) -> ( p vH q ) = ( q vH p ) )
30 27 28 29 syl2an 
 |-  ( ( p e. HAtoms /\ q e. HAtoms ) -> ( p vH q ) = ( q vH p ) )
31 30 adantlr 
 |-  ( ( ( p e. HAtoms /\ r e. HAtoms ) /\ q e. HAtoms ) -> ( p vH q ) = ( q vH p ) )
32 31 sseq2d 
 |-  ( ( ( p e. HAtoms /\ r e. HAtoms ) /\ q e. HAtoms ) -> ( r C_ ( p vH q ) <-> r C_ ( q vH p ) ) )
33 atexch 
 |-  ( ( q e. CH /\ r e. HAtoms /\ p e. HAtoms ) -> ( ( r C_ ( q vH p ) /\ ( q i^i r ) = 0H ) -> p C_ ( q vH r ) ) )
34 28 33 syl3an1 
 |-  ( ( q e. HAtoms /\ r e. HAtoms /\ p e. HAtoms ) -> ( ( r C_ ( q vH p ) /\ ( q i^i r ) = 0H ) -> p C_ ( q vH r ) ) )
35 34 3com13 
 |-  ( ( p e. HAtoms /\ r e. HAtoms /\ q e. HAtoms ) -> ( ( r C_ ( q vH p ) /\ ( q i^i r ) = 0H ) -> p C_ ( q vH r ) ) )
36 35 3expa 
 |-  ( ( ( p e. HAtoms /\ r e. HAtoms ) /\ q e. HAtoms ) -> ( ( r C_ ( q vH p ) /\ ( q i^i r ) = 0H ) -> p C_ ( q vH r ) ) )
37 36 expd 
 |-  ( ( ( p e. HAtoms /\ r e. HAtoms ) /\ q e. HAtoms ) -> ( r C_ ( q vH p ) -> ( ( q i^i r ) = 0H -> p C_ ( q vH r ) ) ) )
38 32 37 sylbid 
 |-  ( ( ( p e. HAtoms /\ r e. HAtoms ) /\ q e. HAtoms ) -> ( r C_ ( p vH q ) -> ( ( q i^i r ) = 0H -> p C_ ( q vH r ) ) ) )
39 38 imp 
 |-  ( ( ( ( p e. HAtoms /\ r e. HAtoms ) /\ q e. HAtoms ) /\ r C_ ( p vH q ) ) -> ( ( q i^i r ) = 0H -> p C_ ( q vH r ) ) )
40 26 39 syld 
 |-  ( ( ( ( p e. HAtoms /\ r e. HAtoms ) /\ q e. HAtoms ) /\ r C_ ( p vH q ) ) -> ( ( q C_ A /\ ( r C_ ( B i^i C ) /\ -. r C_ A ) ) -> p C_ ( q vH r ) ) )
41 40 expd 
 |-  ( ( ( ( p e. HAtoms /\ r e. HAtoms ) /\ q e. HAtoms ) /\ r C_ ( p vH q ) ) -> ( q C_ A -> ( ( r C_ ( B i^i C ) /\ -. r C_ A ) -> p C_ ( q vH r ) ) ) )
42 41 exp31 
 |-  ( ( p e. HAtoms /\ r e. HAtoms ) -> ( q e. HAtoms -> ( r C_ ( p vH q ) -> ( q C_ A -> ( ( r C_ ( B i^i C ) /\ -. r C_ A ) -> p C_ ( q vH r ) ) ) ) ) )
43 42 com24 
 |-  ( ( p e. HAtoms /\ r e. HAtoms ) -> ( q C_ A -> ( r C_ ( p vH q ) -> ( q e. HAtoms -> ( ( r C_ ( B i^i C ) /\ -. r C_ A ) -> p C_ ( q vH r ) ) ) ) ) )
44 43 impd 
 |-  ( ( p e. HAtoms /\ r e. HAtoms ) -> ( ( q C_ A /\ r C_ ( p vH q ) ) -> ( q e. HAtoms -> ( ( r C_ ( B i^i C ) /\ -. r C_ A ) -> p C_ ( q vH r ) ) ) ) )
45 44 com24 
 |-  ( ( p e. HAtoms /\ r e. HAtoms ) -> ( ( r C_ ( B i^i C ) /\ -. r C_ A ) -> ( q e. HAtoms -> ( ( q C_ A /\ r C_ ( p vH q ) ) -> p C_ ( q vH r ) ) ) ) )
46 45 imp4b 
 |-  ( ( ( p e. HAtoms /\ r e. HAtoms ) /\ ( r C_ ( B i^i C ) /\ -. r C_ A ) ) -> ( ( q e. HAtoms /\ ( q C_ A /\ r C_ ( p vH q ) ) ) -> p C_ ( q vH r ) ) )
47 46 anasss 
 |-  ( ( p e. HAtoms /\ ( r e. HAtoms /\ ( r C_ ( B i^i C ) /\ -. r C_ A ) ) ) -> ( ( q e. HAtoms /\ ( q C_ A /\ r C_ ( p vH q ) ) ) -> p C_ ( q vH r ) ) )
48 simprl 
 |-  ( ( q e. HAtoms /\ ( q C_ A /\ r C_ ( p vH q ) ) ) -> q C_ A )
49 48 a1i 
 |-  ( ( p e. HAtoms /\ ( r e. HAtoms /\ ( r C_ ( B i^i C ) /\ -. r C_ A ) ) ) -> ( ( q e. HAtoms /\ ( q C_ A /\ r C_ ( p vH q ) ) ) -> q C_ A ) )
50 simpl 
 |-  ( ( r C_ B /\ r C_ C ) -> r C_ B )
51 4 50 sylbir 
 |-  ( r C_ ( B i^i C ) -> r C_ B )
52 51 ad2antrl 
 |-  ( ( r e. HAtoms /\ ( r C_ ( B i^i C ) /\ -. r C_ A ) ) -> r C_ B )
53 52 adantl 
 |-  ( ( p e. HAtoms /\ ( r e. HAtoms /\ ( r C_ ( B i^i C ) /\ -. r C_ A ) ) ) -> r C_ B )
54 49 53 jctird 
 |-  ( ( p e. HAtoms /\ ( r e. HAtoms /\ ( r C_ ( B i^i C ) /\ -. r C_ A ) ) ) -> ( ( q e. HAtoms /\ ( q C_ A /\ r C_ ( p vH q ) ) ) -> ( q C_ A /\ r C_ B ) ) )
55 47 54 jcad 
 |-  ( ( p e. HAtoms /\ ( r e. HAtoms /\ ( r C_ ( B i^i C ) /\ -. r C_ A ) ) ) -> ( ( q e. HAtoms /\ ( q C_ A /\ r C_ ( p vH q ) ) ) -> ( p C_ ( q vH r ) /\ ( q C_ A /\ r C_ B ) ) ) )
56 55 expd 
 |-  ( ( p e. HAtoms /\ ( r e. HAtoms /\ ( r C_ ( B i^i C ) /\ -. r C_ A ) ) ) -> ( q e. HAtoms -> ( ( q C_ A /\ r C_ ( p vH q ) ) -> ( p C_ ( q vH r ) /\ ( q C_ A /\ r C_ B ) ) ) ) )
57 56 adantlr 
 |-  ( ( ( p e. HAtoms /\ -. ( B i^i C ) C_ A ) /\ ( r e. HAtoms /\ ( r C_ ( B i^i C ) /\ -. r C_ A ) ) ) -> ( q e. HAtoms -> ( ( q C_ A /\ r C_ ( p vH q ) ) -> ( p C_ ( q vH r ) /\ ( q C_ A /\ r C_ B ) ) ) ) )
58 57 adantlr 
 |-  ( ( ( ( p e. HAtoms /\ -. ( B i^i C ) C_ A ) /\ p C_ ( A vH B ) ) /\ ( r e. HAtoms /\ ( r C_ ( B i^i C ) /\ -. r C_ A ) ) ) -> ( q e. HAtoms -> ( ( q C_ A /\ r C_ ( p vH q ) ) -> ( p C_ ( q vH r ) /\ ( q C_ A /\ r C_ B ) ) ) ) )
59 58 adantlr 
 |-  ( ( ( ( ( p e. HAtoms /\ -. ( B i^i C ) C_ A ) /\ p C_ ( A vH B ) ) /\ A =/= 0H ) /\ ( r e. HAtoms /\ ( r C_ ( B i^i C ) /\ -. r C_ A ) ) ) -> ( q e. HAtoms -> ( ( q C_ A /\ r C_ ( p vH q ) ) -> ( p C_ ( q vH r ) /\ ( q C_ A /\ r C_ B ) ) ) ) )
60 59 reximdvai 
 |-  ( ( ( ( ( p e. HAtoms /\ -. ( B i^i C ) C_ A ) /\ p C_ ( A vH B ) ) /\ A =/= 0H ) /\ ( r e. HAtoms /\ ( r C_ ( B i^i C ) /\ -. r C_ A ) ) ) -> ( E. q e. HAtoms ( q C_ A /\ r C_ ( p vH q ) ) -> E. q e. HAtoms ( p C_ ( q vH r ) /\ ( q C_ A /\ r C_ B ) ) ) )
61 19 60 mpd 
 |-  ( ( ( ( ( p e. HAtoms /\ -. ( B i^i C ) C_ A ) /\ p C_ ( A vH B ) ) /\ A =/= 0H ) /\ ( r e. HAtoms /\ ( r C_ ( B i^i C ) /\ -. r C_ A ) ) ) -> E. q e. HAtoms ( p C_ ( q vH r ) /\ ( q C_ A /\ r C_ B ) ) )
62 chjcl 
 |-  ( ( A e. CH /\ p e. CH ) -> ( A vH p ) e. CH )
63 1 62 mpan 
 |-  ( p e. CH -> ( A vH p ) e. CH )
64 3 63 eqeltrid 
 |-  ( p e. CH -> C e. CH )
65 chincl 
 |-  ( ( B e. CH /\ C e. CH ) -> ( B i^i C ) e. CH )
66 2 64 65 sylancr 
 |-  ( p e. CH -> ( B i^i C ) e. CH )
67 27 66 syl 
 |-  ( p e. HAtoms -> ( B i^i C ) e. CH )
68 chrelat2 
 |-  ( ( ( B i^i C ) e. CH /\ A e. CH ) -> ( -. ( B i^i C ) C_ A <-> E. r e. HAtoms ( r C_ ( B i^i C ) /\ -. r C_ A ) ) )
69 67 1 68 sylancl 
 |-  ( p e. HAtoms -> ( -. ( B i^i C ) C_ A <-> E. r e. HAtoms ( r C_ ( B i^i C ) /\ -. r C_ A ) ) )
70 69 biimpa 
 |-  ( ( p e. HAtoms /\ -. ( B i^i C ) C_ A ) -> E. r e. HAtoms ( r C_ ( B i^i C ) /\ -. r C_ A ) )
71 70 ad2antrr 
 |-  ( ( ( ( p e. HAtoms /\ -. ( B i^i C ) C_ A ) /\ p C_ ( A vH B ) ) /\ A =/= 0H ) -> E. r e. HAtoms ( r C_ ( B i^i C ) /\ -. r C_ A ) )
72 61 71 reximddv 
 |-  ( ( ( ( p e. HAtoms /\ -. ( B i^i C ) C_ A ) /\ p C_ ( A vH B ) ) /\ A =/= 0H ) -> E. r e. HAtoms E. q e. HAtoms ( p C_ ( q vH r ) /\ ( q C_ A /\ r C_ B ) ) )