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

Metamath Proof Explorer

Theorem cvrat3

Description: A condition implying that a certain lattice element is an atom. Part of Lemma 3.2.20 of PtakPulmannova p. 68. ( atcvat3i analog.) (Contributed by NM, 30-Nov-2011)

Ref Expression
Hypotheses cvrat3.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
cvrat3.l ⊢ ≤ = ( le ‘ 𝐾 )
cvrat3.j ⊢ ∨ = ( join ‘ 𝐾 )
cvrat3.m ⊢ ∧ = ( meet ‘ 𝐾 )
cvrat3.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
Assertion cvrat3 ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) → ( ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑄 ≤ 𝑋 ∧ 𝑃 ≤ ( 𝑋 ∨ 𝑄 ) ) → ( 𝑋 ∧ ( 𝑃 ∨ 𝑄 ) ) ∈ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 cvrat3.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 cvrat3.l ⊢ ≤ = ( le ‘ 𝐾 )
3 cvrat3.j ⊢ ∨ = ( join ‘ 𝐾 )
4 cvrat3.m ⊢ ∧ = ( meet ‘ 𝐾 )
5 cvrat3.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
6 eqid ⊢ ( ⋖ ‘ 𝐾 ) = ( ⋖ ‘ 𝐾 )
7 1 2 3 6 5 cvr1 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑄 ∈ 𝐴 ) → ( ¬ 𝑄 ≤ 𝑋 ↔ 𝑋 ( ⋖ ‘ 𝐾 ) ( 𝑋 ∨ 𝑄 ) ) )
8 7 3adant3r2 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) → ( ¬ 𝑄 ≤ 𝑋 ↔ 𝑋 ( ⋖ ‘ 𝐾 ) ( 𝑋 ∨ 𝑄 ) ) )
9 8 biimpa ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) ∧ ¬ 𝑄 ≤ 𝑋 ) → 𝑋 ( ⋖ ‘ 𝐾 ) ( 𝑋 ∨ 𝑄 ) )
10 9 adantrr ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) ∧ ( ¬ 𝑄 ≤ 𝑋 ∧ 𝑃 ≤ ( 𝑋 ∨ 𝑄 ) ) ) → 𝑋 ( ⋖ ‘ 𝐾 ) ( 𝑋 ∨ 𝑄 ) )
11 hllat ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ Lat )
12 11 adantr ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) → 𝐾 ∈ Lat )
13 simpr2 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) → 𝑃 ∈ 𝐴 )
14 1 5 atbase ⊢ ( 𝑃 ∈ 𝐴 → 𝑃 ∈ 𝐵 )
15 13 14 syl ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) → 𝑃 ∈ 𝐵 )
16 simpr3 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) → 𝑄 ∈ 𝐴 )
17 1 5 atbase ⊢ ( 𝑄 ∈ 𝐴 → 𝑄 ∈ 𝐵 )
18 16 17 syl ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) → 𝑄 ∈ 𝐵 )
19 1 3 latjcom ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑃 ∈ 𝐵 ∧ 𝑄 ∈ 𝐵 ) → ( 𝑃 ∨ 𝑄 ) = ( 𝑄 ∨ 𝑃 ) )
20 12 15 18 19 syl3anc ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) → ( 𝑃 ∨ 𝑄 ) = ( 𝑄 ∨ 𝑃 ) )
21 20 oveq2d ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) → ( 𝑋 ∨ ( 𝑃 ∨ 𝑄 ) ) = ( 𝑋 ∨ ( 𝑄 ∨ 𝑃 ) ) )
22 simpr1 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) → 𝑋 ∈ 𝐵 )
23 1 3 latjass ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑄 ∈ 𝐵 ∧ 𝑃 ∈ 𝐵 ) ) → ( ( 𝑋 ∨ 𝑄 ) ∨ 𝑃 ) = ( 𝑋 ∨ ( 𝑄 ∨ 𝑃 ) ) )
24 12 22 18 15 23 syl13anc ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) → ( ( 𝑋 ∨ 𝑄 ) ∨ 𝑃 ) = ( 𝑋 ∨ ( 𝑄 ∨ 𝑃 ) ) )
25 21 24 eqtr4d ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) → ( 𝑋 ∨ ( 𝑃 ∨ 𝑄 ) ) = ( ( 𝑋 ∨ 𝑄 ) ∨ 𝑃 ) )
26 25 adantr ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) ∧ 𝑃 ≤ ( 𝑋 ∨ 𝑄 ) ) → ( 𝑋 ∨ ( 𝑃 ∨ 𝑄 ) ) = ( ( 𝑋 ∨ 𝑄 ) ∨ 𝑃 ) )
27 1 3 latjcl ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑄 ∈ 𝐵 ) → ( 𝑋 ∨ 𝑄 ) ∈ 𝐵 )
28 12 22 18 27 syl3anc ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) → ( 𝑋 ∨ 𝑄 ) ∈ 𝐵 )
29 1 2 3 latjlej2 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑃 ∈ 𝐵 ∧ ( 𝑋 ∨ 𝑄 ) ∈ 𝐵 ∧ ( 𝑋 ∨ 𝑄 ) ∈ 𝐵 ) ) → ( 𝑃 ≤ ( 𝑋 ∨ 𝑄 ) → ( ( 𝑋 ∨ 𝑄 ) ∨ 𝑃 ) ≤ ( ( 𝑋 ∨ 𝑄 ) ∨ ( 𝑋 ∨ 𝑄 ) ) ) )
30 12 15 28 28 29 syl13anc ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) → ( 𝑃 ≤ ( 𝑋 ∨ 𝑄 ) → ( ( 𝑋 ∨ 𝑄 ) ∨ 𝑃 ) ≤ ( ( 𝑋 ∨ 𝑄 ) ∨ ( 𝑋 ∨ 𝑄 ) ) ) )
31 30 imp ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) ∧ 𝑃 ≤ ( 𝑋 ∨ 𝑄 ) ) → ( ( 𝑋 ∨ 𝑄 ) ∨ 𝑃 ) ≤ ( ( 𝑋 ∨ 𝑄 ) ∨ ( 𝑋 ∨ 𝑄 ) ) )
32 26 31 eqbrtrd ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) ∧ 𝑃 ≤ ( 𝑋 ∨ 𝑄 ) ) → ( 𝑋 ∨ ( 𝑃 ∨ 𝑄 ) ) ≤ ( ( 𝑋 ∨ 𝑄 ) ∨ ( 𝑋 ∨ 𝑄 ) ) )
33 1 3 latjidm ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∨ 𝑄 ) ∈ 𝐵 ) → ( ( 𝑋 ∨ 𝑄 ) ∨ ( 𝑋 ∨ 𝑄 ) ) = ( 𝑋 ∨ 𝑄 ) )
34 12 28 33 syl2anc ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) → ( ( 𝑋 ∨ 𝑄 ) ∨ ( 𝑋 ∨ 𝑄 ) ) = ( 𝑋 ∨ 𝑄 ) )
35 34 adantr ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) ∧ 𝑃 ≤ ( 𝑋 ∨ 𝑄 ) ) → ( ( 𝑋 ∨ 𝑄 ) ∨ ( 𝑋 ∨ 𝑄 ) ) = ( 𝑋 ∨ 𝑄 ) )
36 32 35 breqtrd ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) ∧ 𝑃 ≤ ( 𝑋 ∨ 𝑄 ) ) → ( 𝑋 ∨ ( 𝑃 ∨ 𝑄 ) ) ≤ ( 𝑋 ∨ 𝑄 ) )
37 simpl ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) → 𝐾 ∈ HL )
38 2 3 5 hlatlej2 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) → 𝑄 ≤ ( 𝑃 ∨ 𝑄 ) )
39 37 13 16 38 syl3anc ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) → 𝑄 ≤ ( 𝑃 ∨ 𝑄 ) )
40 1 3 latjcl ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑃 ∈ 𝐵 ∧ 𝑄 ∈ 𝐵 ) → ( 𝑃 ∨ 𝑄 ) ∈ 𝐵 )
41 12 15 18 40 syl3anc ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) → ( 𝑃 ∨ 𝑄 ) ∈ 𝐵 )
42 1 2 3 latjlej2 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑄 ∈ 𝐵 ∧ ( 𝑃 ∨ 𝑄 ) ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) ) → ( 𝑄 ≤ ( 𝑃 ∨ 𝑄 ) → ( 𝑋 ∨ 𝑄 ) ≤ ( 𝑋 ∨ ( 𝑃 ∨ 𝑄 ) ) ) )
43 12 18 41 22 42 syl13anc ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) → ( 𝑄 ≤ ( 𝑃 ∨ 𝑄 ) → ( 𝑋 ∨ 𝑄 ) ≤ ( 𝑋 ∨ ( 𝑃 ∨ 𝑄 ) ) ) )
44 39 43 mpd ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) → ( 𝑋 ∨ 𝑄 ) ≤ ( 𝑋 ∨ ( 𝑃 ∨ 𝑄 ) ) )
45 44 adantr ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) ∧ 𝑃 ≤ ( 𝑋 ∨ 𝑄 ) ) → ( 𝑋 ∨ 𝑄 ) ≤ ( 𝑋 ∨ ( 𝑃 ∨ 𝑄 ) ) )
46 1 3 latjcl ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ ( 𝑃 ∨ 𝑄 ) ∈ 𝐵 ) → ( 𝑋 ∨ ( 𝑃 ∨ 𝑄 ) ) ∈ 𝐵 )
47 12 22 41 46 syl3anc ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) → ( 𝑋 ∨ ( 𝑃 ∨ 𝑄 ) ) ∈ 𝐵 )
48 1 2 latasymb ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∨ ( 𝑃 ∨ 𝑄 ) ) ∈ 𝐵 ∧ ( 𝑋 ∨ 𝑄 ) ∈ 𝐵 ) → ( ( ( 𝑋 ∨ ( 𝑃 ∨ 𝑄 ) ) ≤ ( 𝑋 ∨ 𝑄 ) ∧ ( 𝑋 ∨ 𝑄 ) ≤ ( 𝑋 ∨ ( 𝑃 ∨ 𝑄 ) ) ) ↔ ( 𝑋 ∨ ( 𝑃 ∨ 𝑄 ) ) = ( 𝑋 ∨ 𝑄 ) ) )
49 12 47 28 48 syl3anc ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) → ( ( ( 𝑋 ∨ ( 𝑃 ∨ 𝑄 ) ) ≤ ( 𝑋 ∨ 𝑄 ) ∧ ( 𝑋 ∨ 𝑄 ) ≤ ( 𝑋 ∨ ( 𝑃 ∨ 𝑄 ) ) ) ↔ ( 𝑋 ∨ ( 𝑃 ∨ 𝑄 ) ) = ( 𝑋 ∨ 𝑄 ) ) )
50 49 adantr ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) ∧ 𝑃 ≤ ( 𝑋 ∨ 𝑄 ) ) → ( ( ( 𝑋 ∨ ( 𝑃 ∨ 𝑄 ) ) ≤ ( 𝑋 ∨ 𝑄 ) ∧ ( 𝑋 ∨ 𝑄 ) ≤ ( 𝑋 ∨ ( 𝑃 ∨ 𝑄 ) ) ) ↔ ( 𝑋 ∨ ( 𝑃 ∨ 𝑄 ) ) = ( 𝑋 ∨ 𝑄 ) ) )
51 36 45 50 mpbi2and ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) ∧ 𝑃 ≤ ( 𝑋 ∨ 𝑄 ) ) → ( 𝑋 ∨ ( 𝑃 ∨ 𝑄 ) ) = ( 𝑋 ∨ 𝑄 ) )
52 51 breq2d ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) ∧ 𝑃 ≤ ( 𝑋 ∨ 𝑄 ) ) → ( 𝑋 ( ⋖ ‘ 𝐾 ) ( 𝑋 ∨ ( 𝑃 ∨ 𝑄 ) ) ↔ 𝑋 ( ⋖ ‘ 𝐾 ) ( 𝑋 ∨ 𝑄 ) ) )
53 52 adantrl ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) ∧ ( ¬ 𝑄 ≤ 𝑋 ∧ 𝑃 ≤ ( 𝑋 ∨ 𝑄 ) ) ) → ( 𝑋 ( ⋖ ‘ 𝐾 ) ( 𝑋 ∨ ( 𝑃 ∨ 𝑄 ) ) ↔ 𝑋 ( ⋖ ‘ 𝐾 ) ( 𝑋 ∨ 𝑄 ) ) )
54 10 53 mpbird ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) ∧ ( ¬ 𝑄 ≤ 𝑋 ∧ 𝑃 ≤ ( 𝑋 ∨ 𝑄 ) ) ) → 𝑋 ( ⋖ ‘ 𝐾 ) ( 𝑋 ∨ ( 𝑃 ∨ 𝑄 ) ) )
55 54 ex ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) → ( ( ¬ 𝑄 ≤ 𝑋 ∧ 𝑃 ≤ ( 𝑋 ∨ 𝑄 ) ) → 𝑋 ( ⋖ ‘ 𝐾 ) ( 𝑋 ∨ ( 𝑃 ∨ 𝑄 ) ) ) )
56 1 3 4 6 cvrexch ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ ( 𝑃 ∨ 𝑄 ) ∈ 𝐵 ) → ( ( 𝑋 ∧ ( 𝑃 ∨ 𝑄 ) ) ( ⋖ ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) ↔ 𝑋 ( ⋖ ‘ 𝐾 ) ( 𝑋 ∨ ( 𝑃 ∨ 𝑄 ) ) ) )
57 37 22 41 56 syl3anc ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) → ( ( 𝑋 ∧ ( 𝑃 ∨ 𝑄 ) ) ( ⋖ ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) ↔ 𝑋 ( ⋖ ‘ 𝐾 ) ( 𝑋 ∨ ( 𝑃 ∨ 𝑄 ) ) ) )
58 55 57 sylibrd ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) → ( ( ¬ 𝑄 ≤ 𝑋 ∧ 𝑃 ≤ ( 𝑋 ∨ 𝑄 ) ) → ( 𝑋 ∧ ( 𝑃 ∨ 𝑄 ) ) ( ⋖ ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) ) )
59 58 adantr ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) ∧ 𝑃 ≠ 𝑄 ) → ( ( ¬ 𝑄 ≤ 𝑋 ∧ 𝑃 ≤ ( 𝑋 ∨ 𝑄 ) ) → ( 𝑋 ∧ ( 𝑃 ∨ 𝑄 ) ) ( ⋖ ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) ) )
60 1 4 latmcl ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ ( 𝑃 ∨ 𝑄 ) ∈ 𝐵 ) → ( 𝑋 ∧ ( 𝑃 ∨ 𝑄 ) ) ∈ 𝐵 )
61 12 22 41 60 syl3anc ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) → ( 𝑋 ∧ ( 𝑃 ∨ 𝑄 ) ) ∈ 𝐵 )
62 1 3 6 5 cvrat2 ⊢ ( ( 𝐾 ∈ HL ∧ ( ( 𝑋 ∧ ( 𝑃 ∨ 𝑄 ) ) ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑋 ∧ ( 𝑃 ∨ 𝑄 ) ) ( ⋖ ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) ) ) → ( 𝑋 ∧ ( 𝑃 ∨ 𝑄 ) ) ∈ 𝐴 )
63 62 3expia ⊢ ( ( 𝐾 ∈ HL ∧ ( ( 𝑋 ∧ ( 𝑃 ∨ 𝑄 ) ) ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) → ( ( 𝑃 ≠ 𝑄 ∧ ( 𝑋 ∧ ( 𝑃 ∨ 𝑄 ) ) ( ⋖ ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) ) → ( 𝑋 ∧ ( 𝑃 ∨ 𝑄 ) ) ∈ 𝐴 ) )
64 37 61 13 16 63 syl13anc ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) → ( ( 𝑃 ≠ 𝑄 ∧ ( 𝑋 ∧ ( 𝑃 ∨ 𝑄 ) ) ( ⋖ ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) ) → ( 𝑋 ∧ ( 𝑃 ∨ 𝑄 ) ) ∈ 𝐴 ) )
65 64 expdimp ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) ∧ 𝑃 ≠ 𝑄 ) → ( ( 𝑋 ∧ ( 𝑃 ∨ 𝑄 ) ) ( ⋖ ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) → ( 𝑋 ∧ ( 𝑃 ∨ 𝑄 ) ) ∈ 𝐴 ) )
66 59 65 syld ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) ∧ 𝑃 ≠ 𝑄 ) → ( ( ¬ 𝑄 ≤ 𝑋 ∧ 𝑃 ≤ ( 𝑋 ∨ 𝑄 ) ) → ( 𝑋 ∧ ( 𝑃 ∨ 𝑄 ) ) ∈ 𝐴 ) )
67 66 exp4b ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) → ( 𝑃 ≠ 𝑄 → ( ¬ 𝑄 ≤ 𝑋 → ( 𝑃 ≤ ( 𝑋 ∨ 𝑄 ) → ( 𝑋 ∧ ( 𝑃 ∨ 𝑄 ) ) ∈ 𝐴 ) ) ) )
68 67 3impd ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) → ( ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑄 ≤ 𝑋 ∧ 𝑃 ≤ ( 𝑋 ∨ 𝑄 ) ) → ( 𝑋 ∧ ( 𝑃 ∨ 𝑄 ) ) ∈ 𝐴 ) )