Metamath Proof Explorer

Theorem 2at0mat0

Description: Special case of 2atmat0 where one atom could be zero. (Contributed by NM, 30-May-2013)

Ref Expression
Hypotheses 2atmatz.j ⊢ ∨ = ( join ‘ 𝐾 )
2atmatz.m ⊢ ∧ = ( meet ‘ 𝐾 )
2atmatz.z ⊢ 0 = ( 0. ‘ 𝐾 )
2atmatz.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
Assertion 2at0mat0 ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ( 𝑆 ∈ 𝐴 ∨ 𝑆 = 0 ) ∧ ( 𝑃 ∨ 𝑄 ) ≠ ( 𝑅 ∨ 𝑆 ) ) ) → ( ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑅 ∨ 𝑆 ) ) ∈ 𝐴 ∨ ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑅 ∨ 𝑆 ) ) = 0 ) )

Proof

Step Hyp Ref Expression
1 2atmatz.j ⊢ ∨ = ( join ‘ 𝐾 )
2 2atmatz.m ⊢ ∧ = ( meet ‘ 𝐾 )
3 2atmatz.z ⊢ 0 = ( 0. ‘ 𝐾 )
4 2atmatz.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
5 simpll ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ( 𝑆 ∈ 𝐴 ∨ 𝑆 = 0 ) ∧ ( 𝑃 ∨ 𝑄 ) ≠ ( 𝑅 ∨ 𝑆 ) ) ) ∧ 𝑆 ∈ 𝐴 ) → ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) )
6 simplr1 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ( 𝑆 ∈ 𝐴 ∨ 𝑆 = 0 ) ∧ ( 𝑃 ∨ 𝑄 ) ≠ ( 𝑅 ∨ 𝑆 ) ) ) ∧ 𝑆 ∈ 𝐴 ) → 𝑅 ∈ 𝐴 )
7 simpr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ( 𝑆 ∈ 𝐴 ∨ 𝑆 = 0 ) ∧ ( 𝑃 ∨ 𝑄 ) ≠ ( 𝑅 ∨ 𝑆 ) ) ) ∧ 𝑆 ∈ 𝐴 ) → 𝑆 ∈ 𝐴 )
8 simplr3 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ( 𝑆 ∈ 𝐴 ∨ 𝑆 = 0 ) ∧ ( 𝑃 ∨ 𝑄 ) ≠ ( 𝑅 ∨ 𝑆 ) ) ) ∧ 𝑆 ∈ 𝐴 ) → ( 𝑃 ∨ 𝑄 ) ≠ ( 𝑅 ∨ 𝑆 ) )
9 simpl1 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ ( 𝑃 ∨ 𝑄 ) ≠ ( 𝑅 ∨ 𝑆 ) ) ) → 𝐾 ∈ HL )
10 hlol ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ OL )
11 9 10 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ ( 𝑃 ∨ 𝑄 ) ≠ ( 𝑅 ∨ 𝑆 ) ) ) → 𝐾 ∈ OL )
12 simpr1 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ ( 𝑃 ∨ 𝑄 ) ≠ ( 𝑅 ∨ 𝑆 ) ) ) → 𝑅 ∈ 𝐴 )
13 simpr2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ ( 𝑃 ∨ 𝑄 ) ≠ ( 𝑅 ∨ 𝑆 ) ) ) → 𝑆 ∈ 𝐴 )
14 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
15 14 1 4 hlatjcl ⊢ ( ( 𝐾 ∈ HL ∧ 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) → ( 𝑅 ∨ 𝑆 ) ∈ ( Base ‘ 𝐾 ) )
16 9 12 13 15 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ ( 𝑃 ∨ 𝑄 ) ≠ ( 𝑅 ∨ 𝑆 ) ) ) → ( 𝑅 ∨ 𝑆 ) ∈ ( Base ‘ 𝐾 ) )
17 simpl3 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ ( 𝑃 ∨ 𝑄 ) ≠ ( 𝑅 ∨ 𝑆 ) ) ) → 𝑄 ∈ 𝐴 )
18 14 2 3 4 meetat2 ⊢ ( ( 𝐾 ∈ OL ∧ ( 𝑅 ∨ 𝑆 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑄 ∈ 𝐴 ) → ( ( ( 𝑅 ∨ 𝑆 ) ∧ 𝑄 ) ∈ 𝐴 ∨ ( ( 𝑅 ∨ 𝑆 ) ∧ 𝑄 ) = 0 ) )
19 11 16 17 18 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ ( 𝑃 ∨ 𝑄 ) ≠ ( 𝑅 ∨ 𝑆 ) ) ) → ( ( ( 𝑅 ∨ 𝑆 ) ∧ 𝑄 ) ∈ 𝐴 ∨ ( ( 𝑅 ∨ 𝑆 ) ∧ 𝑄 ) = 0 ) )
20 19 adantr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ ( 𝑃 ∨ 𝑄 ) ≠ ( 𝑅 ∨ 𝑆 ) ) ) ∧ 𝑃 = 𝑄 ) → ( ( ( 𝑅 ∨ 𝑆 ) ∧ 𝑄 ) ∈ 𝐴 ∨ ( ( 𝑅 ∨ 𝑆 ) ∧ 𝑄 ) = 0 ) )
21 oveq1 ⊢ ( 𝑃 = 𝑄 → ( 𝑃 ∨ 𝑄 ) = ( 𝑄 ∨ 𝑄 ) )
22 1 4 hlatjidm ⊢ ( ( 𝐾 ∈ HL ∧ 𝑄 ∈ 𝐴 ) → ( 𝑄 ∨ 𝑄 ) = 𝑄 )
23 9 17 22 syl2anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ ( 𝑃 ∨ 𝑄 ) ≠ ( 𝑅 ∨ 𝑆 ) ) ) → ( 𝑄 ∨ 𝑄 ) = 𝑄 )
24 21 23 sylan9eqr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ ( 𝑃 ∨ 𝑄 ) ≠ ( 𝑅 ∨ 𝑆 ) ) ) ∧ 𝑃 = 𝑄 ) → ( 𝑃 ∨ 𝑄 ) = 𝑄 )
25 24 oveq1d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ ( 𝑃 ∨ 𝑄 ) ≠ ( 𝑅 ∨ 𝑆 ) ) ) ∧ 𝑃 = 𝑄 ) → ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑅 ∨ 𝑆 ) ) = ( 𝑄 ∧ ( 𝑅 ∨ 𝑆 ) ) )
26 9 hllatd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ ( 𝑃 ∨ 𝑄 ) ≠ ( 𝑅 ∨ 𝑆 ) ) ) → 𝐾 ∈ Lat )
27 14 4 atbase ⊢ ( 𝑄 ∈ 𝐴 → 𝑄 ∈ ( Base ‘ 𝐾 ) )
28 17 27 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ ( 𝑃 ∨ 𝑄 ) ≠ ( 𝑅 ∨ 𝑆 ) ) ) → 𝑄 ∈ ( Base ‘ 𝐾 ) )
29 14 2 latmcom ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑄 ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑅 ∨ 𝑆 ) ∈ ( Base ‘ 𝐾 ) ) → ( 𝑄 ∧ ( 𝑅 ∨ 𝑆 ) ) = ( ( 𝑅 ∨ 𝑆 ) ∧ 𝑄 ) )
30 26 28 16 29 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ ( 𝑃 ∨ 𝑄 ) ≠ ( 𝑅 ∨ 𝑆 ) ) ) → ( 𝑄 ∧ ( 𝑅 ∨ 𝑆 ) ) = ( ( 𝑅 ∨ 𝑆 ) ∧ 𝑄 ) )
31 30 adantr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ ( 𝑃 ∨ 𝑄 ) ≠ ( 𝑅 ∨ 𝑆 ) ) ) ∧ 𝑃 = 𝑄 ) → ( 𝑄 ∧ ( 𝑅 ∨ 𝑆 ) ) = ( ( 𝑅 ∨ 𝑆 ) ∧ 𝑄 ) )
32 25 31 eqtrd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ ( 𝑃 ∨ 𝑄 ) ≠ ( 𝑅 ∨ 𝑆 ) ) ) ∧ 𝑃 = 𝑄 ) → ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑅 ∨ 𝑆 ) ) = ( ( 𝑅 ∨ 𝑆 ) ∧ 𝑄 ) )
33 32 eleq1d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ ( 𝑃 ∨ 𝑄 ) ≠ ( 𝑅 ∨ 𝑆 ) ) ) ∧ 𝑃 = 𝑄 ) → ( ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑅 ∨ 𝑆 ) ) ∈ 𝐴 ↔ ( ( 𝑅 ∨ 𝑆 ) ∧ 𝑄 ) ∈ 𝐴 ) )
34 32 eqeq1d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ ( 𝑃 ∨ 𝑄 ) ≠ ( 𝑅 ∨ 𝑆 ) ) ) ∧ 𝑃 = 𝑄 ) → ( ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑅 ∨ 𝑆 ) ) = 0 ↔ ( ( 𝑅 ∨ 𝑆 ) ∧ 𝑄 ) = 0 ) )
35 33 34 orbi12d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ ( 𝑃 ∨ 𝑄 ) ≠ ( 𝑅 ∨ 𝑆 ) ) ) ∧ 𝑃 = 𝑄 ) → ( ( ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑅 ∨ 𝑆 ) ) ∈ 𝐴 ∨ ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑅 ∨ 𝑆 ) ) = 0 ) ↔ ( ( ( 𝑅 ∨ 𝑆 ) ∧ 𝑄 ) ∈ 𝐴 ∨ ( ( 𝑅 ∨ 𝑆 ) ∧ 𝑄 ) = 0 ) ) )
36 20 35 mpbird ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ ( 𝑃 ∨ 𝑄 ) ≠ ( 𝑅 ∨ 𝑆 ) ) ) ∧ 𝑃 = 𝑄 ) → ( ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑅 ∨ 𝑆 ) ) ∈ 𝐴 ∨ ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑅 ∨ 𝑆 ) ) = 0 ) )
37 14 1 4 hlatjcl ⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) → ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) )
38 37 adantr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ ( 𝑃 ∨ 𝑄 ) ≠ ( 𝑅 ∨ 𝑆 ) ) ) → ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) )
39 14 2 3 4 meetat2 ⊢ ( ( 𝐾 ∈ OL ∧ ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑆 ∈ 𝐴 ) → ( ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑆 ) ∈ 𝐴 ∨ ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑆 ) = 0 ) )
40 11 38 13 39 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ ( 𝑃 ∨ 𝑄 ) ≠ ( 𝑅 ∨ 𝑆 ) ) ) → ( ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑆 ) ∈ 𝐴 ∨ ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑆 ) = 0 ) )
41 40 adantr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ ( 𝑃 ∨ 𝑄 ) ≠ ( 𝑅 ∨ 𝑆 ) ) ) ∧ 𝑅 = 𝑆 ) → ( ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑆 ) ∈ 𝐴 ∨ ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑆 ) = 0 ) )
42 oveq1 ⊢ ( 𝑅 = 𝑆 → ( 𝑅 ∨ 𝑆 ) = ( 𝑆 ∨ 𝑆 ) )
43 1 4 hlatjidm ⊢ ( ( 𝐾 ∈ HL ∧ 𝑆 ∈ 𝐴 ) → ( 𝑆 ∨ 𝑆 ) = 𝑆 )
44 9 13 43 syl2anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ ( 𝑃 ∨ 𝑄 ) ≠ ( 𝑅 ∨ 𝑆 ) ) ) → ( 𝑆 ∨ 𝑆 ) = 𝑆 )
45 42 44 sylan9eqr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ ( 𝑃 ∨ 𝑄 ) ≠ ( 𝑅 ∨ 𝑆 ) ) ) ∧ 𝑅 = 𝑆 ) → ( 𝑅 ∨ 𝑆 ) = 𝑆 )
46 45 oveq2d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ ( 𝑃 ∨ 𝑄 ) ≠ ( 𝑅 ∨ 𝑆 ) ) ) ∧ 𝑅 = 𝑆 ) → ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑅 ∨ 𝑆 ) ) = ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑆 ) )
47 46 eleq1d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ ( 𝑃 ∨ 𝑄 ) ≠ ( 𝑅 ∨ 𝑆 ) ) ) ∧ 𝑅 = 𝑆 ) → ( ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑅 ∨ 𝑆 ) ) ∈ 𝐴 ↔ ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑆 ) ∈ 𝐴 ) )
48 46 eqeq1d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ ( 𝑃 ∨ 𝑄 ) ≠ ( 𝑅 ∨ 𝑆 ) ) ) ∧ 𝑅 = 𝑆 ) → ( ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑅 ∨ 𝑆 ) ) = 0 ↔ ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑆 ) = 0 ) )
49 47 48 orbi12d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ ( 𝑃 ∨ 𝑄 ) ≠ ( 𝑅 ∨ 𝑆 ) ) ) ∧ 𝑅 = 𝑆 ) → ( ( ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑅 ∨ 𝑆 ) ) ∈ 𝐴 ∨ ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑅 ∨ 𝑆 ) ) = 0 ) ↔ ( ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑆 ) ∈ 𝐴 ∨ ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑆 ) = 0 ) ) )
50 41 49 mpbird ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ ( 𝑃 ∨ 𝑄 ) ≠ ( 𝑅 ∨ 𝑆 ) ) ) ∧ 𝑅 = 𝑆 ) → ( ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑅 ∨ 𝑆 ) ) ∈ 𝐴 ∨ ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑅 ∨ 𝑆 ) ) = 0 ) )
51 50 adantlr ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ ( 𝑃 ∨ 𝑄 ) ≠ ( 𝑅 ∨ 𝑆 ) ) ) ∧ 𝑃 ≠ 𝑄 ) ∧ 𝑅 = 𝑆 ) → ( ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑅 ∨ 𝑆 ) ) ∈ 𝐴 ∨ ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑅 ∨ 𝑆 ) ) = 0 ) )
52 df-ne ⊢ ( ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑅 ∨ 𝑆 ) ) ≠ 0 ↔ ¬ ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑅 ∨ 𝑆 ) ) = 0 )
53 simpll1 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ ( 𝑃 ∨ 𝑄 ) ≠ ( 𝑅 ∨ 𝑆 ) ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑅 ≠ 𝑆 ∧ ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑅 ∨ 𝑆 ) ) ≠ 0 ) ) → 𝐾 ∈ HL )
54 simpll2 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ ( 𝑃 ∨ 𝑄 ) ≠ ( 𝑅 ∨ 𝑆 ) ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑅 ≠ 𝑆 ∧ ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑅 ∨ 𝑆 ) ) ≠ 0 ) ) → 𝑃 ∈ 𝐴 )
55 simpll3 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ ( 𝑃 ∨ 𝑄 ) ≠ ( 𝑅 ∨ 𝑆 ) ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑅 ≠ 𝑆 ∧ ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑅 ∨ 𝑆 ) ) ≠ 0 ) ) → 𝑄 ∈ 𝐴 )
56 simpr1 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ ( 𝑃 ∨ 𝑄 ) ≠ ( 𝑅 ∨ 𝑆 ) ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑅 ≠ 𝑆 ∧ ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑅 ∨ 𝑆 ) ) ≠ 0 ) ) → 𝑃 ≠ 𝑄 )
57 eqid ⊢ ( LLines ‘ 𝐾 ) = ( LLines ‘ 𝐾 )
58 1 4 57 llni2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑃 ≠ 𝑄 ) → ( 𝑃 ∨ 𝑄 ) ∈ ( LLines ‘ 𝐾 ) )
59 53 54 55 56 58 syl31anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ ( 𝑃 ∨ 𝑄 ) ≠ ( 𝑅 ∨ 𝑆 ) ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑅 ≠ 𝑆 ∧ ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑅 ∨ 𝑆 ) ) ≠ 0 ) ) → ( 𝑃 ∨ 𝑄 ) ∈ ( LLines ‘ 𝐾 ) )
60 simplr1 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ ( 𝑃 ∨ 𝑄 ) ≠ ( 𝑅 ∨ 𝑆 ) ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑅 ≠ 𝑆 ∧ ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑅 ∨ 𝑆 ) ) ≠ 0 ) ) → 𝑅 ∈ 𝐴 )
61 simplr2 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ ( 𝑃 ∨ 𝑄 ) ≠ ( 𝑅 ∨ 𝑆 ) ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑅 ≠ 𝑆 ∧ ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑅 ∨ 𝑆 ) ) ≠ 0 ) ) → 𝑆 ∈ 𝐴 )
62 simpr2 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ ( 𝑃 ∨ 𝑄 ) ≠ ( 𝑅 ∨ 𝑆 ) ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑅 ≠ 𝑆 ∧ ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑅 ∨ 𝑆 ) ) ≠ 0 ) ) → 𝑅 ≠ 𝑆 )
63 1 4 57 llni2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ 𝑅 ≠ 𝑆 ) → ( 𝑅 ∨ 𝑆 ) ∈ ( LLines ‘ 𝐾 ) )
64 53 60 61 62 63 syl31anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ ( 𝑃 ∨ 𝑄 ) ≠ ( 𝑅 ∨ 𝑆 ) ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑅 ≠ 𝑆 ∧ ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑅 ∨ 𝑆 ) ) ≠ 0 ) ) → ( 𝑅 ∨ 𝑆 ) ∈ ( LLines ‘ 𝐾 ) )
65 simplr3 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ ( 𝑃 ∨ 𝑄 ) ≠ ( 𝑅 ∨ 𝑆 ) ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑅 ≠ 𝑆 ∧ ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑅 ∨ 𝑆 ) ) ≠ 0 ) ) → ( 𝑃 ∨ 𝑄 ) ≠ ( 𝑅 ∨ 𝑆 ) )
66 simpr3 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ ( 𝑃 ∨ 𝑄 ) ≠ ( 𝑅 ∨ 𝑆 ) ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑅 ≠ 𝑆 ∧ ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑅 ∨ 𝑆 ) ) ≠ 0 ) ) → ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑅 ∨ 𝑆 ) ) ≠ 0 )
67 2 3 4 57 2llnmat ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∨ 𝑄 ) ∈ ( LLines ‘ 𝐾 ) ∧ ( 𝑅 ∨ 𝑆 ) ∈ ( LLines ‘ 𝐾 ) ) ∧ ( ( 𝑃 ∨ 𝑄 ) ≠ ( 𝑅 ∨ 𝑆 ) ∧ ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑅 ∨ 𝑆 ) ) ≠ 0 ) ) → ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑅 ∨ 𝑆 ) ) ∈ 𝐴 )
68 53 59 64 65 66 67 syl32anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ ( 𝑃 ∨ 𝑄 ) ≠ ( 𝑅 ∨ 𝑆 ) ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑅 ≠ 𝑆 ∧ ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑅 ∨ 𝑆 ) ) ≠ 0 ) ) → ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑅 ∨ 𝑆 ) ) ∈ 𝐴 )
69 68 3exp2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ ( 𝑃 ∨ 𝑄 ) ≠ ( 𝑅 ∨ 𝑆 ) ) ) → ( 𝑃 ≠ 𝑄 → ( 𝑅 ≠ 𝑆 → ( ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑅 ∨ 𝑆 ) ) ≠ 0 → ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑅 ∨ 𝑆 ) ) ∈ 𝐴 ) ) ) )
70 69 imp31 ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ ( 𝑃 ∨ 𝑄 ) ≠ ( 𝑅 ∨ 𝑆 ) ) ) ∧ 𝑃 ≠ 𝑄 ) ∧ 𝑅 ≠ 𝑆 ) → ( ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑅 ∨ 𝑆 ) ) ≠ 0 → ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑅 ∨ 𝑆 ) ) ∈ 𝐴 ) )
71 52 70 syl5bir ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ ( 𝑃 ∨ 𝑄 ) ≠ ( 𝑅 ∨ 𝑆 ) ) ) ∧ 𝑃 ≠ 𝑄 ) ∧ 𝑅 ≠ 𝑆 ) → ( ¬ ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑅 ∨ 𝑆 ) ) = 0 → ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑅 ∨ 𝑆 ) ) ∈ 𝐴 ) )
72 71 orrd ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ ( 𝑃 ∨ 𝑄 ) ≠ ( 𝑅 ∨ 𝑆 ) ) ) ∧ 𝑃 ≠ 𝑄 ) ∧ 𝑅 ≠ 𝑆 ) → ( ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑅 ∨ 𝑆 ) ) = 0 ∨ ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑅 ∨ 𝑆 ) ) ∈ 𝐴 ) )
73 72 orcomd ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ ( 𝑃 ∨ 𝑄 ) ≠ ( 𝑅 ∨ 𝑆 ) ) ) ∧ 𝑃 ≠ 𝑄 ) ∧ 𝑅 ≠ 𝑆 ) → ( ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑅 ∨ 𝑆 ) ) ∈ 𝐴 ∨ ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑅 ∨ 𝑆 ) ) = 0 ) )
74 51 73 pm2.61dane ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ ( 𝑃 ∨ 𝑄 ) ≠ ( 𝑅 ∨ 𝑆 ) ) ) ∧ 𝑃 ≠ 𝑄 ) → ( ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑅 ∨ 𝑆 ) ) ∈ 𝐴 ∨ ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑅 ∨ 𝑆 ) ) = 0 ) )
75 36 74 pm2.61dane ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ ( 𝑃 ∨ 𝑄 ) ≠ ( 𝑅 ∨ 𝑆 ) ) ) → ( ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑅 ∨ 𝑆 ) ) ∈ 𝐴 ∨ ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑅 ∨ 𝑆 ) ) = 0 ) )
76 5 6 7 8 75 syl13anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ( 𝑆 ∈ 𝐴 ∨ 𝑆 = 0 ) ∧ ( 𝑃 ∨ 𝑄 ) ≠ ( 𝑅 ∨ 𝑆 ) ) ) ∧ 𝑆 ∈ 𝐴 ) → ( ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑅 ∨ 𝑆 ) ) ∈ 𝐴 ∨ ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑅 ∨ 𝑆 ) ) = 0 ) )
77 simpl1 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ( 𝑆 ∈ 𝐴 ∨ 𝑆 = 0 ) ∧ ( 𝑃 ∨ 𝑄 ) ≠ ( 𝑅 ∨ 𝑆 ) ) ) → 𝐾 ∈ HL )
78 77 10 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ( 𝑆 ∈ 𝐴 ∨ 𝑆 = 0 ) ∧ ( 𝑃 ∨ 𝑄 ) ≠ ( 𝑅 ∨ 𝑆 ) ) ) → 𝐾 ∈ OL )
79 37 adantr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ( 𝑆 ∈ 𝐴 ∨ 𝑆 = 0 ) ∧ ( 𝑃 ∨ 𝑄 ) ≠ ( 𝑅 ∨ 𝑆 ) ) ) → ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) )
80 simpr1 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ( 𝑆 ∈ 𝐴 ∨ 𝑆 = 0 ) ∧ ( 𝑃 ∨ 𝑄 ) ≠ ( 𝑅 ∨ 𝑆 ) ) ) → 𝑅 ∈ 𝐴 )
81 14 2 3 4 meetat2 ⊢ ( ( 𝐾 ∈ OL ∧ ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑅 ∈ 𝐴 ) → ( ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑅 ) ∈ 𝐴 ∨ ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑅 ) = 0 ) )
82 78 79 80 81 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ( 𝑆 ∈ 𝐴 ∨ 𝑆 = 0 ) ∧ ( 𝑃 ∨ 𝑄 ) ≠ ( 𝑅 ∨ 𝑆 ) ) ) → ( ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑅 ) ∈ 𝐴 ∨ ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑅 ) = 0 ) )
83 82 adantr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ( 𝑆 ∈ 𝐴 ∨ 𝑆 = 0 ) ∧ ( 𝑃 ∨ 𝑄 ) ≠ ( 𝑅 ∨ 𝑆 ) ) ) ∧ 𝑆 = 0 ) → ( ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑅 ) ∈ 𝐴 ∨ ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑅 ) = 0 ) )
84 oveq2 ⊢ ( 𝑆 = 0 → ( 𝑅 ∨ 𝑆 ) = ( 𝑅 ∨ 0 ) )
85 14 4 atbase ⊢ ( 𝑅 ∈ 𝐴 → 𝑅 ∈ ( Base ‘ 𝐾 ) )
86 80 85 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ( 𝑆 ∈ 𝐴 ∨ 𝑆 = 0 ) ∧ ( 𝑃 ∨ 𝑄 ) ≠ ( 𝑅 ∨ 𝑆 ) ) ) → 𝑅 ∈ ( Base ‘ 𝐾 ) )
87 14 1 3 olj01 ⊢ ( ( 𝐾 ∈ OL ∧ 𝑅 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑅 ∨ 0 ) = 𝑅 )
88 78 86 87 syl2anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ( 𝑆 ∈ 𝐴 ∨ 𝑆 = 0 ) ∧ ( 𝑃 ∨ 𝑄 ) ≠ ( 𝑅 ∨ 𝑆 ) ) ) → ( 𝑅 ∨ 0 ) = 𝑅 )
89 84 88 sylan9eqr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ( 𝑆 ∈ 𝐴 ∨ 𝑆 = 0 ) ∧ ( 𝑃 ∨ 𝑄 ) ≠ ( 𝑅 ∨ 𝑆 ) ) ) ∧ 𝑆 = 0 ) → ( 𝑅 ∨ 𝑆 ) = 𝑅 )
90 89 oveq2d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ( 𝑆 ∈ 𝐴 ∨ 𝑆 = 0 ) ∧ ( 𝑃 ∨ 𝑄 ) ≠ ( 𝑅 ∨ 𝑆 ) ) ) ∧ 𝑆 = 0 ) → ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑅 ∨ 𝑆 ) ) = ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑅 ) )
91 90 eleq1d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ( 𝑆 ∈ 𝐴 ∨ 𝑆 = 0 ) ∧ ( 𝑃 ∨ 𝑄 ) ≠ ( 𝑅 ∨ 𝑆 ) ) ) ∧ 𝑆 = 0 ) → ( ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑅 ∨ 𝑆 ) ) ∈ 𝐴 ↔ ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑅 ) ∈ 𝐴 ) )
92 90 eqeq1d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ( 𝑆 ∈ 𝐴 ∨ 𝑆 = 0 ) ∧ ( 𝑃 ∨ 𝑄 ) ≠ ( 𝑅 ∨ 𝑆 ) ) ) ∧ 𝑆 = 0 ) → ( ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑅 ∨ 𝑆 ) ) = 0 ↔ ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑅 ) = 0 ) )
93 91 92 orbi12d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ( 𝑆 ∈ 𝐴 ∨ 𝑆 = 0 ) ∧ ( 𝑃 ∨ 𝑄 ) ≠ ( 𝑅 ∨ 𝑆 ) ) ) ∧ 𝑆 = 0 ) → ( ( ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑅 ∨ 𝑆 ) ) ∈ 𝐴 ∨ ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑅 ∨ 𝑆 ) ) = 0 ) ↔ ( ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑅 ) ∈ 𝐴 ∨ ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑅 ) = 0 ) ) )
94 83 93 mpbird ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ( 𝑆 ∈ 𝐴 ∨ 𝑆 = 0 ) ∧ ( 𝑃 ∨ 𝑄 ) ≠ ( 𝑅 ∨ 𝑆 ) ) ) ∧ 𝑆 = 0 ) → ( ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑅 ∨ 𝑆 ) ) ∈ 𝐴 ∨ ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑅 ∨ 𝑆 ) ) = 0 ) )
95 simpr2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ( 𝑆 ∈ 𝐴 ∨ 𝑆 = 0 ) ∧ ( 𝑃 ∨ 𝑄 ) ≠ ( 𝑅 ∨ 𝑆 ) ) ) → ( 𝑆 ∈ 𝐴 ∨ 𝑆 = 0 ) )
96 76 94 95 mpjaodan ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ( 𝑆 ∈ 𝐴 ∨ 𝑆 = 0 ) ∧ ( 𝑃 ∨ 𝑄 ) ≠ ( 𝑅 ∨ 𝑆 ) ) ) → ( ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑅 ∨ 𝑆 ) ) ∈ 𝐴 ∨ ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑅 ∨ 𝑆 ) ) = 0 ) )