Metamath Proof Explorer


Theorem atoml2i

Description: An assertion holding in atomic orthomodular lattices that is equivalent to the exchange axiom. Proposition P8(ii) of BeltramettiCassinelli1 p. 400. (Contributed by NM, 12-Jun-2006) (New usage is discouraged.)

Ref Expression
Hypothesis atoml.1 𝐴C
Assertion atoml2i ( ( 𝐵 ∈ HAtoms ∧ ¬ 𝐵𝐴 ) → ( ( 𝐴 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) ∈ HAtoms )

Proof

Step Hyp Ref Expression
1 atoml.1 𝐴C
2 atelch ( 𝐵 ∈ HAtoms → 𝐵C )
3 pjoml5 ( ( 𝐴C𝐵C ) → ( 𝐴 ( ( ⊥ ‘ 𝐴 ) ∩ ( 𝐴 𝐵 ) ) ) = ( 𝐴 𝐵 ) )
4 1 2 3 sylancr ( 𝐵 ∈ HAtoms → ( 𝐴 ( ( ⊥ ‘ 𝐴 ) ∩ ( 𝐴 𝐵 ) ) ) = ( 𝐴 𝐵 ) )
5 incom ( ( 𝐴 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) = ( ( ⊥ ‘ 𝐴 ) ∩ ( 𝐴 𝐵 ) )
6 5 eqeq1i ( ( ( 𝐴 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) = 0 ↔ ( ( ⊥ ‘ 𝐴 ) ∩ ( 𝐴 𝐵 ) ) = 0 )
7 6 biimpi ( ( ( 𝐴 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) = 0 → ( ( ⊥ ‘ 𝐴 ) ∩ ( 𝐴 𝐵 ) ) = 0 )
8 7 oveq2d ( ( ( 𝐴 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) = 0 → ( 𝐴 ( ( ⊥ ‘ 𝐴 ) ∩ ( 𝐴 𝐵 ) ) ) = ( 𝐴 0 ) )
9 1 chj0i ( 𝐴 0 ) = 𝐴
10 8 9 eqtrdi ( ( ( 𝐴 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) = 0 → ( 𝐴 ( ( ⊥ ‘ 𝐴 ) ∩ ( 𝐴 𝐵 ) ) ) = 𝐴 )
11 4 10 sylan9req ( ( 𝐵 ∈ HAtoms ∧ ( ( 𝐴 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) = 0 ) → ( 𝐴 𝐵 ) = 𝐴 )
12 11 ex ( 𝐵 ∈ HAtoms → ( ( ( 𝐴 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) = 0 → ( 𝐴 𝐵 ) = 𝐴 ) )
13 chlejb2 ( ( 𝐵C𝐴C ) → ( 𝐵𝐴 ↔ ( 𝐴 𝐵 ) = 𝐴 ) )
14 2 1 13 sylancl ( 𝐵 ∈ HAtoms → ( 𝐵𝐴 ↔ ( 𝐴 𝐵 ) = 𝐴 ) )
15 12 14 sylibrd ( 𝐵 ∈ HAtoms → ( ( ( 𝐴 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) = 0𝐵𝐴 ) )
16 15 con3d ( 𝐵 ∈ HAtoms → ( ¬ 𝐵𝐴 → ¬ ( ( 𝐴 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) = 0 ) )
17 1 atomli ( 𝐵 ∈ HAtoms → ( ( 𝐴 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) ∈ ( HAtoms ∪ { 0 } ) )
18 elun ( ( ( 𝐴 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) ∈ ( HAtoms ∪ { 0 } ) ↔ ( ( ( 𝐴 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) ∈ HAtoms ∨ ( ( 𝐴 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) ∈ { 0 } ) )
19 h0elch 0C
20 19 elexi 0 ∈ V
21 20 elsn2 ( ( ( 𝐴 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) ∈ { 0 } ↔ ( ( 𝐴 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) = 0 )
22 21 orbi2i ( ( ( ( 𝐴 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) ∈ HAtoms ∨ ( ( 𝐴 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) ∈ { 0 } ) ↔ ( ( ( 𝐴 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) ∈ HAtoms ∨ ( ( 𝐴 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) = 0 ) )
23 orcom ( ( ( ( 𝐴 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) ∈ HAtoms ∨ ( ( 𝐴 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) = 0 ) ↔ ( ( ( 𝐴 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) = 0 ∨ ( ( 𝐴 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) ∈ HAtoms ) )
24 18 22 23 3bitri ( ( ( 𝐴 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) ∈ ( HAtoms ∪ { 0 } ) ↔ ( ( ( 𝐴 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) = 0 ∨ ( ( 𝐴 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) ∈ HAtoms ) )
25 17 24 sylib ( 𝐵 ∈ HAtoms → ( ( ( 𝐴 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) = 0 ∨ ( ( 𝐴 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) ∈ HAtoms ) )
26 25 ord ( 𝐵 ∈ HAtoms → ( ¬ ( ( 𝐴 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) = 0 → ( ( 𝐴 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) ∈ HAtoms ) )
27 16 26 syld ( 𝐵 ∈ HAtoms → ( ¬ 𝐵𝐴 → ( ( 𝐴 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) ∈ HAtoms ) )
28 27 imp ( ( 𝐵 ∈ HAtoms ∧ ¬ 𝐵𝐴 ) → ( ( 𝐴 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) ∈ HAtoms )