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

Metamath Proof Explorer

Theorem dmdsl3

Description: Sublattice mapping for a dual-modular pair. Part of Theorem 1.3 of MaedaMaeda p. 2. (Contributed by NM, 26-Apr-2006) (New usage is discouraged.)

Ref Expression
Assertion dmdsl3 ⊢ A ∈ C ℋ ∧ B ∈ C ℋ ∧ C ∈ C ℋ ∧ B 𝑀 ℋ * A ∧ A ⊆ C ∧ C ⊆ A ∨ ℋ B → C ∩ B ∨ ℋ A = C

Proof

Step Hyp Ref Expression
1 dmdi ⊢ B ∈ C ℋ ∧ A ∈ C ℋ ∧ C ∈ C ℋ ∧ B 𝑀 ℋ * A ∧ A ⊆ C → C ∩ B ∨ ℋ A = C ∩ B ∨ ℋ A
2 1 exp32 ⊢ B ∈ C ℋ ∧ A ∈ C ℋ ∧ C ∈ C ℋ → B 𝑀 ℋ * A → A ⊆ C → C ∩ B ∨ ℋ A = C ∩ B ∨ ℋ A
3 2 3com12 ⊢ A ∈ C ℋ ∧ B ∈ C ℋ ∧ C ∈ C ℋ → B 𝑀 ℋ * A → A ⊆ C → C ∩ B ∨ ℋ A = C ∩ B ∨ ℋ A
4 3 imp32 ⊢ A ∈ C ℋ ∧ B ∈ C ℋ ∧ C ∈ C ℋ ∧ B 𝑀 ℋ * A ∧ A ⊆ C → C ∩ B ∨ ℋ A = C ∩ B ∨ ℋ A
5 4 3adantr3 ⊢ A ∈ C ℋ ∧ B ∈ C ℋ ∧ C ∈ C ℋ ∧ B 𝑀 ℋ * A ∧ A ⊆ C ∧ C ⊆ A ∨ ℋ B → C ∩ B ∨ ℋ A = C ∩ B ∨ ℋ A
6 chjcom ⊢ A ∈ C ℋ ∧ B ∈ C ℋ → A ∨ ℋ B = B ∨ ℋ A
7 6 ineq2d ⊢ A ∈ C ℋ ∧ B ∈ C ℋ → C ∩ A ∨ ℋ B = C ∩ B ∨ ℋ A
8 7 3adant3 ⊢ A ∈ C ℋ ∧ B ∈ C ℋ ∧ C ∈ C ℋ → C ∩ A ∨ ℋ B = C ∩ B ∨ ℋ A
9 dfss2 ⊢ C ⊆ A ∨ ℋ B ↔ C ∩ A ∨ ℋ B = C
10 9 biimpi ⊢ C ⊆ A ∨ ℋ B → C ∩ A ∨ ℋ B = C
11 8 10 sylan9req ⊢ A ∈ C ℋ ∧ B ∈ C ℋ ∧ C ∈ C ℋ ∧ C ⊆ A ∨ ℋ B → C ∩ B ∨ ℋ A = C
12 11 3ad2antr3 ⊢ A ∈ C ℋ ∧ B ∈ C ℋ ∧ C ∈ C ℋ ∧ B 𝑀 ℋ * A ∧ A ⊆ C ∧ C ⊆ A ∨ ℋ B → C ∩ B ∨ ℋ A = C
13 5 12 eqtrd ⊢ A ∈ C ℋ ∧ B ∈ C ℋ ∧ C ∈ C ℋ ∧ B 𝑀 ℋ * A ∧ A ⊆ C ∧ C ⊆ A ∨ ℋ B → C ∩ B ∨ ℋ A = C