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 ⊢ A = Atoms ⁡ K
poml4.p ⊢ ⊥ ˙ = ⊥ 𝑃 ⁡ K
Assertion poml4N ⊢ K ∈ HL ∧ X ⊆ A ∧ Y ⊆ A → X ⊆ Y ∧ ⊥ ˙ ⁡ ⊥ ˙ ⁡ Y = Y → ⊥ ˙ ⁡ ⊥ ˙ ⁡ X ∩ Y ∩ Y = ⊥ ˙ ⁡ ⊥ ˙ ⁡ X

Proof

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