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

Metamath Proof Explorer

Theorem mdsl3

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

Ref Expression
Assertion mdsl3 ( ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) ∧ ( 𝐴 𝑀ℋ 𝐵 ∧ ( 𝐴 ∩ 𝐵 ) ⊆ 𝐶 ∧ 𝐶 ⊆ 𝐵 ) ) → ( ( 𝐶 ∨ℋ 𝐴 ) ∩ 𝐵 ) = 𝐶 )

Proof

Step Hyp Ref Expression
1 mdi ⊢ ( ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) ∧ ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐶 ⊆ 𝐵 ) ) → ( ( 𝐶 ∨ℋ 𝐴 ) ∩ 𝐵 ) = ( 𝐶 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) )
2 1 3adantr2 ⊢ ( ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) ∧ ( 𝐴 𝑀ℋ 𝐵 ∧ ( 𝐴 ∩ 𝐵 ) ⊆ 𝐶 ∧ 𝐶 ⊆ 𝐵 ) ) → ( ( 𝐶 ∨ℋ 𝐴 ) ∩ 𝐵 ) = ( 𝐶 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) )
3 chincl ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( 𝐴 ∩ 𝐵 ) ∈ Cℋ )
4 chlejb2 ⊢ ( ( ( 𝐴 ∩ 𝐵 ) ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) → ( ( 𝐴 ∩ 𝐵 ) ⊆ 𝐶 ↔ ( 𝐶 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) = 𝐶 ) )
5 3 4 stoic3 ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) → ( ( 𝐴 ∩ 𝐵 ) ⊆ 𝐶 ↔ ( 𝐶 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) = 𝐶 ) )
6 5 biimpa ⊢ ( ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) ∧ ( 𝐴 ∩ 𝐵 ) ⊆ 𝐶 ) → ( 𝐶 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) = 𝐶 )
7 6 3ad2antr2 ⊢ ( ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) ∧ ( 𝐴 𝑀ℋ 𝐵 ∧ ( 𝐴 ∩ 𝐵 ) ⊆ 𝐶 ∧ 𝐶 ⊆ 𝐵 ) ) → ( 𝐶 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) = 𝐶 )
8 2 7 eqtrd ⊢ ( ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) ∧ ( 𝐴 𝑀ℋ 𝐵 ∧ ( 𝐴 ∩ 𝐵 ) ⊆ 𝐶 ∧ 𝐶 ⊆ 𝐵 ) ) → ( ( 𝐶 ∨ℋ 𝐴 ) ∩ 𝐵 ) = 𝐶 )