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 eqtrdi 
 |-  ( ( 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 ) ) )