Theorem omllaw5N

Description: The orthomodular law. Remark in Kalmbach p. 22. ( pjoml5 analog.) (Contributed by NM, 14-Nov-2011) (New usage is discouraged.)

	Ref	Expression
Hypotheses	omllaw5.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
	omllaw5.j	⊢ ∨ = ( join ‘ 𝐾 )
	omllaw5.m	⊢ ∧ = ( meet ‘ 𝐾 )
	omllaw5.o	⊢ ⊥ = ( oc ‘ 𝐾 )
Assertion	omllaw5N	⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ∨ ( ( ⊥ ‘ 𝑋 ) ∧ ( 𝑋 ∨ 𝑌 ) ) ) = ( 𝑋 ∨ 𝑌 ) )

Proof

Step	Hyp	Ref	Expression
1		omllaw5.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
2		omllaw5.j	⊢ ∨ = ( join ‘ 𝐾 )
3		omllaw5.m	⊢ ∧ = ( meet ‘ 𝐾 )
4		omllaw5.o	⊢ ⊥ = ( oc ‘ 𝐾 )
5		simp1	⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝐾 ∈ OML )
6		simp2	⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝑋 ∈ 𝐵 )
7		omllat	⊢ ( 𝐾 ∈ OML → 𝐾 ∈ Lat )
8	1 2	latjcl	⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ∨ 𝑌 ) ∈ 𝐵 )
9	7 8	syl3an1	⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ∨ 𝑌 ) ∈ 𝐵 )
10	5 6 9	3jca	⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ ( 𝑋 ∨ 𝑌 ) ∈ 𝐵 ) )
11		eqid	⊢ ( le ‘ 𝐾 ) = ( le ‘ 𝐾 )
12	1 11 2	latlej1	⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝑋 ( le ‘ 𝐾 ) ( 𝑋 ∨ 𝑌 ) )
13	7 12	syl3an1	⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝑋 ( le ‘ 𝐾 ) ( 𝑋 ∨ 𝑌 ) )
14	1 11 2 3 4	omllaw2N	⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ ( 𝑋 ∨ 𝑌 ) ∈ 𝐵 ) → ( 𝑋 ( le ‘ 𝐾 ) ( 𝑋 ∨ 𝑌 ) → ( 𝑋 ∨ ( ( ⊥ ‘ 𝑋 ) ∧ ( 𝑋 ∨ 𝑌 ) ) ) = ( 𝑋 ∨ 𝑌 ) ) )
15	10 13 14	sylc	⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ∨ ( ( ⊥ ‘ 𝑋 ) ∧ ( 𝑋 ∨ 𝑌 ) ) ) = ( 𝑋 ∨ 𝑌 ) )