Metamath Proof Explorer

Theorem poml4N

Description: Orthomodular law for projective lattices. Lemma 3.3(1) in Holland95 p. 215. (Contributed by NM, 25-Jan-2012) (New usage is discouraged.)

Ref Expression
Hypotheses poml4.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
poml4.p ⊢ ⊥ = ( ⊥𝑃 ‘ 𝐾 )
Assertion poml4N ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) → ( ( 𝑋 ⊆ 𝑌 ∧ ( ⊥ ‘ ( ⊥ ‘ 𝑌 ) ) = 𝑌 ) → ( ( ⊥ ‘ ( ( ⊥ ‘ 𝑋 ) ∩ 𝑌 ) ) ∩ 𝑌 ) = ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) ) )

Proof

Step Hyp Ref Expression
1 poml4.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
2 poml4.p ⊢ ⊥ = ( ⊥𝑃 ‘ 𝐾 )
3 eqcom ⊢ ( ( ⊥ ‘ ( ⊥ ‘ 𝑌 ) ) = 𝑌 ↔ 𝑌 = ( ⊥ ‘ ( ⊥ ‘ 𝑌 ) ) )
4 eqid ⊢ ( lub ‘ 𝐾 ) = ( lub ‘ 𝐾 )
5 eqid ⊢ ( pmap ‘ 𝐾 ) = ( pmap ‘ 𝐾 )
6 4 1 5 2 2polvalN ⊢ ( ( 𝐾 ∈ HL ∧ 𝑌 ⊆ 𝐴 ) → ( ⊥ ‘ ( ⊥ ‘ 𝑌 ) ) = ( ( pmap ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ 𝑌 ) ) )
7 6 3adant2 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) → ( ⊥ ‘ ( ⊥ ‘ 𝑌 ) ) = ( ( pmap ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ 𝑌 ) ) )
8 7 eqeq2d ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) → ( 𝑌 = ( ⊥ ‘ ( ⊥ ‘ 𝑌 ) ) ↔ 𝑌 = ( ( pmap ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ 𝑌 ) ) ) )
9 8 biimpd ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) → ( 𝑌 = ( ⊥ ‘ ( ⊥ ‘ 𝑌 ) ) → 𝑌 = ( ( pmap ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ 𝑌 ) ) ) )
10 3 9 syl5bi ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) → ( ( ⊥ ‘ ( ⊥ ‘ 𝑌 ) ) = 𝑌 → 𝑌 = ( ( pmap ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ 𝑌 ) ) ) )
11 simpl1 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ ( 𝑋 ⊆ 𝑌 ∧ 𝑌 = ( ( pmap ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ 𝑌 ) ) ) ) → 𝐾 ∈ HL )
12 hloml ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ OML )
13 11 12 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ ( 𝑋 ⊆ 𝑌 ∧ 𝑌 = ( ( pmap ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ 𝑌 ) ) ) ) → 𝐾 ∈ OML )
14 hlclat ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ CLat )
15 11 14 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ ( 𝑋 ⊆ 𝑌 ∧ 𝑌 = ( ( pmap ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ 𝑌 ) ) ) ) → 𝐾 ∈ CLat )
16 simpl2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ ( 𝑋 ⊆ 𝑌 ∧ 𝑌 = ( ( pmap ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ 𝑌 ) ) ) ) → 𝑋 ⊆ 𝐴 )
17 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
18 17 1 atssbase ⊢ 𝐴 ⊆ ( Base ‘ 𝐾 )
19 16 18 sstrdi ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ ( 𝑋 ⊆ 𝑌 ∧ 𝑌 = ( ( pmap ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ 𝑌 ) ) ) ) → 𝑋 ⊆ ( Base ‘ 𝐾 ) )
20 17 4 clatlubcl ⊢ ( ( 𝐾 ∈ CLat ∧ 𝑋 ⊆ ( Base ‘ 𝐾 ) ) → ( ( lub ‘ 𝐾 ) ‘ 𝑋 ) ∈ ( Base ‘ 𝐾 ) )
21 15 19 20 syl2anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ ( 𝑋 ⊆ 𝑌 ∧ 𝑌 = ( ( pmap ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ 𝑌 ) ) ) ) → ( ( lub ‘ 𝐾 ) ‘ 𝑋 ) ∈ ( Base ‘ 𝐾 ) )
22 simpl3 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ ( 𝑋 ⊆ 𝑌 ∧ 𝑌 = ( ( pmap ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ 𝑌 ) ) ) ) → 𝑌 ⊆ 𝐴 )
23 22 18 sstrdi ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ ( 𝑋 ⊆ 𝑌 ∧ 𝑌 = ( ( pmap ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ 𝑌 ) ) ) ) → 𝑌 ⊆ ( Base ‘ 𝐾 ) )
24 17 4 clatlubcl ⊢ ( ( 𝐾 ∈ CLat ∧ 𝑌 ⊆ ( Base ‘ 𝐾 ) ) → ( ( lub ‘ 𝐾 ) ‘ 𝑌 ) ∈ ( Base ‘ 𝐾 ) )
25 15 23 24 syl2anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ ( 𝑋 ⊆ 𝑌 ∧ 𝑌 = ( ( pmap ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ 𝑌 ) ) ) ) → ( ( lub ‘ 𝐾 ) ‘ 𝑌 ) ∈ ( Base ‘ 𝐾 ) )
26 13 21 25 3jca ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ ( 𝑋 ⊆ 𝑌 ∧ 𝑌 = ( ( pmap ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ 𝑌 ) ) ) ) → ( 𝐾 ∈ OML ∧ ( ( lub ‘ 𝐾 ) ‘ 𝑋 ) ∈ ( Base ‘ 𝐾 ) ∧ ( ( lub ‘ 𝐾 ) ‘ 𝑌 ) ∈ ( Base ‘ 𝐾 ) ) )
27 simprl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ ( 𝑋 ⊆ 𝑌 ∧ 𝑌 = ( ( pmap ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ 𝑌 ) ) ) ) → 𝑋 ⊆ 𝑌 )
28 eqid ⊢ ( le ‘ 𝐾 ) = ( le ‘ 𝐾 )
29 17 28 4 lubss ⊢ ( ( 𝐾 ∈ CLat ∧ 𝑌 ⊆ ( Base ‘ 𝐾 ) ∧ 𝑋 ⊆ 𝑌 ) → ( ( lub ‘ 𝐾 ) ‘ 𝑋 ) ( le ‘ 𝐾 ) ( ( lub ‘ 𝐾 ) ‘ 𝑌 ) )
30 15 23 27 29 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ ( 𝑋 ⊆ 𝑌 ∧ 𝑌 = ( ( pmap ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ 𝑌 ) ) ) ) → ( ( lub ‘ 𝐾 ) ‘ 𝑋 ) ( le ‘ 𝐾 ) ( ( lub ‘ 𝐾 ) ‘ 𝑌 ) )
31 eqid ⊢ ( meet ‘ 𝐾 ) = ( meet ‘ 𝐾 )
32 eqid ⊢ ( oc ‘ 𝐾 ) = ( oc ‘ 𝐾 )
33 17 28 31 32 omllaw4 ⊢ ( ( 𝐾 ∈ OML ∧ ( ( lub ‘ 𝐾 ) ‘ 𝑋 ) ∈ ( Base ‘ 𝐾 ) ∧ ( ( lub ‘ 𝐾 ) ‘ 𝑌 ) ∈ ( Base ‘ 𝐾 ) ) → ( ( ( lub ‘ 𝐾 ) ‘ 𝑋 ) ( le ‘ 𝐾 ) ( ( lub ‘ 𝐾 ) ‘ 𝑌 ) → ( ( ( oc ‘ 𝐾 ) ‘ ( ( ( oc ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ 𝑋 ) ) ( meet ‘ 𝐾 ) ( ( lub ‘ 𝐾 ) ‘ 𝑌 ) ) ) ( meet ‘ 𝐾 ) ( ( lub ‘ 𝐾 ) ‘ 𝑌 ) ) = ( ( lub ‘ 𝐾 ) ‘ 𝑋 ) ) )
34 26 30 33 sylc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ ( 𝑋 ⊆ 𝑌 ∧ 𝑌 = ( ( pmap ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ 𝑌 ) ) ) ) → ( ( ( oc ‘ 𝐾 ) ‘ ( ( ( oc ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ 𝑋 ) ) ( meet ‘ 𝐾 ) ( ( lub ‘ 𝐾 ) ‘ 𝑌 ) ) ) ( meet ‘ 𝐾 ) ( ( lub ‘ 𝐾 ) ‘ 𝑌 ) ) = ( ( lub ‘ 𝐾 ) ‘ 𝑋 ) )
35 34 fveq2d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ ( 𝑋 ⊆ 𝑌 ∧ 𝑌 = ( ( pmap ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ 𝑌 ) ) ) ) → ( ( pmap ‘ 𝐾 ) ‘ ( ( ( oc ‘ 𝐾 ) ‘ ( ( ( oc ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ 𝑋 ) ) ( meet ‘ 𝐾 ) ( ( lub ‘ 𝐾 ) ‘ 𝑌 ) ) ) ( meet ‘ 𝐾 ) ( ( lub ‘ 𝐾 ) ‘ 𝑌 ) ) ) = ( ( pmap ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ 𝑋 ) ) )
36 4 32 1 5 2 polval2N ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ) → ( ⊥ ‘ 𝑋 ) = ( ( pmap ‘ 𝐾 ) ‘ ( ( oc ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ 𝑋 ) ) ) )
37 11 16 36 syl2anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ ( 𝑋 ⊆ 𝑌 ∧ 𝑌 = ( ( pmap ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ 𝑌 ) ) ) ) → ( ⊥ ‘ 𝑋 ) = ( ( pmap ‘ 𝐾 ) ‘ ( ( oc ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ 𝑋 ) ) ) )
38 simprr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ ( 𝑋 ⊆ 𝑌 ∧ 𝑌 = ( ( pmap ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ 𝑌 ) ) ) ) → 𝑌 = ( ( pmap ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ 𝑌 ) ) )
39 37 38 ineq12d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ ( 𝑋 ⊆ 𝑌 ∧ 𝑌 = ( ( pmap ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ 𝑌 ) ) ) ) → ( ( ⊥ ‘ 𝑋 ) ∩ 𝑌 ) = ( ( ( pmap ‘ 𝐾 ) ‘ ( ( oc ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ 𝑋 ) ) ) ∩ ( ( pmap ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ 𝑌 ) ) ) )
40 hlop ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ OP )
41 11 40 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ ( 𝑋 ⊆ 𝑌 ∧ 𝑌 = ( ( pmap ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ 𝑌 ) ) ) ) → 𝐾 ∈ OP )
42 17 32 opoccl ⊢ ( ( 𝐾 ∈ OP ∧ ( ( lub ‘ 𝐾 ) ‘ 𝑋 ) ∈ ( Base ‘ 𝐾 ) ) → ( ( oc ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ 𝑋 ) ) ∈ ( Base ‘ 𝐾 ) )
43 41 21 42 syl2anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ ( 𝑋 ⊆ 𝑌 ∧ 𝑌 = ( ( pmap ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ 𝑌 ) ) ) ) → ( ( oc ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ 𝑋 ) ) ∈ ( Base ‘ 𝐾 ) )
44 17 31 1 5 pmapmeet ⊢ ( ( 𝐾 ∈ HL ∧ ( ( oc ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ 𝑋 ) ) ∈ ( Base ‘ 𝐾 ) ∧ ( ( lub ‘ 𝐾 ) ‘ 𝑌 ) ∈ ( Base ‘ 𝐾 ) ) → ( ( pmap ‘ 𝐾 ) ‘ ( ( ( oc ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ 𝑋 ) ) ( meet ‘ 𝐾 ) ( ( lub ‘ 𝐾 ) ‘ 𝑌 ) ) ) = ( ( ( pmap ‘ 𝐾 ) ‘ ( ( oc ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ 𝑋 ) ) ) ∩ ( ( pmap ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ 𝑌 ) ) ) )
45 11 43 25 44 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ ( 𝑋 ⊆ 𝑌 ∧ 𝑌 = ( ( pmap ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ 𝑌 ) ) ) ) → ( ( pmap ‘ 𝐾 ) ‘ ( ( ( oc ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ 𝑋 ) ) ( meet ‘ 𝐾 ) ( ( lub ‘ 𝐾 ) ‘ 𝑌 ) ) ) = ( ( ( pmap ‘ 𝐾 ) ‘ ( ( oc ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ 𝑋 ) ) ) ∩ ( ( pmap ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ 𝑌 ) ) ) )
46 39 45 eqtr4d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ ( 𝑋 ⊆ 𝑌 ∧ 𝑌 = ( ( pmap ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ 𝑌 ) ) ) ) → ( ( ⊥ ‘ 𝑋 ) ∩ 𝑌 ) = ( ( pmap ‘ 𝐾 ) ‘ ( ( ( oc ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ 𝑋 ) ) ( meet ‘ 𝐾 ) ( ( lub ‘ 𝐾 ) ‘ 𝑌 ) ) ) )
47 46 fveq2d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ ( 𝑋 ⊆ 𝑌 ∧ 𝑌 = ( ( pmap ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ 𝑌 ) ) ) ) → ( ⊥ ‘ ( ( ⊥ ‘ 𝑋 ) ∩ 𝑌 ) ) = ( ⊥ ‘ ( ( pmap ‘ 𝐾 ) ‘ ( ( ( oc ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ 𝑋 ) ) ( meet ‘ 𝐾 ) ( ( lub ‘ 𝐾 ) ‘ 𝑌 ) ) ) ) )
48 11 hllatd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ ( 𝑋 ⊆ 𝑌 ∧ 𝑌 = ( ( pmap ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ 𝑌 ) ) ) ) → 𝐾 ∈ Lat )
49 17 31 latmcl ⊢ ( ( 𝐾 ∈ Lat ∧ ( ( oc ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ 𝑋 ) ) ∈ ( Base ‘ 𝐾 ) ∧ ( ( lub ‘ 𝐾 ) ‘ 𝑌 ) ∈ ( Base ‘ 𝐾 ) ) → ( ( ( oc ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ 𝑋 ) ) ( meet ‘ 𝐾 ) ( ( lub ‘ 𝐾 ) ‘ 𝑌 ) ) ∈ ( Base ‘ 𝐾 ) )
50 48 43 25 49 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ ( 𝑋 ⊆ 𝑌 ∧ 𝑌 = ( ( pmap ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ 𝑌 ) ) ) ) → ( ( ( oc ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ 𝑋 ) ) ( meet ‘ 𝐾 ) ( ( lub ‘ 𝐾 ) ‘ 𝑌 ) ) ∈ ( Base ‘ 𝐾 ) )
51 17 32 5 2 polpmapN ⊢ ( ( 𝐾 ∈ HL ∧ ( ( ( oc ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ 𝑋 ) ) ( meet ‘ 𝐾 ) ( ( lub ‘ 𝐾 ) ‘ 𝑌 ) ) ∈ ( Base ‘ 𝐾 ) ) → ( ⊥ ‘ ( ( pmap ‘ 𝐾 ) ‘ ( ( ( oc ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ 𝑋 ) ) ( meet ‘ 𝐾 ) ( ( lub ‘ 𝐾 ) ‘ 𝑌 ) ) ) ) = ( ( pmap ‘ 𝐾 ) ‘ ( ( oc ‘ 𝐾 ) ‘ ( ( ( oc ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ 𝑋 ) ) ( meet ‘ 𝐾 ) ( ( lub ‘ 𝐾 ) ‘ 𝑌 ) ) ) ) )
52 11 50 51 syl2anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ ( 𝑋 ⊆ 𝑌 ∧ 𝑌 = ( ( pmap ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ 𝑌 ) ) ) ) → ( ⊥ ‘ ( ( pmap ‘ 𝐾 ) ‘ ( ( ( oc ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ 𝑋 ) ) ( meet ‘ 𝐾 ) ( ( lub ‘ 𝐾 ) ‘ 𝑌 ) ) ) ) = ( ( pmap ‘ 𝐾 ) ‘ ( ( oc ‘ 𝐾 ) ‘ ( ( ( oc ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ 𝑋 ) ) ( meet ‘ 𝐾 ) ( ( lub ‘ 𝐾 ) ‘ 𝑌 ) ) ) ) )
53 47 52 eqtrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ ( 𝑋 ⊆ 𝑌 ∧ 𝑌 = ( ( pmap ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ 𝑌 ) ) ) ) → ( ⊥ ‘ ( ( ⊥ ‘ 𝑋 ) ∩ 𝑌 ) ) = ( ( pmap ‘ 𝐾 ) ‘ ( ( oc ‘ 𝐾 ) ‘ ( ( ( oc ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ 𝑋 ) ) ( meet ‘ 𝐾 ) ( ( lub ‘ 𝐾 ) ‘ 𝑌 ) ) ) ) )
54 53 38 ineq12d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ ( 𝑋 ⊆ 𝑌 ∧ 𝑌 = ( ( pmap ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ 𝑌 ) ) ) ) → ( ( ⊥ ‘ ( ( ⊥ ‘ 𝑋 ) ∩ 𝑌 ) ) ∩ 𝑌 ) = ( ( ( pmap ‘ 𝐾 ) ‘ ( ( oc ‘ 𝐾 ) ‘ ( ( ( oc ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ 𝑋 ) ) ( meet ‘ 𝐾 ) ( ( lub ‘ 𝐾 ) ‘ 𝑌 ) ) ) ) ∩ ( ( pmap ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ 𝑌 ) ) ) )
55 17 32 opoccl ⊢ ( ( 𝐾 ∈ OP ∧ ( ( ( oc ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ 𝑋 ) ) ( meet ‘ 𝐾 ) ( ( lub ‘ 𝐾 ) ‘ 𝑌 ) ) ∈ ( Base ‘ 𝐾 ) ) → ( ( oc ‘ 𝐾 ) ‘ ( ( ( oc ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ 𝑋 ) ) ( meet ‘ 𝐾 ) ( ( lub ‘ 𝐾 ) ‘ 𝑌 ) ) ) ∈ ( Base ‘ 𝐾 ) )
56 41 50 55 syl2anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ ( 𝑋 ⊆ 𝑌 ∧ 𝑌 = ( ( pmap ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ 𝑌 ) ) ) ) → ( ( oc ‘ 𝐾 ) ‘ ( ( ( oc ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ 𝑋 ) ) ( meet ‘ 𝐾 ) ( ( lub ‘ 𝐾 ) ‘ 𝑌 ) ) ) ∈ ( Base ‘ 𝐾 ) )
57 17 31 1 5 pmapmeet ⊢ ( ( 𝐾 ∈ HL ∧ ( ( oc ‘ 𝐾 ) ‘ ( ( ( oc ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ 𝑋 ) ) ( meet ‘ 𝐾 ) ( ( lub ‘ 𝐾 ) ‘ 𝑌 ) ) ) ∈ ( Base ‘ 𝐾 ) ∧ ( ( lub ‘ 𝐾 ) ‘ 𝑌 ) ∈ ( Base ‘ 𝐾 ) ) → ( ( pmap ‘ 𝐾 ) ‘ ( ( ( oc ‘ 𝐾 ) ‘ ( ( ( oc ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ 𝑋 ) ) ( meet ‘ 𝐾 ) ( ( lub ‘ 𝐾 ) ‘ 𝑌 ) ) ) ( meet ‘ 𝐾 ) ( ( lub ‘ 𝐾 ) ‘ 𝑌 ) ) ) = ( ( ( pmap ‘ 𝐾 ) ‘ ( ( oc ‘ 𝐾 ) ‘ ( ( ( oc ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ 𝑋 ) ) ( meet ‘ 𝐾 ) ( ( lub ‘ 𝐾 ) ‘ 𝑌 ) ) ) ) ∩ ( ( pmap ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ 𝑌 ) ) ) )
58 11 56 25 57 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ ( 𝑋 ⊆ 𝑌 ∧ 𝑌 = ( ( pmap ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ 𝑌 ) ) ) ) → ( ( pmap ‘ 𝐾 ) ‘ ( ( ( oc ‘ 𝐾 ) ‘ ( ( ( oc ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ 𝑋 ) ) ( meet ‘ 𝐾 ) ( ( lub ‘ 𝐾 ) ‘ 𝑌 ) ) ) ( meet ‘ 𝐾 ) ( ( lub ‘ 𝐾 ) ‘ 𝑌 ) ) ) = ( ( ( pmap ‘ 𝐾 ) ‘ ( ( oc ‘ 𝐾 ) ‘ ( ( ( oc ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ 𝑋 ) ) ( meet ‘ 𝐾 ) ( ( lub ‘ 𝐾 ) ‘ 𝑌 ) ) ) ) ∩ ( ( pmap ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ 𝑌 ) ) ) )
59 54 58 eqtr4d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ ( 𝑋 ⊆ 𝑌 ∧ 𝑌 = ( ( pmap ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ 𝑌 ) ) ) ) → ( ( ⊥ ‘ ( ( ⊥ ‘ 𝑋 ) ∩ 𝑌 ) ) ∩ 𝑌 ) = ( ( pmap ‘ 𝐾 ) ‘ ( ( ( oc ‘ 𝐾 ) ‘ ( ( ( oc ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ 𝑋 ) ) ( meet ‘ 𝐾 ) ( ( lub ‘ 𝐾 ) ‘ 𝑌 ) ) ) ( meet ‘ 𝐾 ) ( ( lub ‘ 𝐾 ) ‘ 𝑌 ) ) ) )
60 4 1 5 2 2polvalN ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ) → ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) = ( ( pmap ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ 𝑋 ) ) )
61 11 16 60 syl2anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ ( 𝑋 ⊆ 𝑌 ∧ 𝑌 = ( ( pmap ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ 𝑌 ) ) ) ) → ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) = ( ( pmap ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ 𝑋 ) ) )
62 35 59 61 3eqtr4d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ ( 𝑋 ⊆ 𝑌 ∧ 𝑌 = ( ( pmap ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ 𝑌 ) ) ) ) → ( ( ⊥ ‘ ( ( ⊥ ‘ 𝑋 ) ∩ 𝑌 ) ) ∩ 𝑌 ) = ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) )
63 62 ex ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) → ( ( 𝑋 ⊆ 𝑌 ∧ 𝑌 = ( ( pmap ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ 𝑌 ) ) ) → ( ( ⊥ ‘ ( ( ⊥ ‘ 𝑋 ) ∩ 𝑌 ) ) ∩ 𝑌 ) = ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) ) )
64 10 63 sylan2d ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) → ( ( 𝑋 ⊆ 𝑌 ∧ ( ⊥ ‘ ( ⊥ ‘ 𝑌 ) ) = 𝑌 ) → ( ( ⊥ ‘ ( ( ⊥ ‘ 𝑋 ) ∩ 𝑌 ) ) ∩ 𝑌 ) = ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) ) )