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 → ( 𝑋𝐶 ↔ ∃ 𝑦𝐵 𝑋 = ( 𝑀𝑦 ) ) )