Theorem pol1N

Description: The polarity of the whole projective subspace is the empty space. Remark in Holland95 p. 223. (Contributed by NM, 24-Jan-2012) (New usage is discouraged.)

	Ref	Expression
Hypotheses	polssat.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
	polssat.p	⊢ ⊥ = ( ⊥𝑃 ‘ 𝐾 )
Assertion	pol1N	⊢ ( 𝐾 ∈ HL → ( ⊥ ‘ 𝐴 ) = ∅ )

Proof

Step	Hyp	Ref	Expression
1		polssat.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
2		polssat.p	⊢ ⊥ = ( ⊥𝑃 ‘ 𝐾 )
3		ssid	⊢ 𝐴 ⊆ 𝐴
4		eqid	⊢ ( lub ‘ 𝐾 ) = ( lub ‘ 𝐾 )
5		eqid	⊢ ( oc ‘ 𝐾 ) = ( oc ‘ 𝐾 )
6		eqid	⊢ ( pmap ‘ 𝐾 ) = ( pmap ‘ 𝐾 )
7	4 5 1 6 2	polval2N	⊢ ( ( 𝐾 ∈ HL ∧ 𝐴 ⊆ 𝐴 ) → ( ⊥ ‘ 𝐴 ) = ( ( pmap ‘ 𝐾 ) ‘ ( ( oc ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ 𝐴 ) ) ) )
8	3 7	mpan2	⊢ ( 𝐾 ∈ HL → ( ⊥ ‘ 𝐴 ) = ( ( pmap ‘ 𝐾 ) ‘ ( ( oc ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ 𝐴 ) ) ) )
9		hlop	⊢ ( 𝐾 ∈ HL → 𝐾 ∈ OP )
10		eqid	⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
11	10 1	atbase	⊢ ( 𝑝 ∈ 𝐴 → 𝑝 ∈ ( Base ‘ 𝐾 ) )
12		eqid	⊢ ( le ‘ 𝐾 ) = ( le ‘ 𝐾 )
13		eqid	⊢ ( 1. ‘ 𝐾 ) = ( 1. ‘ 𝐾 )
14	10 12 13	ople1	⊢ ( ( 𝐾 ∈ OP ∧ 𝑝 ∈ ( Base ‘ 𝐾 ) ) → 𝑝 ( le ‘ 𝐾 ) ( 1. ‘ 𝐾 ) )
15	9 11 14	syl2an	⊢ ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ 𝐴 ) → 𝑝 ( le ‘ 𝐾 ) ( 1. ‘ 𝐾 ) )
16	15	ralrimiva	⊢ ( 𝐾 ∈ HL → ∀ 𝑝 ∈ 𝐴 𝑝 ( le ‘ 𝐾 ) ( 1. ‘ 𝐾 ) )
17		rabid2	⊢ ( 𝐴 = { 𝑝 ∈ 𝐴 ∣ 𝑝 ( le ‘ 𝐾 ) ( 1. ‘ 𝐾 ) } ↔ ∀ 𝑝 ∈ 𝐴 𝑝 ( le ‘ 𝐾 ) ( 1. ‘ 𝐾 ) )
18	16 17	sylibr	⊢ ( 𝐾 ∈ HL → 𝐴 = { 𝑝 ∈ 𝐴 ∣ 𝑝 ( le ‘ 𝐾 ) ( 1. ‘ 𝐾 ) } )
19	18	fveq2d	⊢ ( 𝐾 ∈ HL → ( ( lub ‘ 𝐾 ) ‘ 𝐴 ) = ( ( lub ‘ 𝐾 ) ‘ { 𝑝 ∈ 𝐴 ∣ 𝑝 ( le ‘ 𝐾 ) ( 1. ‘ 𝐾 ) } ) )
20		hlomcmat	⊢ ( 𝐾 ∈ HL → ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat ) )
21	10 13	op1cl	⊢ ( 𝐾 ∈ OP → ( 1. ‘ 𝐾 ) ∈ ( Base ‘ 𝐾 ) )
22	9 21	syl	⊢ ( 𝐾 ∈ HL → ( 1. ‘ 𝐾 ) ∈ ( Base ‘ 𝐾 ) )
23	10 12 4 1	atlatmstc	⊢ ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat ) ∧ ( 1. ‘ 𝐾 ) ∈ ( Base ‘ 𝐾 ) ) → ( ( lub ‘ 𝐾 ) ‘ { 𝑝 ∈ 𝐴 ∣ 𝑝 ( le ‘ 𝐾 ) ( 1. ‘ 𝐾 ) } ) = ( 1. ‘ 𝐾 ) )
24	20 22 23	syl2anc	⊢ ( 𝐾 ∈ HL → ( ( lub ‘ 𝐾 ) ‘ { 𝑝 ∈ 𝐴 ∣ 𝑝 ( le ‘ 𝐾 ) ( 1. ‘ 𝐾 ) } ) = ( 1. ‘ 𝐾 ) )
25	19 24	eqtr2d	⊢ ( 𝐾 ∈ HL → ( 1. ‘ 𝐾 ) = ( ( lub ‘ 𝐾 ) ‘ 𝐴 ) )
26	25	fveq2d	⊢ ( 𝐾 ∈ HL → ( ( oc ‘ 𝐾 ) ‘ ( 1. ‘ 𝐾 ) ) = ( ( oc ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ 𝐴 ) ) )
27		eqid	⊢ ( 0. ‘ 𝐾 ) = ( 0. ‘ 𝐾 )
28	27 13 5	opoc1	⊢ ( 𝐾 ∈ OP → ( ( oc ‘ 𝐾 ) ‘ ( 1. ‘ 𝐾 ) ) = ( 0. ‘ 𝐾 ) )
29	9 28	syl	⊢ ( 𝐾 ∈ HL → ( ( oc ‘ 𝐾 ) ‘ ( 1. ‘ 𝐾 ) ) = ( 0. ‘ 𝐾 ) )
30	26 29	eqtr3d	⊢ ( 𝐾 ∈ HL → ( ( oc ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ 𝐴 ) ) = ( 0. ‘ 𝐾 ) )
31	30	fveq2d	⊢ ( 𝐾 ∈ HL → ( ( pmap ‘ 𝐾 ) ‘ ( ( oc ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ 𝐴 ) ) ) = ( ( pmap ‘ 𝐾 ) ‘ ( 0. ‘ 𝐾 ) ) )
32		hlatl	⊢ ( 𝐾 ∈ HL → 𝐾 ∈ AtLat )
33	27 6	pmap0	⊢ ( 𝐾 ∈ AtLat → ( ( pmap ‘ 𝐾 ) ‘ ( 0. ‘ 𝐾 ) ) = ∅ )
34	32 33	syl	⊢ ( 𝐾 ∈ HL → ( ( pmap ‘ 𝐾 ) ‘ ( 0. ‘ 𝐾 ) ) = ∅ )
35	8 31 34	3eqtrd	⊢ ( 𝐾 ∈ HL → ( ⊥ ‘ 𝐴 ) = ∅ )