Theorem mdbr

Description: Binary relation expressing <. A , B >. is a modular pair. Definition 1.1 of MaedaMaeda p. 1. (Contributed by NM, 14-Jun-2004) (New usage is discouraged.)

	Ref	Expression
Assertion	mdbr	|- ( ( A e. CH /\ B e. CH ) -> ( A MH B <-> A. x e. CH ( x C_ B -> ( ( x vH A ) i^i B ) = ( x vH ( A i^i B ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		eleq1	|- ( y = A -> ( y e. CH <-> A e. CH ) )
2	1	anbi1d	|- ( y = A -> ( ( y e. CH /\ z e. CH ) <-> ( A e. CH /\ z e. CH ) ) )
3		oveq2	|- ( y = A -> ( x vH y ) = ( x vH A ) )
4	3	ineq1d	|- ( y = A -> ( ( x vH y ) i^i z ) = ( ( x vH A ) i^i z ) )
5		ineq1	|- ( y = A -> ( y i^i z ) = ( A i^i z ) )
6	5	oveq2d	|- ( y = A -> ( x vH ( y i^i z ) ) = ( x vH ( A i^i z ) ) )
7	4 6	eqeq12d	|- ( y = A -> ( ( ( x vH y ) i^i z ) = ( x vH ( y i^i z ) ) <-> ( ( x vH A ) i^i z ) = ( x vH ( A i^i z ) ) ) )
8	7	imbi2d	|- ( y = A -> ( ( x C_ z -> ( ( x vH y ) i^i z ) = ( x vH ( y i^i z ) ) ) <-> ( x C_ z -> ( ( x vH A ) i^i z ) = ( x vH ( A i^i z ) ) ) ) )
9	8	ralbidv	|- ( y = A -> ( A. x e. CH ( x C_ z -> ( ( x vH y ) i^i z ) = ( x vH ( y i^i z ) ) ) <-> A. x e. CH ( x C_ z -> ( ( x vH A ) i^i z ) = ( x vH ( A i^i z ) ) ) ) )
10	2 9	anbi12d	|- ( y = A -> ( ( ( y e. CH /\ z e. CH ) /\ A. x e. CH ( x C_ z -> ( ( x vH y ) i^i z ) = ( x vH ( y i^i z ) ) ) ) <-> ( ( A e. CH /\ z e. CH ) /\ A. x e. CH ( x C_ z -> ( ( x vH A ) i^i z ) = ( x vH ( A i^i z ) ) ) ) ) )
11		eleq1	|- ( z = B -> ( z e. CH <-> B e. CH ) )
12	11	anbi2d	|- ( z = B -> ( ( A e. CH /\ z e. CH ) <-> ( A e. CH /\ B e. CH ) ) )
13		sseq2	|- ( z = B -> ( x C_ z <-> x C_ B ) )
14		ineq2	|- ( z = B -> ( ( x vH A ) i^i z ) = ( ( x vH A ) i^i B ) )
15		ineq2	|- ( z = B -> ( A i^i z ) = ( A i^i B ) )
16	15	oveq2d	|- ( z = B -> ( x vH ( A i^i z ) ) = ( x vH ( A i^i B ) ) )
17	14 16	eqeq12d	|- ( z = B -> ( ( ( x vH A ) i^i z ) = ( x vH ( A i^i z ) ) <-> ( ( x vH A ) i^i B ) = ( x vH ( A i^i B ) ) ) )
18	13 17	imbi12d	|- ( z = B -> ( ( x C_ z -> ( ( x vH A ) i^i z ) = ( x vH ( A i^i z ) ) ) <-> ( x C_ B -> ( ( x vH A ) i^i B ) = ( x vH ( A i^i B ) ) ) ) )
19	18	ralbidv	|- ( z = B -> ( A. x e. CH ( x C_ z -> ( ( x vH A ) i^i z ) = ( x vH ( A i^i z ) ) ) <-> A. x e. CH ( x C_ B -> ( ( x vH A ) i^i B ) = ( x vH ( A i^i B ) ) ) ) )
20	12 19	anbi12d	|- ( z = B -> ( ( ( A e. CH /\ z e. CH ) /\ A. x e. CH ( x C_ z -> ( ( x vH A ) i^i z ) = ( x vH ( A i^i z ) ) ) ) <-> ( ( A e. CH /\ B e. CH ) /\ A. x e. CH ( x C_ B -> ( ( x vH A ) i^i B ) = ( x vH ( A i^i B ) ) ) ) ) )
21		df-md	|- MH = { <. y , z >. | ( ( y e. CH /\ z e. CH ) /\ A. x e. CH ( x C_ z -> ( ( x vH y ) i^i z ) = ( x vH ( y i^i z ) ) ) ) }
22	10 20 21	brabg	|- ( ( A e. CH /\ B e. CH ) -> ( A MH B <-> ( ( A e. CH /\ B e. CH ) /\ A. x e. CH ( x C_ B -> ( ( x vH A ) i^i B ) = ( x vH ( A i^i B ) ) ) ) ) )
23	22	bianabs	|- ( ( A e. CH /\ B e. CH ) -> ( A MH B <-> A. x e. CH ( x C_ B -> ( ( x vH A ) i^i B ) = ( x vH ( A i^i B ) ) ) ) )