Theorem omllaw3

Description: Orthomodular law equivalent. Theorem 2(ii) of Kalmbach p. 22. ( pjoml analog.) (Contributed by NM, 19-Oct-2011)

	Ref	Expression
Hypotheses	omllaw3.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
	omllaw3.l	⊢ ≤ = ( le ‘ 𝐾 )
	omllaw3.m	⊢ ∧ = ( meet ‘ 𝐾 )
	omllaw3.o	⊢ ⊥ = ( oc ‘ 𝐾 )
	omllaw3.z	⊢ 0 = ( 0. ‘ 𝐾 )
Assertion	omllaw3	⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( 𝑋 ≤ 𝑌 ∧ ( 𝑌 ∧ ( ⊥ ‘ 𝑋 ) ) = 0 ) → 𝑋 = 𝑌 ) )

Proof

Step	Hyp	Ref	Expression
1		omllaw3.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
2		omllaw3.l	⊢ ≤ = ( le ‘ 𝐾 )
3		omllaw3.m	⊢ ∧ = ( meet ‘ 𝐾 )
4		omllaw3.o	⊢ ⊥ = ( oc ‘ 𝐾 )
5		omllaw3.z	⊢ 0 = ( 0. ‘ 𝐾 )
6		oveq2	⊢ ( ( 𝑌 ∧ ( ⊥ ‘ 𝑋 ) ) = 0 → ( 𝑋 ( join ‘ 𝐾 ) ( 𝑌 ∧ ( ⊥ ‘ 𝑋 ) ) ) = ( 𝑋 ( join ‘ 𝐾 ) 0 ) )
7	6	adantl	⊢ ( ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑌 ∧ ( ⊥ ‘ 𝑋 ) ) = 0 ) → ( 𝑋 ( join ‘ 𝐾 ) ( 𝑌 ∧ ( ⊥ ‘ 𝑋 ) ) ) = ( 𝑋 ( join ‘ 𝐾 ) 0 ) )
8		omlol	⊢ ( 𝐾 ∈ OML → 𝐾 ∈ OL )
9		eqid	⊢ ( join ‘ 𝐾 ) = ( join ‘ 𝐾 )
10	1 9 5	olj01	⊢ ( ( 𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ) → ( 𝑋 ( join ‘ 𝐾 ) 0 ) = 𝑋 )
11	8 10	sylan	⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ) → ( 𝑋 ( join ‘ 𝐾 ) 0 ) = 𝑋 )
12	11	3adant3	⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ( join ‘ 𝐾 ) 0 ) = 𝑋 )
13	12	adantr	⊢ ( ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑌 ∧ ( ⊥ ‘ 𝑋 ) ) = 0 ) → ( 𝑋 ( join ‘ 𝐾 ) 0 ) = 𝑋 )
14	7 13	eqtr2d	⊢ ( ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑌 ∧ ( ⊥ ‘ 𝑋 ) ) = 0 ) → 𝑋 = ( 𝑋 ( join ‘ 𝐾 ) ( 𝑌 ∧ ( ⊥ ‘ 𝑋 ) ) ) )
15	14	adantrl	⊢ ( ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑋 ≤ 𝑌 ∧ ( 𝑌 ∧ ( ⊥ ‘ 𝑋 ) ) = 0 ) ) → 𝑋 = ( 𝑋 ( join ‘ 𝐾 ) ( 𝑌 ∧ ( ⊥ ‘ 𝑋 ) ) ) )
16	1 2 9 3 4	omllaw	⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ≤ 𝑌 → 𝑌 = ( 𝑋 ( join ‘ 𝐾 ) ( 𝑌 ∧ ( ⊥ ‘ 𝑋 ) ) ) ) )
17	16	imp	⊢ ( ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 ≤ 𝑌 ) → 𝑌 = ( 𝑋 ( join ‘ 𝐾 ) ( 𝑌 ∧ ( ⊥ ‘ 𝑋 ) ) ) )
18	17	adantrr	⊢ ( ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑋 ≤ 𝑌 ∧ ( 𝑌 ∧ ( ⊥ ‘ 𝑋 ) ) = 0 ) ) → 𝑌 = ( 𝑋 ( join ‘ 𝐾 ) ( 𝑌 ∧ ( ⊥ ‘ 𝑋 ) ) ) )
19	15 18	eqtr4d	⊢ ( ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑋 ≤ 𝑌 ∧ ( 𝑌 ∧ ( ⊥ ‘ 𝑋 ) ) = 0 ) ) → 𝑋 = 𝑌 )
20	19	ex	⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( 𝑋 ≤ 𝑌 ∧ ( 𝑌 ∧ ( ⊥ ‘ 𝑋 ) ) = 0 ) → 𝑋 = 𝑌 ) )