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

Metamath Proof Explorer

Theorem pclss2polN

Description: The projective subspace closure is a subset of closed subspace closure. (Contributed by NM, 12-Sep-2013) (New usage is discouraged.)

		Ref	Expression
	Hypotheses	pclss2pol.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
		pclss2pol.o	⊢ ⊥ = ( ⊥_𝑃 ‘ 𝐾 )
		pclss2pol.c	⊢ 𝑈 = ( PCl ‘ 𝐾 )
	Assertion	pclss2polN	⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ) → ( 𝑈 ‘ 𝑋 ) ⊆ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) )

Proof

Step	Hyp	Ref	Expression
1		pclss2pol.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
2		pclss2pol.o	⊢ ⊥ = ( ⊥_𝑃 ‘ 𝐾 )
3		pclss2pol.c	⊢ 𝑈 = ( PCl ‘ 𝐾 )
4		simpl	⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ) → 𝐾 ∈ HL )
5	1 2	2polssN	⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ) → 𝑋 ⊆ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) )
6	1 2	polssatN	⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ) → ( ⊥ ‘ 𝑋 ) ⊆ 𝐴 )
7	1 2	polssatN	⊢ ( ( 𝐾 ∈ HL ∧ ( ⊥ ‘ 𝑋 ) ⊆ 𝐴 ) → ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) ⊆ 𝐴 )
8	6 7	syldan	⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ) → ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) ⊆ 𝐴 )
9	1 3	pclssN	⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) ∧ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) ⊆ 𝐴 ) → ( 𝑈 ‘ 𝑋 ) ⊆ ( 𝑈 ‘ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) ) )
10	4 5 8 9	syl3anc	⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ) → ( 𝑈 ‘ 𝑋 ) ⊆ ( 𝑈 ‘ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) ) )
11		eqid	⊢ ( PSubSp ‘ 𝐾 ) = ( PSubSp ‘ 𝐾 )
12	1 11 2	polsubN	⊢ ( ( 𝐾 ∈ HL ∧ ( ⊥ ‘ 𝑋 ) ⊆ 𝐴 ) → ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) ∈ ( PSubSp ‘ 𝐾 ) )
13	6 12	syldan	⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ) → ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) ∈ ( PSubSp ‘ 𝐾 ) )
14	11 3	pclidN	⊢ ( ( 𝐾 ∈ HL ∧ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) ∈ ( PSubSp ‘ 𝐾 ) ) → ( 𝑈 ‘ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) ) = ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) )
15	13 14	syldan	⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ) → ( 𝑈 ‘ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) ) = ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) )
16	10 15	sseqtrd	⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ) → ( 𝑈 ‘ 𝑋 ) ⊆ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) )