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

Metamath Proof Explorer

Theorem mdexchi

Description: An exchange lemma for modular pairs. Lemma 1.6 of MaedaMaeda p. 2. (Contributed by NM, 22-Jun-2004) (New usage is discouraged.)

Ref Expression
Hypotheses mdexch.1 ⊢ 𝐴 ∈ Cℋ
mdexch.2 ⊢ 𝐵 ∈ Cℋ
mdexch.3 ⊢ 𝐶 ∈ Cℋ
Assertion mdexchi ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐶 𝑀ℋ ( 𝐴 ∨ℋ 𝐵 ) ∧ ( 𝐶 ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ 𝐴 ) → ( ( 𝐶 ∨ℋ 𝐴 ) 𝑀ℋ 𝐵 ∧ ( ( 𝐶 ∨ℋ 𝐴 ) ∩ 𝐵 ) = ( 𝐴 ∩ 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 mdexch.1 ⊢ 𝐴 ∈ Cℋ
2 mdexch.2 ⊢ 𝐵 ∈ Cℋ
3 mdexch.3 ⊢ 𝐶 ∈ Cℋ
4 chjass ⊢ ( ( 𝐶 ∈ Cℋ ∧ 𝐴 ∈ Cℋ ∧ 𝑥 ∈ Cℋ ) → ( ( 𝐶 ∨ℋ 𝐴 ) ∨ℋ 𝑥 ) = ( 𝐶 ∨ℋ ( 𝐴 ∨ℋ 𝑥 ) ) )
5 3 1 4 mp3an12 ⊢ ( 𝑥 ∈ Cℋ → ( ( 𝐶 ∨ℋ 𝐴 ) ∨ℋ 𝑥 ) = ( 𝐶 ∨ℋ ( 𝐴 ∨ℋ 𝑥 ) ) )
6 3 1 chjcli ⊢ ( 𝐶 ∨ℋ 𝐴 ) ∈ Cℋ
7 chjcom ⊢ ( ( 𝑥 ∈ Cℋ ∧ ( 𝐶 ∨ℋ 𝐴 ) ∈ Cℋ ) → ( 𝑥 ∨ℋ ( 𝐶 ∨ℋ 𝐴 ) ) = ( ( 𝐶 ∨ℋ 𝐴 ) ∨ℋ 𝑥 ) )
8 6 7 mpan2 ⊢ ( 𝑥 ∈ Cℋ → ( 𝑥 ∨ℋ ( 𝐶 ∨ℋ 𝐴 ) ) = ( ( 𝐶 ∨ℋ 𝐴 ) ∨ℋ 𝑥 ) )
9 chjcl ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝑥 ∈ Cℋ ) → ( 𝐴 ∨ℋ 𝑥 ) ∈ Cℋ )
10 1 9 mpan ⊢ ( 𝑥 ∈ Cℋ → ( 𝐴 ∨ℋ 𝑥 ) ∈ Cℋ )
11 chjcom ⊢ ( ( ( 𝐴 ∨ℋ 𝑥 ) ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) → ( ( 𝐴 ∨ℋ 𝑥 ) ∨ℋ 𝐶 ) = ( 𝐶 ∨ℋ ( 𝐴 ∨ℋ 𝑥 ) ) )
12 10 3 11 sylancl ⊢ ( 𝑥 ∈ Cℋ → ( ( 𝐴 ∨ℋ 𝑥 ) ∨ℋ 𝐶 ) = ( 𝐶 ∨ℋ ( 𝐴 ∨ℋ 𝑥 ) ) )
13 5 8 12 3eqtr4d ⊢ ( 𝑥 ∈ Cℋ → ( 𝑥 ∨ℋ ( 𝐶 ∨ℋ 𝐴 ) ) = ( ( 𝐴 ∨ℋ 𝑥 ) ∨ℋ 𝐶 ) )
14 13 ineq1d ⊢ ( 𝑥 ∈ Cℋ → ( ( 𝑥 ∨ℋ ( 𝐶 ∨ℋ 𝐴 ) ) ∩ 𝐵 ) = ( ( ( 𝐴 ∨ℋ 𝑥 ) ∨ℋ 𝐶 ) ∩ 𝐵 ) )
15 inass ⊢ ( ( ( ( 𝐴 ∨ℋ 𝑥 ) ∨ℋ 𝐶 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ∩ 𝐵 ) = ( ( ( 𝐴 ∨ℋ 𝑥 ) ∨ℋ 𝐶 ) ∩ ( ( 𝐴 ∨ℋ 𝐵 ) ∩ 𝐵 ) )
16 incom ⊢ ( ( 𝐴 ∨ℋ 𝐵 ) ∩ 𝐵 ) = ( 𝐵 ∩ ( 𝐴 ∨ℋ 𝐵 ) )
17 1 2 chjcomi ⊢ ( 𝐴 ∨ℋ 𝐵 ) = ( 𝐵 ∨ℋ 𝐴 )
18 17 ineq2i ⊢ ( 𝐵 ∩ ( 𝐴 ∨ℋ 𝐵 ) ) = ( 𝐵 ∩ ( 𝐵 ∨ℋ 𝐴 ) )
19 2 1 chabs2i ⊢ ( 𝐵 ∩ ( 𝐵 ∨ℋ 𝐴 ) ) = 𝐵
20 18 19 eqtri ⊢ ( 𝐵 ∩ ( 𝐴 ∨ℋ 𝐵 ) ) = 𝐵
21 16 20 eqtri ⊢ ( ( 𝐴 ∨ℋ 𝐵 ) ∩ 𝐵 ) = 𝐵
22 21 ineq2i ⊢ ( ( ( 𝐴 ∨ℋ 𝑥 ) ∨ℋ 𝐶 ) ∩ ( ( 𝐴 ∨ℋ 𝐵 ) ∩ 𝐵 ) ) = ( ( ( 𝐴 ∨ℋ 𝑥 ) ∨ℋ 𝐶 ) ∩ 𝐵 )
23 15 22 eqtri ⊢ ( ( ( ( 𝐴 ∨ℋ 𝑥 ) ∨ℋ 𝐶 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ∩ 𝐵 ) = ( ( ( 𝐴 ∨ℋ 𝑥 ) ∨ℋ 𝐶 ) ∩ 𝐵 )
24 14 23 eqtr4di ⊢ ( 𝑥 ∈ Cℋ → ( ( 𝑥 ∨ℋ ( 𝐶 ∨ℋ 𝐴 ) ) ∩ 𝐵 ) = ( ( ( ( 𝐴 ∨ℋ 𝑥 ) ∨ℋ 𝐶 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ∩ 𝐵 ) )
25 24 ad2antrr ⊢ ( ( ( 𝑥 ∈ Cℋ ∧ 𝑥 ⊆ 𝐵 ) ∧ ( 𝐶 𝑀ℋ ( 𝐴 ∨ℋ 𝐵 ) ∧ ( 𝐶 ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ 𝐴 ) ) → ( ( 𝑥 ∨ℋ ( 𝐶 ∨ℋ 𝐴 ) ) ∩ 𝐵 ) = ( ( ( ( 𝐴 ∨ℋ 𝑥 ) ∨ℋ 𝐶 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ∩ 𝐵 ) )
26 chlej2 ⊢ ( ( ( 𝑥 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐴 ∈ Cℋ ) ∧ 𝑥 ⊆ 𝐵 ) → ( 𝐴 ∨ℋ 𝑥 ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) )
27 26 ex ⊢ ( ( 𝑥 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐴 ∈ Cℋ ) → ( 𝑥 ⊆ 𝐵 → ( 𝐴 ∨ℋ 𝑥 ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) )
28 2 1 27 mp3an23 ⊢ ( 𝑥 ∈ Cℋ → ( 𝑥 ⊆ 𝐵 → ( 𝐴 ∨ℋ 𝑥 ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) )
29 1 2 chjcli ⊢ ( 𝐴 ∨ℋ 𝐵 ) ∈ Cℋ
30 mdi ⊢ ( ( ( 𝐶 ∈ Cℋ ∧ ( 𝐴 ∨ℋ 𝐵 ) ∈ Cℋ ∧ ( 𝐴 ∨ℋ 𝑥 ) ∈ Cℋ ) ∧ ( 𝐶 𝑀ℋ ( 𝐴 ∨ℋ 𝐵 ) ∧ ( 𝐴 ∨ℋ 𝑥 ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) → ( ( ( 𝐴 ∨ℋ 𝑥 ) ∨ℋ 𝐶 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) = ( ( 𝐴 ∨ℋ 𝑥 ) ∨ℋ ( 𝐶 ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ) )
31 30 exp32 ⊢ ( ( 𝐶 ∈ Cℋ ∧ ( 𝐴 ∨ℋ 𝐵 ) ∈ Cℋ ∧ ( 𝐴 ∨ℋ 𝑥 ) ∈ Cℋ ) → ( 𝐶 𝑀ℋ ( 𝐴 ∨ℋ 𝐵 ) → ( ( 𝐴 ∨ℋ 𝑥 ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) → ( ( ( 𝐴 ∨ℋ 𝑥 ) ∨ℋ 𝐶 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) = ( ( 𝐴 ∨ℋ 𝑥 ) ∨ℋ ( 𝐶 ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ) ) ) )
32 3 29 31 mp3an12 ⊢ ( ( 𝐴 ∨ℋ 𝑥 ) ∈ Cℋ → ( 𝐶 𝑀ℋ ( 𝐴 ∨ℋ 𝐵 ) → ( ( 𝐴 ∨ℋ 𝑥 ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) → ( ( ( 𝐴 ∨ℋ 𝑥 ) ∨ℋ 𝐶 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) = ( ( 𝐴 ∨ℋ 𝑥 ) ∨ℋ ( 𝐶 ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ) ) ) )
33 10 32 syl ⊢ ( 𝑥 ∈ Cℋ → ( 𝐶 𝑀ℋ ( 𝐴 ∨ℋ 𝐵 ) → ( ( 𝐴 ∨ℋ 𝑥 ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) → ( ( ( 𝐴 ∨ℋ 𝑥 ) ∨ℋ 𝐶 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) = ( ( 𝐴 ∨ℋ 𝑥 ) ∨ℋ ( 𝐶 ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ) ) ) )
34 33 com23 ⊢ ( 𝑥 ∈ Cℋ → ( ( 𝐴 ∨ℋ 𝑥 ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) → ( 𝐶 𝑀ℋ ( 𝐴 ∨ℋ 𝐵 ) → ( ( ( 𝐴 ∨ℋ 𝑥 ) ∨ℋ 𝐶 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) = ( ( 𝐴 ∨ℋ 𝑥 ) ∨ℋ ( 𝐶 ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ) ) ) )
35 28 34 syld ⊢ ( 𝑥 ∈ Cℋ → ( 𝑥 ⊆ 𝐵 → ( 𝐶 𝑀ℋ ( 𝐴 ∨ℋ 𝐵 ) → ( ( ( 𝐴 ∨ℋ 𝑥 ) ∨ℋ 𝐶 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) = ( ( 𝐴 ∨ℋ 𝑥 ) ∨ℋ ( 𝐶 ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ) ) ) )
36 35 imp31 ⊢ ( ( ( 𝑥 ∈ Cℋ ∧ 𝑥 ⊆ 𝐵 ) ∧ 𝐶 𝑀ℋ ( 𝐴 ∨ℋ 𝐵 ) ) → ( ( ( 𝐴 ∨ℋ 𝑥 ) ∨ℋ 𝐶 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) = ( ( 𝐴 ∨ℋ 𝑥 ) ∨ℋ ( 𝐶 ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ) )
37 36 adantrr ⊢ ( ( ( 𝑥 ∈ Cℋ ∧ 𝑥 ⊆ 𝐵 ) ∧ ( 𝐶 𝑀ℋ ( 𝐴 ∨ℋ 𝐵 ) ∧ ( 𝐶 ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ 𝐴 ) ) → ( ( ( 𝐴 ∨ℋ 𝑥 ) ∨ℋ 𝐶 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) = ( ( 𝐴 ∨ℋ 𝑥 ) ∨ℋ ( 𝐶 ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ) )
38 3 29 chincli ⊢ ( 𝐶 ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ∈ Cℋ
39 chlej2 ⊢ ( ( ( ( 𝐶 ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ∈ Cℋ ∧ 𝐴 ∈ Cℋ ∧ ( 𝐴 ∨ℋ 𝑥 ) ∈ Cℋ ) ∧ ( 𝐶 ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ 𝐴 ) → ( ( 𝐴 ∨ℋ 𝑥 ) ∨ℋ ( 𝐶 ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ) ⊆ ( ( 𝐴 ∨ℋ 𝑥 ) ∨ℋ 𝐴 ) )
40 39 ex ⊢ ( ( ( 𝐶 ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ∈ Cℋ ∧ 𝐴 ∈ Cℋ ∧ ( 𝐴 ∨ℋ 𝑥 ) ∈ Cℋ ) → ( ( 𝐶 ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ 𝐴 → ( ( 𝐴 ∨ℋ 𝑥 ) ∨ℋ ( 𝐶 ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ) ⊆ ( ( 𝐴 ∨ℋ 𝑥 ) ∨ℋ 𝐴 ) ) )
41 38 1 40 mp3an12 ⊢ ( ( 𝐴 ∨ℋ 𝑥 ) ∈ Cℋ → ( ( 𝐶 ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ 𝐴 → ( ( 𝐴 ∨ℋ 𝑥 ) ∨ℋ ( 𝐶 ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ) ⊆ ( ( 𝐴 ∨ℋ 𝑥 ) ∨ℋ 𝐴 ) ) )
42 10 41 syl ⊢ ( 𝑥 ∈ Cℋ → ( ( 𝐶 ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ 𝐴 → ( ( 𝐴 ∨ℋ 𝑥 ) ∨ℋ ( 𝐶 ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ) ⊆ ( ( 𝐴 ∨ℋ 𝑥 ) ∨ℋ 𝐴 ) ) )
43 42 imp ⊢ ( ( 𝑥 ∈ Cℋ ∧ ( 𝐶 ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ 𝐴 ) → ( ( 𝐴 ∨ℋ 𝑥 ) ∨ℋ ( 𝐶 ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ) ⊆ ( ( 𝐴 ∨ℋ 𝑥 ) ∨ℋ 𝐴 ) )
44 chjcom ⊢ ( ( ( 𝐴 ∨ℋ 𝑥 ) ∈ Cℋ ∧ 𝐴 ∈ Cℋ ) → ( ( 𝐴 ∨ℋ 𝑥 ) ∨ℋ 𝐴 ) = ( 𝐴 ∨ℋ ( 𝐴 ∨ℋ 𝑥 ) ) )
45 10 1 44 sylancl ⊢ ( 𝑥 ∈ Cℋ → ( ( 𝐴 ∨ℋ 𝑥 ) ∨ℋ 𝐴 ) = ( 𝐴 ∨ℋ ( 𝐴 ∨ℋ 𝑥 ) ) )
46 1 chjidmi ⊢ ( 𝐴 ∨ℋ 𝐴 ) = 𝐴
47 46 oveq1i ⊢ ( ( 𝐴 ∨ℋ 𝐴 ) ∨ℋ 𝑥 ) = ( 𝐴 ∨ℋ 𝑥 )
48 chjass ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐴 ∈ Cℋ ∧ 𝑥 ∈ Cℋ ) → ( ( 𝐴 ∨ℋ 𝐴 ) ∨ℋ 𝑥 ) = ( 𝐴 ∨ℋ ( 𝐴 ∨ℋ 𝑥 ) ) )
49 1 1 48 mp3an12 ⊢ ( 𝑥 ∈ Cℋ → ( ( 𝐴 ∨ℋ 𝐴 ) ∨ℋ 𝑥 ) = ( 𝐴 ∨ℋ ( 𝐴 ∨ℋ 𝑥 ) ) )
50 chjcom ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝑥 ∈ Cℋ ) → ( 𝐴 ∨ℋ 𝑥 ) = ( 𝑥 ∨ℋ 𝐴 ) )
51 1 50 mpan ⊢ ( 𝑥 ∈ Cℋ → ( 𝐴 ∨ℋ 𝑥 ) = ( 𝑥 ∨ℋ 𝐴 ) )
52 47 49 51 3eqtr3a ⊢ ( 𝑥 ∈ Cℋ → ( 𝐴 ∨ℋ ( 𝐴 ∨ℋ 𝑥 ) ) = ( 𝑥 ∨ℋ 𝐴 ) )
53 45 52 eqtrd ⊢ ( 𝑥 ∈ Cℋ → ( ( 𝐴 ∨ℋ 𝑥 ) ∨ℋ 𝐴 ) = ( 𝑥 ∨ℋ 𝐴 ) )
54 53 adantr ⊢ ( ( 𝑥 ∈ Cℋ ∧ ( 𝐶 ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ 𝐴 ) → ( ( 𝐴 ∨ℋ 𝑥 ) ∨ℋ 𝐴 ) = ( 𝑥 ∨ℋ 𝐴 ) )
55 43 54 sseqtrd ⊢ ( ( 𝑥 ∈ Cℋ ∧ ( 𝐶 ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ 𝐴 ) → ( ( 𝐴 ∨ℋ 𝑥 ) ∨ℋ ( 𝐶 ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ) ⊆ ( 𝑥 ∨ℋ 𝐴 ) )
56 55 ad2ant2rl ⊢ ( ( ( 𝑥 ∈ Cℋ ∧ 𝑥 ⊆ 𝐵 ) ∧ ( 𝐶 𝑀ℋ ( 𝐴 ∨ℋ 𝐵 ) ∧ ( 𝐶 ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ 𝐴 ) ) → ( ( 𝐴 ∨ℋ 𝑥 ) ∨ℋ ( 𝐶 ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ) ⊆ ( 𝑥 ∨ℋ 𝐴 ) )
57 37 56 eqsstrd ⊢ ( ( ( 𝑥 ∈ Cℋ ∧ 𝑥 ⊆ 𝐵 ) ∧ ( 𝐶 𝑀ℋ ( 𝐴 ∨ℋ 𝐵 ) ∧ ( 𝐶 ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ 𝐴 ) ) → ( ( ( 𝐴 ∨ℋ 𝑥 ) ∨ℋ 𝐶 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ ( 𝑥 ∨ℋ 𝐴 ) )
58 57 ssrind ⊢ ( ( ( 𝑥 ∈ Cℋ ∧ 𝑥 ⊆ 𝐵 ) ∧ ( 𝐶 𝑀ℋ ( 𝐴 ∨ℋ 𝐵 ) ∧ ( 𝐶 ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ 𝐴 ) ) → ( ( ( ( 𝐴 ∨ℋ 𝑥 ) ∨ℋ 𝐶 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ∩ 𝐵 ) ⊆ ( ( 𝑥 ∨ℋ 𝐴 ) ∩ 𝐵 ) )
59 25 58 eqsstrd ⊢ ( ( ( 𝑥 ∈ Cℋ ∧ 𝑥 ⊆ 𝐵 ) ∧ ( 𝐶 𝑀ℋ ( 𝐴 ∨ℋ 𝐵 ) ∧ ( 𝐶 ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ 𝐴 ) ) → ( ( 𝑥 ∨ℋ ( 𝐶 ∨ℋ 𝐴 ) ) ∩ 𝐵 ) ⊆ ( ( 𝑥 ∨ℋ 𝐴 ) ∩ 𝐵 ) )
60 59 adantrl ⊢ ( ( ( 𝑥 ∈ Cℋ ∧ 𝑥 ⊆ 𝐵 ) ∧ ( 𝐴 𝑀ℋ 𝐵 ∧ ( 𝐶 𝑀ℋ ( 𝐴 ∨ℋ 𝐵 ) ∧ ( 𝐶 ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ 𝐴 ) ) ) → ( ( 𝑥 ∨ℋ ( 𝐶 ∨ℋ 𝐴 ) ) ∩ 𝐵 ) ⊆ ( ( 𝑥 ∨ℋ 𝐴 ) ∩ 𝐵 ) )
61 mdi ⊢ ( ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝑥 ∈ Cℋ ) ∧ ( 𝐴 𝑀ℋ 𝐵 ∧ 𝑥 ⊆ 𝐵 ) ) → ( ( 𝑥 ∨ℋ 𝐴 ) ∩ 𝐵 ) = ( 𝑥 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) )
62 61 exp32 ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝑥 ∈ Cℋ ) → ( 𝐴 𝑀ℋ 𝐵 → ( 𝑥 ⊆ 𝐵 → ( ( 𝑥 ∨ℋ 𝐴 ) ∩ 𝐵 ) = ( 𝑥 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ) ) )
63 1 2 62 mp3an12 ⊢ ( 𝑥 ∈ Cℋ → ( 𝐴 𝑀ℋ 𝐵 → ( 𝑥 ⊆ 𝐵 → ( ( 𝑥 ∨ℋ 𝐴 ) ∩ 𝐵 ) = ( 𝑥 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ) ) )
64 63 com23 ⊢ ( 𝑥 ∈ Cℋ → ( 𝑥 ⊆ 𝐵 → ( 𝐴 𝑀ℋ 𝐵 → ( ( 𝑥 ∨ℋ 𝐴 ) ∩ 𝐵 ) = ( 𝑥 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ) ) )
65 64 imp31 ⊢ ( ( ( 𝑥 ∈ Cℋ ∧ 𝑥 ⊆ 𝐵 ) ∧ 𝐴 𝑀ℋ 𝐵 ) → ( ( 𝑥 ∨ℋ 𝐴 ) ∩ 𝐵 ) = ( 𝑥 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) )
66 1 3 chub2i ⊢ 𝐴 ⊆ ( 𝐶 ∨ℋ 𝐴 )
67 ssrin ⊢ ( 𝐴 ⊆ ( 𝐶 ∨ℋ 𝐴 ) → ( 𝐴 ∩ 𝐵 ) ⊆ ( ( 𝐶 ∨ℋ 𝐴 ) ∩ 𝐵 ) )
68 66 67 ax-mp ⊢ ( 𝐴 ∩ 𝐵 ) ⊆ ( ( 𝐶 ∨ℋ 𝐴 ) ∩ 𝐵 )
69 1 2 chincli ⊢ ( 𝐴 ∩ 𝐵 ) ∈ Cℋ
70 6 2 chincli ⊢ ( ( 𝐶 ∨ℋ 𝐴 ) ∩ 𝐵 ) ∈ Cℋ
71 chlej2 ⊢ ( ( ( ( 𝐴 ∩ 𝐵 ) ∈ Cℋ ∧ ( ( 𝐶 ∨ℋ 𝐴 ) ∩ 𝐵 ) ∈ Cℋ ∧ 𝑥 ∈ Cℋ ) ∧ ( 𝐴 ∩ 𝐵 ) ⊆ ( ( 𝐶 ∨ℋ 𝐴 ) ∩ 𝐵 ) ) → ( 𝑥 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ⊆ ( 𝑥 ∨ℋ ( ( 𝐶 ∨ℋ 𝐴 ) ∩ 𝐵 ) ) )
72 71 ex ⊢ ( ( ( 𝐴 ∩ 𝐵 ) ∈ Cℋ ∧ ( ( 𝐶 ∨ℋ 𝐴 ) ∩ 𝐵 ) ∈ Cℋ ∧ 𝑥 ∈ Cℋ ) → ( ( 𝐴 ∩ 𝐵 ) ⊆ ( ( 𝐶 ∨ℋ 𝐴 ) ∩ 𝐵 ) → ( 𝑥 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ⊆ ( 𝑥 ∨ℋ ( ( 𝐶 ∨ℋ 𝐴 ) ∩ 𝐵 ) ) ) )
73 69 70 72 mp3an12 ⊢ ( 𝑥 ∈ Cℋ → ( ( 𝐴 ∩ 𝐵 ) ⊆ ( ( 𝐶 ∨ℋ 𝐴 ) ∩ 𝐵 ) → ( 𝑥 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ⊆ ( 𝑥 ∨ℋ ( ( 𝐶 ∨ℋ 𝐴 ) ∩ 𝐵 ) ) ) )
74 68 73 mpi ⊢ ( 𝑥 ∈ Cℋ → ( 𝑥 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ⊆ ( 𝑥 ∨ℋ ( ( 𝐶 ∨ℋ 𝐴 ) ∩ 𝐵 ) ) )
75 74 ad2antrr ⊢ ( ( ( 𝑥 ∈ Cℋ ∧ 𝑥 ⊆ 𝐵 ) ∧ 𝐴 𝑀ℋ 𝐵 ) → ( 𝑥 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ⊆ ( 𝑥 ∨ℋ ( ( 𝐶 ∨ℋ 𝐴 ) ∩ 𝐵 ) ) )
76 65 75 eqsstrd ⊢ ( ( ( 𝑥 ∈ Cℋ ∧ 𝑥 ⊆ 𝐵 ) ∧ 𝐴 𝑀ℋ 𝐵 ) → ( ( 𝑥 ∨ℋ 𝐴 ) ∩ 𝐵 ) ⊆ ( 𝑥 ∨ℋ ( ( 𝐶 ∨ℋ 𝐴 ) ∩ 𝐵 ) ) )
77 76 adantrr ⊢ ( ( ( 𝑥 ∈ Cℋ ∧ 𝑥 ⊆ 𝐵 ) ∧ ( 𝐴 𝑀ℋ 𝐵 ∧ ( 𝐶 𝑀ℋ ( 𝐴 ∨ℋ 𝐵 ) ∧ ( 𝐶 ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ 𝐴 ) ) ) → ( ( 𝑥 ∨ℋ 𝐴 ) ∩ 𝐵 ) ⊆ ( 𝑥 ∨ℋ ( ( 𝐶 ∨ℋ 𝐴 ) ∩ 𝐵 ) ) )
78 60 77 sstrd ⊢ ( ( ( 𝑥 ∈ Cℋ ∧ 𝑥 ⊆ 𝐵 ) ∧ ( 𝐴 𝑀ℋ 𝐵 ∧ ( 𝐶 𝑀ℋ ( 𝐴 ∨ℋ 𝐵 ) ∧ ( 𝐶 ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ 𝐴 ) ) ) → ( ( 𝑥 ∨ℋ ( 𝐶 ∨ℋ 𝐴 ) ) ∩ 𝐵 ) ⊆ ( 𝑥 ∨ℋ ( ( 𝐶 ∨ℋ 𝐴 ) ∩ 𝐵 ) ) )
79 78 exp31 ⊢ ( 𝑥 ∈ Cℋ → ( 𝑥 ⊆ 𝐵 → ( ( 𝐴 𝑀ℋ 𝐵 ∧ ( 𝐶 𝑀ℋ ( 𝐴 ∨ℋ 𝐵 ) ∧ ( 𝐶 ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ 𝐴 ) ) → ( ( 𝑥 ∨ℋ ( 𝐶 ∨ℋ 𝐴 ) ) ∩ 𝐵 ) ⊆ ( 𝑥 ∨ℋ ( ( 𝐶 ∨ℋ 𝐴 ) ∩ 𝐵 ) ) ) ) )
80 79 com3r ⊢ ( ( 𝐴 𝑀ℋ 𝐵 ∧ ( 𝐶 𝑀ℋ ( 𝐴 ∨ℋ 𝐵 ) ∧ ( 𝐶 ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ 𝐴 ) ) → ( 𝑥 ∈ Cℋ → ( 𝑥 ⊆ 𝐵 → ( ( 𝑥 ∨ℋ ( 𝐶 ∨ℋ 𝐴 ) ) ∩ 𝐵 ) ⊆ ( 𝑥 ∨ℋ ( ( 𝐶 ∨ℋ 𝐴 ) ∩ 𝐵 ) ) ) ) )
81 80 3impb ⊢ ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐶 𝑀ℋ ( 𝐴 ∨ℋ 𝐵 ) ∧ ( 𝐶 ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ 𝐴 ) → ( 𝑥 ∈ Cℋ → ( 𝑥 ⊆ 𝐵 → ( ( 𝑥 ∨ℋ ( 𝐶 ∨ℋ 𝐴 ) ) ∩ 𝐵 ) ⊆ ( 𝑥 ∨ℋ ( ( 𝐶 ∨ℋ 𝐴 ) ∩ 𝐵 ) ) ) ) )
82 81 ralrimiv ⊢ ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐶 𝑀ℋ ( 𝐴 ∨ℋ 𝐵 ) ∧ ( 𝐶 ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ 𝐴 ) → ∀ 𝑥 ∈ Cℋ ( 𝑥 ⊆ 𝐵 → ( ( 𝑥 ∨ℋ ( 𝐶 ∨ℋ 𝐴 ) ) ∩ 𝐵 ) ⊆ ( 𝑥 ∨ℋ ( ( 𝐶 ∨ℋ 𝐴 ) ∩ 𝐵 ) ) ) )
83 mdbr2 ⊢ ( ( ( 𝐶 ∨ℋ 𝐴 ) ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( ( 𝐶 ∨ℋ 𝐴 ) 𝑀ℋ 𝐵 ↔ ∀ 𝑥 ∈ Cℋ ( 𝑥 ⊆ 𝐵 → ( ( 𝑥 ∨ℋ ( 𝐶 ∨ℋ 𝐴 ) ) ∩ 𝐵 ) ⊆ ( 𝑥 ∨ℋ ( ( 𝐶 ∨ℋ 𝐴 ) ∩ 𝐵 ) ) ) ) )
84 6 2 83 mp2an ⊢ ( ( 𝐶 ∨ℋ 𝐴 ) 𝑀ℋ 𝐵 ↔ ∀ 𝑥 ∈ Cℋ ( 𝑥 ⊆ 𝐵 → ( ( 𝑥 ∨ℋ ( 𝐶 ∨ℋ 𝐴 ) ) ∩ 𝐵 ) ⊆ ( 𝑥 ∨ℋ ( ( 𝐶 ∨ℋ 𝐴 ) ∩ 𝐵 ) ) ) )
85 82 84 sylibr ⊢ ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐶 𝑀ℋ ( 𝐴 ∨ℋ 𝐵 ) ∧ ( 𝐶 ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ 𝐴 ) → ( 𝐶 ∨ℋ 𝐴 ) 𝑀ℋ 𝐵 )
86 3 1 chjcomi ⊢ ( 𝐶 ∨ℋ 𝐴 ) = ( 𝐴 ∨ℋ 𝐶 )
87 incom ⊢ ( 𝐵 ∩ ( 𝐴 ∨ℋ 𝐵 ) ) = ( ( 𝐴 ∨ℋ 𝐵 ) ∩ 𝐵 )
88 18 87 19 3eqtr3ri ⊢ 𝐵 = ( ( 𝐴 ∨ℋ 𝐵 ) ∩ 𝐵 )
89 86 88 ineq12i ⊢ ( ( 𝐶 ∨ℋ 𝐴 ) ∩ 𝐵 ) = ( ( 𝐴 ∨ℋ 𝐶 ) ∩ ( ( 𝐴 ∨ℋ 𝐵 ) ∩ 𝐵 ) )
90 inass ⊢ ( ( ( 𝐴 ∨ℋ 𝐶 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ∩ 𝐵 ) = ( ( 𝐴 ∨ℋ 𝐶 ) ∩ ( ( 𝐴 ∨ℋ 𝐵 ) ∩ 𝐵 ) )
91 1 2 chub1i ⊢ 𝐴 ⊆ ( 𝐴 ∨ℋ 𝐵 )
92 mdi ⊢ ( ( ( 𝐶 ∈ Cℋ ∧ ( 𝐴 ∨ℋ 𝐵 ) ∈ Cℋ ∧ 𝐴 ∈ Cℋ ) ∧ ( 𝐶 𝑀ℋ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐴 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) → ( ( 𝐴 ∨ℋ 𝐶 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) = ( 𝐴 ∨ℋ ( 𝐶 ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ) )
93 92 exp32 ⊢ ( ( 𝐶 ∈ Cℋ ∧ ( 𝐴 ∨ℋ 𝐵 ) ∈ Cℋ ∧ 𝐴 ∈ Cℋ ) → ( 𝐶 𝑀ℋ ( 𝐴 ∨ℋ 𝐵 ) → ( 𝐴 ⊆ ( 𝐴 ∨ℋ 𝐵 ) → ( ( 𝐴 ∨ℋ 𝐶 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) = ( 𝐴 ∨ℋ ( 𝐶 ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ) ) ) )
94 3 29 1 93 mp3an ⊢ ( 𝐶 𝑀ℋ ( 𝐴 ∨ℋ 𝐵 ) → ( 𝐴 ⊆ ( 𝐴 ∨ℋ 𝐵 ) → ( ( 𝐴 ∨ℋ 𝐶 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) = ( 𝐴 ∨ℋ ( 𝐶 ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ) ) )
95 91 94 mpi ⊢ ( 𝐶 𝑀ℋ ( 𝐴 ∨ℋ 𝐵 ) → ( ( 𝐴 ∨ℋ 𝐶 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) = ( 𝐴 ∨ℋ ( 𝐶 ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ) )
96 1 38 chjcomi ⊢ ( 𝐴 ∨ℋ ( 𝐶 ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ) = ( ( 𝐶 ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ∨ℋ 𝐴 )
97 38 1 chlejb1i ⊢ ( ( 𝐶 ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ 𝐴 ↔ ( ( 𝐶 ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ∨ℋ 𝐴 ) = 𝐴 )
98 97 biimpi ⊢ ( ( 𝐶 ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ 𝐴 → ( ( 𝐶 ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ∨ℋ 𝐴 ) = 𝐴 )
99 96 98 eqtrid ⊢ ( ( 𝐶 ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ 𝐴 → ( 𝐴 ∨ℋ ( 𝐶 ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ) = 𝐴 )
100 95 99 sylan9eq ⊢ ( ( 𝐶 𝑀ℋ ( 𝐴 ∨ℋ 𝐵 ) ∧ ( 𝐶 ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ 𝐴 ) → ( ( 𝐴 ∨ℋ 𝐶 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) = 𝐴 )
101 100 ineq1d ⊢ ( ( 𝐶 𝑀ℋ ( 𝐴 ∨ℋ 𝐵 ) ∧ ( 𝐶 ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ 𝐴 ) → ( ( ( 𝐴 ∨ℋ 𝐶 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ∩ 𝐵 ) = ( 𝐴 ∩ 𝐵 ) )
102 90 101 eqtr3id ⊢ ( ( 𝐶 𝑀ℋ ( 𝐴 ∨ℋ 𝐵 ) ∧ ( 𝐶 ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ 𝐴 ) → ( ( 𝐴 ∨ℋ 𝐶 ) ∩ ( ( 𝐴 ∨ℋ 𝐵 ) ∩ 𝐵 ) ) = ( 𝐴 ∩ 𝐵 ) )
103 89 102 eqtrid ⊢ ( ( 𝐶 𝑀ℋ ( 𝐴 ∨ℋ 𝐵 ) ∧ ( 𝐶 ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ 𝐴 ) → ( ( 𝐶 ∨ℋ 𝐴 ) ∩ 𝐵 ) = ( 𝐴 ∩ 𝐵 ) )
104 103 3adant1 ⊢ ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐶 𝑀ℋ ( 𝐴 ∨ℋ 𝐵 ) ∧ ( 𝐶 ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ 𝐴 ) → ( ( 𝐶 ∨ℋ 𝐴 ) ∩ 𝐵 ) = ( 𝐴 ∩ 𝐵 ) )
105 85 104 jca ⊢ ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐶 𝑀ℋ ( 𝐴 ∨ℋ 𝐵 ) ∧ ( 𝐶 ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ 𝐴 ) → ( ( 𝐶 ∨ℋ 𝐴 ) 𝑀ℋ 𝐵 ∧ ( ( 𝐶 ∨ℋ 𝐴 ) ∩ 𝐵 ) = ( 𝐴 ∩ 𝐵 ) ) )