Metamath Proof Explorer


Theorem poml5N

Description: Orthomodular law for projective lattices. (Contributed by NM, 23-Mar-2012) (New usage is discouraged.)

Ref Expression
Hypotheses poml4.a 𝐴 = ( Atoms ‘ 𝐾 )
poml4.p = ( ⊥𝑃𝐾 )
Assertion poml5N ( ( 𝐾 ∈ HL ∧ 𝑌𝐴𝑋 ⊆ ( 𝑌 ) ) → ( ( ‘ ( ( 𝑋 ) ∩ ( 𝑌 ) ) ) ∩ ( 𝑌 ) ) = ( ‘ ( 𝑋 ) ) )

Proof

Step Hyp Ref Expression
1 poml4.a 𝐴 = ( Atoms ‘ 𝐾 )
2 poml4.p = ( ⊥𝑃𝐾 )
3 simp1 ( ( 𝐾 ∈ HL ∧ 𝑌𝐴𝑋 ⊆ ( 𝑌 ) ) → 𝐾 ∈ HL )
4 simp3 ( ( 𝐾 ∈ HL ∧ 𝑌𝐴𝑋 ⊆ ( 𝑌 ) ) → 𝑋 ⊆ ( 𝑌 ) )
5 1 2 polssatN ( ( 𝐾 ∈ HL ∧ 𝑌𝐴 ) → ( 𝑌 ) ⊆ 𝐴 )
6 5 3adant3 ( ( 𝐾 ∈ HL ∧ 𝑌𝐴𝑋 ⊆ ( 𝑌 ) ) → ( 𝑌 ) ⊆ 𝐴 )
7 4 6 sstrd ( ( 𝐾 ∈ HL ∧ 𝑌𝐴𝑋 ⊆ ( 𝑌 ) ) → 𝑋𝐴 )
8 3 7 6 3jca ( ( 𝐾 ∈ HL ∧ 𝑌𝐴𝑋 ⊆ ( 𝑌 ) ) → ( 𝐾 ∈ HL ∧ 𝑋𝐴 ∧ ( 𝑌 ) ⊆ 𝐴 ) )
9 1 2 3polN ( ( 𝐾 ∈ HL ∧ 𝑌𝐴 ) → ( ‘ ( ‘ ( 𝑌 ) ) ) = ( 𝑌 ) )
10 9 3adant3 ( ( 𝐾 ∈ HL ∧ 𝑌𝐴𝑋 ⊆ ( 𝑌 ) ) → ( ‘ ( ‘ ( 𝑌 ) ) ) = ( 𝑌 ) )
11 4 10 jca ( ( 𝐾 ∈ HL ∧ 𝑌𝐴𝑋 ⊆ ( 𝑌 ) ) → ( 𝑋 ⊆ ( 𝑌 ) ∧ ( ‘ ( ‘ ( 𝑌 ) ) ) = ( 𝑌 ) ) )
12 1 2 poml4N ( ( 𝐾 ∈ HL ∧ 𝑋𝐴 ∧ ( 𝑌 ) ⊆ 𝐴 ) → ( ( 𝑋 ⊆ ( 𝑌 ) ∧ ( ‘ ( ‘ ( 𝑌 ) ) ) = ( 𝑌 ) ) → ( ( ‘ ( ( 𝑋 ) ∩ ( 𝑌 ) ) ) ∩ ( 𝑌 ) ) = ( ‘ ( 𝑋 ) ) ) )
13 8 11 12 sylc ( ( 𝐾 ∈ HL ∧ 𝑌𝐴𝑋 ⊆ ( 𝑌 ) ) → ( ( ‘ ( ( 𝑋 ) ∩ ( 𝑌 ) ) ) ∩ ( 𝑌 ) ) = ( ‘ ( 𝑋 ) ) )