# Metamath Proof Explorer

## Theorem cmdmdi

Description: Commuting subspaces form a dual modular pair. (Contributed by NM, 25-Apr-2006) (New usage is discouraged.)

Ref Expression
Hypotheses sumdmdi.1 ${⊢}{A}\in {\mathbf{C}}_{ℋ}$
sumdmdi.2 ${⊢}{B}\in {\mathbf{C}}_{ℋ}$
Assertion cmdmdi ${⊢}{A}{𝐶}_{ℋ}{B}\to {A}{𝑀}_{ℋ}^{*}{B}$

### Proof

Step Hyp Ref Expression
1 sumdmdi.1 ${⊢}{A}\in {\mathbf{C}}_{ℋ}$
2 sumdmdi.2 ${⊢}{B}\in {\mathbf{C}}_{ℋ}$
3 1 choccli ${⊢}\perp \left({A}\right)\in {\mathbf{C}}_{ℋ}$
4 2 choccli ${⊢}\perp \left({B}\right)\in {\mathbf{C}}_{ℋ}$
5 3 4 cmmdi ${⊢}\perp \left({A}\right){𝐶}_{ℋ}\perp \left({B}\right)\to \perp \left({A}\right){𝑀}_{ℋ}\perp \left({B}\right)$
6 1 2 cmcm4i ${⊢}{A}{𝐶}_{ℋ}{B}↔\perp \left({A}\right){𝐶}_{ℋ}\perp \left({B}\right)$
7 dmdmd ${⊢}\left({A}\in {\mathbf{C}}_{ℋ}\wedge {B}\in {\mathbf{C}}_{ℋ}\right)\to \left({A}{𝑀}_{ℋ}^{*}{B}↔\perp \left({A}\right){𝑀}_{ℋ}\perp \left({B}\right)\right)$
8 1 2 7 mp2an ${⊢}{A}{𝑀}_{ℋ}^{*}{B}↔\perp \left({A}\right){𝑀}_{ℋ}\perp \left({B}\right)$
9 5 6 8 3imtr4i ${⊢}{A}{𝐶}_{ℋ}{B}\to {A}{𝑀}_{ℋ}^{*}{B}$