Metamath Proof Explorer

Theorem mdsymlem8

Description: Lemma for mdsymi . Lemma 4(ii) of Maeda p. 168. (Contributed by NM, 3-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 mdsymlem8 
|- ( ( A =/= 0H /\ B =/= 0H ) -> ( B MH* A <-> A MH* 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 1 2 chjcomi 
 |-  ( A vH B ) = ( B vH A )
5 4 sseq2i 
 |-  ( p C_ ( A vH B ) <-> p C_ ( B vH A ) )
6 atelch 
 |-  ( q e. HAtoms -> q e. CH )
7 atelch 
 |-  ( r e. HAtoms -> r e. CH )
8 chjcom 
 |-  ( ( q e. CH /\ r e. CH ) -> ( q vH r ) = ( r vH q ) )
9 6 7 8 syl2an 
 |-  ( ( q e. HAtoms /\ r e. HAtoms ) -> ( q vH r ) = ( r vH q ) )
10 9 sseq2d 
 |-  ( ( q e. HAtoms /\ r e. HAtoms ) -> ( p C_ ( q vH r ) <-> p C_ ( r vH q ) ) )
11 ancom 
 |-  ( ( q C_ A /\ r C_ B ) <-> ( r C_ B /\ q C_ A ) )
12 11 a1i 
 |-  ( ( q e. HAtoms /\ r e. HAtoms ) -> ( ( q C_ A /\ r C_ B ) <-> ( r C_ B /\ q C_ A ) ) )
13 10 12 anbi12d 
 |-  ( ( q e. HAtoms /\ r e. HAtoms ) -> ( ( p C_ ( q vH r ) /\ ( q C_ A /\ r C_ B ) ) <-> ( p C_ ( r vH q ) /\ ( r C_ B /\ q C_ A ) ) ) )
14 13 2rexbiia 
 |-  ( E. q e. HAtoms E. r e. HAtoms ( p C_ ( q vH r ) /\ ( q C_ A /\ r C_ B ) ) <-> E. q e. HAtoms E. r e. HAtoms ( p C_ ( r vH q ) /\ ( r C_ B /\ q C_ A ) ) )
15 rexcom 
 |-  ( E. q e. HAtoms E. r e. HAtoms ( p C_ ( r vH q ) /\ ( r C_ B /\ q C_ A ) ) <-> E. r e. HAtoms E. q e. HAtoms ( p C_ ( r vH q ) /\ ( r C_ B /\ q C_ A ) ) )
16 14 15 bitri 
 |-  ( E. q e. HAtoms E. r e. HAtoms ( p C_ ( q vH r ) /\ ( q C_ A /\ r C_ B ) ) <-> E. r e. HAtoms E. q e. HAtoms ( p C_ ( r vH q ) /\ ( r C_ B /\ q C_ A ) ) )
17 5 16 imbi12i 
 |-  ( ( p C_ ( A vH B ) -> E. q e. HAtoms E. r e. HAtoms ( p C_ ( q vH r ) /\ ( q C_ A /\ r C_ B ) ) ) <-> ( p C_ ( B vH A ) -> E. r e. HAtoms E. q e. HAtoms ( p C_ ( r vH q ) /\ ( r C_ B /\ q C_ A ) ) ) )
18 17 ralbii 
 |-  ( A. p e. HAtoms ( p C_ ( A vH B ) -> E. q e. HAtoms E. r e. HAtoms ( p C_ ( q vH r ) /\ ( q C_ A /\ r C_ B ) ) ) <-> A. p e. HAtoms ( p C_ ( B vH A ) -> E. r e. HAtoms E. q e. HAtoms ( p C_ ( r vH q ) /\ ( r C_ B /\ q C_ A ) ) ) )
19 18 a1i 
 |-  ( ( A =/= 0H /\ B =/= 0H ) -> ( A. p e. HAtoms ( p C_ ( A vH B ) -> E. q e. HAtoms E. r e. HAtoms ( p C_ ( q vH r ) /\ ( q C_ A /\ r C_ B ) ) ) <-> A. p e. HAtoms ( p C_ ( B vH A ) -> E. r e. HAtoms E. q e. HAtoms ( p C_ ( r vH q ) /\ ( r C_ B /\ q C_ A ) ) ) ) )
20 1 2 3 mdsymlem7 
 |-  ( ( A =/= 0H /\ B =/= 0H ) -> ( B MH* A <-> A. p e. HAtoms ( p C_ ( A vH B ) -> E. q e. HAtoms E. r e. HAtoms ( p C_ ( q vH r ) /\ ( q C_ A /\ r C_ B ) ) ) ) )
21 eqid 
 |-  ( B vH p ) = ( B vH p )
22 2 1 21 mdsymlem7 
 |-  ( ( B =/= 0H /\ A =/= 0H ) -> ( A MH* B <-> A. p e. HAtoms ( p C_ ( B vH A ) -> E. r e. HAtoms E. q e. HAtoms ( p C_ ( r vH q ) /\ ( r C_ B /\ q C_ A ) ) ) ) )
23 22 ancoms 
 |-  ( ( A =/= 0H /\ B =/= 0H ) -> ( A MH* B <-> A. p e. HAtoms ( p C_ ( B vH A ) -> E. r e. HAtoms E. q e. HAtoms ( p C_ ( r vH q ) /\ ( r C_ B /\ q C_ A ) ) ) ) )
24 19 20 23 3bitr4d 
 |-  ( ( A =/= 0H /\ B =/= 0H ) -> ( B MH* A <-> A MH* B ) )