Metamath Proof Explorer

Theorem mdsymlem6

Description: Lemma for mdsymi . This is the converse direction of Lemma 4(i) of Maeda p. 168, and is based on the proof of Theorem 1(d) to (e) of Maeda p. 167. (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 mdsymlem6 
|- ( 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 ) ) ) -> B MH* 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 1 2 chjcomi 
 |-  ( A vH B ) = ( B vH A )
5 4 sseq2i 
 |-  ( p C_ ( A vH B ) <-> p C_ ( B vH A ) )
6 5 anbi2i 
 |-  ( ( p C_ c /\ p C_ ( A vH B ) ) <-> ( p C_ c /\ p C_ ( B vH A ) ) )
7 ssin 
 |-  ( ( p C_ c /\ p C_ ( B vH A ) ) <-> p C_ ( c i^i ( B vH A ) ) )
8 6 7 bitri 
 |-  ( ( p C_ c /\ p C_ ( A vH B ) ) <-> p C_ ( c i^i ( B vH A ) ) )
9 1 2 3 mdsymlem5 
 |-  ( ( q e. HAtoms /\ r e. HAtoms ) -> ( -. q = p -> ( ( p C_ ( q vH r ) /\ ( q C_ A /\ r C_ B ) ) -> ( ( ( c e. CH /\ A C_ c ) /\ p e. HAtoms ) -> ( p C_ c -> p C_ ( ( c i^i B ) vH A ) ) ) ) ) )
10 sseq1 
 |-  ( q = p -> ( q C_ A <-> p C_ A ) )
11 chincl 
 |-  ( ( c e. CH /\ B e. CH ) -> ( c i^i B ) e. CH )
12 2 11 mpan2 
 |-  ( c e. CH -> ( c i^i B ) e. CH )
13 chub2 
 |-  ( ( A e. CH /\ ( c i^i B ) e. CH ) -> A C_ ( ( c i^i B ) vH A ) )
14 1 12 13 sylancr 
 |-  ( c e. CH -> A C_ ( ( c i^i B ) vH A ) )
15 sstr2 
 |-  ( p C_ A -> ( A C_ ( ( c i^i B ) vH A ) -> p C_ ( ( c i^i B ) vH A ) ) )
16 14 15 syl5 
 |-  ( p C_ A -> ( c e. CH -> p C_ ( ( c i^i B ) vH A ) ) )
17 10 16 syl6bi 
 |-  ( q = p -> ( q C_ A -> ( c e. CH -> p C_ ( ( c i^i B ) vH A ) ) ) )
18 17 impd 
 |-  ( q = p -> ( ( q C_ A /\ c e. CH ) -> p C_ ( ( c i^i B ) vH A ) ) )
19 18 a1i 
 |-  ( p C_ c -> ( q = p -> ( ( q C_ A /\ c e. CH ) -> p C_ ( ( c i^i B ) vH A ) ) ) )
20 19 com13 
 |-  ( ( q C_ A /\ c e. CH ) -> ( q = p -> ( p C_ c -> p C_ ( ( c i^i B ) vH A ) ) ) )
21 20 adantrr 
 |-  ( ( q C_ A /\ ( c e. CH /\ A C_ c ) ) -> ( q = p -> ( p C_ c -> p C_ ( ( c i^i B ) vH A ) ) ) )
22 21 ad2ant2r 
 |-  ( ( ( q C_ A /\ r C_ B ) /\ ( ( c e. CH /\ A C_ c ) /\ p e. HAtoms ) ) -> ( q = p -> ( p C_ c -> p C_ ( ( c i^i B ) vH A ) ) ) )
23 22 adantll 
 |-  ( ( ( p C_ ( q vH r ) /\ ( q C_ A /\ r C_ B ) ) /\ ( ( c e. CH /\ A C_ c ) /\ p e. HAtoms ) ) -> ( q = p -> ( p C_ c -> p C_ ( ( c i^i B ) vH A ) ) ) )
24 23 com12 
 |-  ( q = p -> ( ( ( p C_ ( q vH r ) /\ ( q C_ A /\ r C_ B ) ) /\ ( ( c e. CH /\ A C_ c ) /\ p e. HAtoms ) ) -> ( p C_ c -> p C_ ( ( c i^i B ) vH A ) ) ) )
25 24 expd 
 |-  ( q = p -> ( ( p C_ ( q vH r ) /\ ( q C_ A /\ r C_ B ) ) -> ( ( ( c e. CH /\ A C_ c ) /\ p e. HAtoms ) -> ( p C_ c -> p C_ ( ( c i^i B ) vH A ) ) ) ) )
26 9 25 pm2.61d2 
 |-  ( ( q e. HAtoms /\ r e. HAtoms ) -> ( ( p C_ ( q vH r ) /\ ( q C_ A /\ r C_ B ) ) -> ( ( ( c e. CH /\ A C_ c ) /\ p e. HAtoms ) -> ( p C_ c -> p C_ ( ( c i^i B ) vH A ) ) ) ) )
27 26 rexlimivv 
 |-  ( E. q e. HAtoms E. r e. HAtoms ( p C_ ( q vH r ) /\ ( q C_ A /\ r C_ B ) ) -> ( ( ( c e. CH /\ A C_ c ) /\ p e. HAtoms ) -> ( p C_ c -> p C_ ( ( c i^i B ) vH A ) ) ) )
28 27 com12 
 |-  ( ( ( c e. CH /\ A C_ c ) /\ p e. HAtoms ) -> ( E. q e. HAtoms E. r e. HAtoms ( p C_ ( q vH r ) /\ ( q C_ A /\ r C_ B ) ) -> ( p C_ c -> p C_ ( ( c i^i B ) vH A ) ) ) )
29 28 imim2d 
 |-  ( ( ( c e. CH /\ A C_ c ) /\ 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 ) ) ) -> ( p C_ ( A vH B ) -> ( p C_ c -> p C_ ( ( c i^i B ) vH A ) ) ) ) )
30 29 com34 
 |-  ( ( ( c e. CH /\ A C_ c ) /\ 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 ) ) ) -> ( p C_ c -> ( p C_ ( A vH B ) -> p C_ ( ( c i^i B ) vH A ) ) ) ) )
31 30 imp4b 
 |-  ( ( ( ( c e. CH /\ A C_ c ) /\ 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 ) ) ) ) -> ( ( p C_ c /\ p C_ ( A vH B ) ) -> p C_ ( ( c i^i B ) vH A ) ) )
32 8 31 syl5bir 
 |-  ( ( ( ( c e. CH /\ A C_ c ) /\ 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 ) ) ) ) -> ( p C_ ( c i^i ( B vH A ) ) -> p C_ ( ( c i^i B ) vH A ) ) )
33 32 ex 
 |-  ( ( ( c e. CH /\ A C_ c ) /\ 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 ) ) ) -> ( p C_ ( c i^i ( B vH A ) ) -> p C_ ( ( c i^i B ) vH A ) ) ) )
34 33 ralimdva 
 |-  ( ( c e. CH /\ A C_ c ) -> ( 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_ ( c i^i ( B vH A ) ) -> p C_ ( ( c i^i B ) vH A ) ) ) )
35 2 1 chjcli 
 |-  ( B vH A ) e. CH
36 chincl 
 |-  ( ( c e. CH /\ ( B vH A ) e. CH ) -> ( c i^i ( B vH A ) ) e. CH )
37 35 36 mpan2 
 |-  ( c e. CH -> ( c i^i ( B vH A ) ) e. CH )
38 chjcl 
 |-  ( ( ( c i^i B ) e. CH /\ A e. CH ) -> ( ( c i^i B ) vH A ) e. CH )
39 12 1 38 sylancl 
 |-  ( c e. CH -> ( ( c i^i B ) vH A ) e. CH )
40 chrelat3 
 |-  ( ( ( c i^i ( B vH A ) ) e. CH /\ ( ( c i^i B ) vH A ) e. CH ) -> ( ( c i^i ( B vH A ) ) C_ ( ( c i^i B ) vH A ) <-> A. p e. HAtoms ( p C_ ( c i^i ( B vH A ) ) -> p C_ ( ( c i^i B ) vH A ) ) ) )
41 37 39 40 syl2anc 
 |-  ( c e. CH -> ( ( c i^i ( B vH A ) ) C_ ( ( c i^i B ) vH A ) <-> A. p e. HAtoms ( p C_ ( c i^i ( B vH A ) ) -> p C_ ( ( c i^i B ) vH A ) ) ) )
42 41 adantr 
 |-  ( ( c e. CH /\ A C_ c ) -> ( ( c i^i ( B vH A ) ) C_ ( ( c i^i B ) vH A ) <-> A. p e. HAtoms ( p C_ ( c i^i ( B vH A ) ) -> p C_ ( ( c i^i B ) vH A ) ) ) )
43 34 42 sylibrd 
 |-  ( ( c e. CH /\ A C_ c ) -> ( 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 ) ) ) -> ( c i^i ( B vH A ) ) C_ ( ( c i^i B ) vH A ) ) )
44 43 ex 
 |-  ( c e. CH -> ( A C_ c -> ( 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 ) ) ) -> ( c i^i ( B vH A ) ) C_ ( ( c i^i B ) vH A ) ) ) )
45 44 com3r 
 |-  ( 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 ) ) ) -> ( c e. CH -> ( A C_ c -> ( c i^i ( B vH A ) ) C_ ( ( c i^i B ) vH A ) ) ) )
46 45 ralrimiv 
 |-  ( 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. c e. CH ( A C_ c -> ( c i^i ( B vH A ) ) C_ ( ( c i^i B ) vH A ) ) )
47 dmdbr2 
 |-  ( ( B e. CH /\ A e. CH ) -> ( B MH* A <-> A. c e. CH ( A C_ c -> ( c i^i ( B vH A ) ) C_ ( ( c i^i B ) vH A ) ) ) )
48 2 1 47 mp2an 
 |-  ( B MH* A <-> A. c e. CH ( A C_ c -> ( c i^i ( B vH A ) ) C_ ( ( c i^i B ) vH A ) ) )
49 46 48 sylibr 
 |-  ( 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 ) ) ) -> B MH* A )