Mathbox for Norm Megill < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  3atlem5 Structured version   Visualization version   GIF version

Theorem 3atlem5 37056
 Description: Lemma for 3at 37059. (Contributed by NM, 23-Jun-2012.)
Hypotheses
Ref Expression
3at.l = (le‘𝐾)
3at.j = (join‘𝐾)
3at.a 𝐴 = (Atoms‘𝐾)
Assertion
Ref Expression
3atlem5 (((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) ∧ (¬ 𝑅 (𝑃 𝑄) ∧ 𝑃𝑄 ∧ ¬ 𝑄 (𝑃 𝑈)) ∧ ((𝑃 𝑄) 𝑅) ((𝑆 𝑇) 𝑈)) → ((𝑃 𝑄) 𝑅) = ((𝑆 𝑇) 𝑈))

Proof of Theorem 3atlem5
StepHypRef Expression
1 oveq2 7159 . . . . . 6 (𝑈 = 𝑃 → ((𝑆 𝑇) 𝑈) = ((𝑆 𝑇) 𝑃))
21eqcoms 2767 . . . . 5 (𝑃 = 𝑈 → ((𝑆 𝑇) 𝑈) = ((𝑆 𝑇) 𝑃))
32breq2d 5045 . . . 4 (𝑃 = 𝑈 → (((𝑃 𝑄) 𝑅) ((𝑆 𝑇) 𝑈) ↔ ((𝑃 𝑄) 𝑅) ((𝑆 𝑇) 𝑃)))
42eqeq2d 2770 . . . 4 (𝑃 = 𝑈 → (((𝑃 𝑄) 𝑅) = ((𝑆 𝑇) 𝑈) ↔ ((𝑃 𝑄) 𝑅) = ((𝑆 𝑇) 𝑃)))
53, 4imbi12d 349 . . 3 (𝑃 = 𝑈 → ((((𝑃 𝑄) 𝑅) ((𝑆 𝑇) 𝑈) → ((𝑃 𝑄) 𝑅) = ((𝑆 𝑇) 𝑈)) ↔ (((𝑃 𝑄) 𝑅) ((𝑆 𝑇) 𝑃) → ((𝑃 𝑄) 𝑅) = ((𝑆 𝑇) 𝑃))))
6 simp1l 1195 . . . . 5 ((((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) ∧ (¬ 𝑅 (𝑃 𝑄) ∧ 𝑃𝑄 ∧ ¬ 𝑄 (𝑃 𝑈))) ∧ 𝑃𝑈 ∧ ((𝑃 𝑄) 𝑅) ((𝑆 𝑇) 𝑈)) → (𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)))
7 simp1r1 1267 . . . . 5 ((((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) ∧ (¬ 𝑅 (𝑃 𝑄) ∧ 𝑃𝑄 ∧ ¬ 𝑄 (𝑃 𝑈))) ∧ 𝑃𝑈 ∧ ((𝑃 𝑄) 𝑅) ((𝑆 𝑇) 𝑈)) → ¬ 𝑅 (𝑃 𝑄))
8 simp2 1135 . . . . 5 ((((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) ∧ (¬ 𝑅 (𝑃 𝑄) ∧ 𝑃𝑄 ∧ ¬ 𝑄 (𝑃 𝑈))) ∧ 𝑃𝑈 ∧ ((𝑃 𝑄) 𝑅) ((𝑆 𝑇) 𝑈)) → 𝑃𝑈)
9 simp1r3 1269 . . . . 5 ((((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) ∧ (¬ 𝑅 (𝑃 𝑄) ∧ 𝑃𝑄 ∧ ¬ 𝑄 (𝑃 𝑈))) ∧ 𝑃𝑈 ∧ ((𝑃 𝑄) 𝑅) ((𝑆 𝑇) 𝑈)) → ¬ 𝑄 (𝑃 𝑈))
10 simp3 1136 . . . . 5 ((((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) ∧ (¬ 𝑅 (𝑃 𝑄) ∧ 𝑃𝑄 ∧ ¬ 𝑄 (𝑃 𝑈))) ∧ 𝑃𝑈 ∧ ((𝑃 𝑄) 𝑅) ((𝑆 𝑇) 𝑈)) → ((𝑃 𝑄) 𝑅) ((𝑆 𝑇) 𝑈))
11 3at.l . . . . . 6 = (le‘𝐾)
12 3at.j . . . . . 6 = (join‘𝐾)
13 3at.a . . . . . 6 𝐴 = (Atoms‘𝐾)
1411, 12, 133atlem3 37054 . . . . 5 (((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) ∧ (¬ 𝑅 (𝑃 𝑄) ∧ 𝑃𝑈 ∧ ¬ 𝑄 (𝑃 𝑈)) ∧ ((𝑃 𝑄) 𝑅) ((𝑆 𝑇) 𝑈)) → ((𝑃 𝑄) 𝑅) = ((𝑆 𝑇) 𝑈))
156, 7, 8, 9, 10, 14syl131anc 1381 . . . 4 ((((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) ∧ (¬ 𝑅 (𝑃 𝑄) ∧ 𝑃𝑄 ∧ ¬ 𝑄 (𝑃 𝑈))) ∧ 𝑃𝑈 ∧ ((𝑃 𝑄) 𝑅) ((𝑆 𝑇) 𝑈)) → ((𝑃 𝑄) 𝑅) = ((𝑆 𝑇) 𝑈))
16153expia 1119 . . 3 ((((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) ∧ (¬ 𝑅 (𝑃 𝑄) ∧ 𝑃𝑄 ∧ ¬ 𝑄 (𝑃 𝑈))) ∧ 𝑃𝑈) → (((𝑃 𝑄) 𝑅) ((𝑆 𝑇) 𝑈) → ((𝑃 𝑄) 𝑅) = ((𝑆 𝑇) 𝑈)))
17 simp11 1201 . . . . . 6 (((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) ∧ (¬ 𝑅 (𝑃 𝑄) ∧ 𝑃𝑄 ∧ ¬ 𝑄 (𝑃 𝑈)) ∧ ((𝑅 𝑄) 𝑃) ((𝑆 𝑇) 𝑃)) → 𝐾 ∈ HL)
18 simp123 1305 . . . . . . 7 (((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) ∧ (¬ 𝑅 (𝑃 𝑄) ∧ 𝑃𝑄 ∧ ¬ 𝑄 (𝑃 𝑈)) ∧ ((𝑅 𝑄) 𝑃) ((𝑆 𝑇) 𝑃)) → 𝑅𝐴)
19 simp122 1304 . . . . . . 7 (((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) ∧ (¬ 𝑅 (𝑃 𝑄) ∧ 𝑃𝑄 ∧ ¬ 𝑄 (𝑃 𝑈)) ∧ ((𝑅 𝑄) 𝑃) ((𝑆 𝑇) 𝑃)) → 𝑄𝐴)
20 simp121 1303 . . . . . . 7 (((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) ∧ (¬ 𝑅 (𝑃 𝑄) ∧ 𝑃𝑄 ∧ ¬ 𝑄 (𝑃 𝑈)) ∧ ((𝑅 𝑄) 𝑃) ((𝑆 𝑇) 𝑃)) → 𝑃𝐴)
2118, 19, 203jca 1126 . . . . . 6 (((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) ∧ (¬ 𝑅 (𝑃 𝑄) ∧ 𝑃𝑄 ∧ ¬ 𝑄 (𝑃 𝑈)) ∧ ((𝑅 𝑄) 𝑃) ((𝑆 𝑇) 𝑃)) → (𝑅𝐴𝑄𝐴𝑃𝐴))
22 simp131 1306 . . . . . . 7 (((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) ∧ (¬ 𝑅 (𝑃 𝑄) ∧ 𝑃𝑄 ∧ ¬ 𝑄 (𝑃 𝑈)) ∧ ((𝑅 𝑄) 𝑃) ((𝑆 𝑇) 𝑃)) → 𝑆𝐴)
23 simp132 1307 . . . . . . 7 (((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) ∧ (¬ 𝑅 (𝑃 𝑄) ∧ 𝑃𝑄 ∧ ¬ 𝑄 (𝑃 𝑈)) ∧ ((𝑅 𝑄) 𝑃) ((𝑆 𝑇) 𝑃)) → 𝑇𝐴)
2422, 23jca 516 . . . . . 6 (((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) ∧ (¬ 𝑅 (𝑃 𝑄) ∧ 𝑃𝑄 ∧ ¬ 𝑄 (𝑃 𝑈)) ∧ ((𝑅 𝑄) 𝑃) ((𝑆 𝑇) 𝑃)) → (𝑆𝐴𝑇𝐴))
25 simp21 1204 . . . . . . 7 (((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) ∧ (¬ 𝑅 (𝑃 𝑄) ∧ 𝑃𝑄 ∧ ¬ 𝑄 (𝑃 𝑈)) ∧ ((𝑅 𝑄) 𝑃) ((𝑆 𝑇) 𝑃)) → ¬ 𝑅 (𝑃 𝑄))
26 simp22 1205 . . . . . . . 8 (((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) ∧ (¬ 𝑅 (𝑃 𝑄) ∧ 𝑃𝑄 ∧ ¬ 𝑄 (𝑃 𝑈)) ∧ ((𝑅 𝑄) 𝑃) ((𝑆 𝑇) 𝑃)) → 𝑃𝑄)
2711, 12, 13hlatexch2 36965 . . . . . . . 8 ((𝐾 ∈ HL ∧ (𝑃𝐴𝑅𝐴𝑄𝐴) ∧ 𝑃𝑄) → (𝑃 (𝑅 𝑄) → 𝑅 (𝑃 𝑄)))
2817, 20, 18, 19, 26, 27syl131anc 1381 . . . . . . 7 (((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) ∧ (¬ 𝑅 (𝑃 𝑄) ∧ 𝑃𝑄 ∧ ¬ 𝑄 (𝑃 𝑈)) ∧ ((𝑅 𝑄) 𝑃) ((𝑆 𝑇) 𝑃)) → (𝑃 (𝑅 𝑄) → 𝑅 (𝑃 𝑄)))
2925, 28mtod 201 . . . . . 6 (((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) ∧ (¬ 𝑅 (𝑃 𝑄) ∧ 𝑃𝑄 ∧ ¬ 𝑄 (𝑃 𝑈)) ∧ ((𝑅 𝑄) 𝑃) ((𝑆 𝑇) 𝑃)) → ¬ 𝑃 (𝑅 𝑄))
3017hllatd 36933 . . . . . . 7 (((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) ∧ (¬ 𝑅 (𝑃 𝑄) ∧ 𝑃𝑄 ∧ ¬ 𝑄 (𝑃 𝑈)) ∧ ((𝑅 𝑄) 𝑃) ((𝑆 𝑇) 𝑃)) → 𝐾 ∈ Lat)
31 eqid 2759 . . . . . . . . 9 (Base‘𝐾) = (Base‘𝐾)
3231, 13atbase 36858 . . . . . . . 8 (𝑅𝐴𝑅 ∈ (Base‘𝐾))
3318, 32syl 17 . . . . . . 7 (((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) ∧ (¬ 𝑅 (𝑃 𝑄) ∧ 𝑃𝑄 ∧ ¬ 𝑄 (𝑃 𝑈)) ∧ ((𝑅 𝑄) 𝑃) ((𝑆 𝑇) 𝑃)) → 𝑅 ∈ (Base‘𝐾))
3431, 13atbase 36858 . . . . . . . 8 (𝑃𝐴𝑃 ∈ (Base‘𝐾))
3520, 34syl 17 . . . . . . 7 (((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) ∧ (¬ 𝑅 (𝑃 𝑄) ∧ 𝑃𝑄 ∧ ¬ 𝑄 (𝑃 𝑈)) ∧ ((𝑅 𝑄) 𝑃) ((𝑆 𝑇) 𝑃)) → 𝑃 ∈ (Base‘𝐾))
3631, 13atbase 36858 . . . . . . . 8 (𝑄𝐴𝑄 ∈ (Base‘𝐾))
3719, 36syl 17 . . . . . . 7 (((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) ∧ (¬ 𝑅 (𝑃 𝑄) ∧ 𝑃𝑄 ∧ ¬ 𝑄 (𝑃 𝑈)) ∧ ((𝑅 𝑄) 𝑃) ((𝑆 𝑇) 𝑃)) → 𝑄 ∈ (Base‘𝐾))
3831, 11, 12latnlej1r 17739 . . . . . . 7 ((𝐾 ∈ Lat ∧ (𝑅 ∈ (Base‘𝐾) ∧ 𝑃 ∈ (Base‘𝐾) ∧ 𝑄 ∈ (Base‘𝐾)) ∧ ¬ 𝑅 (𝑃 𝑄)) → 𝑅𝑄)
3930, 33, 35, 37, 25, 38syl131anc 1381 . . . . . 6 (((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) ∧ (¬ 𝑅 (𝑃 𝑄) ∧ 𝑃𝑄 ∧ ¬ 𝑄 (𝑃 𝑈)) ∧ ((𝑅 𝑄) 𝑃) ((𝑆 𝑇) 𝑃)) → 𝑅𝑄)
40 simp3 1136 . . . . . 6 (((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) ∧ (¬ 𝑅 (𝑃 𝑄) ∧ 𝑃𝑄 ∧ ¬ 𝑄 (𝑃 𝑈)) ∧ ((𝑅 𝑄) 𝑃) ((𝑆 𝑇) 𝑃)) → ((𝑅 𝑄) 𝑃) ((𝑆 𝑇) 𝑃))
4111, 12, 133atlem4 37055 . . . . . 6 (((𝐾 ∈ HL ∧ (𝑅𝐴𝑄𝐴𝑃𝐴) ∧ (𝑆𝐴𝑇𝐴)) ∧ (¬ 𝑃 (𝑅 𝑄) ∧ 𝑅𝑄) ∧ ((𝑅 𝑄) 𝑃) ((𝑆 𝑇) 𝑃)) → ((𝑅 𝑄) 𝑃) = ((𝑆 𝑇) 𝑃))
4217, 21, 24, 29, 39, 40, 41syl321anc 1390 . . . . 5 (((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) ∧ (¬ 𝑅 (𝑃 𝑄) ∧ 𝑃𝑄 ∧ ¬ 𝑄 (𝑃 𝑈)) ∧ ((𝑅 𝑄) 𝑃) ((𝑆 𝑇) 𝑃)) → ((𝑅 𝑄) 𝑃) = ((𝑆 𝑇) 𝑃))
43423expia 1119 . . . 4 (((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) ∧ (¬ 𝑅 (𝑃 𝑄) ∧ 𝑃𝑄 ∧ ¬ 𝑄 (𝑃 𝑈))) → (((𝑅 𝑄) 𝑃) ((𝑆 𝑇) 𝑃) → ((𝑅 𝑄) 𝑃) = ((𝑆 𝑇) 𝑃)))
44 simpl1 1189 . . . . . . 7 (((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) ∧ (¬ 𝑅 (𝑃 𝑄) ∧ 𝑃𝑄 ∧ ¬ 𝑄 (𝑃 𝑈))) → 𝐾 ∈ HL)
4544hllatd 36933 . . . . . 6 (((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) ∧ (¬ 𝑅 (𝑃 𝑄) ∧ 𝑃𝑄 ∧ ¬ 𝑄 (𝑃 𝑈))) → 𝐾 ∈ Lat)
46 simpl21 1249 . . . . . . 7 (((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) ∧ (¬ 𝑅 (𝑃 𝑄) ∧ 𝑃𝑄 ∧ ¬ 𝑄 (𝑃 𝑈))) → 𝑃𝐴)
4746, 34syl 17 . . . . . 6 (((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) ∧ (¬ 𝑅 (𝑃 𝑄) ∧ 𝑃𝑄 ∧ ¬ 𝑄 (𝑃 𝑈))) → 𝑃 ∈ (Base‘𝐾))
48 simpl22 1250 . . . . . . 7 (((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) ∧ (¬ 𝑅 (𝑃 𝑄) ∧ 𝑃𝑄 ∧ ¬ 𝑄 (𝑃 𝑈))) → 𝑄𝐴)
4948, 36syl 17 . . . . . 6 (((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) ∧ (¬ 𝑅 (𝑃 𝑄) ∧ 𝑃𝑄 ∧ ¬ 𝑄 (𝑃 𝑈))) → 𝑄 ∈ (Base‘𝐾))
50 simpl23 1251 . . . . . . 7 (((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) ∧ (¬ 𝑅 (𝑃 𝑄) ∧ 𝑃𝑄 ∧ ¬ 𝑄 (𝑃 𝑈))) → 𝑅𝐴)
5150, 32syl 17 . . . . . 6 (((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) ∧ (¬ 𝑅 (𝑃 𝑄) ∧ 𝑃𝑄 ∧ ¬ 𝑄 (𝑃 𝑈))) → 𝑅 ∈ (Base‘𝐾))
5231, 12latj31 17768 . . . . . 6 ((𝐾 ∈ Lat ∧ (𝑃 ∈ (Base‘𝐾) ∧ 𝑄 ∈ (Base‘𝐾) ∧ 𝑅 ∈ (Base‘𝐾))) → ((𝑃 𝑄) 𝑅) = ((𝑅 𝑄) 𝑃))
5345, 47, 49, 51, 52syl13anc 1370 . . . . 5 (((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) ∧ (¬ 𝑅 (𝑃 𝑄) ∧ 𝑃𝑄 ∧ ¬ 𝑄 (𝑃 𝑈))) → ((𝑃 𝑄) 𝑅) = ((𝑅 𝑄) 𝑃))
5453breq1d 5043 . . . 4 (((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) ∧ (¬ 𝑅 (𝑃 𝑄) ∧ 𝑃𝑄 ∧ ¬ 𝑄 (𝑃 𝑈))) → (((𝑃 𝑄) 𝑅) ((𝑆 𝑇) 𝑃) ↔ ((𝑅 𝑄) 𝑃) ((𝑆 𝑇) 𝑃)))
5553eqeq1d 2761 . . . 4 (((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) ∧ (¬ 𝑅 (𝑃 𝑄) ∧ 𝑃𝑄 ∧ ¬ 𝑄 (𝑃 𝑈))) → (((𝑃 𝑄) 𝑅) = ((𝑆 𝑇) 𝑃) ↔ ((𝑅 𝑄) 𝑃) = ((𝑆 𝑇) 𝑃)))
5643, 54, 553imtr4d 298 . . 3 (((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) ∧ (¬ 𝑅 (𝑃 𝑄) ∧ 𝑃𝑄 ∧ ¬ 𝑄 (𝑃 𝑈))) → (((𝑃 𝑄) 𝑅) ((𝑆 𝑇) 𝑃) → ((𝑃 𝑄) 𝑅) = ((𝑆 𝑇) 𝑃)))
575, 16, 56pm2.61ne 3037 . 2 (((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) ∧ (¬ 𝑅 (𝑃 𝑄) ∧ 𝑃𝑄 ∧ ¬ 𝑄 (𝑃 𝑈))) → (((𝑃 𝑄) 𝑅) ((𝑆 𝑇) 𝑈) → ((𝑃 𝑄) 𝑅) = ((𝑆 𝑇) 𝑈)))
58573impia 1115 1 (((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑅𝐴) ∧ (𝑆𝐴𝑇𝐴𝑈𝐴)) ∧ (¬ 𝑅 (𝑃 𝑄) ∧ 𝑃𝑄 ∧ ¬ 𝑄 (𝑃 𝑈)) ∧ ((𝑃 𝑄) 𝑅) ((𝑆 𝑇) 𝑈)) → ((𝑃 𝑄) 𝑅) = ((𝑆 𝑇) 𝑈))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 400   ∧ w3a 1085   = wceq 1539   ∈ wcel 2112   ≠ wne 2952   class class class wbr 5033  ‘cfv 6336  (class class class)co 7151  Basecbs 16534  lecple 16623  joincjn 17613  Latclat 17714  Atomscatm 36832  HLchlt 36919 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2730  ax-rep 5157  ax-sep 5170  ax-nul 5177  ax-pow 5235  ax-pr 5299  ax-un 7460 This theorem depends on definitions:  df-bi 210  df-an 401  df-or 846  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2071  df-mo 2558  df-eu 2589  df-clab 2737  df-cleq 2751  df-clel 2831  df-nfc 2902  df-ne 2953  df-ral 3076  df-rex 3077  df-reu 3078  df-rab 3080  df-v 3412  df-sbc 3698  df-csb 3807  df-dif 3862  df-un 3864  df-in 3866  df-ss 3876  df-nul 4227  df-if 4422  df-pw 4497  df-sn 4524  df-pr 4526  df-op 4530  df-uni 4800  df-iun 4886  df-br 5034  df-opab 5096  df-mpt 5114  df-id 5431  df-xp 5531  df-rel 5532  df-cnv 5533  df-co 5534  df-dm 5535  df-rn 5536  df-res 5537  df-ima 5538  df-iota 6295  df-fun 6338  df-fn 6339  df-f 6340  df-f1 6341  df-fo 6342  df-f1o 6343  df-fv 6344  df-riota 7109  df-ov 7154  df-oprab 7155  df-proset 17597  df-poset 17615  df-plt 17627  df-lub 17643  df-glb 17644  df-join 17645  df-meet 17646  df-p0 17708  df-lat 17715  df-covers 36835  df-ats 36836  df-atl 36867  df-cvlat 36891  df-hlat 36920 This theorem is referenced by:  3atlem6  37057  3atlem7  37058
 Copyright terms: Public domain W3C validator