Metamath Proof Explorer

Theorem ispsubcl2N

Description: Alternate predicate for "is a closed projective subspace". Remark in Holland95 p. 223. (Contributed by NM, 24-Jan-2012) (New usage is discouraged.)

Ref Expression
Hypotheses pmapsubcl.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
pmapsubcl.m ⊢ 𝑀 = ( pmap ‘ 𝐾 )
pmapsubcl.c ⊢ 𝐶 = ( PSubCl ‘ 𝐾 )
Assertion ispsubcl2N ( 𝐾 ∈ HL → ( 𝑋 ∈ 𝐶 ↔ ∃ 𝑦 ∈ 𝐵 𝑋 = ( 𝑀 ‘ 𝑦 ) ) )

Proof

Step Hyp Ref Expression
1 pmapsubcl.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 pmapsubcl.m ⊢ 𝑀 = ( pmap ‘ 𝐾 )
3 pmapsubcl.c ⊢ 𝐶 = ( PSubCl ‘ 𝐾 )
4 eqid ⊢ ( Atoms ‘ 𝐾 ) = ( Atoms ‘ 𝐾 )
5 eqid ⊢ ( ⊥𝑃 ‘ 𝐾 ) = ( ⊥𝑃 ‘ 𝐾 )
6 4 5 3 ispsubclN ⊢ ( 𝐾 ∈ HL → ( 𝑋 ∈ 𝐶 ↔ ( 𝑋 ⊆ ( Atoms ‘ 𝐾 ) ∧ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ 𝑋 ) ) = 𝑋 ) ) )
7 hlop ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ OP )
8 7 adantr ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ ( Atoms ‘ 𝐾 ) ) → 𝐾 ∈ OP )
9 hlclat ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ CLat )
10 9 adantr ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ ( Atoms ‘ 𝐾 ) ) → 𝐾 ∈ CLat )
11 4 5 polssatN ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ ( Atoms ‘ 𝐾 ) ) → ( ( ⊥𝑃 ‘ 𝐾 ) ‘ 𝑋 ) ⊆ ( Atoms ‘ 𝐾 ) )
12 1 4 atssbase ⊢ ( Atoms ‘ 𝐾 ) ⊆ 𝐵
13 11 12 sstrdi ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ ( Atoms ‘ 𝐾 ) ) → ( ( ⊥𝑃 ‘ 𝐾 ) ‘ 𝑋 ) ⊆ 𝐵 )
14 eqid ⊢ ( lub ‘ 𝐾 ) = ( lub ‘ 𝐾 )
15 1 14 clatlubcl ⊢ ( ( 𝐾 ∈ CLat ∧ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ 𝑋 ) ⊆ 𝐵 ) → ( ( lub ‘ 𝐾 ) ‘ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ 𝑋 ) ) ∈ 𝐵 )
16 10 13 15 syl2anc ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ ( Atoms ‘ 𝐾 ) ) → ( ( lub ‘ 𝐾 ) ‘ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ 𝑋 ) ) ∈ 𝐵 )
17 eqid ⊢ ( oc ‘ 𝐾 ) = ( oc ‘ 𝐾 )
18 1 17 opoccl ⊢ ( ( 𝐾 ∈ OP ∧ ( ( lub ‘ 𝐾 ) ‘ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ 𝑋 ) ) ∈ 𝐵 ) → ( ( oc ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ 𝑋 ) ) ) ∈ 𝐵 )
19 8 16 18 syl2anc ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ ( Atoms ‘ 𝐾 ) ) → ( ( oc ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ 𝑋 ) ) ) ∈ 𝐵 )
20 19 ex ⊢ ( 𝐾 ∈ HL → ( 𝑋 ⊆ ( Atoms ‘ 𝐾 ) → ( ( oc ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ 𝑋 ) ) ) ∈ 𝐵 ) )
21 20 adantrd ⊢ ( 𝐾 ∈ HL → ( ( 𝑋 ⊆ ( Atoms ‘ 𝐾 ) ∧ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ 𝑋 ) ) = 𝑋 ) → ( ( oc ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ 𝑋 ) ) ) ∈ 𝐵 ) )
22 14 17 4 2 5 polval2N ⊢ ( ( 𝐾 ∈ HL ∧ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ 𝑋 ) ⊆ ( Atoms ‘ 𝐾 ) ) → ( ( ⊥𝑃 ‘ 𝐾 ) ‘ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ 𝑋 ) ) = ( 𝑀 ‘ ( ( oc ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ 𝑋 ) ) ) ) )
23 11 22 syldan ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ ( Atoms ‘ 𝐾 ) ) → ( ( ⊥𝑃 ‘ 𝐾 ) ‘ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ 𝑋 ) ) = ( 𝑀 ‘ ( ( oc ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ 𝑋 ) ) ) ) )
24 23 ex ⊢ ( 𝐾 ∈ HL → ( 𝑋 ⊆ ( Atoms ‘ 𝐾 ) → ( ( ⊥𝑃 ‘ 𝐾 ) ‘ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ 𝑋 ) ) = ( 𝑀 ‘ ( ( oc ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ 𝑋 ) ) ) ) ) )
25 eqeq1 ⊢ ( ( ( ⊥𝑃 ‘ 𝐾 ) ‘ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ 𝑋 ) ) = 𝑋 → ( ( ( ⊥𝑃 ‘ 𝐾 ) ‘ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ 𝑋 ) ) = ( 𝑀 ‘ ( ( oc ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ 𝑋 ) ) ) ) ↔ 𝑋 = ( 𝑀 ‘ ( ( oc ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ 𝑋 ) ) ) ) ) )
26 25 biimpcd ⊢ ( ( ( ⊥𝑃 ‘ 𝐾 ) ‘ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ 𝑋 ) ) = ( 𝑀 ‘ ( ( oc ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ 𝑋 ) ) ) ) → ( ( ( ⊥𝑃 ‘ 𝐾 ) ‘ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ 𝑋 ) ) = 𝑋 → 𝑋 = ( 𝑀 ‘ ( ( oc ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ 𝑋 ) ) ) ) ) )
27 24 26 syl6 ⊢ ( 𝐾 ∈ HL → ( 𝑋 ⊆ ( Atoms ‘ 𝐾 ) → ( ( ( ⊥𝑃 ‘ 𝐾 ) ‘ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ 𝑋 ) ) = 𝑋 → 𝑋 = ( 𝑀 ‘ ( ( oc ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ 𝑋 ) ) ) ) ) ) )
28 27 impd ⊢ ( 𝐾 ∈ HL → ( ( 𝑋 ⊆ ( Atoms ‘ 𝐾 ) ∧ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ 𝑋 ) ) = 𝑋 ) → 𝑋 = ( 𝑀 ‘ ( ( oc ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ 𝑋 ) ) ) ) ) )
29 21 28 jcad ⊢ ( 𝐾 ∈ HL → ( ( 𝑋 ⊆ ( Atoms ‘ 𝐾 ) ∧ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ 𝑋 ) ) = 𝑋 ) → ( ( ( oc ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ 𝑋 ) ) ) ∈ 𝐵 ∧ 𝑋 = ( 𝑀 ‘ ( ( oc ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ 𝑋 ) ) ) ) ) ) )
30 fveq2 ⊢ ( 𝑦 = ( ( oc ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ 𝑋 ) ) ) → ( 𝑀 ‘ 𝑦 ) = ( 𝑀 ‘ ( ( oc ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ 𝑋 ) ) ) ) )
31 30 rspceeqv ⊢ ( ( ( ( oc ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ 𝑋 ) ) ) ∈ 𝐵 ∧ 𝑋 = ( 𝑀 ‘ ( ( oc ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ 𝑋 ) ) ) ) ) → ∃ 𝑦 ∈ 𝐵 𝑋 = ( 𝑀 ‘ 𝑦 ) )
32 29 31 syl6 ⊢ ( 𝐾 ∈ HL → ( ( 𝑋 ⊆ ( Atoms ‘ 𝐾 ) ∧ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ 𝑋 ) ) = 𝑋 ) → ∃ 𝑦 ∈ 𝐵 𝑋 = ( 𝑀 ‘ 𝑦 ) ) )
33 1 4 2 pmapssat ⊢ ( ( 𝐾 ∈ HL ∧ 𝑦 ∈ 𝐵 ) → ( 𝑀 ‘ 𝑦 ) ⊆ ( Atoms ‘ 𝐾 ) )
34 1 2 5 2polpmapN ⊢ ( ( 𝐾 ∈ HL ∧ 𝑦 ∈ 𝐵 ) → ( ( ⊥𝑃 ‘ 𝐾 ) ‘ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ ( 𝑀 ‘ 𝑦 ) ) ) = ( 𝑀 ‘ 𝑦 ) )
35 sseq1 ⊢ ( 𝑋 = ( 𝑀 ‘ 𝑦 ) → ( 𝑋 ⊆ ( Atoms ‘ 𝐾 ) ↔ ( 𝑀 ‘ 𝑦 ) ⊆ ( Atoms ‘ 𝐾 ) ) )
36 2fveq3 ⊢ ( 𝑋 = ( 𝑀 ‘ 𝑦 ) → ( ( ⊥𝑃 ‘ 𝐾 ) ‘ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ 𝑋 ) ) = ( ( ⊥𝑃 ‘ 𝐾 ) ‘ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ ( 𝑀 ‘ 𝑦 ) ) ) )
37 id ⊢ ( 𝑋 = ( 𝑀 ‘ 𝑦 ) → 𝑋 = ( 𝑀 ‘ 𝑦 ) )
38 36 37 eqeq12d ⊢ ( 𝑋 = ( 𝑀 ‘ 𝑦 ) → ( ( ( ⊥𝑃 ‘ 𝐾 ) ‘ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ 𝑋 ) ) = 𝑋 ↔ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ ( 𝑀 ‘ 𝑦 ) ) ) = ( 𝑀 ‘ 𝑦 ) ) )
39 35 38 anbi12d ⊢ ( 𝑋 = ( 𝑀 ‘ 𝑦 ) → ( ( 𝑋 ⊆ ( Atoms ‘ 𝐾 ) ∧ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ 𝑋 ) ) = 𝑋 ) ↔ ( ( 𝑀 ‘ 𝑦 ) ⊆ ( Atoms ‘ 𝐾 ) ∧ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ ( 𝑀 ‘ 𝑦 ) ) ) = ( 𝑀 ‘ 𝑦 ) ) ) )
40 39 biimprcd ⊢ ( ( ( 𝑀 ‘ 𝑦 ) ⊆ ( Atoms ‘ 𝐾 ) ∧ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ ( 𝑀 ‘ 𝑦 ) ) ) = ( 𝑀 ‘ 𝑦 ) ) → ( 𝑋 = ( 𝑀 ‘ 𝑦 ) → ( 𝑋 ⊆ ( Atoms ‘ 𝐾 ) ∧ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ 𝑋 ) ) = 𝑋 ) ) )
41 33 34 40 syl2anc ⊢ ( ( 𝐾 ∈ HL ∧ 𝑦 ∈ 𝐵 ) → ( 𝑋 = ( 𝑀 ‘ 𝑦 ) → ( 𝑋 ⊆ ( Atoms ‘ 𝐾 ) ∧ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ 𝑋 ) ) = 𝑋 ) ) )
42 41 rexlimdva ⊢ ( 𝐾 ∈ HL → ( ∃ 𝑦 ∈ 𝐵 𝑋 = ( 𝑀 ‘ 𝑦 ) → ( 𝑋 ⊆ ( Atoms ‘ 𝐾 ) ∧ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ 𝑋 ) ) = 𝑋 ) ) )
43 32 42 impbid ⊢ ( 𝐾 ∈ HL → ( ( 𝑋 ⊆ ( Atoms ‘ 𝐾 ) ∧ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ 𝑋 ) ) = 𝑋 ) ↔ ∃ 𝑦 ∈ 𝐵 𝑋 = ( 𝑀 ‘ 𝑦 ) ) )
44 6 43 bitrd ⊢ ( 𝐾 ∈ HL → ( 𝑋 ∈ 𝐶 ↔ ∃ 𝑦 ∈ 𝐵 𝑋 = ( 𝑀 ‘ 𝑦 ) ) )