Metamath Proof Explorer

Theorem mdsymlem4

Description: Lemma for mdsymi . This is the forward direction of Lemma 4(i) of Maeda p. 168. (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 mdsymlem4 
|- ( p e. HAtoms -> ( ( B MH* A /\ ( ( A =/= 0H /\ B =/= 0H ) /\ p C_ ( A vH B ) ) ) -> E. q e. HAtoms E. r 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 1 2 3 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 ) ) ) )
5 4 exp31 
 |-  ( 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 ) ) ) ) ) )
6 5 com4t 
 |-  ( ( B MH* A /\ p C_ ( A vH B ) ) -> ( B =/= 0H -> ( p e. HAtoms -> ( ( B i^i C ) C_ A -> E. r e. HAtoms E. q e. HAtoms ( p C_ ( q vH r ) /\ ( q C_ A /\ r C_ B ) ) ) ) ) )
7 6 ex 
 |-  ( B MH* A -> ( p C_ ( A vH B ) -> ( B =/= 0H -> ( p e. HAtoms -> ( ( B i^i C ) C_ A -> E. r e. HAtoms E. q e. HAtoms ( p C_ ( q vH r ) /\ ( q C_ A /\ r C_ B ) ) ) ) ) ) )
8 7 com23 
 |-  ( B MH* A -> ( B =/= 0H -> ( p C_ ( A vH B ) -> ( p e. HAtoms -> ( ( B i^i C ) C_ A -> E. r e. HAtoms E. q e. HAtoms ( p C_ ( q vH r ) /\ ( q C_ A /\ r C_ B ) ) ) ) ) ) )
9 8 a1d 
 |-  ( B MH* A -> ( A =/= 0H -> ( B =/= 0H -> ( p C_ ( A vH B ) -> ( p e. HAtoms -> ( ( B i^i C ) C_ A -> E. r e. HAtoms E. q e. HAtoms ( p C_ ( q vH r ) /\ ( q C_ A /\ r C_ B ) ) ) ) ) ) ) )
10 9 imp44 
 |-  ( ( B MH* A /\ ( ( A =/= 0H /\ B =/= 0H ) /\ p C_ ( A vH B ) ) ) -> ( p e. HAtoms -> ( ( B i^i C ) C_ A -> E. r e. HAtoms E. q e. HAtoms ( p C_ ( q vH r ) /\ ( q C_ A /\ r C_ B ) ) ) ) )
11 10 com3l 
 |-  ( p e. HAtoms -> ( ( B i^i C ) C_ A -> ( ( B MH* A /\ ( ( A =/= 0H /\ B =/= 0H ) /\ p C_ ( A vH B ) ) ) -> E. r e. HAtoms E. q e. HAtoms ( p C_ ( q vH r ) /\ ( q C_ A /\ r C_ B ) ) ) ) )
12 1 2 3 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 ) ) )
13 12 anasss 
 |-  ( ( ( 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 ) ) )
14 13 exp31 
 |-  ( 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 ) ) ) ) )
15 14 com3r 
 |-  ( ( p C_ ( A vH B ) /\ A =/= 0H ) -> ( p e. HAtoms -> ( -. ( B i^i C ) C_ A -> E. r e. HAtoms E. q e. HAtoms ( p C_ ( q vH r ) /\ ( q C_ A /\ r C_ B ) ) ) ) )
16 15 ancoms 
 |-  ( ( A =/= 0H /\ p C_ ( A vH B ) ) -> ( p e. HAtoms -> ( -. ( B i^i C ) C_ A -> E. r e. HAtoms E. q e. HAtoms ( p C_ ( q vH r ) /\ ( q C_ A /\ r C_ B ) ) ) ) )
17 16 adantlr 
 |-  ( ( ( A =/= 0H /\ B =/= 0H ) /\ p C_ ( A vH B ) ) -> ( p e. HAtoms -> ( -. ( B i^i C ) C_ A -> E. r e. HAtoms E. q e. HAtoms ( p C_ ( q vH r ) /\ ( q C_ A /\ r C_ B ) ) ) ) )
18 17 adantl 
 |-  ( ( B MH* A /\ ( ( A =/= 0H /\ B =/= 0H ) /\ p C_ ( A vH B ) ) ) -> ( p e. HAtoms -> ( -. ( B i^i C ) C_ A -> E. r e. HAtoms E. q e. HAtoms ( p C_ ( q vH r ) /\ ( q C_ A /\ r C_ B ) ) ) ) )
19 18 com3l 
 |-  ( p e. HAtoms -> ( -. ( B i^i C ) C_ A -> ( ( B MH* A /\ ( ( A =/= 0H /\ B =/= 0H ) /\ p C_ ( A vH B ) ) ) -> E. r e. HAtoms E. q e. HAtoms ( p C_ ( q vH r ) /\ ( q C_ A /\ r C_ B ) ) ) ) )
20 11 19 pm2.61d 
 |-  ( p e. HAtoms -> ( ( B MH* A /\ ( ( A =/= 0H /\ B =/= 0H ) /\ p C_ ( A vH B ) ) ) -> E. r e. HAtoms E. q e. HAtoms ( p C_ ( q vH r ) /\ ( q C_ A /\ r C_ B ) ) ) )
21 rexcom 
 |-  ( E. r e. HAtoms E. q e. HAtoms ( p C_ ( q vH r ) /\ ( q C_ A /\ r C_ B ) ) <-> E. q e. HAtoms E. r e. HAtoms ( p C_ ( q vH r ) /\ ( q C_ A /\ r C_ B ) ) )
22 20 21 syl6ib 
 |-  ( p e. HAtoms -> ( ( B MH* A /\ ( ( A =/= 0H /\ B =/= 0H ) /\ p C_ ( A vH B ) ) ) -> E. q e. HAtoms E. r e. HAtoms ( p C_ ( q vH r ) /\ ( q C_ A /\ r C_ B ) ) ) )