This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 0ℋ ∈ Cℋ
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 )