Theorem cmbr2i

Description: Alternate definition of the commutes relation. Remark in Kalmbach p. 23. (Contributed by NM, 7-Aug-2004) (New usage is discouraged.)

	Ref	Expression
Hypotheses	pjoml2.1	⊢ 𝐴 ∈ Cℋ
	pjoml2.2	⊢ 𝐵 ∈ Cℋ
Assertion	cmbr2i	⊢ ( 𝐴 𝐶ℋ 𝐵 ↔ 𝐴 = ( ( 𝐴 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ ( ⊥ ‘ 𝐵 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		pjoml2.1	⊢ 𝐴 ∈ Cℋ
2		pjoml2.2	⊢ 𝐵 ∈ Cℋ
3	1 2	cmcm4i	⊢ ( 𝐴 𝐶ℋ 𝐵 ↔ ( ⊥ ‘ 𝐴 ) 𝐶ℋ ( ⊥ ‘ 𝐵 ) )
4	1	choccli	⊢ ( ⊥ ‘ 𝐴 ) ∈ Cℋ
5	2	choccli	⊢ ( ⊥ ‘ 𝐵 ) ∈ Cℋ
6	4 5	cmbri	⊢ ( ( ⊥ ‘ 𝐴 ) 𝐶ℋ ( ⊥ ‘ 𝐵 ) ↔ ( ⊥ ‘ 𝐴 ) = ( ( ( ⊥ ‘ 𝐴 ) ∩ ( ⊥ ‘ 𝐵 ) ) ∨ℋ ( ( ⊥ ‘ 𝐴 ) ∩ ( ⊥ ‘ ( ⊥ ‘ 𝐵 ) ) ) ) )
7		eqcom	⊢ ( 𝐴 = ( ( 𝐴 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ ( ⊥ ‘ 𝐵 ) ) ) ↔ ( ( 𝐴 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ ( ⊥ ‘ 𝐵 ) ) ) = 𝐴 )
8	1 2	chjcli	⊢ ( 𝐴 ∨ℋ 𝐵 ) ∈ Cℋ
9	1 5	chjcli	⊢ ( 𝐴 ∨ℋ ( ⊥ ‘ 𝐵 ) ) ∈ Cℋ
10	8 9	chincli	⊢ ( ( 𝐴 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ ( ⊥ ‘ 𝐵 ) ) ) ∈ Cℋ
11	10 1	chcon3i	⊢ ( ( ( 𝐴 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ ( ⊥ ‘ 𝐵 ) ) ) = 𝐴 ↔ ( ⊥ ‘ 𝐴 ) = ( ⊥ ‘ ( ( 𝐴 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ ( ⊥ ‘ 𝐵 ) ) ) ) )
12	8 9	chdmm1i	⊢ ( ⊥ ‘ ( ( 𝐴 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ ( ⊥ ‘ 𝐵 ) ) ) ) = ( ( ⊥ ‘ ( 𝐴 ∨ℋ 𝐵 ) ) ∨ℋ ( ⊥ ‘ ( 𝐴 ∨ℋ ( ⊥ ‘ 𝐵 ) ) ) )
13	1 2	chdmj1i	⊢ ( ⊥ ‘ ( 𝐴 ∨ℋ 𝐵 ) ) = ( ( ⊥ ‘ 𝐴 ) ∩ ( ⊥ ‘ 𝐵 ) )
14	1 5	chdmj1i	⊢ ( ⊥ ‘ ( 𝐴 ∨ℋ ( ⊥ ‘ 𝐵 ) ) ) = ( ( ⊥ ‘ 𝐴 ) ∩ ( ⊥ ‘ ( ⊥ ‘ 𝐵 ) ) )
15	13 14	oveq12i	⊢ ( ( ⊥ ‘ ( 𝐴 ∨ℋ 𝐵 ) ) ∨ℋ ( ⊥ ‘ ( 𝐴 ∨ℋ ( ⊥ ‘ 𝐵 ) ) ) ) = ( ( ( ⊥ ‘ 𝐴 ) ∩ ( ⊥ ‘ 𝐵 ) ) ∨ℋ ( ( ⊥ ‘ 𝐴 ) ∩ ( ⊥ ‘ ( ⊥ ‘ 𝐵 ) ) ) )
16	12 15	eqtri	⊢ ( ⊥ ‘ ( ( 𝐴 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ ( ⊥ ‘ 𝐵 ) ) ) ) = ( ( ( ⊥ ‘ 𝐴 ) ∩ ( ⊥ ‘ 𝐵 ) ) ∨ℋ ( ( ⊥ ‘ 𝐴 ) ∩ ( ⊥ ‘ ( ⊥ ‘ 𝐵 ) ) ) )
17	16	eqeq2i	⊢ ( ( ⊥ ‘ 𝐴 ) = ( ⊥ ‘ ( ( 𝐴 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ ( ⊥ ‘ 𝐵 ) ) ) ) ↔ ( ⊥ ‘ 𝐴 ) = ( ( ( ⊥ ‘ 𝐴 ) ∩ ( ⊥ ‘ 𝐵 ) ) ∨ℋ ( ( ⊥ ‘ 𝐴 ) ∩ ( ⊥ ‘ ( ⊥ ‘ 𝐵 ) ) ) ) )
18	7 11 17	3bitrri	⊢ ( ( ⊥ ‘ 𝐴 ) = ( ( ( ⊥ ‘ 𝐴 ) ∩ ( ⊥ ‘ 𝐵 ) ) ∨ℋ ( ( ⊥ ‘ 𝐴 ) ∩ ( ⊥ ‘ ( ⊥ ‘ 𝐵 ) ) ) ) ↔ 𝐴 = ( ( 𝐴 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ ( ⊥ ‘ 𝐵 ) ) ) )
19	3 6 18	3bitri	⊢ ( 𝐴 𝐶ℋ 𝐵 ↔ 𝐴 = ( ( 𝐴 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ ( ⊥ ‘ 𝐵 ) ) ) )