Metamath Proof Explorer

Theorem sumdmdii

Description: If the subspace sum of two Hilbert lattice elements is closed, then the elements are a dual modular pair. Remark in MaedaMaeda p. 139. (Contributed by NM, 12-Jul-2004) (New usage is discouraged.)

Ref Expression
Hypotheses sumdmdi.1 ⊢ 𝐴 ∈ Cℋ
sumdmdi.2 ⊢ 𝐵 ∈ Cℋ
Assertion sumdmdii ( ( 𝐴 +ℋ 𝐵 ) = ( 𝐴 ∨ℋ 𝐵 ) → 𝐴 𝑀ℋ* 𝐵 )

Proof

Step Hyp Ref Expression
1 sumdmdi.1 ⊢ 𝐴 ∈ Cℋ
2 sumdmdi.2 ⊢ 𝐵 ∈ Cℋ
3 ineq2 ⊢ ( ( 𝐴 +ℋ 𝐵 ) = ( 𝐴 ∨ℋ 𝐵 ) → ( 𝑥 ∩ ( 𝐴 +ℋ 𝐵 ) ) = ( 𝑥 ∩ ( 𝐴 ∨ℋ 𝐵 ) ) )
4 3 adantr ⊢ ( ( ( 𝐴 +ℋ 𝐵 ) = ( 𝐴 ∨ℋ 𝐵 ) ∧ ( 𝑥 ∈ Cℋ ∧ 𝐵 ⊆ 𝑥 ) ) → ( 𝑥 ∩ ( 𝐴 +ℋ 𝐵 ) ) = ( 𝑥 ∩ ( 𝐴 ∨ℋ 𝐵 ) ) )
5 elin ⊢ ( 𝑦 ∈ ( 𝑥 ∩ ( 𝐴 +ℋ 𝐵 ) ) ↔ ( 𝑦 ∈ 𝑥 ∧ 𝑦 ∈ ( 𝐴 +ℋ 𝐵 ) ) )
6 1 2 chseli ⊢ ( 𝑦 ∈ ( 𝐴 +ℋ 𝐵 ) ↔ ∃ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝐵 𝑦 = ( 𝑧 +ℎ 𝑤 ) )
7 ssel2 ⊢ ( ( 𝐵 ⊆ 𝑥 ∧ 𝑤 ∈ 𝐵 ) → 𝑤 ∈ 𝑥 )
8 chsh ⊢ ( 𝑥 ∈ Cℋ → 𝑥 ∈ Sℋ )
9 shsubcl ⊢ ( ( 𝑥 ∈ Sℋ ∧ 𝑦 ∈ 𝑥 ∧ 𝑤 ∈ 𝑥 ) → ( 𝑦 −ℎ 𝑤 ) ∈ 𝑥 )
10 9 3exp ⊢ ( 𝑥 ∈ Sℋ → ( 𝑦 ∈ 𝑥 → ( 𝑤 ∈ 𝑥 → ( 𝑦 −ℎ 𝑤 ) ∈ 𝑥 ) ) )
11 8 10 syl ⊢ ( 𝑥 ∈ Cℋ → ( 𝑦 ∈ 𝑥 → ( 𝑤 ∈ 𝑥 → ( 𝑦 −ℎ 𝑤 ) ∈ 𝑥 ) ) )
12 7 11 syl7 ⊢ ( 𝑥 ∈ Cℋ → ( 𝑦 ∈ 𝑥 → ( ( 𝐵 ⊆ 𝑥 ∧ 𝑤 ∈ 𝐵 ) → ( 𝑦 −ℎ 𝑤 ) ∈ 𝑥 ) ) )
13 12 exp4a ⊢ ( 𝑥 ∈ Cℋ → ( 𝑦 ∈ 𝑥 → ( 𝐵 ⊆ 𝑥 → ( 𝑤 ∈ 𝐵 → ( 𝑦 −ℎ 𝑤 ) ∈ 𝑥 ) ) ) )
14 13 com23 ⊢ ( 𝑥 ∈ Cℋ → ( 𝐵 ⊆ 𝑥 → ( 𝑦 ∈ 𝑥 → ( 𝑤 ∈ 𝐵 → ( 𝑦 −ℎ 𝑤 ) ∈ 𝑥 ) ) ) )
15 14 imp41 ⊢ ( ( ( ( 𝑥 ∈ Cℋ ∧ 𝐵 ⊆ 𝑥 ) ∧ 𝑦 ∈ 𝑥 ) ∧ 𝑤 ∈ 𝐵 ) → ( 𝑦 −ℎ 𝑤 ) ∈ 𝑥 )
16 15 adantlr ⊢ ( ( ( ( ( 𝑥 ∈ Cℋ ∧ 𝐵 ⊆ 𝑥 ) ∧ 𝑦 ∈ 𝑥 ) ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑤 ∈ 𝐵 ) → ( 𝑦 −ℎ 𝑤 ) ∈ 𝑥 )
17 16 adantr ⊢ ( ( ( ( ( ( 𝑥 ∈ Cℋ ∧ 𝐵 ⊆ 𝑥 ) ∧ 𝑦 ∈ 𝑥 ) ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑤 ∈ 𝐵 ) ∧ 𝑦 = ( 𝑧 +ℎ 𝑤 ) ) → ( 𝑦 −ℎ 𝑤 ) ∈ 𝑥 )
18 chel ⊢ ( ( 𝑥 ∈ Cℋ ∧ 𝑦 ∈ 𝑥 ) → 𝑦 ∈ ℋ )
19 18 adantlr ⊢ ( ( ( 𝑥 ∈ Cℋ ∧ 𝐵 ⊆ 𝑥 ) ∧ 𝑦 ∈ 𝑥 ) → 𝑦 ∈ ℋ )
20 1 cheli ⊢ ( 𝑧 ∈ 𝐴 → 𝑧 ∈ ℋ )
21 2 cheli ⊢ ( 𝑤 ∈ 𝐵 → 𝑤 ∈ ℋ )
22 hvsubadd ⊢ ( ( 𝑦 ∈ ℋ ∧ 𝑤 ∈ ℋ ∧ 𝑧 ∈ ℋ ) → ( ( 𝑦 −ℎ 𝑤 ) = 𝑧 ↔ ( 𝑤 +ℎ 𝑧 ) = 𝑦 ) )
23 ax-hvcom ⊢ ( ( 𝑤 ∈ ℋ ∧ 𝑧 ∈ ℋ ) → ( 𝑤 +ℎ 𝑧 ) = ( 𝑧 +ℎ 𝑤 ) )
24 23 eqeq1d ⊢ ( ( 𝑤 ∈ ℋ ∧ 𝑧 ∈ ℋ ) → ( ( 𝑤 +ℎ 𝑧 ) = 𝑦 ↔ ( 𝑧 +ℎ 𝑤 ) = 𝑦 ) )
25 eqcom ⊢ ( ( 𝑧 +ℎ 𝑤 ) = 𝑦 ↔ 𝑦 = ( 𝑧 +ℎ 𝑤 ) )
26 24 25 bitrdi ⊢ ( ( 𝑤 ∈ ℋ ∧ 𝑧 ∈ ℋ ) → ( ( 𝑤 +ℎ 𝑧 ) = 𝑦 ↔ 𝑦 = ( 𝑧 +ℎ 𝑤 ) ) )
27 26 3adant1 ⊢ ( ( 𝑦 ∈ ℋ ∧ 𝑤 ∈ ℋ ∧ 𝑧 ∈ ℋ ) → ( ( 𝑤 +ℎ 𝑧 ) = 𝑦 ↔ 𝑦 = ( 𝑧 +ℎ 𝑤 ) ) )
28 22 27 bitrd ⊢ ( ( 𝑦 ∈ ℋ ∧ 𝑤 ∈ ℋ ∧ 𝑧 ∈ ℋ ) → ( ( 𝑦 −ℎ 𝑤 ) = 𝑧 ↔ 𝑦 = ( 𝑧 +ℎ 𝑤 ) ) )
29 28 3com23 ⊢ ( ( 𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ ∧ 𝑤 ∈ ℋ ) → ( ( 𝑦 −ℎ 𝑤 ) = 𝑧 ↔ 𝑦 = ( 𝑧 +ℎ 𝑤 ) ) )
30 19 20 21 29 syl3an ⊢ ( ( ( ( 𝑥 ∈ Cℋ ∧ 𝐵 ⊆ 𝑥 ) ∧ 𝑦 ∈ 𝑥 ) ∧ 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵 ) → ( ( 𝑦 −ℎ 𝑤 ) = 𝑧 ↔ 𝑦 = ( 𝑧 +ℎ 𝑤 ) ) )
31 30 3expa ⊢ ( ( ( ( ( 𝑥 ∈ Cℋ ∧ 𝐵 ⊆ 𝑥 ) ∧ 𝑦 ∈ 𝑥 ) ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑤 ∈ 𝐵 ) → ( ( 𝑦 −ℎ 𝑤 ) = 𝑧 ↔ 𝑦 = ( 𝑧 +ℎ 𝑤 ) ) )
32 eleq1 ⊢ ( ( 𝑦 −ℎ 𝑤 ) = 𝑧 → ( ( 𝑦 −ℎ 𝑤 ) ∈ 𝑥 ↔ 𝑧 ∈ 𝑥 ) )
33 31 32 syl6bir ⊢ ( ( ( ( ( 𝑥 ∈ Cℋ ∧ 𝐵 ⊆ 𝑥 ) ∧ 𝑦 ∈ 𝑥 ) ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑤 ∈ 𝐵 ) → ( 𝑦 = ( 𝑧 +ℎ 𝑤 ) → ( ( 𝑦 −ℎ 𝑤 ) ∈ 𝑥 ↔ 𝑧 ∈ 𝑥 ) ) )
34 33 imp ⊢ ( ( ( ( ( ( 𝑥 ∈ Cℋ ∧ 𝐵 ⊆ 𝑥 ) ∧ 𝑦 ∈ 𝑥 ) ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑤 ∈ 𝐵 ) ∧ 𝑦 = ( 𝑧 +ℎ 𝑤 ) ) → ( ( 𝑦 −ℎ 𝑤 ) ∈ 𝑥 ↔ 𝑧 ∈ 𝑥 ) )
35 17 34 mpbid ⊢ ( ( ( ( ( ( 𝑥 ∈ Cℋ ∧ 𝐵 ⊆ 𝑥 ) ∧ 𝑦 ∈ 𝑥 ) ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑤 ∈ 𝐵 ) ∧ 𝑦 = ( 𝑧 +ℎ 𝑤 ) ) → 𝑧 ∈ 𝑥 )
36 simpr ⊢ ( ( ( ( ( ( 𝑥 ∈ Cℋ ∧ 𝐵 ⊆ 𝑥 ) ∧ 𝑦 ∈ 𝑥 ) ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑤 ∈ 𝐵 ) ∧ 𝑦 = ( 𝑧 +ℎ 𝑤 ) ) → 𝑦 = ( 𝑧 +ℎ 𝑤 ) )
37 35 36 jca ⊢ ( ( ( ( ( ( 𝑥 ∈ Cℋ ∧ 𝐵 ⊆ 𝑥 ) ∧ 𝑦 ∈ 𝑥 ) ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑤 ∈ 𝐵 ) ∧ 𝑦 = ( 𝑧 +ℎ 𝑤 ) ) → ( 𝑧 ∈ 𝑥 ∧ 𝑦 = ( 𝑧 +ℎ 𝑤 ) ) )
38 37 exp31 ⊢ ( ( ( ( 𝑥 ∈ Cℋ ∧ 𝐵 ⊆ 𝑥 ) ∧ 𝑦 ∈ 𝑥 ) ∧ 𝑧 ∈ 𝐴 ) → ( 𝑤 ∈ 𝐵 → ( 𝑦 = ( 𝑧 +ℎ 𝑤 ) → ( 𝑧 ∈ 𝑥 ∧ 𝑦 = ( 𝑧 +ℎ 𝑤 ) ) ) ) )
39 38 reximdvai ⊢ ( ( ( ( 𝑥 ∈ Cℋ ∧ 𝐵 ⊆ 𝑥 ) ∧ 𝑦 ∈ 𝑥 ) ∧ 𝑧 ∈ 𝐴 ) → ( ∃ 𝑤 ∈ 𝐵 𝑦 = ( 𝑧 +ℎ 𝑤 ) → ∃ 𝑤 ∈ 𝐵 ( 𝑧 ∈ 𝑥 ∧ 𝑦 = ( 𝑧 +ℎ 𝑤 ) ) ) )
40 r19.42v ⊢ ( ∃ 𝑤 ∈ 𝐵 ( 𝑧 ∈ 𝑥 ∧ 𝑦 = ( 𝑧 +ℎ 𝑤 ) ) ↔ ( 𝑧 ∈ 𝑥 ∧ ∃ 𝑤 ∈ 𝐵 𝑦 = ( 𝑧 +ℎ 𝑤 ) ) )
41 39 40 syl6ib ⊢ ( ( ( ( 𝑥 ∈ Cℋ ∧ 𝐵 ⊆ 𝑥 ) ∧ 𝑦 ∈ 𝑥 ) ∧ 𝑧 ∈ 𝐴 ) → ( ∃ 𝑤 ∈ 𝐵 𝑦 = ( 𝑧 +ℎ 𝑤 ) → ( 𝑧 ∈ 𝑥 ∧ ∃ 𝑤 ∈ 𝐵 𝑦 = ( 𝑧 +ℎ 𝑤 ) ) ) )
42 41 reximdva ⊢ ( ( ( 𝑥 ∈ Cℋ ∧ 𝐵 ⊆ 𝑥 ) ∧ 𝑦 ∈ 𝑥 ) → ( ∃ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝐵 𝑦 = ( 𝑧 +ℎ 𝑤 ) → ∃ 𝑧 ∈ 𝐴 ( 𝑧 ∈ 𝑥 ∧ ∃ 𝑤 ∈ 𝐵 𝑦 = ( 𝑧 +ℎ 𝑤 ) ) ) )
43 elin ⊢ ( 𝑧 ∈ ( 𝑥 ∩ 𝐴 ) ↔ ( 𝑧 ∈ 𝑥 ∧ 𝑧 ∈ 𝐴 ) )
44 ancom ⊢ ( ( 𝑧 ∈ 𝑥 ∧ 𝑧 ∈ 𝐴 ) ↔ ( 𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝑥 ) )
45 43 44 bitri ⊢ ( 𝑧 ∈ ( 𝑥 ∩ 𝐴 ) ↔ ( 𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝑥 ) )
46 45 anbi1i ⊢ ( ( 𝑧 ∈ ( 𝑥 ∩ 𝐴 ) ∧ ∃ 𝑤 ∈ 𝐵 𝑦 = ( 𝑧 +ℎ 𝑤 ) ) ↔ ( ( 𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝑥 ) ∧ ∃ 𝑤 ∈ 𝐵 𝑦 = ( 𝑧 +ℎ 𝑤 ) ) )
47 anass ⊢ ( ( ( 𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝑥 ) ∧ ∃ 𝑤 ∈ 𝐵 𝑦 = ( 𝑧 +ℎ 𝑤 ) ) ↔ ( 𝑧 ∈ 𝐴 ∧ ( 𝑧 ∈ 𝑥 ∧ ∃ 𝑤 ∈ 𝐵 𝑦 = ( 𝑧 +ℎ 𝑤 ) ) ) )
48 46 47 bitri ⊢ ( ( 𝑧 ∈ ( 𝑥 ∩ 𝐴 ) ∧ ∃ 𝑤 ∈ 𝐵 𝑦 = ( 𝑧 +ℎ 𝑤 ) ) ↔ ( 𝑧 ∈ 𝐴 ∧ ( 𝑧 ∈ 𝑥 ∧ ∃ 𝑤 ∈ 𝐵 𝑦 = ( 𝑧 +ℎ 𝑤 ) ) ) )
49 48 rexbii2 ⊢ ( ∃ 𝑧 ∈ ( 𝑥 ∩ 𝐴 ) ∃ 𝑤 ∈ 𝐵 𝑦 = ( 𝑧 +ℎ 𝑤 ) ↔ ∃ 𝑧 ∈ 𝐴 ( 𝑧 ∈ 𝑥 ∧ ∃ 𝑤 ∈ 𝐵 𝑦 = ( 𝑧 +ℎ 𝑤 ) ) )
50 42 49 syl6ibr ⊢ ( ( ( 𝑥 ∈ Cℋ ∧ 𝐵 ⊆ 𝑥 ) ∧ 𝑦 ∈ 𝑥 ) → ( ∃ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝐵 𝑦 = ( 𝑧 +ℎ 𝑤 ) → ∃ 𝑧 ∈ ( 𝑥 ∩ 𝐴 ) ∃ 𝑤 ∈ 𝐵 𝑦 = ( 𝑧 +ℎ 𝑤 ) ) )
51 1 chshii ⊢ 𝐴 ∈ Sℋ
52 shincl ⊢ ( ( 𝑥 ∈ Sℋ ∧ 𝐴 ∈ Sℋ ) → ( 𝑥 ∩ 𝐴 ) ∈ Sℋ )
53 8 51 52 sylancl ⊢ ( 𝑥 ∈ Cℋ → ( 𝑥 ∩ 𝐴 ) ∈ Sℋ )
54 53 ad2antrr ⊢ ( ( ( 𝑥 ∈ Cℋ ∧ 𝐵 ⊆ 𝑥 ) ∧ 𝑦 ∈ 𝑥 ) → ( 𝑥 ∩ 𝐴 ) ∈ Sℋ )
55 2 chshii ⊢ 𝐵 ∈ Sℋ
56 shsel ⊢ ( ( ( 𝑥 ∩ 𝐴 ) ∈ Sℋ ∧ 𝐵 ∈ Sℋ ) → ( 𝑦 ∈ ( ( 𝑥 ∩ 𝐴 ) +ℋ 𝐵 ) ↔ ∃ 𝑧 ∈ ( 𝑥 ∩ 𝐴 ) ∃ 𝑤 ∈ 𝐵 𝑦 = ( 𝑧 +ℎ 𝑤 ) ) )
57 54 55 56 sylancl ⊢ ( ( ( 𝑥 ∈ Cℋ ∧ 𝐵 ⊆ 𝑥 ) ∧ 𝑦 ∈ 𝑥 ) → ( 𝑦 ∈ ( ( 𝑥 ∩ 𝐴 ) +ℋ 𝐵 ) ↔ ∃ 𝑧 ∈ ( 𝑥 ∩ 𝐴 ) ∃ 𝑤 ∈ 𝐵 𝑦 = ( 𝑧 +ℎ 𝑤 ) ) )
58 50 57 sylibrd ⊢ ( ( ( 𝑥 ∈ Cℋ ∧ 𝐵 ⊆ 𝑥 ) ∧ 𝑦 ∈ 𝑥 ) → ( ∃ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝐵 𝑦 = ( 𝑧 +ℎ 𝑤 ) → 𝑦 ∈ ( ( 𝑥 ∩ 𝐴 ) +ℋ 𝐵 ) ) )
59 6 58 syl5bi ⊢ ( ( ( 𝑥 ∈ Cℋ ∧ 𝐵 ⊆ 𝑥 ) ∧ 𝑦 ∈ 𝑥 ) → ( 𝑦 ∈ ( 𝐴 +ℋ 𝐵 ) → 𝑦 ∈ ( ( 𝑥 ∩ 𝐴 ) +ℋ 𝐵 ) ) )
60 59 expimpd ⊢ ( ( 𝑥 ∈ Cℋ ∧ 𝐵 ⊆ 𝑥 ) → ( ( 𝑦 ∈ 𝑥 ∧ 𝑦 ∈ ( 𝐴 +ℋ 𝐵 ) ) → 𝑦 ∈ ( ( 𝑥 ∩ 𝐴 ) +ℋ 𝐵 ) ) )
61 5 60 syl5bi ⊢ ( ( 𝑥 ∈ Cℋ ∧ 𝐵 ⊆ 𝑥 ) → ( 𝑦 ∈ ( 𝑥 ∩ ( 𝐴 +ℋ 𝐵 ) ) → 𝑦 ∈ ( ( 𝑥 ∩ 𝐴 ) +ℋ 𝐵 ) ) )
62 61 ssrdv ⊢ ( ( 𝑥 ∈ Cℋ ∧ 𝐵 ⊆ 𝑥 ) → ( 𝑥 ∩ ( 𝐴 +ℋ 𝐵 ) ) ⊆ ( ( 𝑥 ∩ 𝐴 ) +ℋ 𝐵 ) )
63 62 adantl ⊢ ( ( ( 𝐴 +ℋ 𝐵 ) = ( 𝐴 ∨ℋ 𝐵 ) ∧ ( 𝑥 ∈ Cℋ ∧ 𝐵 ⊆ 𝑥 ) ) → ( 𝑥 ∩ ( 𝐴 +ℋ 𝐵 ) ) ⊆ ( ( 𝑥 ∩ 𝐴 ) +ℋ 𝐵 ) )
64 4 63 eqsstrrd ⊢ ( ( ( 𝐴 +ℋ 𝐵 ) = ( 𝐴 ∨ℋ 𝐵 ) ∧ ( 𝑥 ∈ Cℋ ∧ 𝐵 ⊆ 𝑥 ) ) → ( 𝑥 ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ ( ( 𝑥 ∩ 𝐴 ) +ℋ 𝐵 ) )
65 chincl ⊢ ( ( 𝑥 ∈ Cℋ ∧ 𝐴 ∈ Cℋ ) → ( 𝑥 ∩ 𝐴 ) ∈ Cℋ )
66 1 65 mpan2 ⊢ ( 𝑥 ∈ Cℋ → ( 𝑥 ∩ 𝐴 ) ∈ Cℋ )
67 chslej ⊢ ( ( ( 𝑥 ∩ 𝐴 ) ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( ( 𝑥 ∩ 𝐴 ) +ℋ 𝐵 ) ⊆ ( ( 𝑥 ∩ 𝐴 ) ∨ℋ 𝐵 ) )
68 66 2 67 sylancl ⊢ ( 𝑥 ∈ Cℋ → ( ( 𝑥 ∩ 𝐴 ) +ℋ 𝐵 ) ⊆ ( ( 𝑥 ∩ 𝐴 ) ∨ℋ 𝐵 ) )
69 68 ad2antrl ⊢ ( ( ( 𝐴 +ℋ 𝐵 ) = ( 𝐴 ∨ℋ 𝐵 ) ∧ ( 𝑥 ∈ Cℋ ∧ 𝐵 ⊆ 𝑥 ) ) → ( ( 𝑥 ∩ 𝐴 ) +ℋ 𝐵 ) ⊆ ( ( 𝑥 ∩ 𝐴 ) ∨ℋ 𝐵 ) )
70 64 69 sstrd ⊢ ( ( ( 𝐴 +ℋ 𝐵 ) = ( 𝐴 ∨ℋ 𝐵 ) ∧ ( 𝑥 ∈ Cℋ ∧ 𝐵 ⊆ 𝑥 ) ) → ( 𝑥 ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ ( ( 𝑥 ∩ 𝐴 ) ∨ℋ 𝐵 ) )
71 70 exp32 ⊢ ( ( 𝐴 +ℋ 𝐵 ) = ( 𝐴 ∨ℋ 𝐵 ) → ( 𝑥 ∈ Cℋ → ( 𝐵 ⊆ 𝑥 → ( 𝑥 ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ ( ( 𝑥 ∩ 𝐴 ) ∨ℋ 𝐵 ) ) ) )
72 71 ralrimiv ⊢ ( ( 𝐴 +ℋ 𝐵 ) = ( 𝐴 ∨ℋ 𝐵 ) → ∀ 𝑥 ∈ Cℋ ( 𝐵 ⊆ 𝑥 → ( 𝑥 ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ ( ( 𝑥 ∩ 𝐴 ) ∨ℋ 𝐵 ) ) )
73 dmdbr2 ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( 𝐴 𝑀ℋ* 𝐵 ↔ ∀ 𝑥 ∈ Cℋ ( 𝐵 ⊆ 𝑥 → ( 𝑥 ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ ( ( 𝑥 ∩ 𝐴 ) ∨ℋ 𝐵 ) ) ) )
74 1 2 73 mp2an ⊢ ( 𝐴 𝑀ℋ* 𝐵 ↔ ∀ 𝑥 ∈ Cℋ ( 𝐵 ⊆ 𝑥 → ( 𝑥 ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ ( ( 𝑥 ∩ 𝐴 ) ∨ℋ 𝐵 ) ) )
75 72 74 sylibr ⊢ ( ( 𝐴 +ℋ 𝐵 ) = ( 𝐴 ∨ℋ 𝐵 ) → 𝐴 𝑀ℋ* 𝐵 )