Metamath Proof Explorer

Theorem islvol2aN

Description: The predicate "is a lattice volume". (Contributed by NM, 16-Jul-2012) (New usage is discouraged.)

Ref Expression
Hypotheses islvol2a.l ⊢ ≤ = ( le ‘ 𝐾 )
islvol2a.j ⊢ ∨ = ( join ‘ 𝐾 )
islvol2a.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
islvol2a.v ⊢ 𝑉 = ( LVols ‘ 𝐾 )
Assertion islvol2aN ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ) → ( ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∨ 𝑆 ) ∈ 𝑉 ↔ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) )

Proof

Step Hyp Ref Expression
1 islvol2a.l ⊢ ≤ = ( le ‘ 𝐾 )
2 islvol2a.j ⊢ ∨ = ( join ‘ 𝐾 )
3 islvol2a.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
4 islvol2a.v ⊢ 𝑉 = ( LVols ‘ 𝐾 )
5 oveq1 ⊢ ( 𝑃 = 𝑄 → ( 𝑃 ∨ 𝑄 ) = ( 𝑄 ∨ 𝑄 ) )
6 simpl1 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ) → 𝐾 ∈ HL )
7 simpl3 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ) → 𝑄 ∈ 𝐴 )
8 2 3 hlatjidm ⊢ ( ( 𝐾 ∈ HL ∧ 𝑄 ∈ 𝐴 ) → ( 𝑄 ∨ 𝑄 ) = 𝑄 )
9 6 7 8 syl2anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ) → ( 𝑄 ∨ 𝑄 ) = 𝑄 )
10 5 9 sylan9eqr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ) ∧ 𝑃 = 𝑄 ) → ( 𝑃 ∨ 𝑄 ) = 𝑄 )
11 10 oveq1d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ) ∧ 𝑃 = 𝑄 ) → ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) = ( 𝑄 ∨ 𝑅 ) )
12 11 oveq1d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ) ∧ 𝑃 = 𝑄 ) → ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∨ 𝑆 ) = ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) )
13 simprl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ) → 𝑅 ∈ 𝐴 )
14 simprr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ) → 𝑆 ∈ 𝐴 )
15 2 3 4 3atnelvolN ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ) → ¬ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ∈ 𝑉 )
16 6 7 13 14 15 syl13anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ) → ¬ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ∈ 𝑉 )
17 16 adantr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ) ∧ 𝑃 = 𝑄 ) → ¬ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ∈ 𝑉 )
18 12 17 eqneltrd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ) ∧ 𝑃 = 𝑄 ) → ¬ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∨ 𝑆 ) ∈ 𝑉 )
19 18 ex ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ) → ( 𝑃 = 𝑄 → ¬ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∨ 𝑆 ) ∈ 𝑉 ) )
20 19 necon2ad ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ) → ( ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∨ 𝑆 ) ∈ 𝑉 → 𝑃 ≠ 𝑄 ) )
21 6 hllatd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ) → 𝐾 ∈ Lat )
22 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
23 22 3 atbase ⊢ ( 𝑅 ∈ 𝐴 → 𝑅 ∈ ( Base ‘ 𝐾 ) )
24 23 ad2antrl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ) → 𝑅 ∈ ( Base ‘ 𝐾 ) )
25 22 2 3 hlatjcl ⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) → ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) )
26 25 adantr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ) → ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) )
27 22 1 2 latleeqj2 ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑅 ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) ) → ( 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ↔ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) = ( 𝑃 ∨ 𝑄 ) ) )
28 21 24 26 27 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ) → ( 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ↔ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) = ( 𝑃 ∨ 𝑄 ) ) )
29 simpl2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ) → 𝑃 ∈ 𝐴 )
30 2 3 4 3atnelvolN ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ) → ¬ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑆 ) ∈ 𝑉 )
31 6 29 7 14 30 syl13anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ) → ¬ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑆 ) ∈ 𝑉 )
32 oveq1 ⊢ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) = ( 𝑃 ∨ 𝑄 ) → ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∨ 𝑆 ) = ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑆 ) )
33 32 eleq1d ⊢ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) = ( 𝑃 ∨ 𝑄 ) → ( ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∨ 𝑆 ) ∈ 𝑉 ↔ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑆 ) ∈ 𝑉 ) )
34 33 notbid ⊢ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) = ( 𝑃 ∨ 𝑄 ) → ( ¬ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∨ 𝑆 ) ∈ 𝑉 ↔ ¬ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑆 ) ∈ 𝑉 ) )
35 31 34 syl5ibrcom ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ) → ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) = ( 𝑃 ∨ 𝑄 ) → ¬ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∨ 𝑆 ) ∈ 𝑉 ) )
36 28 35 sylbid ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ) → ( 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) → ¬ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∨ 𝑆 ) ∈ 𝑉 ) )
37 36 con2d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ) → ( ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∨ 𝑆 ) ∈ 𝑉 → ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) )
38 22 3 atbase ⊢ ( 𝑆 ∈ 𝐴 → 𝑆 ∈ ( Base ‘ 𝐾 ) )
39 38 ad2antll ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ) → 𝑆 ∈ ( Base ‘ 𝐾 ) )
40 22 2 latjcl ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑅 ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∈ ( Base ‘ 𝐾 ) )
41 21 26 24 40 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ) → ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∈ ( Base ‘ 𝐾 ) )
42 22 1 2 latleeqj2 ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑆 ∈ ( Base ‘ 𝐾 ) ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∈ ( Base ‘ 𝐾 ) ) → ( 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ↔ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∨ 𝑆 ) = ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) )
43 21 39 41 42 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ) → ( 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ↔ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∨ 𝑆 ) = ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) )
44 2 3 4 3atnelvolN ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) → ¬ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∈ 𝑉 )
45 6 29 7 13 44 syl13anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ) → ¬ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∈ 𝑉 )
46 eleq1 ⊢ ( ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∨ 𝑆 ) = ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) → ( ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∨ 𝑆 ) ∈ 𝑉 ↔ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∈ 𝑉 ) )
47 46 notbid ⊢ ( ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∨ 𝑆 ) = ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) → ( ¬ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∨ 𝑆 ) ∈ 𝑉 ↔ ¬ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∈ 𝑉 ) )
48 45 47 syl5ibrcom ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ) → ( ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∨ 𝑆 ) = ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) → ¬ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∨ 𝑆 ) ∈ 𝑉 ) )
49 43 48 sylbid ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ) → ( 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) → ¬ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∨ 𝑆 ) ∈ 𝑉 ) )
50 49 con2d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ) → ( ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∨ 𝑆 ) ∈ 𝑉 → ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) )
51 20 37 50 3jcad ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ) → ( ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∨ 𝑆 ) ∈ 𝑉 → ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) )
52 1 2 3 4 lvoli2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∨ 𝑆 ) ∈ 𝑉 )
53 52 3expia ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ) → ( ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) → ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∨ 𝑆 ) ∈ 𝑉 ) )
54 51 53 impbid ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ) → ( ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∨ 𝑆 ) ∈ 𝑉 ↔ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) )