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

Metamath Proof Explorer

Theorem mdsl0

Description: A sublattice condition that transfers the modular pair property. Exercise 12 of Kalmbach p. 103. Also Lemma 1.5.3 of MaedaMaeda p. 2. (Contributed by NM, 22-Jun-2004) (New usage is discouraged.)

Ref Expression
Assertion mdsl0 ( ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) ∧ ( 𝐶 ∈ Cℋ ∧ 𝐷 ∈ Cℋ ) ) → ( ( ( ( 𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐵 ) ∧ ( 𝐴 ∩ 𝐵 ) = 0ℋ ) ∧ 𝐴 𝑀ℋ 𝐵 ) → 𝐶 𝑀ℋ 𝐷 ) )

Proof

Step Hyp Ref Expression
1 sstr2 ⊢ ( 𝑥 ⊆ 𝐷 → ( 𝐷 ⊆ 𝐵 → 𝑥 ⊆ 𝐵 ) )
2 1 com12 ⊢ ( 𝐷 ⊆ 𝐵 → ( 𝑥 ⊆ 𝐷 → 𝑥 ⊆ 𝐵 ) )
3 2 ad2antlr ⊢ ( ( ( 𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐵 ) ∧ ( 𝐴 ∩ 𝐵 ) = 0ℋ ) → ( 𝑥 ⊆ 𝐷 → 𝑥 ⊆ 𝐵 ) )
4 3 ad2antlr ⊢ ( ( ( ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) ∧ ( 𝐶 ∈ Cℋ ∧ 𝐷 ∈ Cℋ ) ) ∧ ( ( 𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐵 ) ∧ ( 𝐴 ∩ 𝐵 ) = 0ℋ ) ) ∧ 𝑥 ∈ Cℋ ) → ( 𝑥 ⊆ 𝐷 → 𝑥 ⊆ 𝐵 ) )
5 chlej2 ⊢ ( ( ( 𝐶 ∈ Cℋ ∧ 𝐴 ∈ Cℋ ∧ 𝑥 ∈ Cℋ ) ∧ 𝐶 ⊆ 𝐴 ) → ( 𝑥 ∨ℋ 𝐶 ) ⊆ ( 𝑥 ∨ℋ 𝐴 ) )
6 ss2in ⊢ ( ( ( 𝑥 ∨ℋ 𝐶 ) ⊆ ( 𝑥 ∨ℋ 𝐴 ) ∧ 𝐷 ⊆ 𝐵 ) → ( ( 𝑥 ∨ℋ 𝐶 ) ∩ 𝐷 ) ⊆ ( ( 𝑥 ∨ℋ 𝐴 ) ∩ 𝐵 ) )
7 6 ex ⊢ ( ( 𝑥 ∨ℋ 𝐶 ) ⊆ ( 𝑥 ∨ℋ 𝐴 ) → ( 𝐷 ⊆ 𝐵 → ( ( 𝑥 ∨ℋ 𝐶 ) ∩ 𝐷 ) ⊆ ( ( 𝑥 ∨ℋ 𝐴 ) ∩ 𝐵 ) ) )
8 5 7 syl ⊢ ( ( ( 𝐶 ∈ Cℋ ∧ 𝐴 ∈ Cℋ ∧ 𝑥 ∈ Cℋ ) ∧ 𝐶 ⊆ 𝐴 ) → ( 𝐷 ⊆ 𝐵 → ( ( 𝑥 ∨ℋ 𝐶 ) ∩ 𝐷 ) ⊆ ( ( 𝑥 ∨ℋ 𝐴 ) ∩ 𝐵 ) ) )
9 8 ex ⊢ ( ( 𝐶 ∈ Cℋ ∧ 𝐴 ∈ Cℋ ∧ 𝑥 ∈ Cℋ ) → ( 𝐶 ⊆ 𝐴 → ( 𝐷 ⊆ 𝐵 → ( ( 𝑥 ∨ℋ 𝐶 ) ∩ 𝐷 ) ⊆ ( ( 𝑥 ∨ℋ 𝐴 ) ∩ 𝐵 ) ) ) )
10 9 3expia ⊢ ( ( 𝐶 ∈ Cℋ ∧ 𝐴 ∈ Cℋ ) → ( 𝑥 ∈ Cℋ → ( 𝐶 ⊆ 𝐴 → ( 𝐷 ⊆ 𝐵 → ( ( 𝑥 ∨ℋ 𝐶 ) ∩ 𝐷 ) ⊆ ( ( 𝑥 ∨ℋ 𝐴 ) ∩ 𝐵 ) ) ) ) )
11 10 ancoms ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) → ( 𝑥 ∈ Cℋ → ( 𝐶 ⊆ 𝐴 → ( 𝐷 ⊆ 𝐵 → ( ( 𝑥 ∨ℋ 𝐶 ) ∩ 𝐷 ) ⊆ ( ( 𝑥 ∨ℋ 𝐴 ) ∩ 𝐵 ) ) ) ) )
12 11 ad2ant2r ⊢ ( ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) ∧ ( 𝐶 ∈ Cℋ ∧ 𝐷 ∈ Cℋ ) ) → ( 𝑥 ∈ Cℋ → ( 𝐶 ⊆ 𝐴 → ( 𝐷 ⊆ 𝐵 → ( ( 𝑥 ∨ℋ 𝐶 ) ∩ 𝐷 ) ⊆ ( ( 𝑥 ∨ℋ 𝐴 ) ∩ 𝐵 ) ) ) ) )
13 12 imp43 ⊢ ( ( ( ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) ∧ ( 𝐶 ∈ Cℋ ∧ 𝐷 ∈ Cℋ ) ) ∧ 𝑥 ∈ Cℋ ) ∧ ( 𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐵 ) ) → ( ( 𝑥 ∨ℋ 𝐶 ) ∩ 𝐷 ) ⊆ ( ( 𝑥 ∨ℋ 𝐴 ) ∩ 𝐵 ) )
14 13 adantrr ⊢ ( ( ( ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) ∧ ( 𝐶 ∈ Cℋ ∧ 𝐷 ∈ Cℋ ) ) ∧ 𝑥 ∈ Cℋ ) ∧ ( ( 𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐵 ) ∧ ( 𝐴 ∩ 𝐵 ) = 0ℋ ) ) → ( ( 𝑥 ∨ℋ 𝐶 ) ∩ 𝐷 ) ⊆ ( ( 𝑥 ∨ℋ 𝐴 ) ∩ 𝐵 ) )
15 oveq2 ⊢ ( ( 𝐴 ∩ 𝐵 ) = 0ℋ → ( 𝑥 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) = ( 𝑥 ∨ℋ 0ℋ ) )
16 chj0 ⊢ ( 𝑥 ∈ Cℋ → ( 𝑥 ∨ℋ 0ℋ ) = 𝑥 )
17 15 16 sylan9eqr ⊢ ( ( 𝑥 ∈ Cℋ ∧ ( 𝐴 ∩ 𝐵 ) = 0ℋ ) → ( 𝑥 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) = 𝑥 )
18 17 adantl ⊢ ( ( ( 𝐶 ∈ Cℋ ∧ 𝐷 ∈ Cℋ ) ∧ ( 𝑥 ∈ Cℋ ∧ ( 𝐴 ∩ 𝐵 ) = 0ℋ ) ) → ( 𝑥 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) = 𝑥 )
19 chincl ⊢ ( ( 𝐶 ∈ Cℋ ∧ 𝐷 ∈ Cℋ ) → ( 𝐶 ∩ 𝐷 ) ∈ Cℋ )
20 chub1 ⊢ ( ( 𝑥 ∈ Cℋ ∧ ( 𝐶 ∩ 𝐷 ) ∈ Cℋ ) → 𝑥 ⊆ ( 𝑥 ∨ℋ ( 𝐶 ∩ 𝐷 ) ) )
21 20 ancoms ⊢ ( ( ( 𝐶 ∩ 𝐷 ) ∈ Cℋ ∧ 𝑥 ∈ Cℋ ) → 𝑥 ⊆ ( 𝑥 ∨ℋ ( 𝐶 ∩ 𝐷 ) ) )
22 19 21 sylan ⊢ ( ( ( 𝐶 ∈ Cℋ ∧ 𝐷 ∈ Cℋ ) ∧ 𝑥 ∈ Cℋ ) → 𝑥 ⊆ ( 𝑥 ∨ℋ ( 𝐶 ∩ 𝐷 ) ) )
23 22 adantrr ⊢ ( ( ( 𝐶 ∈ Cℋ ∧ 𝐷 ∈ Cℋ ) ∧ ( 𝑥 ∈ Cℋ ∧ ( 𝐴 ∩ 𝐵 ) = 0ℋ ) ) → 𝑥 ⊆ ( 𝑥 ∨ℋ ( 𝐶 ∩ 𝐷 ) ) )
24 18 23 eqsstrd ⊢ ( ( ( 𝐶 ∈ Cℋ ∧ 𝐷 ∈ Cℋ ) ∧ ( 𝑥 ∈ Cℋ ∧ ( 𝐴 ∩ 𝐵 ) = 0ℋ ) ) → ( 𝑥 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ⊆ ( 𝑥 ∨ℋ ( 𝐶 ∩ 𝐷 ) ) )
25 24 adantll ⊢ ( ( ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) ∧ ( 𝐶 ∈ Cℋ ∧ 𝐷 ∈ Cℋ ) ) ∧ ( 𝑥 ∈ Cℋ ∧ ( 𝐴 ∩ 𝐵 ) = 0ℋ ) ) → ( 𝑥 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ⊆ ( 𝑥 ∨ℋ ( 𝐶 ∩ 𝐷 ) ) )
26 25 anassrs ⊢ ( ( ( ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) ∧ ( 𝐶 ∈ Cℋ ∧ 𝐷 ∈ Cℋ ) ) ∧ 𝑥 ∈ Cℋ ) ∧ ( 𝐴 ∩ 𝐵 ) = 0ℋ ) → ( 𝑥 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ⊆ ( 𝑥 ∨ℋ ( 𝐶 ∩ 𝐷 ) ) )
27 26 adantrl ⊢ ( ( ( ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) ∧ ( 𝐶 ∈ Cℋ ∧ 𝐷 ∈ Cℋ ) ) ∧ 𝑥 ∈ Cℋ ) ∧ ( ( 𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐵 ) ∧ ( 𝐴 ∩ 𝐵 ) = 0ℋ ) ) → ( 𝑥 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ⊆ ( 𝑥 ∨ℋ ( 𝐶 ∩ 𝐷 ) ) )
28 sstr2 ⊢ ( ( ( 𝑥 ∨ℋ 𝐶 ) ∩ 𝐷 ) ⊆ ( ( 𝑥 ∨ℋ 𝐴 ) ∩ 𝐵 ) → ( ( ( 𝑥 ∨ℋ 𝐴 ) ∩ 𝐵 ) ⊆ ( 𝑥 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) → ( ( 𝑥 ∨ℋ 𝐶 ) ∩ 𝐷 ) ⊆ ( 𝑥 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ) )
29 sstr2 ⊢ ( ( ( 𝑥 ∨ℋ 𝐶 ) ∩ 𝐷 ) ⊆ ( 𝑥 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) → ( ( 𝑥 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ⊆ ( 𝑥 ∨ℋ ( 𝐶 ∩ 𝐷 ) ) → ( ( 𝑥 ∨ℋ 𝐶 ) ∩ 𝐷 ) ⊆ ( 𝑥 ∨ℋ ( 𝐶 ∩ 𝐷 ) ) ) )
30 28 29 syl6 ⊢ ( ( ( 𝑥 ∨ℋ 𝐶 ) ∩ 𝐷 ) ⊆ ( ( 𝑥 ∨ℋ 𝐴 ) ∩ 𝐵 ) → ( ( ( 𝑥 ∨ℋ 𝐴 ) ∩ 𝐵 ) ⊆ ( 𝑥 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) → ( ( 𝑥 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ⊆ ( 𝑥 ∨ℋ ( 𝐶 ∩ 𝐷 ) ) → ( ( 𝑥 ∨ℋ 𝐶 ) ∩ 𝐷 ) ⊆ ( 𝑥 ∨ℋ ( 𝐶 ∩ 𝐷 ) ) ) ) )
31 30 com23 ⊢ ( ( ( 𝑥 ∨ℋ 𝐶 ) ∩ 𝐷 ) ⊆ ( ( 𝑥 ∨ℋ 𝐴 ) ∩ 𝐵 ) → ( ( 𝑥 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ⊆ ( 𝑥 ∨ℋ ( 𝐶 ∩ 𝐷 ) ) → ( ( ( 𝑥 ∨ℋ 𝐴 ) ∩ 𝐵 ) ⊆ ( 𝑥 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) → ( ( 𝑥 ∨ℋ 𝐶 ) ∩ 𝐷 ) ⊆ ( 𝑥 ∨ℋ ( 𝐶 ∩ 𝐷 ) ) ) ) )
32 14 27 31 sylc ⊢ ( ( ( ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) ∧ ( 𝐶 ∈ Cℋ ∧ 𝐷 ∈ Cℋ ) ) ∧ 𝑥 ∈ Cℋ ) ∧ ( ( 𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐵 ) ∧ ( 𝐴 ∩ 𝐵 ) = 0ℋ ) ) → ( ( ( 𝑥 ∨ℋ 𝐴 ) ∩ 𝐵 ) ⊆ ( 𝑥 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) → ( ( 𝑥 ∨ℋ 𝐶 ) ∩ 𝐷 ) ⊆ ( 𝑥 ∨ℋ ( 𝐶 ∩ 𝐷 ) ) ) )
33 32 an32s ⊢ ( ( ( ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) ∧ ( 𝐶 ∈ Cℋ ∧ 𝐷 ∈ Cℋ ) ) ∧ ( ( 𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐵 ) ∧ ( 𝐴 ∩ 𝐵 ) = 0ℋ ) ) ∧ 𝑥 ∈ Cℋ ) → ( ( ( 𝑥 ∨ℋ 𝐴 ) ∩ 𝐵 ) ⊆ ( 𝑥 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) → ( ( 𝑥 ∨ℋ 𝐶 ) ∩ 𝐷 ) ⊆ ( 𝑥 ∨ℋ ( 𝐶 ∩ 𝐷 ) ) ) )
34 4 33 imim12d ⊢ ( ( ( ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) ∧ ( 𝐶 ∈ Cℋ ∧ 𝐷 ∈ Cℋ ) ) ∧ ( ( 𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐵 ) ∧ ( 𝐴 ∩ 𝐵 ) = 0ℋ ) ) ∧ 𝑥 ∈ Cℋ ) → ( ( 𝑥 ⊆ 𝐵 → ( ( 𝑥 ∨ℋ 𝐴 ) ∩ 𝐵 ) ⊆ ( 𝑥 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ) → ( 𝑥 ⊆ 𝐷 → ( ( 𝑥 ∨ℋ 𝐶 ) ∩ 𝐷 ) ⊆ ( 𝑥 ∨ℋ ( 𝐶 ∩ 𝐷 ) ) ) ) )
35 34 ralimdva ⊢ ( ( ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) ∧ ( 𝐶 ∈ Cℋ ∧ 𝐷 ∈ Cℋ ) ) ∧ ( ( 𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐵 ) ∧ ( 𝐴 ∩ 𝐵 ) = 0ℋ ) ) → ( ∀ 𝑥 ∈ Cℋ ( 𝑥 ⊆ 𝐵 → ( ( 𝑥 ∨ℋ 𝐴 ) ∩ 𝐵 ) ⊆ ( 𝑥 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ) → ∀ 𝑥 ∈ Cℋ ( 𝑥 ⊆ 𝐷 → ( ( 𝑥 ∨ℋ 𝐶 ) ∩ 𝐷 ) ⊆ ( 𝑥 ∨ℋ ( 𝐶 ∩ 𝐷 ) ) ) ) )
36 mdbr2 ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( 𝐴 𝑀ℋ 𝐵 ↔ ∀ 𝑥 ∈ Cℋ ( 𝑥 ⊆ 𝐵 → ( ( 𝑥 ∨ℋ 𝐴 ) ∩ 𝐵 ) ⊆ ( 𝑥 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ) ) )
37 36 ad2antrr ⊢ ( ( ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) ∧ ( 𝐶 ∈ Cℋ ∧ 𝐷 ∈ Cℋ ) ) ∧ ( ( 𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐵 ) ∧ ( 𝐴 ∩ 𝐵 ) = 0ℋ ) ) → ( 𝐴 𝑀ℋ 𝐵 ↔ ∀ 𝑥 ∈ Cℋ ( 𝑥 ⊆ 𝐵 → ( ( 𝑥 ∨ℋ 𝐴 ) ∩ 𝐵 ) ⊆ ( 𝑥 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ) ) )
38 mdbr2 ⊢ ( ( 𝐶 ∈ Cℋ ∧ 𝐷 ∈ Cℋ ) → ( 𝐶 𝑀ℋ 𝐷 ↔ ∀ 𝑥 ∈ Cℋ ( 𝑥 ⊆ 𝐷 → ( ( 𝑥 ∨ℋ 𝐶 ) ∩ 𝐷 ) ⊆ ( 𝑥 ∨ℋ ( 𝐶 ∩ 𝐷 ) ) ) ) )
39 38 ad2antlr ⊢ ( ( ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) ∧ ( 𝐶 ∈ Cℋ ∧ 𝐷 ∈ Cℋ ) ) ∧ ( ( 𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐵 ) ∧ ( 𝐴 ∩ 𝐵 ) = 0ℋ ) ) → ( 𝐶 𝑀ℋ 𝐷 ↔ ∀ 𝑥 ∈ Cℋ ( 𝑥 ⊆ 𝐷 → ( ( 𝑥 ∨ℋ 𝐶 ) ∩ 𝐷 ) ⊆ ( 𝑥 ∨ℋ ( 𝐶 ∩ 𝐷 ) ) ) ) )
40 35 37 39 3imtr4d ⊢ ( ( ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) ∧ ( 𝐶 ∈ Cℋ ∧ 𝐷 ∈ Cℋ ) ) ∧ ( ( 𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐵 ) ∧ ( 𝐴 ∩ 𝐵 ) = 0ℋ ) ) → ( 𝐴 𝑀ℋ 𝐵 → 𝐶 𝑀ℋ 𝐷 ) )
41 40 expimpd ⊢ ( ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) ∧ ( 𝐶 ∈ Cℋ ∧ 𝐷 ∈ Cℋ ) ) → ( ( ( ( 𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐵 ) ∧ ( 𝐴 ∩ 𝐵 ) = 0ℋ ) ∧ 𝐴 𝑀ℋ 𝐵 ) → 𝐶 𝑀ℋ 𝐷 ) )