Metamath Proof Explorer

Theorem mdsymlem1

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 mdsymlem1 
|- ( ( ( p e. CH /\ ( B i^i C ) C_ A ) /\ ( B MH* A /\ p C_ ( A vH B ) ) ) -> p C_ A )

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 chub2 
 |-  ( ( p e. CH /\ A e. CH ) -> p C_ ( A vH p ) )
5 1 4 mpan2 
 |-  ( p e. CH -> p C_ ( A vH p ) )
6 5 3 sseqtrrdi 
 |-  ( p e. CH -> p C_ C )
7 1 2 chjcomi 
 |-  ( A vH B ) = ( B vH A )
8 7 sseq2i 
 |-  ( p C_ ( A vH B ) <-> p C_ ( B vH A ) )
9 8 biimpi 
 |-  ( p C_ ( A vH B ) -> p C_ ( B vH A ) )
10 6 9 anim12i 
 |-  ( ( p e. CH /\ p C_ ( A vH B ) ) -> ( p C_ C /\ p C_ ( B vH A ) ) )
11 ssin 
 |-  ( ( p C_ C /\ p C_ ( B vH A ) ) <-> p C_ ( C i^i ( B vH A ) ) )
12 10 11 sylib 
 |-  ( ( p e. CH /\ p C_ ( A vH B ) ) -> p C_ ( C i^i ( B vH A ) ) )
13 12 ad2ant2rl 
 |-  ( ( ( p e. CH /\ ( B i^i C ) C_ A ) /\ ( B MH* A /\ p C_ ( A vH B ) ) ) -> p C_ ( C i^i ( B vH A ) ) )
14 chjcl 
 |-  ( ( A e. CH /\ p e. CH ) -> ( A vH p ) e. CH )
15 1 14 mpan 
 |-  ( p e. CH -> ( A vH p ) e. CH )
16 3 15 eqeltrid 
 |-  ( p e. CH -> C e. CH )
17 16 adantr 
 |-  ( ( p e. CH /\ B MH* A ) -> C e. CH )
18 chub1 
 |-  ( ( A e. CH /\ p e. CH ) -> A C_ ( A vH p ) )
19 1 18 mpan 
 |-  ( p e. CH -> A C_ ( A vH p ) )
20 19 3 sseqtrrdi 
 |-  ( p e. CH -> A C_ C )
21 20 anim2i 
 |-  ( ( B MH* A /\ p e. CH ) -> ( B MH* A /\ A C_ C ) )
22 21 ancoms 
 |-  ( ( p e. CH /\ B MH* A ) -> ( B MH* A /\ A C_ C ) )
23 dmdi 
 |-  ( ( ( B e. CH /\ A e. CH /\ C e. CH ) /\ ( B MH* A /\ A C_ C ) ) -> ( ( C i^i B ) vH A ) = ( C i^i ( B vH A ) ) )
24 2 23 mp3anl1 
 |-  ( ( ( A e. CH /\ C e. CH ) /\ ( B MH* A /\ A C_ C ) ) -> ( ( C i^i B ) vH A ) = ( C i^i ( B vH A ) ) )
25 1 24 mpanl1 
 |-  ( ( C e. CH /\ ( B MH* A /\ A C_ C ) ) -> ( ( C i^i B ) vH A ) = ( C i^i ( B vH A ) ) )
26 17 22 25 syl2anc 
 |-  ( ( p e. CH /\ B MH* A ) -> ( ( C i^i B ) vH A ) = ( C i^i ( B vH A ) ) )
27 26 adantlr 
 |-  ( ( ( p e. CH /\ ( B i^i C ) C_ A ) /\ B MH* A ) -> ( ( C i^i B ) vH A ) = ( C i^i ( B vH A ) ) )
28 incom 
 |-  ( C i^i B ) = ( B i^i C )
29 28 oveq1i 
 |-  ( ( C i^i B ) vH A ) = ( ( B i^i C ) vH A )
30 chincl 
 |-  ( ( B e. CH /\ C e. CH ) -> ( B i^i C ) e. CH )
31 2 30 mpan 
 |-  ( C e. CH -> ( B i^i C ) e. CH )
32 chlejb1 
 |-  ( ( ( B i^i C ) e. CH /\ A e. CH ) -> ( ( B i^i C ) C_ A <-> ( ( B i^i C ) vH A ) = A ) )
33 1 32 mpan2 
 |-  ( ( B i^i C ) e. CH -> ( ( B i^i C ) C_ A <-> ( ( B i^i C ) vH A ) = A ) )
34 16 31 33 3syl 
 |-  ( p e. CH -> ( ( B i^i C ) C_ A <-> ( ( B i^i C ) vH A ) = A ) )
35 34 biimpa 
 |-  ( ( p e. CH /\ ( B i^i C ) C_ A ) -> ( ( B i^i C ) vH A ) = A )
36 29 35 eqtrid 
 |-  ( ( p e. CH /\ ( B i^i C ) C_ A ) -> ( ( C i^i B ) vH A ) = A )
37 36 adantr 
 |-  ( ( ( p e. CH /\ ( B i^i C ) C_ A ) /\ B MH* A ) -> ( ( C i^i B ) vH A ) = A )
38 27 37 eqtr3d 
 |-  ( ( ( p e. CH /\ ( B i^i C ) C_ A ) /\ B MH* A ) -> ( C i^i ( B vH A ) ) = A )
39 38 adantrr 
 |-  ( ( ( p e. CH /\ ( B i^i C ) C_ A ) /\ ( B MH* A /\ p C_ ( A vH B ) ) ) -> ( C i^i ( B vH A ) ) = A )
40 13 39 sseqtrd 
 |-  ( ( ( p e. CH /\ ( B i^i C ) C_ A ) /\ ( B MH* A /\ p C_ ( A vH B ) ) ) -> p C_ A )