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 e. CH
atabs.2
|- B e. CH
Assertion atabsi
|- ( C e. HAtoms -> ( -. C C_ ( A vH B ) -> ( ( A vH C ) i^i B ) = ( A i^i B ) ) )

Proof

Step Hyp Ref Expression
1 atabs.1
 |-  A e. CH
2 atabs.2
 |-  B e. CH
3 inass
 |-  ( ( ( A vH C ) i^i ( A vH B ) ) i^i B ) = ( ( A vH C ) i^i ( ( A vH B ) i^i B ) )
4 1 2 chjcomi
 |-  ( A vH B ) = ( B vH A )
5 4 ineq1i
 |-  ( ( A vH B ) i^i B ) = ( ( B vH A ) i^i B )
6 incom
 |-  ( ( B vH A ) i^i B ) = ( B i^i ( B vH A ) )
7 2 1 chabs2i
 |-  ( B i^i ( B vH A ) ) = B
8 5 6 7 3eqtri
 |-  ( ( A vH B ) i^i B ) = B
9 8 ineq2i
 |-  ( ( A vH C ) i^i ( ( A vH B ) i^i B ) ) = ( ( A vH C ) i^i B )
10 3 9 eqtr2i
 |-  ( ( A vH C ) i^i B ) = ( ( ( A vH C ) i^i ( A vH B ) ) i^i B )
11 1 2 chub1i
 |-  A C_ ( A vH B )
12 atelch
 |-  ( C e. HAtoms -> C e. CH )
13 1 2 chjcli
 |-  ( A vH B ) e. CH
14 atmd
 |-  ( ( C e. HAtoms /\ ( A vH B ) e. CH ) -> C MH ( A vH B ) )
15 13 14 mpan2
 |-  ( C e. HAtoms -> C MH ( A vH B ) )
16 mdi
 |-  ( ( ( C e. CH /\ ( A vH B ) e. CH /\ A e. CH ) /\ ( C MH ( A vH B ) /\ A C_ ( A vH B ) ) ) -> ( ( A vH C ) i^i ( A vH B ) ) = ( A vH ( C i^i ( A vH B ) ) ) )
17 16 exp32
 |-  ( ( C e. CH /\ ( A vH B ) e. CH /\ A e. CH ) -> ( C MH ( A vH B ) -> ( A C_ ( A vH B ) -> ( ( A vH C ) i^i ( A vH B ) ) = ( A vH ( C i^i ( A vH B ) ) ) ) ) )
18 13 1 17 mp3an23
 |-  ( C e. CH -> ( C MH ( A vH B ) -> ( A C_ ( A vH B ) -> ( ( A vH C ) i^i ( A vH B ) ) = ( A vH ( C i^i ( A vH B ) ) ) ) ) )
19 12 15 18 sylc
 |-  ( C e. HAtoms -> ( A C_ ( A vH B ) -> ( ( A vH C ) i^i ( A vH B ) ) = ( A vH ( C i^i ( A vH B ) ) ) ) )
20 11 19 mpi
 |-  ( C e. HAtoms -> ( ( A vH C ) i^i ( A vH B ) ) = ( A vH ( C i^i ( A vH B ) ) ) )
21 20 adantr
 |-  ( ( C e. HAtoms /\ -. C C_ ( A vH B ) ) -> ( ( A vH C ) i^i ( A vH B ) ) = ( A vH ( C i^i ( A vH B ) ) ) )
22 incom
 |-  ( C i^i ( A vH B ) ) = ( ( A vH B ) i^i C )
23 atnssm0
 |-  ( ( ( A vH B ) e. CH /\ C e. HAtoms ) -> ( -. C C_ ( A vH B ) <-> ( ( A vH B ) i^i C ) = 0H ) )
24 13 23 mpan
 |-  ( C e. HAtoms -> ( -. C C_ ( A vH B ) <-> ( ( A vH B ) i^i C ) = 0H ) )
25 24 biimpa
 |-  ( ( C e. HAtoms /\ -. C C_ ( A vH B ) ) -> ( ( A vH B ) i^i C ) = 0H )
26 22 25 syl5eq
 |-  ( ( C e. HAtoms /\ -. C C_ ( A vH B ) ) -> ( C i^i ( A vH B ) ) = 0H )
27 26 oveq2d
 |-  ( ( C e. HAtoms /\ -. C C_ ( A vH B ) ) -> ( A vH ( C i^i ( A vH B ) ) ) = ( A vH 0H ) )
28 1 chj0i
 |-  ( A vH 0H ) = A
29 27 28 syl6eq
 |-  ( ( C e. HAtoms /\ -. C C_ ( A vH B ) ) -> ( A vH ( C i^i ( A vH B ) ) ) = A )
30 21 29 eqtrd
 |-  ( ( C e. HAtoms /\ -. C C_ ( A vH B ) ) -> ( ( A vH C ) i^i ( A vH B ) ) = A )
31 30 ineq1d
 |-  ( ( C e. HAtoms /\ -. C C_ ( A vH B ) ) -> ( ( ( A vH C ) i^i ( A vH B ) ) i^i B ) = ( A i^i B ) )
32 10 31 syl5eq
 |-  ( ( C e. HAtoms /\ -. C C_ ( A vH B ) ) -> ( ( A vH C ) i^i B ) = ( A i^i B ) )
33 32 ex
 |-  ( C e. HAtoms -> ( -. C C_ ( A vH B ) -> ( ( A vH C ) i^i B ) = ( A i^i B ) ) )