# Metamath Proof Explorer

## Theorem dmdmd

Description: The dual modular pair property expressed in terms of the modular pair property, that hold in Hilbert lattices. Remark 29.6 of MaedaMaeda p. 130. (Contributed by NM, 27-Apr-2006) (New usage is discouraged.)

Ref Expression
Assertion dmdmd
`|- ( ( A e. CH /\ B e. CH ) -> ( A MH* B <-> ( _|_ ` A ) MH ( _|_ ` B ) ) )`

### Proof

Step Hyp Ref Expression
1 sseq1
` |-  ( y = ( _|_ ` x ) -> ( y C_ ( _|_ ` B ) <-> ( _|_ ` x ) C_ ( _|_ ` B ) ) )`
2 oveq1
` |-  ( y = ( _|_ ` x ) -> ( y vH ( _|_ ` A ) ) = ( ( _|_ ` x ) vH ( _|_ ` A ) ) )`
3 2 ineq1d
` |-  ( y = ( _|_ ` x ) -> ( ( y vH ( _|_ ` A ) ) i^i ( _|_ ` B ) ) = ( ( ( _|_ ` x ) vH ( _|_ ` A ) ) i^i ( _|_ ` B ) ) )`
4 oveq1
` |-  ( y = ( _|_ ` x ) -> ( y vH ( ( _|_ ` A ) i^i ( _|_ ` B ) ) ) = ( ( _|_ ` x ) vH ( ( _|_ ` A ) i^i ( _|_ ` B ) ) ) )`
5 3 4 eqeq12d
` |-  ( y = ( _|_ ` x ) -> ( ( ( y vH ( _|_ ` A ) ) i^i ( _|_ ` B ) ) = ( y vH ( ( _|_ ` A ) i^i ( _|_ ` B ) ) ) <-> ( ( ( _|_ ` x ) vH ( _|_ ` A ) ) i^i ( _|_ ` B ) ) = ( ( _|_ ` x ) vH ( ( _|_ ` A ) i^i ( _|_ ` B ) ) ) ) )`
6 1 5 imbi12d
` |-  ( y = ( _|_ ` x ) -> ( ( y C_ ( _|_ ` B ) -> ( ( y vH ( _|_ ` A ) ) i^i ( _|_ ` B ) ) = ( y vH ( ( _|_ ` A ) i^i ( _|_ ` B ) ) ) ) <-> ( ( _|_ ` x ) C_ ( _|_ ` B ) -> ( ( ( _|_ ` x ) vH ( _|_ ` A ) ) i^i ( _|_ ` B ) ) = ( ( _|_ ` x ) vH ( ( _|_ ` A ) i^i ( _|_ ` B ) ) ) ) ) )`
7 6 rspccv
` |-  ( A. y e. CH ( y C_ ( _|_ ` B ) -> ( ( y vH ( _|_ ` A ) ) i^i ( _|_ ` B ) ) = ( y vH ( ( _|_ ` A ) i^i ( _|_ ` B ) ) ) ) -> ( ( _|_ ` x ) e. CH -> ( ( _|_ ` x ) C_ ( _|_ ` B ) -> ( ( ( _|_ ` x ) vH ( _|_ ` A ) ) i^i ( _|_ ` B ) ) = ( ( _|_ ` x ) vH ( ( _|_ ` A ) i^i ( _|_ ` B ) ) ) ) ) )`
8 choccl
` |-  ( x e. CH -> ( _|_ ` x ) e. CH )`
9 8 imim1i
` |-  ( ( ( _|_ ` x ) e. CH -> ( ( _|_ ` x ) C_ ( _|_ ` B ) -> ( ( ( _|_ ` x ) vH ( _|_ ` A ) ) i^i ( _|_ ` B ) ) = ( ( _|_ ` x ) vH ( ( _|_ ` A ) i^i ( _|_ ` B ) ) ) ) ) -> ( x e. CH -> ( ( _|_ ` x ) C_ ( _|_ ` B ) -> ( ( ( _|_ ` x ) vH ( _|_ ` A ) ) i^i ( _|_ ` B ) ) = ( ( _|_ ` x ) vH ( ( _|_ ` A ) i^i ( _|_ ` B ) ) ) ) ) )`
10 9 com12
` |-  ( x e. CH -> ( ( ( _|_ ` x ) e. CH -> ( ( _|_ ` x ) C_ ( _|_ ` B ) -> ( ( ( _|_ ` x ) vH ( _|_ ` A ) ) i^i ( _|_ ` B ) ) = ( ( _|_ ` x ) vH ( ( _|_ ` A ) i^i ( _|_ ` B ) ) ) ) ) -> ( ( _|_ ` x ) C_ ( _|_ ` B ) -> ( ( ( _|_ ` x ) vH ( _|_ ` A ) ) i^i ( _|_ ` B ) ) = ( ( _|_ ` x ) vH ( ( _|_ ` A ) i^i ( _|_ ` B ) ) ) ) ) )`
` |-  ( ( ( A e. CH /\ B e. CH ) /\ x e. CH ) -> ( ( ( _|_ ` x ) e. CH -> ( ( _|_ ` x ) C_ ( _|_ ` B ) -> ( ( ( _|_ ` x ) vH ( _|_ ` A ) ) i^i ( _|_ ` B ) ) = ( ( _|_ ` x ) vH ( ( _|_ ` A ) i^i ( _|_ ` B ) ) ) ) ) -> ( ( _|_ ` x ) C_ ( _|_ ` B ) -> ( ( ( _|_ ` x ) vH ( _|_ ` A ) ) i^i ( _|_ ` B ) ) = ( ( _|_ ` x ) vH ( ( _|_ ` A ) i^i ( _|_ ` B ) ) ) ) ) )`
12 chsscon3
` |-  ( ( B e. CH /\ x e. CH ) -> ( B C_ x <-> ( _|_ ` x ) C_ ( _|_ ` B ) ) )`
13 12 biimpd
` |-  ( ( B e. CH /\ x e. CH ) -> ( B C_ x -> ( _|_ ` x ) C_ ( _|_ ` B ) ) )`
` |-  ( ( ( A e. CH /\ B e. CH ) /\ x e. CH ) -> ( B C_ x -> ( _|_ ` x ) C_ ( _|_ ` B ) ) )`
15 fveq2
` |-  ( ( ( ( _|_ ` x ) vH ( _|_ ` A ) ) i^i ( _|_ ` B ) ) = ( ( _|_ ` x ) vH ( ( _|_ ` A ) i^i ( _|_ ` B ) ) ) -> ( _|_ ` ( ( ( _|_ ` x ) vH ( _|_ ` A ) ) i^i ( _|_ ` B ) ) ) = ( _|_ ` ( ( _|_ ` x ) vH ( ( _|_ ` A ) i^i ( _|_ ` B ) ) ) ) )`
16 choccl
` |-  ( A e. CH -> ( _|_ ` A ) e. CH )`
17 chjcl
` |-  ( ( ( _|_ ` x ) e. CH /\ ( _|_ ` A ) e. CH ) -> ( ( _|_ ` x ) vH ( _|_ ` A ) ) e. CH )`
18 8 16 17 syl2an
` |-  ( ( x e. CH /\ A e. CH ) -> ( ( _|_ ` x ) vH ( _|_ ` A ) ) e. CH )`
19 chdmm3
` |-  ( ( ( ( _|_ ` x ) vH ( _|_ ` A ) ) e. CH /\ B e. CH ) -> ( _|_ ` ( ( ( _|_ ` x ) vH ( _|_ ` A ) ) i^i ( _|_ ` B ) ) ) = ( ( _|_ ` ( ( _|_ ` x ) vH ( _|_ ` A ) ) ) vH B ) )`
20 18 19 sylan
` |-  ( ( ( x e. CH /\ A e. CH ) /\ B e. CH ) -> ( _|_ ` ( ( ( _|_ ` x ) vH ( _|_ ` A ) ) i^i ( _|_ ` B ) ) ) = ( ( _|_ ` ( ( _|_ ` x ) vH ( _|_ ` A ) ) ) vH B ) )`
21 chdmj4
` |-  ( ( x e. CH /\ A e. CH ) -> ( _|_ ` ( ( _|_ ` x ) vH ( _|_ ` A ) ) ) = ( x i^i A ) )`
` |-  ( ( ( x e. CH /\ A e. CH ) /\ B e. CH ) -> ( _|_ ` ( ( _|_ ` x ) vH ( _|_ ` A ) ) ) = ( x i^i A ) )`
23 22 oveq1d
` |-  ( ( ( x e. CH /\ A e. CH ) /\ B e. CH ) -> ( ( _|_ ` ( ( _|_ ` x ) vH ( _|_ ` A ) ) ) vH B ) = ( ( x i^i A ) vH B ) )`
24 20 23 eqtrd
` |-  ( ( ( x e. CH /\ A e. CH ) /\ B e. CH ) -> ( _|_ ` ( ( ( _|_ ` x ) vH ( _|_ ` A ) ) i^i ( _|_ ` B ) ) ) = ( ( x i^i A ) vH B ) )`
25 24 anasss
` |-  ( ( x e. CH /\ ( A e. CH /\ B e. CH ) ) -> ( _|_ ` ( ( ( _|_ ` x ) vH ( _|_ ` A ) ) i^i ( _|_ ` B ) ) ) = ( ( x i^i A ) vH B ) )`
26 choccl
` |-  ( B e. CH -> ( _|_ ` B ) e. CH )`
27 chincl
` |-  ( ( ( _|_ ` A ) e. CH /\ ( _|_ ` B ) e. CH ) -> ( ( _|_ ` A ) i^i ( _|_ ` B ) ) e. CH )`
28 16 26 27 syl2an
` |-  ( ( A e. CH /\ B e. CH ) -> ( ( _|_ ` A ) i^i ( _|_ ` B ) ) e. CH )`
29 chdmj2
` |-  ( ( x e. CH /\ ( ( _|_ ` A ) i^i ( _|_ ` B ) ) e. CH ) -> ( _|_ ` ( ( _|_ ` x ) vH ( ( _|_ ` A ) i^i ( _|_ ` B ) ) ) ) = ( x i^i ( _|_ ` ( ( _|_ ` A ) i^i ( _|_ ` B ) ) ) ) )`
30 28 29 sylan2
` |-  ( ( x e. CH /\ ( A e. CH /\ B e. CH ) ) -> ( _|_ ` ( ( _|_ ` x ) vH ( ( _|_ ` A ) i^i ( _|_ ` B ) ) ) ) = ( x i^i ( _|_ ` ( ( _|_ ` A ) i^i ( _|_ ` B ) ) ) ) )`
31 chdmm4
` |-  ( ( A e. CH /\ B e. CH ) -> ( _|_ ` ( ( _|_ ` A ) i^i ( _|_ ` B ) ) ) = ( A vH B ) )`
` |-  ( ( x e. CH /\ ( A e. CH /\ B e. CH ) ) -> ( _|_ ` ( ( _|_ ` A ) i^i ( _|_ ` B ) ) ) = ( A vH B ) )`
33 32 ineq2d
` |-  ( ( x e. CH /\ ( A e. CH /\ B e. CH ) ) -> ( x i^i ( _|_ ` ( ( _|_ ` A ) i^i ( _|_ ` B ) ) ) ) = ( x i^i ( A vH B ) ) )`
34 30 33 eqtrd
` |-  ( ( x e. CH /\ ( A e. CH /\ B e. CH ) ) -> ( _|_ ` ( ( _|_ ` x ) vH ( ( _|_ ` A ) i^i ( _|_ ` B ) ) ) ) = ( x i^i ( A vH B ) ) )`
35 25 34 eqeq12d
` |-  ( ( x e. CH /\ ( A e. CH /\ B e. CH ) ) -> ( ( _|_ ` ( ( ( _|_ ` x ) vH ( _|_ ` A ) ) i^i ( _|_ ` B ) ) ) = ( _|_ ` ( ( _|_ ` x ) vH ( ( _|_ ` A ) i^i ( _|_ ` B ) ) ) ) <-> ( ( x i^i A ) vH B ) = ( x i^i ( A vH B ) ) ) )`
36 35 ancoms
` |-  ( ( ( A e. CH /\ B e. CH ) /\ x e. CH ) -> ( ( _|_ ` ( ( ( _|_ ` x ) vH ( _|_ ` A ) ) i^i ( _|_ ` B ) ) ) = ( _|_ ` ( ( _|_ ` x ) vH ( ( _|_ ` A ) i^i ( _|_ ` B ) ) ) ) <-> ( ( x i^i A ) vH B ) = ( x i^i ( A vH B ) ) ) )`
37 15 36 syl5ib
` |-  ( ( ( A e. CH /\ B e. CH ) /\ x e. CH ) -> ( ( ( ( _|_ ` x ) vH ( _|_ ` A ) ) i^i ( _|_ ` B ) ) = ( ( _|_ ` x ) vH ( ( _|_ ` A ) i^i ( _|_ ` B ) ) ) -> ( ( x i^i A ) vH B ) = ( x i^i ( A vH B ) ) ) )`
38 14 37 imim12d
` |-  ( ( ( A e. CH /\ B e. CH ) /\ x e. CH ) -> ( ( ( _|_ ` x ) C_ ( _|_ ` B ) -> ( ( ( _|_ ` x ) vH ( _|_ ` A ) ) i^i ( _|_ ` B ) ) = ( ( _|_ ` x ) vH ( ( _|_ ` A ) i^i ( _|_ ` B ) ) ) ) -> ( B C_ x -> ( ( x i^i A ) vH B ) = ( x i^i ( A vH B ) ) ) ) )`
39 11 38 syld
` |-  ( ( ( A e. CH /\ B e. CH ) /\ x e. CH ) -> ( ( ( _|_ ` x ) e. CH -> ( ( _|_ ` x ) C_ ( _|_ ` B ) -> ( ( ( _|_ ` x ) vH ( _|_ ` A ) ) i^i ( _|_ ` B ) ) = ( ( _|_ ` x ) vH ( ( _|_ ` A ) i^i ( _|_ ` B ) ) ) ) ) -> ( B C_ x -> ( ( x i^i A ) vH B ) = ( x i^i ( A vH B ) ) ) ) )`
40 39 ex
` |-  ( ( A e. CH /\ B e. CH ) -> ( x e. CH -> ( ( ( _|_ ` x ) e. CH -> ( ( _|_ ` x ) C_ ( _|_ ` B ) -> ( ( ( _|_ ` x ) vH ( _|_ ` A ) ) i^i ( _|_ ` B ) ) = ( ( _|_ ` x ) vH ( ( _|_ ` A ) i^i ( _|_ ` B ) ) ) ) ) -> ( B C_ x -> ( ( x i^i A ) vH B ) = ( x i^i ( A vH B ) ) ) ) ) )`
41 40 com23
` |-  ( ( A e. CH /\ B e. CH ) -> ( ( ( _|_ ` x ) e. CH -> ( ( _|_ ` x ) C_ ( _|_ ` B ) -> ( ( ( _|_ ` x ) vH ( _|_ ` A ) ) i^i ( _|_ ` B ) ) = ( ( _|_ ` x ) vH ( ( _|_ ` A ) i^i ( _|_ ` B ) ) ) ) ) -> ( x e. CH -> ( B C_ x -> ( ( x i^i A ) vH B ) = ( x i^i ( A vH B ) ) ) ) ) )`
42 7 41 syl5
` |-  ( ( A e. CH /\ B e. CH ) -> ( A. y e. CH ( y C_ ( _|_ ` B ) -> ( ( y vH ( _|_ ` A ) ) i^i ( _|_ ` B ) ) = ( y vH ( ( _|_ ` A ) i^i ( _|_ ` B ) ) ) ) -> ( x e. CH -> ( B C_ x -> ( ( x i^i A ) vH B ) = ( x i^i ( A vH B ) ) ) ) ) )`
43 42 ralrimdv
` |-  ( ( A e. CH /\ B e. CH ) -> ( A. y e. CH ( y C_ ( _|_ ` B ) -> ( ( y vH ( _|_ ` A ) ) i^i ( _|_ ` B ) ) = ( y vH ( ( _|_ ` A ) i^i ( _|_ ` B ) ) ) ) -> A. x e. CH ( B C_ x -> ( ( x i^i A ) vH B ) = ( x i^i ( A vH B ) ) ) ) )`
44 sseq2
` |-  ( x = ( _|_ ` y ) -> ( B C_ x <-> B C_ ( _|_ ` y ) ) )`
45 ineq1
` |-  ( x = ( _|_ ` y ) -> ( x i^i A ) = ( ( _|_ ` y ) i^i A ) )`
46 45 oveq1d
` |-  ( x = ( _|_ ` y ) -> ( ( x i^i A ) vH B ) = ( ( ( _|_ ` y ) i^i A ) vH B ) )`
47 ineq1
` |-  ( x = ( _|_ ` y ) -> ( x i^i ( A vH B ) ) = ( ( _|_ ` y ) i^i ( A vH B ) ) )`
48 46 47 eqeq12d
` |-  ( x = ( _|_ ` y ) -> ( ( ( x i^i A ) vH B ) = ( x i^i ( A vH B ) ) <-> ( ( ( _|_ ` y ) i^i A ) vH B ) = ( ( _|_ ` y ) i^i ( A vH B ) ) ) )`
49 44 48 imbi12d
` |-  ( x = ( _|_ ` y ) -> ( ( B C_ x -> ( ( x i^i A ) vH B ) = ( x i^i ( A vH B ) ) ) <-> ( B C_ ( _|_ ` y ) -> ( ( ( _|_ ` y ) i^i A ) vH B ) = ( ( _|_ ` y ) i^i ( A vH B ) ) ) ) )`
50 49 rspccv
` |-  ( A. x e. CH ( B C_ x -> ( ( x i^i A ) vH B ) = ( x i^i ( A vH B ) ) ) -> ( ( _|_ ` y ) e. CH -> ( B C_ ( _|_ ` y ) -> ( ( ( _|_ ` y ) i^i A ) vH B ) = ( ( _|_ ` y ) i^i ( A vH B ) ) ) ) )`
51 choccl
` |-  ( y e. CH -> ( _|_ ` y ) e. CH )`
52 51 imim1i
` |-  ( ( ( _|_ ` y ) e. CH -> ( B C_ ( _|_ ` y ) -> ( ( ( _|_ ` y ) i^i A ) vH B ) = ( ( _|_ ` y ) i^i ( A vH B ) ) ) ) -> ( y e. CH -> ( B C_ ( _|_ ` y ) -> ( ( ( _|_ ` y ) i^i A ) vH B ) = ( ( _|_ ` y ) i^i ( A vH B ) ) ) ) )`
53 52 com12
` |-  ( y e. CH -> ( ( ( _|_ ` y ) e. CH -> ( B C_ ( _|_ ` y ) -> ( ( ( _|_ ` y ) i^i A ) vH B ) = ( ( _|_ ` y ) i^i ( A vH B ) ) ) ) -> ( B C_ ( _|_ ` y ) -> ( ( ( _|_ ` y ) i^i A ) vH B ) = ( ( _|_ ` y ) i^i ( A vH B ) ) ) ) )`
` |-  ( ( ( A e. CH /\ B e. CH ) /\ y e. CH ) -> ( ( ( _|_ ` y ) e. CH -> ( B C_ ( _|_ ` y ) -> ( ( ( _|_ ` y ) i^i A ) vH B ) = ( ( _|_ ` y ) i^i ( A vH B ) ) ) ) -> ( B C_ ( _|_ ` y ) -> ( ( ( _|_ ` y ) i^i A ) vH B ) = ( ( _|_ ` y ) i^i ( A vH B ) ) ) ) )`
55 chsscon2
` |-  ( ( B e. CH /\ y e. CH ) -> ( B C_ ( _|_ ` y ) <-> y C_ ( _|_ ` B ) ) )`
56 55 biimprd
` |-  ( ( B e. CH /\ y e. CH ) -> ( y C_ ( _|_ ` B ) -> B C_ ( _|_ ` y ) ) )`
` |-  ( ( ( A e. CH /\ B e. CH ) /\ y e. CH ) -> ( y C_ ( _|_ ` B ) -> B C_ ( _|_ ` y ) ) )`
58 fveq2
` |-  ( ( ( ( _|_ ` y ) i^i A ) vH B ) = ( ( _|_ ` y ) i^i ( A vH B ) ) -> ( _|_ ` ( ( ( _|_ ` y ) i^i A ) vH B ) ) = ( _|_ ` ( ( _|_ ` y ) i^i ( A vH B ) ) ) )`
59 chincl
` |-  ( ( ( _|_ ` y ) e. CH /\ A e. CH ) -> ( ( _|_ ` y ) i^i A ) e. CH )`
60 51 59 sylan
` |-  ( ( y e. CH /\ A e. CH ) -> ( ( _|_ ` y ) i^i A ) e. CH )`
61 chdmj1
` |-  ( ( ( ( _|_ ` y ) i^i A ) e. CH /\ B e. CH ) -> ( _|_ ` ( ( ( _|_ ` y ) i^i A ) vH B ) ) = ( ( _|_ ` ( ( _|_ ` y ) i^i A ) ) i^i ( _|_ ` B ) ) )`
62 60 61 sylan
` |-  ( ( ( y e. CH /\ A e. CH ) /\ B e. CH ) -> ( _|_ ` ( ( ( _|_ ` y ) i^i A ) vH B ) ) = ( ( _|_ ` ( ( _|_ ` y ) i^i A ) ) i^i ( _|_ ` B ) ) )`
63 chdmm2
` |-  ( ( y e. CH /\ A e. CH ) -> ( _|_ ` ( ( _|_ ` y ) i^i A ) ) = ( y vH ( _|_ ` A ) ) )`
` |-  ( ( ( y e. CH /\ A e. CH ) /\ B e. CH ) -> ( _|_ ` ( ( _|_ ` y ) i^i A ) ) = ( y vH ( _|_ ` A ) ) )`
65 64 ineq1d
` |-  ( ( ( y e. CH /\ A e. CH ) /\ B e. CH ) -> ( ( _|_ ` ( ( _|_ ` y ) i^i A ) ) i^i ( _|_ ` B ) ) = ( ( y vH ( _|_ ` A ) ) i^i ( _|_ ` B ) ) )`
66 62 65 eqtrd
` |-  ( ( ( y e. CH /\ A e. CH ) /\ B e. CH ) -> ( _|_ ` ( ( ( _|_ ` y ) i^i A ) vH B ) ) = ( ( y vH ( _|_ ` A ) ) i^i ( _|_ ` B ) ) )`
67 66 anasss
` |-  ( ( y e. CH /\ ( A e. CH /\ B e. CH ) ) -> ( _|_ ` ( ( ( _|_ ` y ) i^i A ) vH B ) ) = ( ( y vH ( _|_ ` A ) ) i^i ( _|_ ` B ) ) )`
68 chjcl
` |-  ( ( A e. CH /\ B e. CH ) -> ( A vH B ) e. CH )`
69 chdmm2
` |-  ( ( y e. CH /\ ( A vH B ) e. CH ) -> ( _|_ ` ( ( _|_ ` y ) i^i ( A vH B ) ) ) = ( y vH ( _|_ ` ( A vH B ) ) ) )`
70 68 69 sylan2
` |-  ( ( y e. CH /\ ( A e. CH /\ B e. CH ) ) -> ( _|_ ` ( ( _|_ ` y ) i^i ( A vH B ) ) ) = ( y vH ( _|_ ` ( A vH B ) ) ) )`
71 chdmj1
` |-  ( ( A e. CH /\ B e. CH ) -> ( _|_ ` ( A vH B ) ) = ( ( _|_ ` A ) i^i ( _|_ ` B ) ) )`
` |-  ( ( y e. CH /\ ( A e. CH /\ B e. CH ) ) -> ( _|_ ` ( A vH B ) ) = ( ( _|_ ` A ) i^i ( _|_ ` B ) ) )`
73 72 oveq2d
` |-  ( ( y e. CH /\ ( A e. CH /\ B e. CH ) ) -> ( y vH ( _|_ ` ( A vH B ) ) ) = ( y vH ( ( _|_ ` A ) i^i ( _|_ ` B ) ) ) )`
74 70 73 eqtrd
` |-  ( ( y e. CH /\ ( A e. CH /\ B e. CH ) ) -> ( _|_ ` ( ( _|_ ` y ) i^i ( A vH B ) ) ) = ( y vH ( ( _|_ ` A ) i^i ( _|_ ` B ) ) ) )`
75 67 74 eqeq12d
` |-  ( ( y e. CH /\ ( A e. CH /\ B e. CH ) ) -> ( ( _|_ ` ( ( ( _|_ ` y ) i^i A ) vH B ) ) = ( _|_ ` ( ( _|_ ` y ) i^i ( A vH B ) ) ) <-> ( ( y vH ( _|_ ` A ) ) i^i ( _|_ ` B ) ) = ( y vH ( ( _|_ ` A ) i^i ( _|_ ` B ) ) ) ) )`
76 75 ancoms
` |-  ( ( ( A e. CH /\ B e. CH ) /\ y e. CH ) -> ( ( _|_ ` ( ( ( _|_ ` y ) i^i A ) vH B ) ) = ( _|_ ` ( ( _|_ ` y ) i^i ( A vH B ) ) ) <-> ( ( y vH ( _|_ ` A ) ) i^i ( _|_ ` B ) ) = ( y vH ( ( _|_ ` A ) i^i ( _|_ ` B ) ) ) ) )`
77 58 76 syl5ib
` |-  ( ( ( A e. CH /\ B e. CH ) /\ y e. CH ) -> ( ( ( ( _|_ ` y ) i^i A ) vH B ) = ( ( _|_ ` y ) i^i ( A vH B ) ) -> ( ( y vH ( _|_ ` A ) ) i^i ( _|_ ` B ) ) = ( y vH ( ( _|_ ` A ) i^i ( _|_ ` B ) ) ) ) )`
78 57 77 imim12d
` |-  ( ( ( A e. CH /\ B e. CH ) /\ y e. CH ) -> ( ( B C_ ( _|_ ` y ) -> ( ( ( _|_ ` y ) i^i A ) vH B ) = ( ( _|_ ` y ) i^i ( A vH B ) ) ) -> ( y C_ ( _|_ ` B ) -> ( ( y vH ( _|_ ` A ) ) i^i ( _|_ ` B ) ) = ( y vH ( ( _|_ ` A ) i^i ( _|_ ` B ) ) ) ) ) )`
79 54 78 syld
` |-  ( ( ( A e. CH /\ B e. CH ) /\ y e. CH ) -> ( ( ( _|_ ` y ) e. CH -> ( B C_ ( _|_ ` y ) -> ( ( ( _|_ ` y ) i^i A ) vH B ) = ( ( _|_ ` y ) i^i ( A vH B ) ) ) ) -> ( y C_ ( _|_ ` B ) -> ( ( y vH ( _|_ ` A ) ) i^i ( _|_ ` B ) ) = ( y vH ( ( _|_ ` A ) i^i ( _|_ ` B ) ) ) ) ) )`
80 79 ex
` |-  ( ( A e. CH /\ B e. CH ) -> ( y e. CH -> ( ( ( _|_ ` y ) e. CH -> ( B C_ ( _|_ ` y ) -> ( ( ( _|_ ` y ) i^i A ) vH B ) = ( ( _|_ ` y ) i^i ( A vH B ) ) ) ) -> ( y C_ ( _|_ ` B ) -> ( ( y vH ( _|_ ` A ) ) i^i ( _|_ ` B ) ) = ( y vH ( ( _|_ ` A ) i^i ( _|_ ` B ) ) ) ) ) ) )`
81 80 com23
` |-  ( ( A e. CH /\ B e. CH ) -> ( ( ( _|_ ` y ) e. CH -> ( B C_ ( _|_ ` y ) -> ( ( ( _|_ ` y ) i^i A ) vH B ) = ( ( _|_ ` y ) i^i ( A vH B ) ) ) ) -> ( y e. CH -> ( y C_ ( _|_ ` B ) -> ( ( y vH ( _|_ ` A ) ) i^i ( _|_ ` B ) ) = ( y vH ( ( _|_ ` A ) i^i ( _|_ ` B ) ) ) ) ) ) )`
82 50 81 syl5
` |-  ( ( A e. CH /\ B e. CH ) -> ( A. x e. CH ( B C_ x -> ( ( x i^i A ) vH B ) = ( x i^i ( A vH B ) ) ) -> ( y e. CH -> ( y C_ ( _|_ ` B ) -> ( ( y vH ( _|_ ` A ) ) i^i ( _|_ ` B ) ) = ( y vH ( ( _|_ ` A ) i^i ( _|_ ` B ) ) ) ) ) ) )`
83 82 ralrimdv
` |-  ( ( A e. CH /\ B e. CH ) -> ( A. x e. CH ( B C_ x -> ( ( x i^i A ) vH B ) = ( x i^i ( A vH B ) ) ) -> A. y e. CH ( y C_ ( _|_ ` B ) -> ( ( y vH ( _|_ ` A ) ) i^i ( _|_ ` B ) ) = ( y vH ( ( _|_ ` A ) i^i ( _|_ ` B ) ) ) ) ) )`
84 43 83 impbid
` |-  ( ( A e. CH /\ B e. CH ) -> ( A. y e. CH ( y C_ ( _|_ ` B ) -> ( ( y vH ( _|_ ` A ) ) i^i ( _|_ ` B ) ) = ( y vH ( ( _|_ ` A ) i^i ( _|_ ` B ) ) ) ) <-> A. x e. CH ( B C_ x -> ( ( x i^i A ) vH B ) = ( x i^i ( A vH B ) ) ) ) )`
85 mdbr
` |-  ( ( ( _|_ ` A ) e. CH /\ ( _|_ ` B ) e. CH ) -> ( ( _|_ ` A ) MH ( _|_ ` B ) <-> A. y e. CH ( y C_ ( _|_ ` B ) -> ( ( y vH ( _|_ ` A ) ) i^i ( _|_ ` B ) ) = ( y vH ( ( _|_ ` A ) i^i ( _|_ ` B ) ) ) ) ) )`
86 16 26 85 syl2an
` |-  ( ( A e. CH /\ B e. CH ) -> ( ( _|_ ` A ) MH ( _|_ ` B ) <-> A. y e. CH ( y C_ ( _|_ ` B ) -> ( ( y vH ( _|_ ` A ) ) i^i ( _|_ ` B ) ) = ( y vH ( ( _|_ ` A ) i^i ( _|_ ` B ) ) ) ) ) )`
87 dmdbr
` |-  ( ( A e. CH /\ B e. CH ) -> ( A MH* B <-> A. x e. CH ( B C_ x -> ( ( x i^i A ) vH B ) = ( x i^i ( A vH B ) ) ) ) )`
88 84 86 87 3bitr4rd
` |-  ( ( A e. CH /\ B e. CH ) -> ( A MH* B <-> ( _|_ ` A ) MH ( _|_ ` B ) ) )`