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 
|- A e. CH
Assertion atoml2i 
|- ( ( B e. HAtoms /\ -. B C_ A ) -> ( ( A vH B ) i^i ( _|_ ` A ) ) e. HAtoms )

Proof

Step Hyp Ref Expression
1 atoml.1 
 |-  A e. CH
2 atelch 
 |-  ( B e. HAtoms -> B e. CH )
3 pjoml5 
 |-  ( ( A e. CH /\ B e. CH ) -> ( A vH ( ( _|_ ` A ) i^i ( A vH B ) ) ) = ( A vH B ) )
4 1 2 3 sylancr 
 |-  ( B e. HAtoms -> ( A vH ( ( _|_ ` A ) i^i ( A vH B ) ) ) = ( A vH B ) )
5 incom 
 |-  ( ( A vH B ) i^i ( _|_ ` A ) ) = ( ( _|_ ` A ) i^i ( A vH B ) )
6 5 eqeq1i 
 |-  ( ( ( A vH B ) i^i ( _|_ ` A ) ) = 0H <-> ( ( _|_ ` A ) i^i ( A vH B ) ) = 0H )
7 6 biimpi 
 |-  ( ( ( A vH B ) i^i ( _|_ ` A ) ) = 0H -> ( ( _|_ ` A ) i^i ( A vH B ) ) = 0H )
8 7 oveq2d 
 |-  ( ( ( A vH B ) i^i ( _|_ ` A ) ) = 0H -> ( A vH ( ( _|_ ` A ) i^i ( A vH B ) ) ) = ( A vH 0H ) )
9 1 chj0i 
 |-  ( A vH 0H ) = A
10 8 9 eqtrdi 
 |-  ( ( ( A vH B ) i^i ( _|_ ` A ) ) = 0H -> ( A vH ( ( _|_ ` A ) i^i ( A vH B ) ) ) = A )
11 4 10 sylan9req 
 |-  ( ( B e. HAtoms /\ ( ( A vH B ) i^i ( _|_ ` A ) ) = 0H ) -> ( A vH B ) = A )
12 11 ex 
 |-  ( B e. HAtoms -> ( ( ( A vH B ) i^i ( _|_ ` A ) ) = 0H -> ( A vH B ) = A ) )
13 chlejb2 
 |-  ( ( B e. CH /\ A e. CH ) -> ( B C_ A <-> ( A vH B ) = A ) )
14 2 1 13 sylancl 
 |-  ( B e. HAtoms -> ( B C_ A <-> ( A vH B ) = A ) )
15 12 14 sylibrd 
 |-  ( B e. HAtoms -> ( ( ( A vH B ) i^i ( _|_ ` A ) ) = 0H -> B C_ A ) )
16 15 con3d 
 |-  ( B e. HAtoms -> ( -. B C_ A -> -. ( ( A vH B ) i^i ( _|_ ` A ) ) = 0H ) )
17 1 atomli 
 |-  ( B e. HAtoms -> ( ( A vH B ) i^i ( _|_ ` A ) ) e. ( HAtoms u. { 0H } ) )
18 elun 
 |-  ( ( ( A vH B ) i^i ( _|_ ` A ) ) e. ( HAtoms u. { 0H } ) <-> ( ( ( A vH B ) i^i ( _|_ ` A ) ) e. HAtoms \/ ( ( A vH B ) i^i ( _|_ ` A ) ) e. { 0H } ) )
19 h0elch 
 |-  0H e. CH
20 19 elexi 
 |-  0H e. _V
21 20 elsn2 
 |-  ( ( ( A vH B ) i^i ( _|_ ` A ) ) e. { 0H } <-> ( ( A vH B ) i^i ( _|_ ` A ) ) = 0H )
22 21 orbi2i 
 |-  ( ( ( ( A vH B ) i^i ( _|_ ` A ) ) e. HAtoms \/ ( ( A vH B ) i^i ( _|_ ` A ) ) e. { 0H } ) <-> ( ( ( A vH B ) i^i ( _|_ ` A ) ) e. HAtoms \/ ( ( A vH B ) i^i ( _|_ ` A ) ) = 0H ) )
23 orcom 
 |-  ( ( ( ( A vH B ) i^i ( _|_ ` A ) ) e. HAtoms \/ ( ( A vH B ) i^i ( _|_ ` A ) ) = 0H ) <-> ( ( ( A vH B ) i^i ( _|_ ` A ) ) = 0H \/ ( ( A vH B ) i^i ( _|_ ` A ) ) e. HAtoms ) )
24 18 22 23 3bitri 
 |-  ( ( ( A vH B ) i^i ( _|_ ` A ) ) e. ( HAtoms u. { 0H } ) <-> ( ( ( A vH B ) i^i ( _|_ ` A ) ) = 0H \/ ( ( A vH B ) i^i ( _|_ ` A ) ) e. HAtoms ) )
25 17 24 sylib 
 |-  ( B e. HAtoms -> ( ( ( A vH B ) i^i ( _|_ ` A ) ) = 0H \/ ( ( A vH B ) i^i ( _|_ ` A ) ) e. HAtoms ) )
26 25 ord 
 |-  ( B e. HAtoms -> ( -. ( ( A vH B ) i^i ( _|_ ` A ) ) = 0H -> ( ( A vH B ) i^i ( _|_ ` A ) ) e. HAtoms ) )
27 16 26 syld 
 |-  ( B e. HAtoms -> ( -. B C_ A -> ( ( A vH B ) i^i ( _|_ ` A ) ) e. HAtoms ) )
28 27 imp 
 |-  ( ( B e. HAtoms /\ -. B C_ A ) -> ( ( A vH B ) i^i ( _|_ ` A ) ) e. HAtoms )