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 ) ) ) ) ) )
11	10	adantl	|- ( ( ( 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 ) ) )
14	13	adantll	|- ( ( ( 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 ) )
22	21	adantr	|- ( ( ( 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 ) )
32	31	adantl	|- ( ( 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	imbitrid	|- ( ( ( 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 ) ) ) ) )
54	53	adantl	|- ( ( ( 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 ) ) )
57	56	adantll	|- ( ( ( 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 ) ) )
64	63	adantr	|- ( ( ( 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 ) ) )
72	71	adantl	|- ( ( 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	imbitrid	|- ( ( ( 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 ) ) )