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

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 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑋 ⊆ ( ⊥ ‘ 𝑌 ) ) → ( ( ⊥ ‘ ( ( ⊥ ‘ 𝑋 ) ∩ ( ⊥ ‘ 𝑌 ) ) ) ∩ ( ⊥ ‘ 𝑌 ) ) = ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) )