# Metamath Proof Explorer

## Theorem atabsi

Description: Absorption of an incomparable atom. Similar to Exercise 7.1 of MaedaMaeda p. 34. (Contributed by NM, 15-Jul-2004) (New usage is discouraged.)

Ref Expression
Hypotheses atabs.1 ${⊢}{A}\in {\mathbf{C}}_{ℋ}$
atabs.2 ${⊢}{B}\in {\mathbf{C}}_{ℋ}$
Assertion atabsi ${⊢}{C}\in \mathrm{HAtoms}\to \left(¬{C}\subseteq {A}{\vee }_{ℋ}{B}\to \left({A}{\vee }_{ℋ}{C}\right)\cap {B}={A}\cap {B}\right)$

### Proof

Step Hyp Ref Expression
1 atabs.1 ${⊢}{A}\in {\mathbf{C}}_{ℋ}$
2 atabs.2 ${⊢}{B}\in {\mathbf{C}}_{ℋ}$
3 inass ${⊢}\left(\left({A}{\vee }_{ℋ}{C}\right)\cap \left({A}{\vee }_{ℋ}{B}\right)\right)\cap {B}=\left({A}{\vee }_{ℋ}{C}\right)\cap \left(\left({A}{\vee }_{ℋ}{B}\right)\cap {B}\right)$
4 1 2 chjcomi ${⊢}{A}{\vee }_{ℋ}{B}={B}{\vee }_{ℋ}{A}$
5 4 ineq1i ${⊢}\left({A}{\vee }_{ℋ}{B}\right)\cap {B}=\left({B}{\vee }_{ℋ}{A}\right)\cap {B}$
6 incom ${⊢}\left({B}{\vee }_{ℋ}{A}\right)\cap {B}={B}\cap \left({B}{\vee }_{ℋ}{A}\right)$
7 2 1 chabs2i ${⊢}{B}\cap \left({B}{\vee }_{ℋ}{A}\right)={B}$
8 5 6 7 3eqtri ${⊢}\left({A}{\vee }_{ℋ}{B}\right)\cap {B}={B}$
9 8 ineq2i ${⊢}\left({A}{\vee }_{ℋ}{C}\right)\cap \left(\left({A}{\vee }_{ℋ}{B}\right)\cap {B}\right)=\left({A}{\vee }_{ℋ}{C}\right)\cap {B}$
10 3 9 eqtr2i ${⊢}\left({A}{\vee }_{ℋ}{C}\right)\cap {B}=\left(\left({A}{\vee }_{ℋ}{C}\right)\cap \left({A}{\vee }_{ℋ}{B}\right)\right)\cap {B}$
11 1 2 chub1i ${⊢}{A}\subseteq {A}{\vee }_{ℋ}{B}$
12 atelch ${⊢}{C}\in \mathrm{HAtoms}\to {C}\in {\mathbf{C}}_{ℋ}$
13 1 2 chjcli ${⊢}{A}{\vee }_{ℋ}{B}\in {\mathbf{C}}_{ℋ}$
14 atmd ${⊢}\left({C}\in \mathrm{HAtoms}\wedge {A}{\vee }_{ℋ}{B}\in {\mathbf{C}}_{ℋ}\right)\to {C}{𝑀}_{ℋ}\left({A}{\vee }_{ℋ}{B}\right)$
15 13 14 mpan2 ${⊢}{C}\in \mathrm{HAtoms}\to {C}{𝑀}_{ℋ}\left({A}{\vee }_{ℋ}{B}\right)$
16 mdi ${⊢}\left(\left({C}\in {\mathbf{C}}_{ℋ}\wedge {A}{\vee }_{ℋ}{B}\in {\mathbf{C}}_{ℋ}\wedge {A}\in {\mathbf{C}}_{ℋ}\right)\wedge \left({C}{𝑀}_{ℋ}\left({A}{\vee }_{ℋ}{B}\right)\wedge {A}\subseteq {A}{\vee }_{ℋ}{B}\right)\right)\to \left({A}{\vee }_{ℋ}{C}\right)\cap \left({A}{\vee }_{ℋ}{B}\right)={A}{\vee }_{ℋ}\left({C}\cap \left({A}{\vee }_{ℋ}{B}\right)\right)$
17 16 exp32 ${⊢}\left({C}\in {\mathbf{C}}_{ℋ}\wedge {A}{\vee }_{ℋ}{B}\in {\mathbf{C}}_{ℋ}\wedge {A}\in {\mathbf{C}}_{ℋ}\right)\to \left({C}{𝑀}_{ℋ}\left({A}{\vee }_{ℋ}{B}\right)\to \left({A}\subseteq {A}{\vee }_{ℋ}{B}\to \left({A}{\vee }_{ℋ}{C}\right)\cap \left({A}{\vee }_{ℋ}{B}\right)={A}{\vee }_{ℋ}\left({C}\cap \left({A}{\vee }_{ℋ}{B}\right)\right)\right)\right)$
18 13 1 17 mp3an23 ${⊢}{C}\in {\mathbf{C}}_{ℋ}\to \left({C}{𝑀}_{ℋ}\left({A}{\vee }_{ℋ}{B}\right)\to \left({A}\subseteq {A}{\vee }_{ℋ}{B}\to \left({A}{\vee }_{ℋ}{C}\right)\cap \left({A}{\vee }_{ℋ}{B}\right)={A}{\vee }_{ℋ}\left({C}\cap \left({A}{\vee }_{ℋ}{B}\right)\right)\right)\right)$
19 12 15 18 sylc ${⊢}{C}\in \mathrm{HAtoms}\to \left({A}\subseteq {A}{\vee }_{ℋ}{B}\to \left({A}{\vee }_{ℋ}{C}\right)\cap \left({A}{\vee }_{ℋ}{B}\right)={A}{\vee }_{ℋ}\left({C}\cap \left({A}{\vee }_{ℋ}{B}\right)\right)\right)$
20 11 19 mpi ${⊢}{C}\in \mathrm{HAtoms}\to \left({A}{\vee }_{ℋ}{C}\right)\cap \left({A}{\vee }_{ℋ}{B}\right)={A}{\vee }_{ℋ}\left({C}\cap \left({A}{\vee }_{ℋ}{B}\right)\right)$
21 20 adantr ${⊢}\left({C}\in \mathrm{HAtoms}\wedge ¬{C}\subseteq {A}{\vee }_{ℋ}{B}\right)\to \left({A}{\vee }_{ℋ}{C}\right)\cap \left({A}{\vee }_{ℋ}{B}\right)={A}{\vee }_{ℋ}\left({C}\cap \left({A}{\vee }_{ℋ}{B}\right)\right)$
22 incom ${⊢}{C}\cap \left({A}{\vee }_{ℋ}{B}\right)=\left({A}{\vee }_{ℋ}{B}\right)\cap {C}$
23 atnssm0 ${⊢}\left({A}{\vee }_{ℋ}{B}\in {\mathbf{C}}_{ℋ}\wedge {C}\in \mathrm{HAtoms}\right)\to \left(¬{C}\subseteq {A}{\vee }_{ℋ}{B}↔\left({A}{\vee }_{ℋ}{B}\right)\cap {C}={0}_{ℋ}\right)$
24 13 23 mpan ${⊢}{C}\in \mathrm{HAtoms}\to \left(¬{C}\subseteq {A}{\vee }_{ℋ}{B}↔\left({A}{\vee }_{ℋ}{B}\right)\cap {C}={0}_{ℋ}\right)$
25 24 biimpa ${⊢}\left({C}\in \mathrm{HAtoms}\wedge ¬{C}\subseteq {A}{\vee }_{ℋ}{B}\right)\to \left({A}{\vee }_{ℋ}{B}\right)\cap {C}={0}_{ℋ}$
26 22 25 syl5eq ${⊢}\left({C}\in \mathrm{HAtoms}\wedge ¬{C}\subseteq {A}{\vee }_{ℋ}{B}\right)\to {C}\cap \left({A}{\vee }_{ℋ}{B}\right)={0}_{ℋ}$
27 26 oveq2d ${⊢}\left({C}\in \mathrm{HAtoms}\wedge ¬{C}\subseteq {A}{\vee }_{ℋ}{B}\right)\to {A}{\vee }_{ℋ}\left({C}\cap \left({A}{\vee }_{ℋ}{B}\right)\right)={A}{\vee }_{ℋ}{0}_{ℋ}$
28 1 chj0i ${⊢}{A}{\vee }_{ℋ}{0}_{ℋ}={A}$
29 27 28 syl6eq ${⊢}\left({C}\in \mathrm{HAtoms}\wedge ¬{C}\subseteq {A}{\vee }_{ℋ}{B}\right)\to {A}{\vee }_{ℋ}\left({C}\cap \left({A}{\vee }_{ℋ}{B}\right)\right)={A}$
30 21 29 eqtrd ${⊢}\left({C}\in \mathrm{HAtoms}\wedge ¬{C}\subseteq {A}{\vee }_{ℋ}{B}\right)\to \left({A}{\vee }_{ℋ}{C}\right)\cap \left({A}{\vee }_{ℋ}{B}\right)={A}$
31 30 ineq1d ${⊢}\left({C}\in \mathrm{HAtoms}\wedge ¬{C}\subseteq {A}{\vee }_{ℋ}{B}\right)\to \left(\left({A}{\vee }_{ℋ}{C}\right)\cap \left({A}{\vee }_{ℋ}{B}\right)\right)\cap {B}={A}\cap {B}$
32 10 31 syl5eq ${⊢}\left({C}\in \mathrm{HAtoms}\wedge ¬{C}\subseteq {A}{\vee }_{ℋ}{B}\right)\to \left({A}{\vee }_{ℋ}{C}\right)\cap {B}={A}\cap {B}$
33 32 ex ${⊢}{C}\in \mathrm{HAtoms}\to \left(¬{C}\subseteq {A}{\vee }_{ℋ}{B}\to \left({A}{\vee }_{ℋ}{C}\right)\cap {B}={A}\cap {B}\right)$