Metamath Proof Explorer

Theorem omlspjN

Description: Contraction of a Sasaki projection. (Contributed by NM, 6-Dec-2013) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 omlspj.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 omlspj.l ⊢ ≤ = ( le ‘ 𝐾 )
3 omlspj.j ⊢ ∨ = ( join ‘ 𝐾 )
4 omlspj.m ⊢ ∧ = ( meet ‘ 𝐾 )
5 omlspj.o ⊢ ⊥ = ( oc ‘ 𝐾 )
6 omllat ⊢ ( 𝐾 ∈ OML → 𝐾 ∈ Lat )
7 6 3ad2ant1 ⊢ ( ( 𝐾 ∈ OML ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 ≤ 𝑌 ) → 𝐾 ∈ Lat )
8 omlop ⊢ ( 𝐾 ∈ OML → 𝐾 ∈ OP )
9 8 3ad2ant1 ⊢ ( ( 𝐾 ∈ OML ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 ≤ 𝑌 ) → 𝐾 ∈ OP )
10 simp2r ⊢ ( ( 𝐾 ∈ OML ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 ≤ 𝑌 ) → 𝑌 ∈ 𝐵 )
11 1 5 opoccl ⊢ ( ( 𝐾 ∈ OP ∧ 𝑌 ∈ 𝐵 ) → ( ⊥ ‘ 𝑌 ) ∈ 𝐵 )
12 9 10 11 syl2anc ⊢ ( ( 𝐾 ∈ OML ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 ≤ 𝑌 ) → ( ⊥ ‘ 𝑌 ) ∈ 𝐵 )
13 1 4 latmcom ⊢ ( ( 𝐾 ∈ Lat ∧ ( ⊥ ‘ 𝑌 ) ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( ⊥ ‘ 𝑌 ) ∧ 𝑌 ) = ( 𝑌 ∧ ( ⊥ ‘ 𝑌 ) ) )
14 7 12 10 13 syl3anc ⊢ ( ( 𝐾 ∈ OML ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 ≤ 𝑌 ) → ( ( ⊥ ‘ 𝑌 ) ∧ 𝑌 ) = ( 𝑌 ∧ ( ⊥ ‘ 𝑌 ) ) )
15 eqid ⊢ ( 0. ‘ 𝐾 ) = ( 0. ‘ 𝐾 )
16 1 5 4 15 opnoncon ⊢ ( ( 𝐾 ∈ OP ∧ 𝑌 ∈ 𝐵 ) → ( 𝑌 ∧ ( ⊥ ‘ 𝑌 ) ) = ( 0. ‘ 𝐾 ) )
17 9 10 16 syl2anc ⊢ ( ( 𝐾 ∈ OML ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 ≤ 𝑌 ) → ( 𝑌 ∧ ( ⊥ ‘ 𝑌 ) ) = ( 0. ‘ 𝐾 ) )
18 14 17 eqtrd ⊢ ( ( 𝐾 ∈ OML ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 ≤ 𝑌 ) → ( ( ⊥ ‘ 𝑌 ) ∧ 𝑌 ) = ( 0. ‘ 𝐾 ) )
19 18 oveq2d ⊢ ( ( 𝐾 ∈ OML ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 ≤ 𝑌 ) → ( 𝑋 ∨ ( ( ⊥ ‘ 𝑌 ) ∧ 𝑌 ) ) = ( 𝑋 ∨ ( 0. ‘ 𝐾 ) ) )
20 simp1 ⊢ ( ( 𝐾 ∈ OML ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 ≤ 𝑌 ) → 𝐾 ∈ OML )
21 simp2l ⊢ ( ( 𝐾 ∈ OML ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 ≤ 𝑌 ) → 𝑋 ∈ 𝐵 )
22 simp3 ⊢ ( ( 𝐾 ∈ OML ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 ≤ 𝑌 ) → 𝑋 ≤ 𝑌 )
23 eqid ⊢ ( cm ‘ 𝐾 ) = ( cm ‘ 𝐾 )
24 1 23 cmtidN ⊢ ( ( 𝐾 ∈ OML ∧ 𝑌 ∈ 𝐵 ) → 𝑌 ( cm ‘ 𝐾 ) 𝑌 )
25 20 10 24 syl2anc ⊢ ( ( 𝐾 ∈ OML ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 ≤ 𝑌 ) → 𝑌 ( cm ‘ 𝐾 ) 𝑌 )
26 1 5 23 cmt3N ⊢ ( ( 𝐾 ∈ OML ∧ 𝑌 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑌 ( cm ‘ 𝐾 ) 𝑌 ↔ ( ⊥ ‘ 𝑌 ) ( cm ‘ 𝐾 ) 𝑌 ) )
27 20 10 10 26 syl3anc ⊢ ( ( 𝐾 ∈ OML ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 ≤ 𝑌 ) → ( 𝑌 ( cm ‘ 𝐾 ) 𝑌 ↔ ( ⊥ ‘ 𝑌 ) ( cm ‘ 𝐾 ) 𝑌 ) )
28 25 27 mpbid ⊢ ( ( 𝐾 ∈ OML ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 ≤ 𝑌 ) → ( ⊥ ‘ 𝑌 ) ( cm ‘ 𝐾 ) 𝑌 )
29 1 2 3 4 23 omlmod1i2N ⊢ ( ( 𝐾 ∈ OML ∧ ( 𝑋 ∈ 𝐵 ∧ ( ⊥ ‘ 𝑌 ) ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑋 ≤ 𝑌 ∧ ( ⊥ ‘ 𝑌 ) ( cm ‘ 𝐾 ) 𝑌 ) ) → ( 𝑋 ∨ ( ( ⊥ ‘ 𝑌 ) ∧ 𝑌 ) ) = ( ( 𝑋 ∨ ( ⊥ ‘ 𝑌 ) ) ∧ 𝑌 ) )
30 20 21 12 10 22 28 29 syl132anc ⊢ ( ( 𝐾 ∈ OML ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 ≤ 𝑌 ) → ( 𝑋 ∨ ( ( ⊥ ‘ 𝑌 ) ∧ 𝑌 ) ) = ( ( 𝑋 ∨ ( ⊥ ‘ 𝑌 ) ) ∧ 𝑌 ) )
31 omlol ⊢ ( 𝐾 ∈ OML → 𝐾 ∈ OL )
32 31 3ad2ant1 ⊢ ( ( 𝐾 ∈ OML ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 ≤ 𝑌 ) → 𝐾 ∈ OL )
33 1 3 15 olj01 ⊢ ( ( 𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ) → ( 𝑋 ∨ ( 0. ‘ 𝐾 ) ) = 𝑋 )
34 32 21 33 syl2anc ⊢ ( ( 𝐾 ∈ OML ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 ≤ 𝑌 ) → ( 𝑋 ∨ ( 0. ‘ 𝐾 ) ) = 𝑋 )
35 19 30 34 3eqtr3d ⊢ ( ( 𝐾 ∈ OML ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 ≤ 𝑌 ) → ( ( 𝑋 ∨ ( ⊥ ‘ 𝑌 ) ) ∧ 𝑌 ) = 𝑋 )