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

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 ⊢ 𝐴 ∈ Cℋ
atabs.2 ⊢ 𝐵 ∈ Cℋ
Assertion atabsi ( 𝐶 ∈ HAtoms → ( ¬ 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) → ( ( 𝐴 ∨ℋ 𝐶 ) ∩ 𝐵 ) = ( 𝐴 ∩ 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 atabs.1 ⊢ 𝐴 ∈ Cℋ
2 atabs.2 ⊢ 𝐵 ∈ Cℋ
3 inass ⊢ ( ( ( 𝐴 ∨ℋ 𝐶 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ∩ 𝐵 ) = ( ( 𝐴 ∨ℋ 𝐶 ) ∩ ( ( 𝐴 ∨ℋ 𝐵 ) ∩ 𝐵 ) )
4 1 2 chjcomi ⊢ ( 𝐴 ∨ℋ 𝐵 ) = ( 𝐵 ∨ℋ 𝐴 )
5 4 ineq1i ⊢ ( ( 𝐴 ∨ℋ 𝐵 ) ∩ 𝐵 ) = ( ( 𝐵 ∨ℋ 𝐴 ) ∩ 𝐵 )
6 incom ⊢ ( ( 𝐵 ∨ℋ 𝐴 ) ∩ 𝐵 ) = ( 𝐵 ∩ ( 𝐵 ∨ℋ 𝐴 ) )
7 2 1 chabs2i ⊢ ( 𝐵 ∩ ( 𝐵 ∨ℋ 𝐴 ) ) = 𝐵
8 5 6 7 3eqtri ⊢ ( ( 𝐴 ∨ℋ 𝐵 ) ∩ 𝐵 ) = 𝐵
9 8 ineq2i ⊢ ( ( 𝐴 ∨ℋ 𝐶 ) ∩ ( ( 𝐴 ∨ℋ 𝐵 ) ∩ 𝐵 ) ) = ( ( 𝐴 ∨ℋ 𝐶 ) ∩ 𝐵 )
10 3 9 eqtr2i ⊢ ( ( 𝐴 ∨ℋ 𝐶 ) ∩ 𝐵 ) = ( ( ( 𝐴 ∨ℋ 𝐶 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ∩ 𝐵 )
11 1 2 chub1i ⊢ 𝐴 ⊆ ( 𝐴 ∨ℋ 𝐵 )
12 atelch ⊢ ( 𝐶 ∈ HAtoms → 𝐶 ∈ Cℋ )
13 1 2 chjcli ⊢ ( 𝐴 ∨ℋ 𝐵 ) ∈ Cℋ
14 atmd ⊢ ( ( 𝐶 ∈ HAtoms ∧ ( 𝐴 ∨ℋ 𝐵 ) ∈ Cℋ ) → 𝐶 𝑀ℋ ( 𝐴 ∨ℋ 𝐵 ) )
15 13 14 mpan2 ⊢ ( 𝐶 ∈ HAtoms → 𝐶 𝑀ℋ ( 𝐴 ∨ℋ 𝐵 ) )
16 mdi ⊢ ( ( ( 𝐶 ∈ Cℋ ∧ ( 𝐴 ∨ℋ 𝐵 ) ∈ Cℋ ∧ 𝐴 ∈ Cℋ ) ∧ ( 𝐶 𝑀ℋ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐴 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) → ( ( 𝐴 ∨ℋ 𝐶 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) = ( 𝐴 ∨ℋ ( 𝐶 ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ) )
17 16 exp32 ⊢ ( ( 𝐶 ∈ Cℋ ∧ ( 𝐴 ∨ℋ 𝐵 ) ∈ Cℋ ∧ 𝐴 ∈ Cℋ ) → ( 𝐶 𝑀ℋ ( 𝐴 ∨ℋ 𝐵 ) → ( 𝐴 ⊆ ( 𝐴 ∨ℋ 𝐵 ) → ( ( 𝐴 ∨ℋ 𝐶 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) = ( 𝐴 ∨ℋ ( 𝐶 ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ) ) ) )
18 13 1 17 mp3an23 ⊢ ( 𝐶 ∈ Cℋ → ( 𝐶 𝑀ℋ ( 𝐴 ∨ℋ 𝐵 ) → ( 𝐴 ⊆ ( 𝐴 ∨ℋ 𝐵 ) → ( ( 𝐴 ∨ℋ 𝐶 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) = ( 𝐴 ∨ℋ ( 𝐶 ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ) ) ) )
19 12 15 18 sylc ⊢ ( 𝐶 ∈ HAtoms → ( 𝐴 ⊆ ( 𝐴 ∨ℋ 𝐵 ) → ( ( 𝐴 ∨ℋ 𝐶 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) = ( 𝐴 ∨ℋ ( 𝐶 ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ) ) )
20 11 19 mpi ⊢ ( 𝐶 ∈ HAtoms → ( ( 𝐴 ∨ℋ 𝐶 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) = ( 𝐴 ∨ℋ ( 𝐶 ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ) )
21 20 adantr ⊢ ( ( 𝐶 ∈ HAtoms ∧ ¬ 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) → ( ( 𝐴 ∨ℋ 𝐶 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) = ( 𝐴 ∨ℋ ( 𝐶 ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ) )
22 incom ⊢ ( 𝐶 ∩ ( 𝐴 ∨ℋ 𝐵 ) ) = ( ( 𝐴 ∨ℋ 𝐵 ) ∩ 𝐶 )
23 atnssm0 ⊢ ( ( ( 𝐴 ∨ℋ 𝐵 ) ∈ Cℋ ∧ 𝐶 ∈ HAtoms ) → ( ¬ 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ↔ ( ( 𝐴 ∨ℋ 𝐵 ) ∩ 𝐶 ) = 0ℋ ) )
24 13 23 mpan ⊢ ( 𝐶 ∈ HAtoms → ( ¬ 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ↔ ( ( 𝐴 ∨ℋ 𝐵 ) ∩ 𝐶 ) = 0ℋ ) )
25 24 biimpa ⊢ ( ( 𝐶 ∈ HAtoms ∧ ¬ 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) → ( ( 𝐴 ∨ℋ 𝐵 ) ∩ 𝐶 ) = 0ℋ )
26 22 25 eqtrid ⊢ ( ( 𝐶 ∈ HAtoms ∧ ¬ 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) → ( 𝐶 ∩ ( 𝐴 ∨ℋ 𝐵 ) ) = 0ℋ )
27 26 oveq2d ⊢ ( ( 𝐶 ∈ HAtoms ∧ ¬ 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) → ( 𝐴 ∨ℋ ( 𝐶 ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ) = ( 𝐴 ∨ℋ 0ℋ ) )
28 1 chj0i ⊢ ( 𝐴 ∨ℋ 0ℋ ) = 𝐴
29 27 28 eqtrdi ⊢ ( ( 𝐶 ∈ HAtoms ∧ ¬ 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) → ( 𝐴 ∨ℋ ( 𝐶 ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ) = 𝐴 )
30 21 29 eqtrd ⊢ ( ( 𝐶 ∈ HAtoms ∧ ¬ 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) → ( ( 𝐴 ∨ℋ 𝐶 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) = 𝐴 )
31 30 ineq1d ⊢ ( ( 𝐶 ∈ HAtoms ∧ ¬ 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) → ( ( ( 𝐴 ∨ℋ 𝐶 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ∩ 𝐵 ) = ( 𝐴 ∩ 𝐵 ) )
32 10 31 eqtrid ⊢ ( ( 𝐶 ∈ HAtoms ∧ ¬ 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) → ( ( 𝐴 ∨ℋ 𝐶 ) ∩ 𝐵 ) = ( 𝐴 ∩ 𝐵 ) )
33 32 ex ⊢ ( 𝐶 ∈ HAtoms → ( ¬ 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) → ( ( 𝐴 ∨ℋ 𝐶 ) ∩ 𝐵 ) = ( 𝐴 ∩ 𝐵 ) ) )