Metamath Proof Explorer


Theorem oldmm3N

Description: De Morgan's law for meet in an ortholattice. ( chdmm3 analog.) (Contributed by NM, 8-Nov-2011) (New usage is discouraged.)

Ref Expression
Hypotheses oldmm1.b 𝐵 = ( Base ‘ 𝐾 )
oldmm1.j = ( join ‘ 𝐾 )
oldmm1.m = ( meet ‘ 𝐾 )
oldmm1.o = ( oc ‘ 𝐾 )
Assertion oldmm3N ( ( 𝐾 ∈ OL ∧ 𝑋𝐵𝑌𝐵 ) → ( ‘ ( 𝑋 ( 𝑌 ) ) ) = ( ( 𝑋 ) 𝑌 ) )

Proof

Step Hyp Ref Expression
1 oldmm1.b 𝐵 = ( Base ‘ 𝐾 )
2 oldmm1.j = ( join ‘ 𝐾 )
3 oldmm1.m = ( meet ‘ 𝐾 )
4 oldmm1.o = ( oc ‘ 𝐾 )
5 olop ( 𝐾 ∈ OL → 𝐾 ∈ OP )
6 5 3ad2ant1 ( ( 𝐾 ∈ OL ∧ 𝑋𝐵𝑌𝐵 ) → 𝐾 ∈ OP )
7 simp3 ( ( 𝐾 ∈ OL ∧ 𝑋𝐵𝑌𝐵 ) → 𝑌𝐵 )
8 1 4 opoccl ( ( 𝐾 ∈ OP ∧ 𝑌𝐵 ) → ( 𝑌 ) ∈ 𝐵 )
9 6 7 8 syl2anc ( ( 𝐾 ∈ OL ∧ 𝑋𝐵𝑌𝐵 ) → ( 𝑌 ) ∈ 𝐵 )
10 1 2 3 4 oldmm1 ( ( 𝐾 ∈ OL ∧ 𝑋𝐵 ∧ ( 𝑌 ) ∈ 𝐵 ) → ( ‘ ( 𝑋 ( 𝑌 ) ) ) = ( ( 𝑋 ) ( ‘ ( 𝑌 ) ) ) )
11 9 10 syld3an3 ( ( 𝐾 ∈ OL ∧ 𝑋𝐵𝑌𝐵 ) → ( ‘ ( 𝑋 ( 𝑌 ) ) ) = ( ( 𝑋 ) ( ‘ ( 𝑌 ) ) ) )
12 1 4 opococ ( ( 𝐾 ∈ OP ∧ 𝑌𝐵 ) → ( ‘ ( 𝑌 ) ) = 𝑌 )
13 6 7 12 syl2anc ( ( 𝐾 ∈ OL ∧ 𝑋𝐵𝑌𝐵 ) → ( ‘ ( 𝑌 ) ) = 𝑌 )
14 13 oveq2d ( ( 𝐾 ∈ OL ∧ 𝑋𝐵𝑌𝐵 ) → ( ( 𝑋 ) ( ‘ ( 𝑌 ) ) ) = ( ( 𝑋 ) 𝑌 ) )
15 11 14 eqtrd ( ( 𝐾 ∈ OL ∧ 𝑋𝐵𝑌𝐵 ) → ( ‘ ( 𝑋 ( 𝑌 ) ) ) = ( ( 𝑋 ) 𝑌 ) )