Metamath Proof Explorer

Theorem mdsymlem2

Description: Lemma for mdsymi . (Contributed by NM, 1-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 mdsymlem2 
|- ( ( ( p e. HAtoms /\ ( B i^i C ) C_ A ) /\ ( B MH* A /\ p C_ ( A vH B ) ) ) -> ( B =/= 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 2 hatomici 
 |-  ( B =/= 0H -> E. r e. HAtoms r C_ B )
5 simplll 
 |-  ( ( ( ( p e. HAtoms /\ ( B i^i C ) C_ A ) /\ ( B MH* A /\ p C_ ( A vH B ) ) ) /\ ( r e. HAtoms /\ r C_ B ) ) -> p e. HAtoms )
6 atelch 
 |-  ( p e. HAtoms -> p e. CH )
7 atelch 
 |-  ( r e. HAtoms -> r e. CH )
8 chub1 
 |-  ( ( p e. CH /\ r e. CH ) -> p C_ ( p vH r ) )
9 6 7 8 syl2an 
 |-  ( ( p e. HAtoms /\ r e. HAtoms ) -> p C_ ( p vH r ) )
10 9 adantlr 
 |-  ( ( ( p e. HAtoms /\ ( B i^i C ) C_ A ) /\ r e. HAtoms ) -> p C_ ( p vH r ) )
11 10 adantlr 
 |-  ( ( ( ( p e. HAtoms /\ ( B i^i C ) C_ A ) /\ ( B MH* A /\ p C_ ( A vH B ) ) ) /\ r e. HAtoms ) -> p C_ ( p vH r ) )
12 1 2 3 mdsymlem1 
 |-  ( ( ( p e. CH /\ ( B i^i C ) C_ A ) /\ ( B MH* A /\ p C_ ( A vH B ) ) ) -> p C_ A )
13 6 12 sylanl1 
 |-  ( ( ( p e. HAtoms /\ ( B i^i C ) C_ A ) /\ ( B MH* A /\ p C_ ( A vH B ) ) ) -> p C_ A )
14 13 adantr 
 |-  ( ( ( ( p e. HAtoms /\ ( B i^i C ) C_ A ) /\ ( B MH* A /\ p C_ ( A vH B ) ) ) /\ r e. HAtoms ) -> p C_ A )
15 11 14 jca 
 |-  ( ( ( ( p e. HAtoms /\ ( B i^i C ) C_ A ) /\ ( B MH* A /\ p C_ ( A vH B ) ) ) /\ r e. HAtoms ) -> ( p C_ ( p vH r ) /\ p C_ A ) )
16 15 anim1i 
 |-  ( ( ( ( ( p e. HAtoms /\ ( B i^i C ) C_ A ) /\ ( B MH* A /\ p C_ ( A vH B ) ) ) /\ r e. HAtoms ) /\ r C_ B ) -> ( ( p C_ ( p vH r ) /\ p C_ A ) /\ r C_ B ) )
17 anass 
 |-  ( ( ( p C_ ( p vH r ) /\ p C_ A ) /\ r C_ B ) <-> ( p C_ ( p vH r ) /\ ( p C_ A /\ r C_ B ) ) )
18 16 17 sylib 
 |-  ( ( ( ( ( p e. HAtoms /\ ( B i^i C ) C_ A ) /\ ( B MH* A /\ p C_ ( A vH B ) ) ) /\ r e. HAtoms ) /\ r C_ B ) -> ( p C_ ( p vH r ) /\ ( p C_ A /\ r C_ B ) ) )
19 18 anasss 
 |-  ( ( ( ( p e. HAtoms /\ ( B i^i C ) C_ A ) /\ ( B MH* A /\ p C_ ( A vH B ) ) ) /\ ( r e. HAtoms /\ r C_ B ) ) -> ( p C_ ( p vH r ) /\ ( p C_ A /\ r C_ B ) ) )
20 oveq1 
 |-  ( q = p -> ( q vH r ) = ( p vH r ) )
21 20 sseq2d 
 |-  ( q = p -> ( p C_ ( q vH r ) <-> p C_ ( p vH r ) ) )
22 sseq1 
 |-  ( q = p -> ( q C_ A <-> p C_ A ) )
23 22 anbi1d 
 |-  ( q = p -> ( ( q C_ A /\ r C_ B ) <-> ( p C_ A /\ r C_ B ) ) )
24 21 23 anbi12d 
 |-  ( q = p -> ( ( p C_ ( q vH r ) /\ ( q C_ A /\ r C_ B ) ) <-> ( p C_ ( p vH r ) /\ ( p C_ A /\ r C_ B ) ) ) )
25 24 rspcev 
 |-  ( ( p e. HAtoms /\ ( p C_ ( p vH r ) /\ ( p C_ A /\ r C_ B ) ) ) -> E. q e. HAtoms ( p C_ ( q vH r ) /\ ( q C_ A /\ r C_ B ) ) )
26 5 19 25 syl2anc 
 |-  ( ( ( ( p e. HAtoms /\ ( B i^i C ) C_ A ) /\ ( B MH* A /\ p C_ ( A vH B ) ) ) /\ ( r e. HAtoms /\ r C_ B ) ) -> E. q e. HAtoms ( p C_ ( q vH r ) /\ ( q C_ A /\ r C_ B ) ) )
27 26 exp32 
 |-  ( ( ( p e. HAtoms /\ ( B i^i C ) C_ A ) /\ ( B MH* A /\ p C_ ( A vH B ) ) ) -> ( r e. HAtoms -> ( r C_ B -> E. q e. HAtoms ( p C_ ( q vH r ) /\ ( q C_ A /\ r C_ B ) ) ) ) )
28 27 reximdvai 
 |-  ( ( ( p e. HAtoms /\ ( B i^i C ) C_ A ) /\ ( B MH* A /\ p C_ ( A vH B ) ) ) -> ( E. r e. HAtoms r C_ B -> E. r e. HAtoms E. q e. HAtoms ( p C_ ( q vH r ) /\ ( q C_ A /\ r C_ B ) ) ) )
29 4 28 syl5 
 |-  ( ( ( p e. HAtoms /\ ( B i^i C ) C_ A ) /\ ( B MH* A /\ p C_ ( A vH B ) ) ) -> ( B =/= 0H -> E. r e. HAtoms E. q e. HAtoms ( p C_ ( q vH r ) /\ ( q C_ A /\ r C_ B ) ) ) )