Users' Mathboxes Mathbox for Norm Megill < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  2at0mat0 Structured version   Visualization version   GIF version

Theorem 2at0mat0 34326
Description: Special case of 2atmat0 34327 where one atom could be zero. (Contributed by NM, 30-May-2013.)
Hypotheses
Ref Expression
2atmatz.j = (join‘𝐾)
2atmatz.m = (meet‘𝐾)
2atmatz.z 0 = (0.‘𝐾)
2atmatz.a 𝐴 = (Atoms‘𝐾)
Assertion
Ref Expression
2at0mat0 (((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴 ∧ (𝑆𝐴𝑆 = 0 ) ∧ (𝑃 𝑄) ≠ (𝑅 𝑆))) → (((𝑃 𝑄) (𝑅 𝑆)) ∈ 𝐴 ∨ ((𝑃 𝑄) (𝑅 𝑆)) = 0 ))

Proof of Theorem 2at0mat0
StepHypRef Expression
1 simpll 789 . . 3 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴 ∧ (𝑆𝐴𝑆 = 0 ) ∧ (𝑃 𝑄) ≠ (𝑅 𝑆))) ∧ 𝑆𝐴) → (𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴))
2 simplr1 1101 . . 3 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴 ∧ (𝑆𝐴𝑆 = 0 ) ∧ (𝑃 𝑄) ≠ (𝑅 𝑆))) ∧ 𝑆𝐴) → 𝑅𝐴)
3 simpr 477 . . 3 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴 ∧ (𝑆𝐴𝑆 = 0 ) ∧ (𝑃 𝑄) ≠ (𝑅 𝑆))) ∧ 𝑆𝐴) → 𝑆𝐴)
4 simplr3 1103 . . 3 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴 ∧ (𝑆𝐴𝑆 = 0 ) ∧ (𝑃 𝑄) ≠ (𝑅 𝑆))) ∧ 𝑆𝐴) → (𝑃 𝑄) ≠ (𝑅 𝑆))
5 simpl1 1062 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴 ∧ (𝑃 𝑄) ≠ (𝑅 𝑆))) → 𝐾 ∈ HL)
6 hlol 34163 . . . . . . . 8 (𝐾 ∈ HL → 𝐾 ∈ OL)
75, 6syl 17 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴 ∧ (𝑃 𝑄) ≠ (𝑅 𝑆))) → 𝐾 ∈ OL)
8 simpr1 1065 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴 ∧ (𝑃 𝑄) ≠ (𝑅 𝑆))) → 𝑅𝐴)
9 simpr2 1066 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴 ∧ (𝑃 𝑄) ≠ (𝑅 𝑆))) → 𝑆𝐴)
10 eqid 2621 . . . . . . . . 9 (Base‘𝐾) = (Base‘𝐾)
11 2atmatz.j . . . . . . . . 9 = (join‘𝐾)
12 2atmatz.a . . . . . . . . 9 𝐴 = (Atoms‘𝐾)
1310, 11, 12hlatjcl 34168 . . . . . . . 8 ((𝐾 ∈ HL ∧ 𝑅𝐴𝑆𝐴) → (𝑅 𝑆) ∈ (Base‘𝐾))
145, 8, 9, 13syl3anc 1323 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴 ∧ (𝑃 𝑄) ≠ (𝑅 𝑆))) → (𝑅 𝑆) ∈ (Base‘𝐾))
15 simpl3 1064 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴 ∧ (𝑃 𝑄) ≠ (𝑅 𝑆))) → 𝑄𝐴)
16 2atmatz.m . . . . . . . 8 = (meet‘𝐾)
17 2atmatz.z . . . . . . . 8 0 = (0.‘𝐾)
1810, 16, 17, 12meetat2 34099 . . . . . . 7 ((𝐾 ∈ OL ∧ (𝑅 𝑆) ∈ (Base‘𝐾) ∧ 𝑄𝐴) → (((𝑅 𝑆) 𝑄) ∈ 𝐴 ∨ ((𝑅 𝑆) 𝑄) = 0 ))
197, 14, 15, 18syl3anc 1323 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴 ∧ (𝑃 𝑄) ≠ (𝑅 𝑆))) → (((𝑅 𝑆) 𝑄) ∈ 𝐴 ∨ ((𝑅 𝑆) 𝑄) = 0 ))
2019adantr 481 . . . . 5 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴 ∧ (𝑃 𝑄) ≠ (𝑅 𝑆))) ∧ 𝑃 = 𝑄) → (((𝑅 𝑆) 𝑄) ∈ 𝐴 ∨ ((𝑅 𝑆) 𝑄) = 0 ))
21 oveq1 6617 . . . . . . . . . 10 (𝑃 = 𝑄 → (𝑃 𝑄) = (𝑄 𝑄))
2211, 12hlatjidm 34170 . . . . . . . . . . 11 ((𝐾 ∈ HL ∧ 𝑄𝐴) → (𝑄 𝑄) = 𝑄)
235, 15, 22syl2anc 692 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴 ∧ (𝑃 𝑄) ≠ (𝑅 𝑆))) → (𝑄 𝑄) = 𝑄)
2421, 23sylan9eqr 2677 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴 ∧ (𝑃 𝑄) ≠ (𝑅 𝑆))) ∧ 𝑃 = 𝑄) → (𝑃 𝑄) = 𝑄)
2524oveq1d 6625 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴 ∧ (𝑃 𝑄) ≠ (𝑅 𝑆))) ∧ 𝑃 = 𝑄) → ((𝑃 𝑄) (𝑅 𝑆)) = (𝑄 (𝑅 𝑆)))
26 hllat 34165 . . . . . . . . . . 11 (𝐾 ∈ HL → 𝐾 ∈ Lat)
275, 26syl 17 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴 ∧ (𝑃 𝑄) ≠ (𝑅 𝑆))) → 𝐾 ∈ Lat)
2810, 12atbase 34091 . . . . . . . . . . 11 (𝑄𝐴𝑄 ∈ (Base‘𝐾))
2915, 28syl 17 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴 ∧ (𝑃 𝑄) ≠ (𝑅 𝑆))) → 𝑄 ∈ (Base‘𝐾))
3010, 16latmcom 17007 . . . . . . . . . 10 ((𝐾 ∈ Lat ∧ 𝑄 ∈ (Base‘𝐾) ∧ (𝑅 𝑆) ∈ (Base‘𝐾)) → (𝑄 (𝑅 𝑆)) = ((𝑅 𝑆) 𝑄))
3127, 29, 14, 30syl3anc 1323 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴 ∧ (𝑃 𝑄) ≠ (𝑅 𝑆))) → (𝑄 (𝑅 𝑆)) = ((𝑅 𝑆) 𝑄))
3231adantr 481 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴 ∧ (𝑃 𝑄) ≠ (𝑅 𝑆))) ∧ 𝑃 = 𝑄) → (𝑄 (𝑅 𝑆)) = ((𝑅 𝑆) 𝑄))
3325, 32eqtrd 2655 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴 ∧ (𝑃 𝑄) ≠ (𝑅 𝑆))) ∧ 𝑃 = 𝑄) → ((𝑃 𝑄) (𝑅 𝑆)) = ((𝑅 𝑆) 𝑄))
3433eleq1d 2683 . . . . . 6 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴 ∧ (𝑃 𝑄) ≠ (𝑅 𝑆))) ∧ 𝑃 = 𝑄) → (((𝑃 𝑄) (𝑅 𝑆)) ∈ 𝐴 ↔ ((𝑅 𝑆) 𝑄) ∈ 𝐴))
3533eqeq1d 2623 . . . . . 6 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴 ∧ (𝑃 𝑄) ≠ (𝑅 𝑆))) ∧ 𝑃 = 𝑄) → (((𝑃 𝑄) (𝑅 𝑆)) = 0 ↔ ((𝑅 𝑆) 𝑄) = 0 ))
3634, 35orbi12d 745 . . . . 5 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴 ∧ (𝑃 𝑄) ≠ (𝑅 𝑆))) ∧ 𝑃 = 𝑄) → ((((𝑃 𝑄) (𝑅 𝑆)) ∈ 𝐴 ∨ ((𝑃 𝑄) (𝑅 𝑆)) = 0 ) ↔ (((𝑅 𝑆) 𝑄) ∈ 𝐴 ∨ ((𝑅 𝑆) 𝑄) = 0 )))
3720, 36mpbird 247 . . . 4 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴 ∧ (𝑃 𝑄) ≠ (𝑅 𝑆))) ∧ 𝑃 = 𝑄) → (((𝑃 𝑄) (𝑅 𝑆)) ∈ 𝐴 ∨ ((𝑃 𝑄) (𝑅 𝑆)) = 0 ))
3810, 11, 12hlatjcl 34168 . . . . . . . . . 10 ((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) → (𝑃 𝑄) ∈ (Base‘𝐾))
3938adantr 481 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴 ∧ (𝑃 𝑄) ≠ (𝑅 𝑆))) → (𝑃 𝑄) ∈ (Base‘𝐾))
4010, 16, 17, 12meetat2 34099 . . . . . . . . 9 ((𝐾 ∈ OL ∧ (𝑃 𝑄) ∈ (Base‘𝐾) ∧ 𝑆𝐴) → (((𝑃 𝑄) 𝑆) ∈ 𝐴 ∨ ((𝑃 𝑄) 𝑆) = 0 ))
417, 39, 9, 40syl3anc 1323 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴 ∧ (𝑃 𝑄) ≠ (𝑅 𝑆))) → (((𝑃 𝑄) 𝑆) ∈ 𝐴 ∨ ((𝑃 𝑄) 𝑆) = 0 ))
4241adantr 481 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴 ∧ (𝑃 𝑄) ≠ (𝑅 𝑆))) ∧ 𝑅 = 𝑆) → (((𝑃 𝑄) 𝑆) ∈ 𝐴 ∨ ((𝑃 𝑄) 𝑆) = 0 ))
43 oveq1 6617 . . . . . . . . . . 11 (𝑅 = 𝑆 → (𝑅 𝑆) = (𝑆 𝑆))
4411, 12hlatjidm 34170 . . . . . . . . . . . 12 ((𝐾 ∈ HL ∧ 𝑆𝐴) → (𝑆 𝑆) = 𝑆)
455, 9, 44syl2anc 692 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴 ∧ (𝑃 𝑄) ≠ (𝑅 𝑆))) → (𝑆 𝑆) = 𝑆)
4643, 45sylan9eqr 2677 . . . . . . . . . 10 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴 ∧ (𝑃 𝑄) ≠ (𝑅 𝑆))) ∧ 𝑅 = 𝑆) → (𝑅 𝑆) = 𝑆)
4746oveq2d 6626 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴 ∧ (𝑃 𝑄) ≠ (𝑅 𝑆))) ∧ 𝑅 = 𝑆) → ((𝑃 𝑄) (𝑅 𝑆)) = ((𝑃 𝑄) 𝑆))
4847eleq1d 2683 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴 ∧ (𝑃 𝑄) ≠ (𝑅 𝑆))) ∧ 𝑅 = 𝑆) → (((𝑃 𝑄) (𝑅 𝑆)) ∈ 𝐴 ↔ ((𝑃 𝑄) 𝑆) ∈ 𝐴))
4947eqeq1d 2623 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴 ∧ (𝑃 𝑄) ≠ (𝑅 𝑆))) ∧ 𝑅 = 𝑆) → (((𝑃 𝑄) (𝑅 𝑆)) = 0 ↔ ((𝑃 𝑄) 𝑆) = 0 ))
5048, 49orbi12d 745 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴 ∧ (𝑃 𝑄) ≠ (𝑅 𝑆))) ∧ 𝑅 = 𝑆) → ((((𝑃 𝑄) (𝑅 𝑆)) ∈ 𝐴 ∨ ((𝑃 𝑄) (𝑅 𝑆)) = 0 ) ↔ (((𝑃 𝑄) 𝑆) ∈ 𝐴 ∨ ((𝑃 𝑄) 𝑆) = 0 )))
5142, 50mpbird 247 . . . . . 6 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴 ∧ (𝑃 𝑄) ≠ (𝑅 𝑆))) ∧ 𝑅 = 𝑆) → (((𝑃 𝑄) (𝑅 𝑆)) ∈ 𝐴 ∨ ((𝑃 𝑄) (𝑅 𝑆)) = 0 ))
5251adantlr 750 . . . . 5 (((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴 ∧ (𝑃 𝑄) ≠ (𝑅 𝑆))) ∧ 𝑃𝑄) ∧ 𝑅 = 𝑆) → (((𝑃 𝑄) (𝑅 𝑆)) ∈ 𝐴 ∨ ((𝑃 𝑄) (𝑅 𝑆)) = 0 ))
53 df-ne 2791 . . . . . . . 8 (((𝑃 𝑄) (𝑅 𝑆)) ≠ 0 ↔ ¬ ((𝑃 𝑄) (𝑅 𝑆)) = 0 )
54 simpll1 1098 . . . . . . . . . . 11 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴 ∧ (𝑃 𝑄) ≠ (𝑅 𝑆))) ∧ (𝑃𝑄𝑅𝑆 ∧ ((𝑃 𝑄) (𝑅 𝑆)) ≠ 0 )) → 𝐾 ∈ HL)
55 simpll2 1099 . . . . . . . . . . . 12 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴 ∧ (𝑃 𝑄) ≠ (𝑅 𝑆))) ∧ (𝑃𝑄𝑅𝑆 ∧ ((𝑃 𝑄) (𝑅 𝑆)) ≠ 0 )) → 𝑃𝐴)
56 simpll3 1100 . . . . . . . . . . . 12 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴 ∧ (𝑃 𝑄) ≠ (𝑅 𝑆))) ∧ (𝑃𝑄𝑅𝑆 ∧ ((𝑃 𝑄) (𝑅 𝑆)) ≠ 0 )) → 𝑄𝐴)
57 simpr1 1065 . . . . . . . . . . . 12 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴 ∧ (𝑃 𝑄) ≠ (𝑅 𝑆))) ∧ (𝑃𝑄𝑅𝑆 ∧ ((𝑃 𝑄) (𝑅 𝑆)) ≠ 0 )) → 𝑃𝑄)
58 eqid 2621 . . . . . . . . . . . . 13 (LLines‘𝐾) = (LLines‘𝐾)
5911, 12, 58llni2 34313 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ 𝑃𝑄) → (𝑃 𝑄) ∈ (LLines‘𝐾))
6054, 55, 56, 57, 59syl31anc 1326 . . . . . . . . . . 11 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴 ∧ (𝑃 𝑄) ≠ (𝑅 𝑆))) ∧ (𝑃𝑄𝑅𝑆 ∧ ((𝑃 𝑄) (𝑅 𝑆)) ≠ 0 )) → (𝑃 𝑄) ∈ (LLines‘𝐾))
61 simplr1 1101 . . . . . . . . . . . 12 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴 ∧ (𝑃 𝑄) ≠ (𝑅 𝑆))) ∧ (𝑃𝑄𝑅𝑆 ∧ ((𝑃 𝑄) (𝑅 𝑆)) ≠ 0 )) → 𝑅𝐴)
62 simplr2 1102 . . . . . . . . . . . 12 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴 ∧ (𝑃 𝑄) ≠ (𝑅 𝑆))) ∧ (𝑃𝑄𝑅𝑆 ∧ ((𝑃 𝑄) (𝑅 𝑆)) ≠ 0 )) → 𝑆𝐴)
63 simpr2 1066 . . . . . . . . . . . 12 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴 ∧ (𝑃 𝑄) ≠ (𝑅 𝑆))) ∧ (𝑃𝑄𝑅𝑆 ∧ ((𝑃 𝑄) (𝑅 𝑆)) ≠ 0 )) → 𝑅𝑆)
6411, 12, 58llni2 34313 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ 𝑅𝐴𝑆𝐴) ∧ 𝑅𝑆) → (𝑅 𝑆) ∈ (LLines‘𝐾))
6554, 61, 62, 63, 64syl31anc 1326 . . . . . . . . . . 11 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴 ∧ (𝑃 𝑄) ≠ (𝑅 𝑆))) ∧ (𝑃𝑄𝑅𝑆 ∧ ((𝑃 𝑄) (𝑅 𝑆)) ≠ 0 )) → (𝑅 𝑆) ∈ (LLines‘𝐾))
66 simplr3 1103 . . . . . . . . . . 11 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴 ∧ (𝑃 𝑄) ≠ (𝑅 𝑆))) ∧ (𝑃𝑄𝑅𝑆 ∧ ((𝑃 𝑄) (𝑅 𝑆)) ≠ 0 )) → (𝑃 𝑄) ≠ (𝑅 𝑆))
67 simpr3 1067 . . . . . . . . . . 11 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴 ∧ (𝑃 𝑄) ≠ (𝑅 𝑆))) ∧ (𝑃𝑄𝑅𝑆 ∧ ((𝑃 𝑄) (𝑅 𝑆)) ≠ 0 )) → ((𝑃 𝑄) (𝑅 𝑆)) ≠ 0 )
6816, 17, 12, 582llnmat 34325 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ (𝑃 𝑄) ∈ (LLines‘𝐾) ∧ (𝑅 𝑆) ∈ (LLines‘𝐾)) ∧ ((𝑃 𝑄) ≠ (𝑅 𝑆) ∧ ((𝑃 𝑄) (𝑅 𝑆)) ≠ 0 )) → ((𝑃 𝑄) (𝑅 𝑆)) ∈ 𝐴)
6954, 60, 65, 66, 67, 68syl32anc 1331 . . . . . . . . . 10 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴 ∧ (𝑃 𝑄) ≠ (𝑅 𝑆))) ∧ (𝑃𝑄𝑅𝑆 ∧ ((𝑃 𝑄) (𝑅 𝑆)) ≠ 0 )) → ((𝑃 𝑄) (𝑅 𝑆)) ∈ 𝐴)
70693exp2 1282 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴 ∧ (𝑃 𝑄) ≠ (𝑅 𝑆))) → (𝑃𝑄 → (𝑅𝑆 → (((𝑃 𝑄) (𝑅 𝑆)) ≠ 0 → ((𝑃 𝑄) (𝑅 𝑆)) ∈ 𝐴))))
7170imp31 448 . . . . . . . 8 (((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴 ∧ (𝑃 𝑄) ≠ (𝑅 𝑆))) ∧ 𝑃𝑄) ∧ 𝑅𝑆) → (((𝑃 𝑄) (𝑅 𝑆)) ≠ 0 → ((𝑃 𝑄) (𝑅 𝑆)) ∈ 𝐴))
7253, 71syl5bir 233 . . . . . . 7 (((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴 ∧ (𝑃 𝑄) ≠ (𝑅 𝑆))) ∧ 𝑃𝑄) ∧ 𝑅𝑆) → (¬ ((𝑃 𝑄) (𝑅 𝑆)) = 0 → ((𝑃 𝑄) (𝑅 𝑆)) ∈ 𝐴))
7372orrd 393 . . . . . 6 (((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴 ∧ (𝑃 𝑄) ≠ (𝑅 𝑆))) ∧ 𝑃𝑄) ∧ 𝑅𝑆) → (((𝑃 𝑄) (𝑅 𝑆)) = 0 ∨ ((𝑃 𝑄) (𝑅 𝑆)) ∈ 𝐴))
7473orcomd 403 . . . . 5 (((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴 ∧ (𝑃 𝑄) ≠ (𝑅 𝑆))) ∧ 𝑃𝑄) ∧ 𝑅𝑆) → (((𝑃 𝑄) (𝑅 𝑆)) ∈ 𝐴 ∨ ((𝑃 𝑄) (𝑅 𝑆)) = 0 ))
7552, 74pm2.61dane 2877 . . . 4 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴 ∧ (𝑃 𝑄) ≠ (𝑅 𝑆))) ∧ 𝑃𝑄) → (((𝑃 𝑄) (𝑅 𝑆)) ∈ 𝐴 ∨ ((𝑃 𝑄) (𝑅 𝑆)) = 0 ))
7637, 75pm2.61dane 2877 . . 3 (((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴𝑆𝐴 ∧ (𝑃 𝑄) ≠ (𝑅 𝑆))) → (((𝑃 𝑄) (𝑅 𝑆)) ∈ 𝐴 ∨ ((𝑃 𝑄) (𝑅 𝑆)) = 0 ))
771, 2, 3, 4, 76syl13anc 1325 . 2 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴 ∧ (𝑆𝐴𝑆 = 0 ) ∧ (𝑃 𝑄) ≠ (𝑅 𝑆))) ∧ 𝑆𝐴) → (((𝑃 𝑄) (𝑅 𝑆)) ∈ 𝐴 ∨ ((𝑃 𝑄) (𝑅 𝑆)) = 0 ))
78 simpl1 1062 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴 ∧ (𝑆𝐴𝑆 = 0 ) ∧ (𝑃 𝑄) ≠ (𝑅 𝑆))) → 𝐾 ∈ HL)
7978, 6syl 17 . . . . 5 (((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴 ∧ (𝑆𝐴𝑆 = 0 ) ∧ (𝑃 𝑄) ≠ (𝑅 𝑆))) → 𝐾 ∈ OL)
8038adantr 481 . . . . 5 (((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴 ∧ (𝑆𝐴𝑆 = 0 ) ∧ (𝑃 𝑄) ≠ (𝑅 𝑆))) → (𝑃 𝑄) ∈ (Base‘𝐾))
81 simpr1 1065 . . . . 5 (((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴 ∧ (𝑆𝐴𝑆 = 0 ) ∧ (𝑃 𝑄) ≠ (𝑅 𝑆))) → 𝑅𝐴)
8210, 16, 17, 12meetat2 34099 . . . . 5 ((𝐾 ∈ OL ∧ (𝑃 𝑄) ∈ (Base‘𝐾) ∧ 𝑅𝐴) → (((𝑃 𝑄) 𝑅) ∈ 𝐴 ∨ ((𝑃 𝑄) 𝑅) = 0 ))
8379, 80, 81, 82syl3anc 1323 . . . 4 (((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴 ∧ (𝑆𝐴𝑆 = 0 ) ∧ (𝑃 𝑄) ≠ (𝑅 𝑆))) → (((𝑃 𝑄) 𝑅) ∈ 𝐴 ∨ ((𝑃 𝑄) 𝑅) = 0 ))
8483adantr 481 . . 3 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴 ∧ (𝑆𝐴𝑆 = 0 ) ∧ (𝑃 𝑄) ≠ (𝑅 𝑆))) ∧ 𝑆 = 0 ) → (((𝑃 𝑄) 𝑅) ∈ 𝐴 ∨ ((𝑃 𝑄) 𝑅) = 0 ))
85 oveq2 6618 . . . . . . 7 (𝑆 = 0 → (𝑅 𝑆) = (𝑅 0 ))
8610, 12atbase 34091 . . . . . . . . 9 (𝑅𝐴𝑅 ∈ (Base‘𝐾))
8781, 86syl 17 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴 ∧ (𝑆𝐴𝑆 = 0 ) ∧ (𝑃 𝑄) ≠ (𝑅 𝑆))) → 𝑅 ∈ (Base‘𝐾))
8810, 11, 17olj01 34027 . . . . . . . 8 ((𝐾 ∈ OL ∧ 𝑅 ∈ (Base‘𝐾)) → (𝑅 0 ) = 𝑅)
8979, 87, 88syl2anc 692 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴 ∧ (𝑆𝐴𝑆 = 0 ) ∧ (𝑃 𝑄) ≠ (𝑅 𝑆))) → (𝑅 0 ) = 𝑅)
9085, 89sylan9eqr 2677 . . . . . 6 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴 ∧ (𝑆𝐴𝑆 = 0 ) ∧ (𝑃 𝑄) ≠ (𝑅 𝑆))) ∧ 𝑆 = 0 ) → (𝑅 𝑆) = 𝑅)
9190oveq2d 6626 . . . . 5 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴 ∧ (𝑆𝐴𝑆 = 0 ) ∧ (𝑃 𝑄) ≠ (𝑅 𝑆))) ∧ 𝑆 = 0 ) → ((𝑃 𝑄) (𝑅 𝑆)) = ((𝑃 𝑄) 𝑅))
9291eleq1d 2683 . . . 4 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴 ∧ (𝑆𝐴𝑆 = 0 ) ∧ (𝑃 𝑄) ≠ (𝑅 𝑆))) ∧ 𝑆 = 0 ) → (((𝑃 𝑄) (𝑅 𝑆)) ∈ 𝐴 ↔ ((𝑃 𝑄) 𝑅) ∈ 𝐴))
9391eqeq1d 2623 . . . 4 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴 ∧ (𝑆𝐴𝑆 = 0 ) ∧ (𝑃 𝑄) ≠ (𝑅 𝑆))) ∧ 𝑆 = 0 ) → (((𝑃 𝑄) (𝑅 𝑆)) = 0 ↔ ((𝑃 𝑄) 𝑅) = 0 ))
9492, 93orbi12d 745 . . 3 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴 ∧ (𝑆𝐴𝑆 = 0 ) ∧ (𝑃 𝑄) ≠ (𝑅 𝑆))) ∧ 𝑆 = 0 ) → ((((𝑃 𝑄) (𝑅 𝑆)) ∈ 𝐴 ∨ ((𝑃 𝑄) (𝑅 𝑆)) = 0 ) ↔ (((𝑃 𝑄) 𝑅) ∈ 𝐴 ∨ ((𝑃 𝑄) 𝑅) = 0 )))
9584, 94mpbird 247 . 2 ((((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴 ∧ (𝑆𝐴𝑆 = 0 ) ∧ (𝑃 𝑄) ≠ (𝑅 𝑆))) ∧ 𝑆 = 0 ) → (((𝑃 𝑄) (𝑅 𝑆)) ∈ 𝐴 ∨ ((𝑃 𝑄) (𝑅 𝑆)) = 0 ))
96 simpr2 1066 . 2 (((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴 ∧ (𝑆𝐴𝑆 = 0 ) ∧ (𝑃 𝑄) ≠ (𝑅 𝑆))) → (𝑆𝐴𝑆 = 0 ))
9777, 95, 96mpjaodan 826 1 (((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) ∧ (𝑅𝐴 ∧ (𝑆𝐴𝑆 = 0 ) ∧ (𝑃 𝑄) ≠ (𝑅 𝑆))) → (((𝑃 𝑄) (𝑅 𝑆)) ∈ 𝐴 ∨ ((𝑃 𝑄) (𝑅 𝑆)) = 0 ))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wo 383  wa 384  w3a 1036   = wceq 1480  wcel 1987  wne 2790  cfv 5852  (class class class)co 6610  Basecbs 15792  joincjn 16876  meetcmee 16877  0.cp0 16969  Latclat 16977  OLcol 33976  Atomscatm 34065  HLchlt 34152  LLinesclln 34292
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4736  ax-sep 4746  ax-nul 4754  ax-pow 4808  ax-pr 4872  ax-un 6909
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-ral 2912  df-rex 2913  df-reu 2914  df-rab 2916  df-v 3191  df-sbc 3422  df-csb 3519  df-dif 3562  df-un 3564  df-in 3566  df-ss 3573  df-nul 3897  df-if 4064  df-pw 4137  df-sn 4154  df-pr 4156  df-op 4160  df-uni 4408  df-iun 4492  df-br 4619  df-opab 4679  df-mpt 4680  df-id 4994  df-xp 5085  df-rel 5086  df-cnv 5087  df-co 5088  df-dm 5089  df-rn 5090  df-res 5091  df-ima 5092  df-iota 5815  df-fun 5854  df-fn 5855  df-f 5856  df-f1 5857  df-fo 5858  df-f1o 5859  df-fv 5860  df-riota 6571  df-ov 6613  df-oprab 6614  df-preset 16860  df-poset 16878  df-plt 16890  df-lub 16906  df-glb 16907  df-join 16908  df-meet 16909  df-p0 16971  df-lat 16978  df-clat 17040  df-oposet 33978  df-ol 33980  df-oml 33981  df-covers 34068  df-ats 34069  df-atl 34100  df-cvlat 34124  df-hlat 34153  df-llines 34299
This theorem is referenced by:  2atmat0  34327  cdlemg31b0a  35498
  Copyright terms: Public domain W3C validator