Theorem pjoml5

Description: The orthomodular law. Remark in Kalmbach p. 22. (Contributed by NM, 12-Jun-2006) (New usage is discouraged.)

	Ref	Expression
Assertion	pjoml5	⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( 𝐴 ∨ℋ ( ( ⊥ ‘ 𝐴 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ) = ( 𝐴 ∨ℋ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		simpl	⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → 𝐴 ∈ Cℋ )
2		chjcl	⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( 𝐴 ∨ℋ 𝐵 ) ∈ Cℋ )
3		chub1	⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → 𝐴 ⊆ ( 𝐴 ∨ℋ 𝐵 ) )
4		pjoml2	⊢ ( ( 𝐴 ∈ Cℋ ∧ ( 𝐴 ∨ℋ 𝐵 ) ∈ Cℋ ∧ 𝐴 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) → ( 𝐴 ∨ℋ ( ( ⊥ ‘ 𝐴 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ) = ( 𝐴 ∨ℋ 𝐵 ) )
5	1 2 3 4	syl3anc	⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( 𝐴 ∨ℋ ( ( ⊥ ‘ 𝐴 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ) = ( 𝐴 ∨ℋ 𝐵 ) )