# Metamath Proof Explorer

## Theorem mddmd

Description: The modular pair property expressed in terms of the dual modular pair property. (Contributed by NM, 27-Apr-2006) (New usage is discouraged.)

Ref Expression
Assertion mddmd ${⊢}\left({A}\in {\mathbf{C}}_{ℋ}\wedge {B}\in {\mathbf{C}}_{ℋ}\right)\to \left({A}{𝑀}_{ℋ}{B}↔\perp \left({A}\right){𝑀}_{ℋ}^{*}\perp \left({B}\right)\right)$

### Proof

Step Hyp Ref Expression
1 choccl ${⊢}{A}\in {\mathbf{C}}_{ℋ}\to \perp \left({A}\right)\in {\mathbf{C}}_{ℋ}$
2 choccl ${⊢}{B}\in {\mathbf{C}}_{ℋ}\to \perp \left({B}\right)\in {\mathbf{C}}_{ℋ}$
3 dmdmd ${⊢}\left(\perp \left({A}\right)\in {\mathbf{C}}_{ℋ}\wedge \perp \left({B}\right)\in {\mathbf{C}}_{ℋ}\right)\to \left(\perp \left({A}\right){𝑀}_{ℋ}^{*}\perp \left({B}\right)↔\perp \left(\perp \left({A}\right)\right){𝑀}_{ℋ}\perp \left(\perp \left({B}\right)\right)\right)$
4 1 2 3 syl2an ${⊢}\left({A}\in {\mathbf{C}}_{ℋ}\wedge {B}\in {\mathbf{C}}_{ℋ}\right)\to \left(\perp \left({A}\right){𝑀}_{ℋ}^{*}\perp \left({B}\right)↔\perp \left(\perp \left({A}\right)\right){𝑀}_{ℋ}\perp \left(\perp \left({B}\right)\right)\right)$
5 ococ ${⊢}{A}\in {\mathbf{C}}_{ℋ}\to \perp \left(\perp \left({A}\right)\right)={A}$
6 ococ ${⊢}{B}\in {\mathbf{C}}_{ℋ}\to \perp \left(\perp \left({B}\right)\right)={B}$
7 5 6 breqan12d ${⊢}\left({A}\in {\mathbf{C}}_{ℋ}\wedge {B}\in {\mathbf{C}}_{ℋ}\right)\to \left(\perp \left(\perp \left({A}\right)\right){𝑀}_{ℋ}\perp \left(\perp \left({B}\right)\right)↔{A}{𝑀}_{ℋ}{B}\right)$
8 4 7 bitr2d ${⊢}\left({A}\in {\mathbf{C}}_{ℋ}\wedge {B}\in {\mathbf{C}}_{ℋ}\right)\to \left({A}{𝑀}_{ℋ}{B}↔\perp \left({A}\right){𝑀}_{ℋ}^{*}\perp \left({B}\right)\right)$