This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem olm11

Description: The meet of an ortholattice element with one equals itself. ( chm1i analog.) (Contributed by NM, 22-May-2012)

Ref Expression
Hypotheses olm1.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
olm1.m ⊢ ∧ = ( meet ‘ 𝐾 )
olm1.u ⊢ 1 = ( 1. ‘ 𝐾 )
Assertion olm11 ( ( 𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ) → ( 𝑋 ∧ 1 ) = 𝑋 )

Proof

Step Hyp Ref Expression
1 olm1.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 olm1.m ⊢ ∧ = ( meet ‘ 𝐾 )
3 olm1.u ⊢ 1 = ( 1. ‘ 𝐾 )
4 olop ⊢ ( 𝐾 ∈ OL → 𝐾 ∈ OP )
5 4 adantr ⊢ ( ( 𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ) → 𝐾 ∈ OP )
6 eqid ⊢ ( 0. ‘ 𝐾 ) = ( 0. ‘ 𝐾 )
7 eqid ⊢ ( oc ‘ 𝐾 ) = ( oc ‘ 𝐾 )
8 6 3 7 opoc1 ⊢ ( 𝐾 ∈ OP → ( ( oc ‘ 𝐾 ) ‘ 1 ) = ( 0. ‘ 𝐾 ) )
9 5 8 syl ⊢ ( ( 𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ) → ( ( oc ‘ 𝐾 ) ‘ 1 ) = ( 0. ‘ 𝐾 ) )
10 9 oveq2d ⊢ ( ( 𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ) → ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ 1 ) ) = ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) ( 0. ‘ 𝐾 ) ) )
11 1 7 opoccl ⊢ ( ( 𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ) → ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∈ 𝐵 )
12 4 11 sylan ⊢ ( ( 𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ) → ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∈ 𝐵 )
13 eqid ⊢ ( join ‘ 𝐾 ) = ( join ‘ 𝐾 )
14 1 13 6 olj01 ⊢ ( ( 𝐾 ∈ OL ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∈ 𝐵 ) → ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) ( 0. ‘ 𝐾 ) ) = ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) )
15 12 14 syldan ⊢ ( ( 𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ) → ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) ( 0. ‘ 𝐾 ) ) = ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) )
16 10 15 eqtrd ⊢ ( ( 𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ) → ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ 1 ) ) = ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) )
17 16 fveq2d ⊢ ( ( 𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ) → ( ( oc ‘ 𝐾 ) ‘ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ 1 ) ) ) = ( ( oc ‘ 𝐾 ) ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ) )
18 1 3 op1cl ⊢ ( 𝐾 ∈ OP → 1 ∈ 𝐵 )
19 5 18 syl ⊢ ( ( 𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ) → 1 ∈ 𝐵 )
20 1 13 2 7 oldmj4 ⊢ ( ( 𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ∧ 1 ∈ 𝐵 ) → ( ( oc ‘ 𝐾 ) ‘ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ 1 ) ) ) = ( 𝑋 ∧ 1 ) )
21 19 20 mpd3an3 ⊢ ( ( 𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ) → ( ( oc ‘ 𝐾 ) ‘ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( join ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ 1 ) ) ) = ( 𝑋 ∧ 1 ) )
22 1 7 opococ ⊢ ( ( 𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ) → ( ( oc ‘ 𝐾 ) ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ) = 𝑋 )
23 4 22 sylan ⊢ ( ( 𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ) → ( ( oc ‘ 𝐾 ) ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ) = 𝑋 )
24 17 21 23 3eqtr3d ⊢ ( ( 𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ) → ( 𝑋 ∧ 1 ) = 𝑋 )