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