Theorem mdcompli

Description: A condition equivalent to the modular pair property. Part of proof of Theorem 1.14 of MaedaMaeda p. 4. (Contributed by NM, 29-Apr-2006) (New usage is discouraged.)

	Ref	Expression
Hypotheses	mdcompl.1	⊢ 𝐴 ∈ Cℋ
	mdcompl.2	⊢ 𝐵 ∈ Cℋ
Assertion	mdcompli	⊢ ( 𝐴 𝑀ℋ 𝐵 ↔ ( 𝐴 ∩ ( ⊥ ‘ ( 𝐴 ∩ 𝐵 ) ) ) 𝑀ℋ ( 𝐵 ∩ ( ⊥ ‘ ( 𝐴 ∩ 𝐵 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		mdcompl.1	⊢ 𝐴 ∈ Cℋ
2		mdcompl.2	⊢ 𝐵 ∈ Cℋ
3	1 2	chincli	⊢ ( 𝐴 ∩ 𝐵 ) ∈ Cℋ
4	3	mdoc1i	⊢ ( 𝐴 ∩ 𝐵 ) 𝑀ℋ ( ⊥ ‘ ( 𝐴 ∩ 𝐵 ) )
5	3	dmdoc2i	⊢ ( ⊥ ‘ ( 𝐴 ∩ 𝐵 ) ) 𝑀ℋ* ( 𝐴 ∩ 𝐵 )
6		ssid	⊢ ( 𝐴 ∩ 𝐵 ) ⊆ ( 𝐴 ∩ 𝐵 )
7	1 2	chjcli	⊢ ( 𝐴 ∨ℋ 𝐵 ) ∈ Cℋ
8	7	chssii	⊢ ( 𝐴 ∨ℋ 𝐵 ) ⊆ ℋ
9	3	chjoi	⊢ ( ( 𝐴 ∩ 𝐵 ) ∨ℋ ( ⊥ ‘ ( 𝐴 ∩ 𝐵 ) ) ) = ℋ
10	8 9	sseqtrri	⊢ ( 𝐴 ∨ℋ 𝐵 ) ⊆ ( ( 𝐴 ∩ 𝐵 ) ∨ℋ ( ⊥ ‘ ( 𝐴 ∩ 𝐵 ) ) )
11	3	choccli	⊢ ( ⊥ ‘ ( 𝐴 ∩ 𝐵 ) ) ∈ Cℋ
12	3 11 1 2	mdslmd1i	⊢ ( ( ( ( 𝐴 ∩ 𝐵 ) 𝑀ℋ ( ⊥ ‘ ( 𝐴 ∩ 𝐵 ) ) ∧ ( ⊥ ‘ ( 𝐴 ∩ 𝐵 ) ) 𝑀ℋ* ( 𝐴 ∩ 𝐵 ) ) ∧ ( ( 𝐴 ∩ 𝐵 ) ⊆ ( 𝐴 ∩ 𝐵 ) ∧ ( 𝐴 ∨ℋ 𝐵 ) ⊆ ( ( 𝐴 ∩ 𝐵 ) ∨ℋ ( ⊥ ‘ ( 𝐴 ∩ 𝐵 ) ) ) ) ) → ( 𝐴 𝑀ℋ 𝐵 ↔ ( 𝐴 ∩ ( ⊥ ‘ ( 𝐴 ∩ 𝐵 ) ) ) 𝑀ℋ ( 𝐵 ∩ ( ⊥ ‘ ( 𝐴 ∩ 𝐵 ) ) ) ) )
13	4 5 6 10 12	mp4an	⊢ ( 𝐴 𝑀ℋ 𝐵 ↔ ( 𝐴 ∩ ( ⊥ ‘ ( 𝐴 ∩ 𝐵 ) ) ) 𝑀ℋ ( 𝐵 ∩ ( ⊥ ‘ ( 𝐴 ∩ 𝐵 ) ) ) )