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

Metamath Proof Explorer

Theorem poml6N

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

Ref Expression
Hypotheses poml6.c ⊢ 𝐶 = ( PSubCl ‘ 𝐾 )
poml6.p ⊢ ⊥ = ( ⊥𝑃 ‘ 𝐾 )
Assertion poml6N ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ) ∧ 𝑋 ⊆ 𝑌 ) → ( ( ⊥ ‘ ( ( ⊥ ‘ 𝑋 ) ∩ 𝑌 ) ) ∩ 𝑌 ) = 𝑋 )

Proof

Step Hyp Ref Expression
1 poml6.c ⊢ 𝐶 = ( PSubCl ‘ 𝐾 )
2 poml6.p ⊢ ⊥ = ( ⊥𝑃 ‘ 𝐾 )
3 simpl1 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ) ∧ 𝑋 ⊆ 𝑌 ) → 𝐾 ∈ HL )
4 simpl2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ) ∧ 𝑋 ⊆ 𝑌 ) → 𝑋 ∈ 𝐶 )
5 eqid ⊢ ( Atoms ‘ 𝐾 ) = ( Atoms ‘ 𝐾 )
6 5 1 psubclssatN ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ) → 𝑋 ⊆ ( Atoms ‘ 𝐾 ) )
7 3 4 6 syl2anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ) ∧ 𝑋 ⊆ 𝑌 ) → 𝑋 ⊆ ( Atoms ‘ 𝐾 ) )
8 simpl3 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ) ∧ 𝑋 ⊆ 𝑌 ) → 𝑌 ∈ 𝐶 )
9 5 1 psubclssatN ⊢ ( ( 𝐾 ∈ HL ∧ 𝑌 ∈ 𝐶 ) → 𝑌 ⊆ ( Atoms ‘ 𝐾 ) )
10 3 8 9 syl2anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ) ∧ 𝑋 ⊆ 𝑌 ) → 𝑌 ⊆ ( Atoms ‘ 𝐾 ) )
11 simpr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ) ∧ 𝑋 ⊆ 𝑌 ) → 𝑋 ⊆ 𝑌 )
12 2 1 psubcli2N ⊢ ( ( 𝐾 ∈ HL ∧ 𝑌 ∈ 𝐶 ) → ( ⊥ ‘ ( ⊥ ‘ 𝑌 ) ) = 𝑌 )
13 3 8 12 syl2anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ) ∧ 𝑋 ⊆ 𝑌 ) → ( ⊥ ‘ ( ⊥ ‘ 𝑌 ) ) = 𝑌 )
14 5 2 poml4N ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ ( Atoms ‘ 𝐾 ) ∧ 𝑌 ⊆ ( Atoms ‘ 𝐾 ) ) → ( ( 𝑋 ⊆ 𝑌 ∧ ( ⊥ ‘ ( ⊥ ‘ 𝑌 ) ) = 𝑌 ) → ( ( ⊥ ‘ ( ( ⊥ ‘ 𝑋 ) ∩ 𝑌 ) ) ∩ 𝑌 ) = ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) ) )
15 14 imp ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ ( Atoms ‘ 𝐾 ) ∧ 𝑌 ⊆ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑋 ⊆ 𝑌 ∧ ( ⊥ ‘ ( ⊥ ‘ 𝑌 ) ) = 𝑌 ) ) → ( ( ⊥ ‘ ( ( ⊥ ‘ 𝑋 ) ∩ 𝑌 ) ) ∩ 𝑌 ) = ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) )
16 3 7 10 11 13 15 syl32anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ) ∧ 𝑋 ⊆ 𝑌 ) → ( ( ⊥ ‘ ( ( ⊥ ‘ 𝑋 ) ∩ 𝑌 ) ) ∩ 𝑌 ) = ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) )
17 2 1 psubcli2N ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ) → ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) = 𝑋 )
18 3 4 17 syl2anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ) ∧ 𝑋 ⊆ 𝑌 ) → ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) = 𝑋 )
19 16 18 eqtrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ) ∧ 𝑋 ⊆ 𝑌 ) → ( ( ⊥ ‘ ( ( ⊥ ‘ 𝑋 ) ∩ 𝑌 ) ) ∩ 𝑌 ) = 𝑋 )