Metamath Proof Explorer

Theorem csmdsymi

Description: Cross-symmetry implies M-symmetry. Theorem 1.9.1 of MaedaMaeda p. 3. (Contributed by NM, 24-Dec-2006) (New usage is discouraged.)

Ref Expression
Hypotheses csmdsym.1 
|- A e. CH
csmdsym.2 
|- B e. CH
Assertion csmdsymi 
|- ( ( A. c e. CH ( c MH B -> B MH* c ) /\ A MH B ) -> B MH A )

Proof

Step Hyp Ref Expression
1 csmdsym.1 
 |-  A e. CH
2 csmdsym.2 
 |-  B e. CH
3 incom 
 |-  ( A i^i B ) = ( B i^i A )
4 3 sseq1i 
 |-  ( ( A i^i B ) C_ x <-> ( B i^i A ) C_ x )
5 4 biimpri 
 |-  ( ( B i^i A ) C_ x -> ( A i^i B ) C_ x )
6 chjcom 
 |-  ( ( x e. CH /\ B e. CH ) -> ( x vH B ) = ( B vH x ) )
7 2 6 mpan2 
 |-  ( x e. CH -> ( x vH B ) = ( B vH x ) )
8 7 ineq1d 
 |-  ( x e. CH -> ( ( x vH B ) i^i A ) = ( ( B vH x ) i^i A ) )
9 incom 
 |-  ( ( B vH x ) i^i A ) = ( A i^i ( B vH x ) )
10 8 9 eqtrdi 
 |-  ( x e. CH -> ( ( x vH B ) i^i A ) = ( A i^i ( B vH x ) ) )
11 10 ad2antlr 
 |-  ( ( ( ( A. c e. CH ( c MH B -> B MH* c ) /\ A MH B ) /\ x e. CH ) /\ ( ( A i^i B ) C_ x /\ x C_ A ) ) -> ( ( x vH B ) i^i A ) = ( A i^i ( B vH x ) ) )
12 2 a1i 
 |-  ( x e. CH -> B e. CH )
13 id 
 |-  ( x e. CH -> x e. CH )
14 1 a1i 
 |-  ( x e. CH -> A e. CH )
15 12 13 14 3jca 
 |-  ( x e. CH -> ( B e. CH /\ x e. CH /\ A e. CH ) )
16 15 ad2antlr 
 |-  ( ( ( ( A. c e. CH ( c MH B -> B MH* c ) /\ A MH B ) /\ x e. CH ) /\ ( ( A i^i B ) C_ x /\ x C_ A ) ) -> ( B e. CH /\ x e. CH /\ A e. CH ) )
17 inss2 
 |-  ( A i^i B ) C_ B
18 ssid 
 |-  B C_ B
19 17 18 pm3.2i 
 |-  ( ( A i^i B ) C_ B /\ B C_ B )
20 sseq2 
 |-  ( x = if ( x e. CH , x , 0H ) -> ( ( A i^i B ) C_ x <-> ( A i^i B ) C_ if ( x e. CH , x , 0H ) ) )
21 sseq1 
 |-  ( x = if ( x e. CH , x , 0H ) -> ( x C_ A <-> if ( x e. CH , x , 0H ) C_ A ) )
22 20 21 anbi12d 
 |-  ( x = if ( x e. CH , x , 0H ) -> ( ( ( A i^i B ) C_ x /\ x C_ A ) <-> ( ( A i^i B ) C_ if ( x e. CH , x , 0H ) /\ if ( x e. CH , x , 0H ) C_ A ) ) )
23 22 3anbi2d 
 |-  ( x = if ( x e. CH , x , 0H ) -> ( ( A MH B /\ ( ( A i^i B ) C_ x /\ x C_ A ) /\ ( ( A i^i B ) C_ B /\ B C_ B ) ) <-> ( A MH B /\ ( ( A i^i B ) C_ if ( x e. CH , x , 0H ) /\ if ( x e. CH , x , 0H ) C_ A ) /\ ( ( A i^i B ) C_ B /\ B C_ B ) ) ) )
24 breq1 
 |-  ( x = if ( x e. CH , x , 0H ) -> ( x MH B <-> if ( x e. CH , x , 0H ) MH B ) )
25 23 24 imbi12d 
 |-  ( x = if ( x e. CH , x , 0H ) -> ( ( ( A MH B /\ ( ( A i^i B ) C_ x /\ x C_ A ) /\ ( ( A i^i B ) C_ B /\ B C_ B ) ) -> x MH B ) <-> ( ( A MH B /\ ( ( A i^i B ) C_ if ( x e. CH , x , 0H ) /\ if ( x e. CH , x , 0H ) C_ A ) /\ ( ( A i^i B ) C_ B /\ B C_ B ) ) -> if ( x e. CH , x , 0H ) MH B ) ) )
26 h0elch 
 |-  0H e. CH
27 26 elimel 
 |-  if ( x e. CH , x , 0H ) e. CH
28 1 2 27 2 mdslmd4i 
 |-  ( ( A MH B /\ ( ( A i^i B ) C_ if ( x e. CH , x , 0H ) /\ if ( x e. CH , x , 0H ) C_ A ) /\ ( ( A i^i B ) C_ B /\ B C_ B ) ) -> if ( x e. CH , x , 0H ) MH B )
29 25 28 dedth 
 |-  ( x e. CH -> ( ( A MH B /\ ( ( A i^i B ) C_ x /\ x C_ A ) /\ ( ( A i^i B ) C_ B /\ B C_ B ) ) -> x MH B ) )
30 29 com12 
 |-  ( ( A MH B /\ ( ( A i^i B ) C_ x /\ x C_ A ) /\ ( ( A i^i B ) C_ B /\ B C_ B ) ) -> ( x e. CH -> x MH B ) )
31 19 30 mp3an3 
 |-  ( ( A MH B /\ ( ( A i^i B ) C_ x /\ x C_ A ) ) -> ( x e. CH -> x MH B ) )
32 31 imp 
 |-  ( ( ( A MH B /\ ( ( A i^i B ) C_ x /\ x C_ A ) ) /\ x e. CH ) -> x MH B )
33 32 an32s 
 |-  ( ( ( A MH B /\ x e. CH ) /\ ( ( A i^i B ) C_ x /\ x C_ A ) ) -> x MH B )
34 33 adantlll 
 |-  ( ( ( ( A. c e. CH ( c MH B -> B MH* c ) /\ A MH B ) /\ x e. CH ) /\ ( ( A i^i B ) C_ x /\ x C_ A ) ) -> x MH B )
35 breq1 
 |-  ( c = x -> ( c MH B <-> x MH B ) )
36 breq2 
 |-  ( c = x -> ( B MH* c <-> B MH* x ) )
37 35 36 imbi12d 
 |-  ( c = x -> ( ( c MH B -> B MH* c ) <-> ( x MH B -> B MH* x ) ) )
38 37 rspccva 
 |-  ( ( A. c e. CH ( c MH B -> B MH* c ) /\ x e. CH ) -> ( x MH B -> B MH* x ) )
39 38 adantlr 
 |-  ( ( ( A. c e. CH ( c MH B -> B MH* c ) /\ A MH B ) /\ x e. CH ) -> ( x MH B -> B MH* x ) )
40 39 adantr 
 |-  ( ( ( ( A. c e. CH ( c MH B -> B MH* c ) /\ A MH B ) /\ x e. CH ) /\ ( ( A i^i B ) C_ x /\ x C_ A ) ) -> ( x MH B -> B MH* x ) )
41 34 40 mpd 
 |-  ( ( ( ( A. c e. CH ( c MH B -> B MH* c ) /\ A MH B ) /\ x e. CH ) /\ ( ( A i^i B ) C_ x /\ x C_ A ) ) -> B MH* x )
42 simprr 
 |-  ( ( ( ( A. c e. CH ( c MH B -> B MH* c ) /\ A MH B ) /\ x e. CH ) /\ ( ( A i^i B ) C_ x /\ x C_ A ) ) -> x C_ A )
43 dmdi 
 |-  ( ( ( B e. CH /\ x e. CH /\ A e. CH ) /\ ( B MH* x /\ x C_ A ) ) -> ( ( A i^i B ) vH x ) = ( A i^i ( B vH x ) ) )
44 16 41 42 43 syl12anc 
 |-  ( ( ( ( A. c e. CH ( c MH B -> B MH* c ) /\ A MH B ) /\ x e. CH ) /\ ( ( A i^i B ) C_ x /\ x C_ A ) ) -> ( ( A i^i B ) vH x ) = ( A i^i ( B vH x ) ) )
45 1 2 chincli 
 |-  ( A i^i B ) e. CH
46 chjcom 
 |-  ( ( ( A i^i B ) e. CH /\ x e. CH ) -> ( ( A i^i B ) vH x ) = ( x vH ( A i^i B ) ) )
47 45 46 mpan 
 |-  ( x e. CH -> ( ( A i^i B ) vH x ) = ( x vH ( A i^i B ) ) )
48 3 oveq2i 
 |-  ( x vH ( A i^i B ) ) = ( x vH ( B i^i A ) )
49 47 48 eqtrdi 
 |-  ( x e. CH -> ( ( A i^i B ) vH x ) = ( x vH ( B i^i A ) ) )
50 49 ad2antlr 
 |-  ( ( ( ( A. c e. CH ( c MH B -> B MH* c ) /\ A MH B ) /\ x e. CH ) /\ ( ( A i^i B ) C_ x /\ x C_ A ) ) -> ( ( A i^i B ) vH x ) = ( x vH ( B i^i A ) ) )
51 11 44 50 3eqtr2d 
 |-  ( ( ( ( A. c e. CH ( c MH B -> B MH* c ) /\ A MH B ) /\ x e. CH ) /\ ( ( A i^i B ) C_ x /\ x C_ A ) ) -> ( ( x vH B ) i^i A ) = ( x vH ( B i^i A ) ) )
52 51 ex 
 |-  ( ( ( A. c e. CH ( c MH B -> B MH* c ) /\ A MH B ) /\ x e. CH ) -> ( ( ( A i^i B ) C_ x /\ x C_ A ) -> ( ( x vH B ) i^i A ) = ( x vH ( B i^i A ) ) ) )
53 5 52 sylani 
 |-  ( ( ( A. c e. CH ( c MH B -> B MH* c ) /\ A MH B ) /\ x e. CH ) -> ( ( ( B i^i A ) C_ x /\ x C_ A ) -> ( ( x vH B ) i^i A ) = ( x vH ( B i^i A ) ) ) )
54 53 ralrimiva 
 |-  ( ( A. c e. CH ( c MH B -> B MH* c ) /\ A MH B ) -> A. x e. CH ( ( ( B i^i A ) C_ x /\ x C_ A ) -> ( ( x vH B ) i^i A ) = ( x vH ( B i^i A ) ) ) )
55 2 1 mdsl2bi 
 |-  ( B MH A <-> A. x e. CH ( ( ( B i^i A ) C_ x /\ x C_ A ) -> ( ( x vH B ) i^i A ) = ( x vH ( B i^i A ) ) ) )
56 54 55 sylibr 
 |-  ( ( A. c e. CH ( c MH B -> B MH* c ) /\ A MH B ) -> B MH A )