Metamath Proof Explorer

Theorem pl42N

Description: Law holding in a Hilbert lattice that fails in orthomodular lattice L42 (Figure 7 in MegPav2000 p. 2366). (Contributed by NM, 8-Apr-2012) (New usage is discouraged.)

Ref Expression
Hypotheses pl42.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
pl42.l ⊢ ≤ = ( le ‘ 𝐾 )
pl42.j ⊢ ∨ = ( join ‘ 𝐾 )
pl42.m ⊢ ∧ = ( meet ‘ 𝐾 )
pl42.o ⊢ ⊥ = ( oc ‘ 𝐾 )
Assertion pl42N ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵 ) ) → ( ( 𝑋 ≤ ( ⊥ ‘ 𝑌 ) ∧ 𝑍 ≤ ( ⊥ ‘ 𝑊 ) ) → ( ( ( ( 𝑋 ∨ 𝑌 ) ∧ 𝑍 ) ∨ 𝑊 ) ∧ 𝑉 ) ≤ ( ( 𝑋 ∨ 𝑌 ) ∨ ( ( 𝑋 ∨ 𝑊 ) ∧ ( 𝑌 ∨ 𝑉 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 pl42.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 pl42.l ⊢ ≤ = ( le ‘ 𝐾 )
3 pl42.j ⊢ ∨ = ( join ‘ 𝐾 )
4 pl42.m ⊢ ∧ = ( meet ‘ 𝐾 )
5 pl42.o ⊢ ⊥ = ( oc ‘ 𝐾 )
6 eqid ⊢ ( pmap ‘ 𝐾 ) = ( pmap ‘ 𝐾 )
7 eqid ⊢ ( +𝑃 ‘ 𝐾 ) = ( +𝑃 ‘ 𝐾 )
8 1 2 3 4 5 6 7 pl42lem4N ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵 ) ) → ( ( 𝑋 ≤ ( ⊥ ‘ 𝑌 ) ∧ 𝑍 ≤ ( ⊥ ‘ 𝑊 ) ) → ( ( pmap ‘ 𝐾 ) ‘ ( ( ( ( 𝑋 ∨ 𝑌 ) ∧ 𝑍 ) ∨ 𝑊 ) ∧ 𝑉 ) ) ⊆ ( ( pmap ‘ 𝐾 ) ‘ ( ( 𝑋 ∨ 𝑌 ) ∨ ( ( 𝑋 ∨ 𝑊 ) ∧ ( 𝑌 ∨ 𝑉 ) ) ) ) ) )
9 simpl1 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵 ) ) → 𝐾 ∈ HL )
10 9 hllatd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵 ) ) → 𝐾 ∈ Lat )
11 simpl2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵 ) ) → 𝑋 ∈ 𝐵 )
12 simpl3 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵 ) ) → 𝑌 ∈ 𝐵 )
13 1 3 latjcl ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ∨ 𝑌 ) ∈ 𝐵 )
14 10 11 12 13 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵 ) ) → ( 𝑋 ∨ 𝑌 ) ∈ 𝐵 )
15 simpr1 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵 ) ) → 𝑍 ∈ 𝐵 )
16 1 4 latmcl ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∨ 𝑌 ) ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) → ( ( 𝑋 ∨ 𝑌 ) ∧ 𝑍 ) ∈ 𝐵 )
17 10 14 15 16 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵 ) ) → ( ( 𝑋 ∨ 𝑌 ) ∧ 𝑍 ) ∈ 𝐵 )
18 simpr2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵 ) ) → 𝑊 ∈ 𝐵 )
19 1 3 latjcl ⊢ ( ( 𝐾 ∈ Lat ∧ ( ( 𝑋 ∨ 𝑌 ) ∧ 𝑍 ) ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) → ( ( ( 𝑋 ∨ 𝑌 ) ∧ 𝑍 ) ∨ 𝑊 ) ∈ 𝐵 )
20 10 17 18 19 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵 ) ) → ( ( ( 𝑋 ∨ 𝑌 ) ∧ 𝑍 ) ∨ 𝑊 ) ∈ 𝐵 )
21 simpr3 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵 ) ) → 𝑉 ∈ 𝐵 )
22 1 4 latmcl ⊢ ( ( 𝐾 ∈ Lat ∧ ( ( ( 𝑋 ∨ 𝑌 ) ∧ 𝑍 ) ∨ 𝑊 ) ∈ 𝐵 ∧ 𝑉 ∈ 𝐵 ) → ( ( ( ( 𝑋 ∨ 𝑌 ) ∧ 𝑍 ) ∨ 𝑊 ) ∧ 𝑉 ) ∈ 𝐵 )
23 10 20 21 22 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵 ) ) → ( ( ( ( 𝑋 ∨ 𝑌 ) ∧ 𝑍 ) ∨ 𝑊 ) ∧ 𝑉 ) ∈ 𝐵 )
24 1 3 latjcl ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) → ( 𝑋 ∨ 𝑊 ) ∈ 𝐵 )
25 10 11 18 24 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵 ) ) → ( 𝑋 ∨ 𝑊 ) ∈ 𝐵 )
26 1 3 latjcl ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑌 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵 ) → ( 𝑌 ∨ 𝑉 ) ∈ 𝐵 )
27 10 12 21 26 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵 ) ) → ( 𝑌 ∨ 𝑉 ) ∈ 𝐵 )
28 1 4 latmcl ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∨ 𝑊 ) ∈ 𝐵 ∧ ( 𝑌 ∨ 𝑉 ) ∈ 𝐵 ) → ( ( 𝑋 ∨ 𝑊 ) ∧ ( 𝑌 ∨ 𝑉 ) ) ∈ 𝐵 )
29 10 25 27 28 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵 ) ) → ( ( 𝑋 ∨ 𝑊 ) ∧ ( 𝑌 ∨ 𝑉 ) ) ∈ 𝐵 )
30 1 3 latjcl ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∨ 𝑌 ) ∈ 𝐵 ∧ ( ( 𝑋 ∨ 𝑊 ) ∧ ( 𝑌 ∨ 𝑉 ) ) ∈ 𝐵 ) → ( ( 𝑋 ∨ 𝑌 ) ∨ ( ( 𝑋 ∨ 𝑊 ) ∧ ( 𝑌 ∨ 𝑉 ) ) ) ∈ 𝐵 )
31 10 14 29 30 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵 ) ) → ( ( 𝑋 ∨ 𝑌 ) ∨ ( ( 𝑋 ∨ 𝑊 ) ∧ ( 𝑌 ∨ 𝑉 ) ) ) ∈ 𝐵 )
32 1 2 6 pmaple ⊢ ( ( 𝐾 ∈ HL ∧ ( ( ( ( 𝑋 ∨ 𝑌 ) ∧ 𝑍 ) ∨ 𝑊 ) ∧ 𝑉 ) ∈ 𝐵 ∧ ( ( 𝑋 ∨ 𝑌 ) ∨ ( ( 𝑋 ∨ 𝑊 ) ∧ ( 𝑌 ∨ 𝑉 ) ) ) ∈ 𝐵 ) → ( ( ( ( ( 𝑋 ∨ 𝑌 ) ∧ 𝑍 ) ∨ 𝑊 ) ∧ 𝑉 ) ≤ ( ( 𝑋 ∨ 𝑌 ) ∨ ( ( 𝑋 ∨ 𝑊 ) ∧ ( 𝑌 ∨ 𝑉 ) ) ) ↔ ( ( pmap ‘ 𝐾 ) ‘ ( ( ( ( 𝑋 ∨ 𝑌 ) ∧ 𝑍 ) ∨ 𝑊 ) ∧ 𝑉 ) ) ⊆ ( ( pmap ‘ 𝐾 ) ‘ ( ( 𝑋 ∨ 𝑌 ) ∨ ( ( 𝑋 ∨ 𝑊 ) ∧ ( 𝑌 ∨ 𝑉 ) ) ) ) ) )
33 9 23 31 32 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵 ) ) → ( ( ( ( ( 𝑋 ∨ 𝑌 ) ∧ 𝑍 ) ∨ 𝑊 ) ∧ 𝑉 ) ≤ ( ( 𝑋 ∨ 𝑌 ) ∨ ( ( 𝑋 ∨ 𝑊 ) ∧ ( 𝑌 ∨ 𝑉 ) ) ) ↔ ( ( pmap ‘ 𝐾 ) ‘ ( ( ( ( 𝑋 ∨ 𝑌 ) ∧ 𝑍 ) ∨ 𝑊 ) ∧ 𝑉 ) ) ⊆ ( ( pmap ‘ 𝐾 ) ‘ ( ( 𝑋 ∨ 𝑌 ) ∨ ( ( 𝑋 ∨ 𝑊 ) ∧ ( 𝑌 ∨ 𝑉 ) ) ) ) ) )
34 8 33 sylibrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵 ) ) → ( ( 𝑋 ≤ ( ⊥ ‘ 𝑌 ) ∧ 𝑍 ≤ ( ⊥ ‘ 𝑊 ) ) → ( ( ( ( 𝑋 ∨ 𝑌 ) ∧ 𝑍 ) ∨ 𝑊 ) ∧ 𝑉 ) ≤ ( ( 𝑋 ∨ 𝑌 ) ∨ ( ( 𝑋 ∨ 𝑊 ) ∧ ( 𝑌 ∨ 𝑉 ) ) ) ) )