Metamath Proof Explorer

Theorem chirredlem2

Description: Lemma for chirredi . (Contributed by NM, 15-Jun-2006) (New usage is discouraged.)

Ref Expression
Hypothesis chirred.1 ⊢ 𝐴 ∈ Cℋ
Assertion chirredlem2 ( ( ( ( 𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴 ) ∧ ( 𝑞 ∈ Cℋ ∧ 𝑞 ⊆ ( ⊥ ‘ 𝐴 ) ) ) ∧ ( ( 𝑟 ∈ HAtoms ∧ 𝑟 ⊆ 𝐴 ) ∧ 𝑟 ⊆ ( 𝑝 ∨ℋ 𝑞 ) ) ) → ( ( ⊥ ‘ 𝑟 ) ∩ ( 𝑝 ∨ℋ 𝑞 ) ) = 𝑞 )

Proof

Step Hyp Ref Expression
1 chirred.1 ⊢ 𝐴 ∈ Cℋ
2 atelch ⊢ ( 𝑝 ∈ HAtoms → 𝑝 ∈ Cℋ )
3 chjcom ⊢ ( ( 𝑝 ∈ Cℋ ∧ 𝑞 ∈ Cℋ ) → ( 𝑝 ∨ℋ 𝑞 ) = ( 𝑞 ∨ℋ 𝑝 ) )
4 2 3 sylan ⊢ ( ( 𝑝 ∈ HAtoms ∧ 𝑞 ∈ Cℋ ) → ( 𝑝 ∨ℋ 𝑞 ) = ( 𝑞 ∨ℋ 𝑝 ) )
5 4 ad2ant2r ⊢ ( ( ( 𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴 ) ∧ ( 𝑞 ∈ Cℋ ∧ 𝑞 ⊆ ( ⊥ ‘ 𝐴 ) ) ) → ( 𝑝 ∨ℋ 𝑞 ) = ( 𝑞 ∨ℋ 𝑝 ) )
6 5 adantr ⊢ ( ( ( ( 𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴 ) ∧ ( 𝑞 ∈ Cℋ ∧ 𝑞 ⊆ ( ⊥ ‘ 𝐴 ) ) ) ∧ ( ( 𝑟 ∈ HAtoms ∧ 𝑟 ⊆ 𝐴 ) ∧ 𝑟 ⊆ ( 𝑝 ∨ℋ 𝑞 ) ) ) → ( 𝑝 ∨ℋ 𝑞 ) = ( 𝑞 ∨ℋ 𝑝 ) )
7 6 ineq2d ⊢ ( ( ( ( 𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴 ) ∧ ( 𝑞 ∈ Cℋ ∧ 𝑞 ⊆ ( ⊥ ‘ 𝐴 ) ) ) ∧ ( ( 𝑟 ∈ HAtoms ∧ 𝑟 ⊆ 𝐴 ) ∧ 𝑟 ⊆ ( 𝑝 ∨ℋ 𝑞 ) ) ) → ( ( ⊥ ‘ 𝑟 ) ∩ ( 𝑝 ∨ℋ 𝑞 ) ) = ( ( ⊥ ‘ 𝑟 ) ∩ ( 𝑞 ∨ℋ 𝑝 ) ) )
8 atelch ⊢ ( 𝑟 ∈ HAtoms → 𝑟 ∈ Cℋ )
9 choccl ⊢ ( 𝑟 ∈ Cℋ → ( ⊥ ‘ 𝑟 ) ∈ Cℋ )
10 8 9 syl ⊢ ( 𝑟 ∈ HAtoms → ( ⊥ ‘ 𝑟 ) ∈ Cℋ )
11 id ⊢ ( 𝑞 ∈ Cℋ → 𝑞 ∈ Cℋ )
12 10 11 2 3anim123i ⊢ ( ( 𝑟 ∈ HAtoms ∧ 𝑞 ∈ Cℋ ∧ 𝑝 ∈ HAtoms ) → ( ( ⊥ ‘ 𝑟 ) ∈ Cℋ ∧ 𝑞 ∈ Cℋ ∧ 𝑝 ∈ Cℋ ) )
13 12 3com13 ⊢ ( ( 𝑝 ∈ HAtoms ∧ 𝑞 ∈ Cℋ ∧ 𝑟 ∈ HAtoms ) → ( ( ⊥ ‘ 𝑟 ) ∈ Cℋ ∧ 𝑞 ∈ Cℋ ∧ 𝑝 ∈ Cℋ ) )
14 13 3expa ⊢ ( ( ( 𝑝 ∈ HAtoms ∧ 𝑞 ∈ Cℋ ) ∧ 𝑟 ∈ HAtoms ) → ( ( ⊥ ‘ 𝑟 ) ∈ Cℋ ∧ 𝑞 ∈ Cℋ ∧ 𝑝 ∈ Cℋ ) )
15 14 adantllr ⊢ ( ( ( ( 𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴 ) ∧ 𝑞 ∈ Cℋ ) ∧ 𝑟 ∈ HAtoms ) → ( ( ⊥ ‘ 𝑟 ) ∈ Cℋ ∧ 𝑞 ∈ Cℋ ∧ 𝑝 ∈ Cℋ ) )
16 15 adantlrr ⊢ ( ( ( ( 𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴 ) ∧ ( 𝑞 ∈ Cℋ ∧ 𝑞 ⊆ ( ⊥ ‘ 𝐴 ) ) ) ∧ 𝑟 ∈ HAtoms ) → ( ( ⊥ ‘ 𝑟 ) ∈ Cℋ ∧ 𝑞 ∈ Cℋ ∧ 𝑝 ∈ Cℋ ) )
17 16 adantrr ⊢ ( ( ( ( 𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴 ) ∧ ( 𝑞 ∈ Cℋ ∧ 𝑞 ⊆ ( ⊥ ‘ 𝐴 ) ) ) ∧ ( 𝑟 ∈ HAtoms ∧ 𝑟 ⊆ 𝐴 ) ) → ( ( ⊥ ‘ 𝑟 ) ∈ Cℋ ∧ 𝑞 ∈ Cℋ ∧ 𝑝 ∈ Cℋ ) )
18 17 adantrr ⊢ ( ( ( ( 𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴 ) ∧ ( 𝑞 ∈ Cℋ ∧ 𝑞 ⊆ ( ⊥ ‘ 𝐴 ) ) ) ∧ ( ( 𝑟 ∈ HAtoms ∧ 𝑟 ⊆ 𝐴 ) ∧ 𝑟 ⊆ ( 𝑝 ∨ℋ 𝑞 ) ) ) → ( ( ⊥ ‘ 𝑟 ) ∈ Cℋ ∧ 𝑞 ∈ Cℋ ∧ 𝑝 ∈ Cℋ ) )
19 simpll ⊢ ( ( ( 𝑞 ∈ Cℋ ∧ 𝑞 ⊆ ( ⊥ ‘ 𝐴 ) ) ∧ ( 𝑟 ∈ HAtoms ∧ 𝑟 ⊆ 𝐴 ) ) → 𝑞 ∈ Cℋ )
20 10 ad2antrl ⊢ ( ( ( 𝑞 ∈ Cℋ ∧ 𝑞 ⊆ ( ⊥ ‘ 𝐴 ) ) ∧ ( 𝑟 ∈ HAtoms ∧ 𝑟 ⊆ 𝐴 ) ) → ( ⊥ ‘ 𝑟 ) ∈ Cℋ )
21 chsscon3 ⊢ ( ( 𝑟 ∈ Cℋ ∧ 𝐴 ∈ Cℋ ) → ( 𝑟 ⊆ 𝐴 ↔ ( ⊥ ‘ 𝐴 ) ⊆ ( ⊥ ‘ 𝑟 ) ) )
22 8 1 21 sylancl ⊢ ( 𝑟 ∈ HAtoms → ( 𝑟 ⊆ 𝐴 ↔ ( ⊥ ‘ 𝐴 ) ⊆ ( ⊥ ‘ 𝑟 ) ) )
23 22 biimpa ⊢ ( ( 𝑟 ∈ HAtoms ∧ 𝑟 ⊆ 𝐴 ) → ( ⊥ ‘ 𝐴 ) ⊆ ( ⊥ ‘ 𝑟 ) )
24 sstr ⊢ ( ( 𝑞 ⊆ ( ⊥ ‘ 𝐴 ) ∧ ( ⊥ ‘ 𝐴 ) ⊆ ( ⊥ ‘ 𝑟 ) ) → 𝑞 ⊆ ( ⊥ ‘ 𝑟 ) )
25 23 24 sylan2 ⊢ ( ( 𝑞 ⊆ ( ⊥ ‘ 𝐴 ) ∧ ( 𝑟 ∈ HAtoms ∧ 𝑟 ⊆ 𝐴 ) ) → 𝑞 ⊆ ( ⊥ ‘ 𝑟 ) )
26 25 adantll ⊢ ( ( ( 𝑞 ∈ Cℋ ∧ 𝑞 ⊆ ( ⊥ ‘ 𝐴 ) ) ∧ ( 𝑟 ∈ HAtoms ∧ 𝑟 ⊆ 𝐴 ) ) → 𝑞 ⊆ ( ⊥ ‘ 𝑟 ) )
27 lecm ⊢ ( ( 𝑞 ∈ Cℋ ∧ ( ⊥ ‘ 𝑟 ) ∈ Cℋ ∧ 𝑞 ⊆ ( ⊥ ‘ 𝑟 ) ) → 𝑞 𝐶ℋ ( ⊥ ‘ 𝑟 ) )
28 19 20 26 27 syl3anc ⊢ ( ( ( 𝑞 ∈ Cℋ ∧ 𝑞 ⊆ ( ⊥ ‘ 𝐴 ) ) ∧ ( 𝑟 ∈ HAtoms ∧ 𝑟 ⊆ 𝐴 ) ) → 𝑞 𝐶ℋ ( ⊥ ‘ 𝑟 ) )
29 28 ad2ant2lr ⊢ ( ( ( ( 𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴 ) ∧ ( 𝑞 ∈ Cℋ ∧ 𝑞 ⊆ ( ⊥ ‘ 𝐴 ) ) ) ∧ ( ( 𝑟 ∈ HAtoms ∧ 𝑟 ⊆ 𝐴 ) ∧ 𝑟 ⊆ ( 𝑝 ∨ℋ 𝑞 ) ) ) → 𝑞 𝐶ℋ ( ⊥ ‘ 𝑟 ) )
30 chsscon3 ⊢ ( ( 𝑝 ∈ Cℋ ∧ 𝐴 ∈ Cℋ ) → ( 𝑝 ⊆ 𝐴 ↔ ( ⊥ ‘ 𝐴 ) ⊆ ( ⊥ ‘ 𝑝 ) ) )
31 1 30 mpan2 ⊢ ( 𝑝 ∈ Cℋ → ( 𝑝 ⊆ 𝐴 ↔ ( ⊥ ‘ 𝐴 ) ⊆ ( ⊥ ‘ 𝑝 ) ) )
32 31 biimpa ⊢ ( ( 𝑝 ∈ Cℋ ∧ 𝑝 ⊆ 𝐴 ) → ( ⊥ ‘ 𝐴 ) ⊆ ( ⊥ ‘ 𝑝 ) )
33 sstr ⊢ ( ( 𝑞 ⊆ ( ⊥ ‘ 𝐴 ) ∧ ( ⊥ ‘ 𝐴 ) ⊆ ( ⊥ ‘ 𝑝 ) ) → 𝑞 ⊆ ( ⊥ ‘ 𝑝 ) )
34 32 33 sylan2 ⊢ ( ( 𝑞 ⊆ ( ⊥ ‘ 𝐴 ) ∧ ( 𝑝 ∈ Cℋ ∧ 𝑝 ⊆ 𝐴 ) ) → 𝑞 ⊆ ( ⊥ ‘ 𝑝 ) )
35 34 an12s ⊢ ( ( 𝑝 ∈ Cℋ ∧ ( 𝑞 ⊆ ( ⊥ ‘ 𝐴 ) ∧ 𝑝 ⊆ 𝐴 ) ) → 𝑞 ⊆ ( ⊥ ‘ 𝑝 ) )
36 35 ancom2s ⊢ ( ( 𝑝 ∈ Cℋ ∧ ( 𝑝 ⊆ 𝐴 ∧ 𝑞 ⊆ ( ⊥ ‘ 𝐴 ) ) ) → 𝑞 ⊆ ( ⊥ ‘ 𝑝 ) )
37 36 adantll ⊢ ( ( ( 𝑞 ∈ Cℋ ∧ 𝑝 ∈ Cℋ ) ∧ ( 𝑝 ⊆ 𝐴 ∧ 𝑞 ⊆ ( ⊥ ‘ 𝐴 ) ) ) → 𝑞 ⊆ ( ⊥ ‘ 𝑝 ) )
38 choccl ⊢ ( 𝑝 ∈ Cℋ → ( ⊥ ‘ 𝑝 ) ∈ Cℋ )
39 lecm ⊢ ( ( 𝑞 ∈ Cℋ ∧ ( ⊥ ‘ 𝑝 ) ∈ Cℋ ∧ 𝑞 ⊆ ( ⊥ ‘ 𝑝 ) ) → 𝑞 𝐶ℋ ( ⊥ ‘ 𝑝 ) )
40 38 39 syl3an2 ⊢ ( ( 𝑞 ∈ Cℋ ∧ 𝑝 ∈ Cℋ ∧ 𝑞 ⊆ ( ⊥ ‘ 𝑝 ) ) → 𝑞 𝐶ℋ ( ⊥ ‘ 𝑝 ) )
41 40 3expia ⊢ ( ( 𝑞 ∈ Cℋ ∧ 𝑝 ∈ Cℋ ) → ( 𝑞 ⊆ ( ⊥ ‘ 𝑝 ) → 𝑞 𝐶ℋ ( ⊥ ‘ 𝑝 ) ) )
42 cmcm2 ⊢ ( ( 𝑞 ∈ Cℋ ∧ 𝑝 ∈ Cℋ ) → ( 𝑞 𝐶ℋ 𝑝 ↔ 𝑞 𝐶ℋ ( ⊥ ‘ 𝑝 ) ) )
43 41 42 sylibrd ⊢ ( ( 𝑞 ∈ Cℋ ∧ 𝑝 ∈ Cℋ ) → ( 𝑞 ⊆ ( ⊥ ‘ 𝑝 ) → 𝑞 𝐶ℋ 𝑝 ) )
44 43 adantr ⊢ ( ( ( 𝑞 ∈ Cℋ ∧ 𝑝 ∈ Cℋ ) ∧ ( 𝑝 ⊆ 𝐴 ∧ 𝑞 ⊆ ( ⊥ ‘ 𝐴 ) ) ) → ( 𝑞 ⊆ ( ⊥ ‘ 𝑝 ) → 𝑞 𝐶ℋ 𝑝 ) )
45 37 44 mpd ⊢ ( ( ( 𝑞 ∈ Cℋ ∧ 𝑝 ∈ Cℋ ) ∧ ( 𝑝 ⊆ 𝐴 ∧ 𝑞 ⊆ ( ⊥ ‘ 𝐴 ) ) ) → 𝑞 𝐶ℋ 𝑝 )
46 2 45 sylanl2 ⊢ ( ( ( 𝑞 ∈ Cℋ ∧ 𝑝 ∈ HAtoms ) ∧ ( 𝑝 ⊆ 𝐴 ∧ 𝑞 ⊆ ( ⊥ ‘ 𝐴 ) ) ) → 𝑞 𝐶ℋ 𝑝 )
47 46 ancom1s ⊢ ( ( ( 𝑝 ∈ HAtoms ∧ 𝑞 ∈ Cℋ ) ∧ ( 𝑝 ⊆ 𝐴 ∧ 𝑞 ⊆ ( ⊥ ‘ 𝐴 ) ) ) → 𝑞 𝐶ℋ 𝑝 )
48 47 an4s ⊢ ( ( ( 𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴 ) ∧ ( 𝑞 ∈ Cℋ ∧ 𝑞 ⊆ ( ⊥ ‘ 𝐴 ) ) ) → 𝑞 𝐶ℋ 𝑝 )
49 48 adantr ⊢ ( ( ( ( 𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴 ) ∧ ( 𝑞 ∈ Cℋ ∧ 𝑞 ⊆ ( ⊥ ‘ 𝐴 ) ) ) ∧ ( ( 𝑟 ∈ HAtoms ∧ 𝑟 ⊆ 𝐴 ) ∧ 𝑟 ⊆ ( 𝑝 ∨ℋ 𝑞 ) ) ) → 𝑞 𝐶ℋ 𝑝 )
50 fh2 ⊢ ( ( ( ( ⊥ ‘ 𝑟 ) ∈ Cℋ ∧ 𝑞 ∈ Cℋ ∧ 𝑝 ∈ Cℋ ) ∧ ( 𝑞 𝐶ℋ ( ⊥ ‘ 𝑟 ) ∧ 𝑞 𝐶ℋ 𝑝 ) ) → ( ( ⊥ ‘ 𝑟 ) ∩ ( 𝑞 ∨ℋ 𝑝 ) ) = ( ( ( ⊥ ‘ 𝑟 ) ∩ 𝑞 ) ∨ℋ ( ( ⊥ ‘ 𝑟 ) ∩ 𝑝 ) ) )
51 18 29 49 50 syl12anc ⊢ ( ( ( ( 𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴 ) ∧ ( 𝑞 ∈ Cℋ ∧ 𝑞 ⊆ ( ⊥ ‘ 𝐴 ) ) ) ∧ ( ( 𝑟 ∈ HAtoms ∧ 𝑟 ⊆ 𝐴 ) ∧ 𝑟 ⊆ ( 𝑝 ∨ℋ 𝑞 ) ) ) → ( ( ⊥ ‘ 𝑟 ) ∩ ( 𝑞 ∨ℋ 𝑝 ) ) = ( ( ( ⊥ ‘ 𝑟 ) ∩ 𝑞 ) ∨ℋ ( ( ⊥ ‘ 𝑟 ) ∩ 𝑝 ) ) )
52 sseqin2 ⊢ ( 𝑞 ⊆ ( ⊥ ‘ 𝑟 ) ↔ ( ( ⊥ ‘ 𝑟 ) ∩ 𝑞 ) = 𝑞 )
53 26 52 sylib ⊢ ( ( ( 𝑞 ∈ Cℋ ∧ 𝑞 ⊆ ( ⊥ ‘ 𝐴 ) ) ∧ ( 𝑟 ∈ HAtoms ∧ 𝑟 ⊆ 𝐴 ) ) → ( ( ⊥ ‘ 𝑟 ) ∩ 𝑞 ) = 𝑞 )
54 53 ad2ant2lr ⊢ ( ( ( ( 𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴 ) ∧ ( 𝑞 ∈ Cℋ ∧ 𝑞 ⊆ ( ⊥ ‘ 𝐴 ) ) ) ∧ ( ( 𝑟 ∈ HAtoms ∧ 𝑟 ⊆ 𝐴 ) ∧ 𝑟 ⊆ ( 𝑝 ∨ℋ 𝑞 ) ) ) → ( ( ⊥ ‘ 𝑟 ) ∩ 𝑞 ) = 𝑞 )
55 incom ⊢ ( ( ⊥ ‘ 𝑟 ) ∩ 𝑝 ) = ( 𝑝 ∩ ( ⊥ ‘ 𝑟 ) )
56 1 chirredlem1 ⊢ ( ( ( 𝑝 ∈ HAtoms ∧ ( 𝑞 ∈ Cℋ ∧ 𝑞 ⊆ ( ⊥ ‘ 𝐴 ) ) ) ∧ ( ( 𝑟 ∈ HAtoms ∧ 𝑟 ⊆ 𝐴 ) ∧ 𝑟 ⊆ ( 𝑝 ∨ℋ 𝑞 ) ) ) → ( 𝑝 ∩ ( ⊥ ‘ 𝑟 ) ) = 0ℋ )
57 56 adantllr ⊢ ( ( ( ( 𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴 ) ∧ ( 𝑞 ∈ Cℋ ∧ 𝑞 ⊆ ( ⊥ ‘ 𝐴 ) ) ) ∧ ( ( 𝑟 ∈ HAtoms ∧ 𝑟 ⊆ 𝐴 ) ∧ 𝑟 ⊆ ( 𝑝 ∨ℋ 𝑞 ) ) ) → ( 𝑝 ∩ ( ⊥ ‘ 𝑟 ) ) = 0ℋ )
58 55 57 eqtrid ⊢ ( ( ( ( 𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴 ) ∧ ( 𝑞 ∈ Cℋ ∧ 𝑞 ⊆ ( ⊥ ‘ 𝐴 ) ) ) ∧ ( ( 𝑟 ∈ HAtoms ∧ 𝑟 ⊆ 𝐴 ) ∧ 𝑟 ⊆ ( 𝑝 ∨ℋ 𝑞 ) ) ) → ( ( ⊥ ‘ 𝑟 ) ∩ 𝑝 ) = 0ℋ )
59 54 58 oveq12d ⊢ ( ( ( ( 𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴 ) ∧ ( 𝑞 ∈ Cℋ ∧ 𝑞 ⊆ ( ⊥ ‘ 𝐴 ) ) ) ∧ ( ( 𝑟 ∈ HAtoms ∧ 𝑟 ⊆ 𝐴 ) ∧ 𝑟 ⊆ ( 𝑝 ∨ℋ 𝑞 ) ) ) → ( ( ( ⊥ ‘ 𝑟 ) ∩ 𝑞 ) ∨ℋ ( ( ⊥ ‘ 𝑟 ) ∩ 𝑝 ) ) = ( 𝑞 ∨ℋ 0ℋ ) )
60 chj0 ⊢ ( 𝑞 ∈ Cℋ → ( 𝑞 ∨ℋ 0ℋ ) = 𝑞 )
61 60 adantr ⊢ ( ( 𝑞 ∈ Cℋ ∧ 𝑞 ⊆ ( ⊥ ‘ 𝐴 ) ) → ( 𝑞 ∨ℋ 0ℋ ) = 𝑞 )
62 61 ad2antlr ⊢ ( ( ( ( 𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴 ) ∧ ( 𝑞 ∈ Cℋ ∧ 𝑞 ⊆ ( ⊥ ‘ 𝐴 ) ) ) ∧ ( ( 𝑟 ∈ HAtoms ∧ 𝑟 ⊆ 𝐴 ) ∧ 𝑟 ⊆ ( 𝑝 ∨ℋ 𝑞 ) ) ) → ( 𝑞 ∨ℋ 0ℋ ) = 𝑞 )
63 59 62 eqtrd ⊢ ( ( ( ( 𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴 ) ∧ ( 𝑞 ∈ Cℋ ∧ 𝑞 ⊆ ( ⊥ ‘ 𝐴 ) ) ) ∧ ( ( 𝑟 ∈ HAtoms ∧ 𝑟 ⊆ 𝐴 ) ∧ 𝑟 ⊆ ( 𝑝 ∨ℋ 𝑞 ) ) ) → ( ( ( ⊥ ‘ 𝑟 ) ∩ 𝑞 ) ∨ℋ ( ( ⊥ ‘ 𝑟 ) ∩ 𝑝 ) ) = 𝑞 )
64 7 51 63 3eqtrd ⊢ ( ( ( ( 𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴 ) ∧ ( 𝑞 ∈ Cℋ ∧ 𝑞 ⊆ ( ⊥ ‘ 𝐴 ) ) ) ∧ ( ( 𝑟 ∈ HAtoms ∧ 𝑟 ⊆ 𝐴 ) ∧ 𝑟 ⊆ ( 𝑝 ∨ℋ 𝑞 ) ) ) → ( ( ⊥ ‘ 𝑟 ) ∩ ( 𝑝 ∨ℋ 𝑞 ) ) = 𝑞 )