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