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

Theorem cdlemk22 36703
 Description: Part of proof of Lemma K of [Crawley] p. 118. Lines 26-27, p. 119 for i=1 and j=2. (Contributed by NM, 5-Jul-2013.)
Hypotheses
Ref Expression
cdlemk2.b 𝐵 = (Base‘𝐾)
cdlemk2.l = (le‘𝐾)
cdlemk2.j = (join‘𝐾)
cdlemk2.m = (meet‘𝐾)
cdlemk2.a 𝐴 = (Atoms‘𝐾)
cdlemk2.h 𝐻 = (LHyp‘𝐾)
cdlemk2.t 𝑇 = ((LTrn‘𝐾)‘𝑊)
cdlemk2.r 𝑅 = ((trL‘𝐾)‘𝑊)
cdlemk2.s 𝑆 = (𝑓𝑇 ↦ (𝑖𝑇 (𝑖𝑃) = ((𝑃 (𝑅𝑓)) ((𝑁𝑃) (𝑅‘(𝑓𝐹))))))
cdlemk2.q 𝑄 = (𝑆𝐶)
cdlemk2.v 𝑉 = (𝑑𝑇 ↦ (𝑘𝑇 (𝑘𝑃) = ((𝑃 (𝑅𝑑)) ((𝑄𝑃) (𝑅‘(𝑑𝐶))))))
cdlemk2a.o 𝑂 = (𝑆𝐷)
cdlemk2.u 𝑈 = (𝑒𝑇 ↦ (𝑗𝑇 (𝑗𝑃) = ((𝑃 (𝑅𝑒)) ((𝑂𝑃) (𝑅‘(𝑒𝐷))))))
Assertion
Ref Expression
cdlemk22 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇𝐷𝑇) ∧ ((𝑁𝑇𝐺𝑇𝐶𝑇) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑅𝐹) = (𝑅𝑁)) ∧ ((𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐷 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵)) ∧ (𝐶 ≠ ( I ↾ 𝐵) ∧ (𝑅𝐺) ≠ (𝑅𝐶) ∧ (𝑅𝐶) ≠ (𝑅𝐹)) ∧ ((𝑅𝐷) ≠ (𝑅𝐹) ∧ (𝑅𝐺) ≠ (𝑅𝐷) ∧ (𝑅𝐶) ≠ (𝑅𝐷)))) → ((𝑈𝐺)‘𝑃) = ((𝑉𝐺)‘𝑃))
Distinct variable groups:   𝑓,𝑖,   ,𝑖   ,𝑓,𝑖   𝐴,𝑖   𝐶,𝑓,𝑖   𝑓,𝐹,𝑖   𝑖,𝐻   𝑖,𝐾   𝑓,𝑁,𝑖   𝑃,𝑓,𝑖   𝑅,𝑓,𝑖   𝑇,𝑓,𝑖   𝑓,𝑊,𝑖   ,𝑑   ,𝑑   𝐶,𝑑,𝑘   𝐺,𝑑,𝑘   𝑄,𝑑   𝑃,𝑑   𝑅,𝑑   𝑇,𝑑   𝑊,𝑑   ,𝑘   ,𝑘   ,𝑘   𝐴,𝑘   𝐶,𝑘   𝑘,𝐹   𝑘,𝐻   𝑘,𝐾   𝑘,𝑁   𝑄,𝑘   𝑃,𝑘   𝑅,𝑘   𝑇,𝑘   𝑘,𝑊   𝐹,𝑑   𝑖,𝐺,𝑓,𝑘   𝐷,𝑘   𝑖,𝑑,𝐷,𝑓   𝑒,𝑗,   ,𝑒,𝑗   ,𝑒,𝑗   𝐴,𝑗   𝐶,𝑒,𝑗   𝐷,𝑒,𝑗   𝑒,𝐹,𝑗   𝑒,𝐺,𝑗   𝑗,𝐻   𝑗,𝐾   𝑗,𝑁   𝑒,𝑂,𝑗   𝑃,𝑒,𝑗   𝑅,𝑒,𝑗   𝑇,𝑒,𝑗   𝑒,𝑊,𝑗,𝑓,𝑖
Allowed substitution hints:   𝐴(𝑒,𝑓,𝑑)   𝐵(𝑒,𝑓,𝑖,𝑗,𝑘,𝑑)   𝑄(𝑒,𝑓,𝑖,𝑗)   𝑆(𝑒,𝑓,𝑖,𝑗,𝑘,𝑑)   𝑈(𝑒,𝑓,𝑖,𝑗,𝑘,𝑑)   𝐻(𝑒,𝑓,𝑑)   𝐾(𝑒,𝑓,𝑑)   (𝑓,𝑑)   𝑁(𝑒,𝑑)   𝑂(𝑓,𝑖,𝑘,𝑑)   𝑉(𝑒,𝑓,𝑖,𝑗,𝑘,𝑑)

Proof of Theorem cdlemk22
StepHypRef Expression
1 simp11 1245 . . . 4 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇𝐷𝑇) ∧ ((𝑁𝑇𝐺𝑇𝐶𝑇) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑅𝐹) = (𝑅𝑁)) ∧ ((𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐷 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵)) ∧ (𝐶 ≠ ( I ↾ 𝐵) ∧ (𝑅𝐺) ≠ (𝑅𝐶) ∧ (𝑅𝐶) ≠ (𝑅𝐹)) ∧ ((𝑅𝐷) ≠ (𝑅𝐹) ∧ (𝑅𝐺) ≠ (𝑅𝐷) ∧ (𝑅𝐶) ≠ (𝑅𝐷)))) → (𝐾 ∈ HL ∧ 𝑊𝐻))
2 simp212 1396 . . . 4 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇𝐷𝑇) ∧ ((𝑁𝑇𝐺𝑇𝐶𝑇) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑅𝐹) = (𝑅𝑁)) ∧ ((𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐷 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵)) ∧ (𝐶 ≠ ( I ↾ 𝐵) ∧ (𝑅𝐺) ≠ (𝑅𝐶) ∧ (𝑅𝐶) ≠ (𝑅𝐹)) ∧ ((𝑅𝐷) ≠ (𝑅𝐹) ∧ (𝑅𝐺) ≠ (𝑅𝐷) ∧ (𝑅𝐶) ≠ (𝑅𝐷)))) → 𝐺𝑇)
3 simp22 1249 . . . 4 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇𝐷𝑇) ∧ ((𝑁𝑇𝐺𝑇𝐶𝑇) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑅𝐹) = (𝑅𝑁)) ∧ ((𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐷 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵)) ∧ (𝐶 ≠ ( I ↾ 𝐵) ∧ (𝑅𝐺) ≠ (𝑅𝐶) ∧ (𝑅𝐶) ≠ (𝑅𝐹)) ∧ ((𝑅𝐷) ≠ (𝑅𝐹) ∧ (𝑅𝐺) ≠ (𝑅𝐷) ∧ (𝑅𝐶) ≠ (𝑅𝐷)))) → (𝑃𝐴 ∧ ¬ 𝑃 𝑊))
4 cdlemk2.l . . . . 5 = (le‘𝐾)
5 cdlemk2.j . . . . 5 = (join‘𝐾)
6 cdlemk2.a . . . . 5 𝐴 = (Atoms‘𝐾)
7 cdlemk2.h . . . . 5 𝐻 = (LHyp‘𝐾)
8 cdlemk2.t . . . . 5 𝑇 = ((LTrn‘𝐾)‘𝑊)
9 cdlemk2.r . . . . 5 𝑅 = ((trL‘𝐾)‘𝑊)
104, 5, 6, 7, 8, 9trljat1 35976 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐺𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → (𝑃 (𝑅𝐺)) = (𝑃 (𝐺𝑃)))
111, 2, 3, 10syl3anc 1476 . . 3 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇𝐷𝑇) ∧ ((𝑁𝑇𝐺𝑇𝐶𝑇) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑅𝐹) = (𝑅𝑁)) ∧ ((𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐷 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵)) ∧ (𝐶 ≠ ( I ↾ 𝐵) ∧ (𝑅𝐺) ≠ (𝑅𝐶) ∧ (𝑅𝐶) ≠ (𝑅𝐹)) ∧ ((𝑅𝐷) ≠ (𝑅𝐹) ∧ (𝑅𝐺) ≠ (𝑅𝐷) ∧ (𝑅𝐶) ≠ (𝑅𝐷)))) → (𝑃 (𝑅𝐺)) = (𝑃 (𝐺𝑃)))
12 simp1 1130 . . . . . 6 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇𝐷𝑇) ∧ ((𝑁𝑇𝐺𝑇𝐶𝑇) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑅𝐹) = (𝑅𝑁)) ∧ ((𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐷 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵)) ∧ (𝐶 ≠ ( I ↾ 𝐵) ∧ (𝑅𝐺) ≠ (𝑅𝐶) ∧ (𝑅𝐶) ≠ (𝑅𝐹)) ∧ ((𝑅𝐷) ≠ (𝑅𝐹) ∧ (𝑅𝐺) ≠ (𝑅𝐷) ∧ (𝑅𝐶) ≠ (𝑅𝐷)))) → ((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇𝐷𝑇))
13 simp211 1395 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇𝐷𝑇) ∧ ((𝑁𝑇𝐺𝑇𝐶𝑇) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑅𝐹) = (𝑅𝑁)) ∧ ((𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐷 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵)) ∧ (𝐶 ≠ ( I ↾ 𝐵) ∧ (𝑅𝐺) ≠ (𝑅𝐶) ∧ (𝑅𝐶) ≠ (𝑅𝐹)) ∧ ((𝑅𝐷) ≠ (𝑅𝐹) ∧ (𝑅𝐺) ≠ (𝑅𝐷) ∧ (𝑅𝐶) ≠ (𝑅𝐷)))) → 𝑁𝑇)
14 simp213 1397 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇𝐷𝑇) ∧ ((𝑁𝑇𝐺𝑇𝐶𝑇) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑅𝐹) = (𝑅𝑁)) ∧ ((𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐷 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵)) ∧ (𝐶 ≠ ( I ↾ 𝐵) ∧ (𝑅𝐺) ≠ (𝑅𝐶) ∧ (𝑅𝐶) ≠ (𝑅𝐹)) ∧ ((𝑅𝐷) ≠ (𝑅𝐹) ∧ (𝑅𝐺) ≠ (𝑅𝐷) ∧ (𝑅𝐶) ≠ (𝑅𝐷)))) → 𝐶𝑇)
1513, 14jca 501 . . . . . 6 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇𝐷𝑇) ∧ ((𝑁𝑇𝐺𝑇𝐶𝑇) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑅𝐹) = (𝑅𝑁)) ∧ ((𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐷 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵)) ∧ (𝐶 ≠ ( I ↾ 𝐵) ∧ (𝑅𝐺) ≠ (𝑅𝐶) ∧ (𝑅𝐶) ≠ (𝑅𝐹)) ∧ ((𝑅𝐷) ≠ (𝑅𝐹) ∧ (𝑅𝐺) ≠ (𝑅𝐷) ∧ (𝑅𝐶) ≠ (𝑅𝐷)))) → (𝑁𝑇𝐶𝑇))
16 simp23 1250 . . . . . 6 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇𝐷𝑇) ∧ ((𝑁𝑇𝐺𝑇𝐶𝑇) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑅𝐹) = (𝑅𝑁)) ∧ ((𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐷 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵)) ∧ (𝐶 ≠ ( I ↾ 𝐵) ∧ (𝑅𝐺) ≠ (𝑅𝐶) ∧ (𝑅𝐶) ≠ (𝑅𝐹)) ∧ ((𝑅𝐷) ≠ (𝑅𝐹) ∧ (𝑅𝐺) ≠ (𝑅𝐷) ∧ (𝑅𝐶) ≠ (𝑅𝐷)))) → (𝑅𝐹) = (𝑅𝑁))
17 simp311 1404 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇𝐷𝑇) ∧ ((𝑁𝑇𝐺𝑇𝐶𝑇) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑅𝐹) = (𝑅𝑁)) ∧ ((𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐷 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵)) ∧ (𝐶 ≠ ( I ↾ 𝐵) ∧ (𝑅𝐺) ≠ (𝑅𝐶) ∧ (𝑅𝐶) ≠ (𝑅𝐹)) ∧ ((𝑅𝐷) ≠ (𝑅𝐹) ∧ (𝑅𝐺) ≠ (𝑅𝐷) ∧ (𝑅𝐶) ≠ (𝑅𝐷)))) → 𝐹 ≠ ( I ↾ 𝐵))
18 simp312 1405 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇𝐷𝑇) ∧ ((𝑁𝑇𝐺𝑇𝐶𝑇) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑅𝐹) = (𝑅𝑁)) ∧ ((𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐷 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵)) ∧ (𝐶 ≠ ( I ↾ 𝐵) ∧ (𝑅𝐺) ≠ (𝑅𝐶) ∧ (𝑅𝐶) ≠ (𝑅𝐹)) ∧ ((𝑅𝐷) ≠ (𝑅𝐹) ∧ (𝑅𝐺) ≠ (𝑅𝐷) ∧ (𝑅𝐶) ≠ (𝑅𝐷)))) → 𝐷 ≠ ( I ↾ 𝐵))
19 simp321 1407 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇𝐷𝑇) ∧ ((𝑁𝑇𝐺𝑇𝐶𝑇) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑅𝐹) = (𝑅𝑁)) ∧ ((𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐷 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵)) ∧ (𝐶 ≠ ( I ↾ 𝐵) ∧ (𝑅𝐺) ≠ (𝑅𝐶) ∧ (𝑅𝐶) ≠ (𝑅𝐹)) ∧ ((𝑅𝐷) ≠ (𝑅𝐹) ∧ (𝑅𝐺) ≠ (𝑅𝐷) ∧ (𝑅𝐶) ≠ (𝑅𝐷)))) → 𝐶 ≠ ( I ↾ 𝐵))
2017, 18, 193jca 1122 . . . . . 6 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇𝐷𝑇) ∧ ((𝑁𝑇𝐺𝑇𝐶𝑇) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑅𝐹) = (𝑅𝑁)) ∧ ((𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐷 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵)) ∧ (𝐶 ≠ ( I ↾ 𝐵) ∧ (𝑅𝐺) ≠ (𝑅𝐶) ∧ (𝑅𝐶) ≠ (𝑅𝐹)) ∧ ((𝑅𝐷) ≠ (𝑅𝐹) ∧ (𝑅𝐺) ≠ (𝑅𝐷) ∧ (𝑅𝐶) ≠ (𝑅𝐷)))) → (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐷 ≠ ( I ↾ 𝐵) ∧ 𝐶 ≠ ( I ↾ 𝐵)))
21 simp331 1410 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇𝐷𝑇) ∧ ((𝑁𝑇𝐺𝑇𝐶𝑇) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑅𝐹) = (𝑅𝑁)) ∧ ((𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐷 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵)) ∧ (𝐶 ≠ ( I ↾ 𝐵) ∧ (𝑅𝐺) ≠ (𝑅𝐶) ∧ (𝑅𝐶) ≠ (𝑅𝐹)) ∧ ((𝑅𝐷) ≠ (𝑅𝐹) ∧ (𝑅𝐺) ≠ (𝑅𝐷) ∧ (𝑅𝐶) ≠ (𝑅𝐷)))) → (𝑅𝐷) ≠ (𝑅𝐹))
22 simp323 1409 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇𝐷𝑇) ∧ ((𝑁𝑇𝐺𝑇𝐶𝑇) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑅𝐹) = (𝑅𝑁)) ∧ ((𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐷 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵)) ∧ (𝐶 ≠ ( I ↾ 𝐵) ∧ (𝑅𝐺) ≠ (𝑅𝐶) ∧ (𝑅𝐶) ≠ (𝑅𝐹)) ∧ ((𝑅𝐷) ≠ (𝑅𝐹) ∧ (𝑅𝐺) ≠ (𝑅𝐷) ∧ (𝑅𝐶) ≠ (𝑅𝐷)))) → (𝑅𝐶) ≠ (𝑅𝐹))
23 simp333 1412 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇𝐷𝑇) ∧ ((𝑁𝑇𝐺𝑇𝐶𝑇) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑅𝐹) = (𝑅𝑁)) ∧ ((𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐷 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵)) ∧ (𝐶 ≠ ( I ↾ 𝐵) ∧ (𝑅𝐺) ≠ (𝑅𝐶) ∧ (𝑅𝐶) ≠ (𝑅𝐹)) ∧ ((𝑅𝐷) ≠ (𝑅𝐹) ∧ (𝑅𝐺) ≠ (𝑅𝐷) ∧ (𝑅𝐶) ≠ (𝑅𝐷)))) → (𝑅𝐶) ≠ (𝑅𝐷))
2421, 22, 233jca 1122 . . . . . 6 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇𝐷𝑇) ∧ ((𝑁𝑇𝐺𝑇𝐶𝑇) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑅𝐹) = (𝑅𝑁)) ∧ ((𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐷 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵)) ∧ (𝐶 ≠ ( I ↾ 𝐵) ∧ (𝑅𝐺) ≠ (𝑅𝐶) ∧ (𝑅𝐶) ≠ (𝑅𝐹)) ∧ ((𝑅𝐷) ≠ (𝑅𝐹) ∧ (𝑅𝐺) ≠ (𝑅𝐷) ∧ (𝑅𝐶) ≠ (𝑅𝐷)))) → ((𝑅𝐷) ≠ (𝑅𝐹) ∧ (𝑅𝐶) ≠ (𝑅𝐹) ∧ (𝑅𝐶) ≠ (𝑅𝐷)))
25 cdlemk2.b . . . . . . 7 𝐵 = (Base‘𝐾)
26 cdlemk2.m . . . . . . 7 = (meet‘𝐾)
27 cdlemk2.s . . . . . . 7 𝑆 = (𝑓𝑇 ↦ (𝑖𝑇 (𝑖𝑃) = ((𝑃 (𝑅𝑓)) ((𝑁𝑃) (𝑅‘(𝑓𝐹))))))
28 cdlemk2a.o . . . . . . 7 𝑂 = (𝑆𝐷)
29 cdlemk2.u . . . . . . 7 𝑈 = (𝑒𝑇 ↦ (𝑗𝑇 (𝑗𝑃) = ((𝑃 (𝑅𝑒)) ((𝑂𝑃) (𝑅‘(𝑒𝐷))))))
30 cdlemk2.q . . . . . . 7 𝑄 = (𝑆𝐶)
3125, 4, 5, 26, 6, 7, 8, 9, 27, 28, 29, 30cdlemk20 36684 . . . . . 6 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇𝐷𝑇) ∧ ((𝑁𝑇𝐶𝑇) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑅𝐹) = (𝑅𝑁)) ∧ ((𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐷 ≠ ( I ↾ 𝐵) ∧ 𝐶 ≠ ( I ↾ 𝐵)) ∧ ((𝑅𝐷) ≠ (𝑅𝐹) ∧ (𝑅𝐶) ≠ (𝑅𝐹) ∧ (𝑅𝐶) ≠ (𝑅𝐷)))) → ((𝑈𝐶)‘𝑃) = (𝑄𝑃))
3212, 15, 3, 16, 20, 24, 31syl132anc 1494 . . . . 5 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇𝐷𝑇) ∧ ((𝑁𝑇𝐺𝑇𝐶𝑇) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑅𝐹) = (𝑅𝑁)) ∧ ((𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐷 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵)) ∧ (𝐶 ≠ ( I ↾ 𝐵) ∧ (𝑅𝐺) ≠ (𝑅𝐶) ∧ (𝑅𝐶) ≠ (𝑅𝐹)) ∧ ((𝑅𝐷) ≠ (𝑅𝐹) ∧ (𝑅𝐺) ≠ (𝑅𝐷) ∧ (𝑅𝐶) ≠ (𝑅𝐷)))) → ((𝑈𝐶)‘𝑃) = (𝑄𝑃))
3332eqcomd 2777 . . . 4 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇𝐷𝑇) ∧ ((𝑁𝑇𝐺𝑇𝐶𝑇) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑅𝐹) = (𝑅𝑁)) ∧ ((𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐷 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵)) ∧ (𝐶 ≠ ( I ↾ 𝐵) ∧ (𝑅𝐺) ≠ (𝑅𝐶) ∧ (𝑅𝐶) ≠ (𝑅𝐹)) ∧ ((𝑅𝐷) ≠ (𝑅𝐹) ∧ (𝑅𝐺) ≠ (𝑅𝐷) ∧ (𝑅𝐶) ≠ (𝑅𝐷)))) → (𝑄𝑃) = ((𝑈𝐶)‘𝑃))
347, 8, 9trlcocnv 36530 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐺𝑇𝐶𝑇) → (𝑅‘(𝐺𝐶)) = (𝑅‘(𝐶𝐺)))
351, 2, 14, 34syl3anc 1476 . . . 4 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇𝐷𝑇) ∧ ((𝑁𝑇𝐺𝑇𝐶𝑇) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑅𝐹) = (𝑅𝑁)) ∧ ((𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐷 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵)) ∧ (𝐶 ≠ ( I ↾ 𝐵) ∧ (𝑅𝐺) ≠ (𝑅𝐶) ∧ (𝑅𝐶) ≠ (𝑅𝐹)) ∧ ((𝑅𝐷) ≠ (𝑅𝐹) ∧ (𝑅𝐺) ≠ (𝑅𝐷) ∧ (𝑅𝐶) ≠ (𝑅𝐷)))) → (𝑅‘(𝐺𝐶)) = (𝑅‘(𝐶𝐺)))
3633, 35oveq12d 6814 . . 3 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇𝐷𝑇) ∧ ((𝑁𝑇𝐺𝑇𝐶𝑇) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑅𝐹) = (𝑅𝑁)) ∧ ((𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐷 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵)) ∧ (𝐶 ≠ ( I ↾ 𝐵) ∧ (𝑅𝐺) ≠ (𝑅𝐶) ∧ (𝑅𝐶) ≠ (𝑅𝐹)) ∧ ((𝑅𝐷) ≠ (𝑅𝐹) ∧ (𝑅𝐺) ≠ (𝑅𝐷) ∧ (𝑅𝐶) ≠ (𝑅𝐷)))) → ((𝑄𝑃) (𝑅‘(𝐺𝐶))) = (((𝑈𝐶)‘𝑃) (𝑅‘(𝐶𝐺))))
3711, 36oveq12d 6814 . 2 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇𝐷𝑇) ∧ ((𝑁𝑇𝐺𝑇𝐶𝑇) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑅𝐹) = (𝑅𝑁)) ∧ ((𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐷 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵)) ∧ (𝐶 ≠ ( I ↾ 𝐵) ∧ (𝑅𝐺) ≠ (𝑅𝐶) ∧ (𝑅𝐶) ≠ (𝑅𝐹)) ∧ ((𝑅𝐷) ≠ (𝑅𝐹) ∧ (𝑅𝐺) ≠ (𝑅𝐷) ∧ (𝑅𝐶) ≠ (𝑅𝐷)))) → ((𝑃 (𝑅𝐺)) ((𝑄𝑃) (𝑅‘(𝐺𝐶)))) = ((𝑃 (𝐺𝑃)) (((𝑈𝐶)‘𝑃) (𝑅‘(𝐶𝐺)))))
38 simp12 1246 . . 3 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇𝐷𝑇) ∧ ((𝑁𝑇𝐺𝑇𝐶𝑇) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑅𝐹) = (𝑅𝑁)) ∧ ((𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐷 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵)) ∧ (𝐶 ≠ ( I ↾ 𝐵) ∧ (𝑅𝐺) ≠ (𝑅𝐶) ∧ (𝑅𝐶) ≠ (𝑅𝐹)) ∧ ((𝑅𝐷) ≠ (𝑅𝐹) ∧ (𝑅𝐺) ≠ (𝑅𝐷) ∧ (𝑅𝐶) ≠ (𝑅𝐷)))) → 𝐹𝑇)
39 simp322 1408 . . . . 5 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇𝐷𝑇) ∧ ((𝑁𝑇𝐺𝑇𝐶𝑇) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑅𝐹) = (𝑅𝑁)) ∧ ((𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐷 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵)) ∧ (𝐶 ≠ ( I ↾ 𝐵) ∧ (𝑅𝐺) ≠ (𝑅𝐶) ∧ (𝑅𝐶) ≠ (𝑅𝐹)) ∧ ((𝑅𝐷) ≠ (𝑅𝐹) ∧ (𝑅𝐺) ≠ (𝑅𝐷) ∧ (𝑅𝐶) ≠ (𝑅𝐷)))) → (𝑅𝐺) ≠ (𝑅𝐶))
4039necomd 2998 . . . 4 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇𝐷𝑇) ∧ ((𝑁𝑇𝐺𝑇𝐶𝑇) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑅𝐹) = (𝑅𝑁)) ∧ ((𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐷 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵)) ∧ (𝐶 ≠ ( I ↾ 𝐵) ∧ (𝑅𝐺) ≠ (𝑅𝐶) ∧ (𝑅𝐶) ≠ (𝑅𝐹)) ∧ ((𝑅𝐷) ≠ (𝑅𝐹) ∧ (𝑅𝐺) ≠ (𝑅𝐷) ∧ (𝑅𝐶) ≠ (𝑅𝐷)))) → (𝑅𝐶) ≠ (𝑅𝐺))
4122, 40jca 501 . . 3 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇𝐷𝑇) ∧ ((𝑁𝑇𝐺𝑇𝐶𝑇) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑅𝐹) = (𝑅𝑁)) ∧ ((𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐷 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵)) ∧ (𝐶 ≠ ( I ↾ 𝐵) ∧ (𝑅𝐺) ≠ (𝑅𝐶) ∧ (𝑅𝐶) ≠ (𝑅𝐹)) ∧ ((𝑅𝐷) ≠ (𝑅𝐹) ∧ (𝑅𝐺) ≠ (𝑅𝐷) ∧ (𝑅𝐶) ≠ (𝑅𝐷)))) → ((𝑅𝐶) ≠ (𝑅𝐹) ∧ (𝑅𝐶) ≠ (𝑅𝐺)))
42 simp313 1406 . . . 4 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇𝐷𝑇) ∧ ((𝑁𝑇𝐺𝑇𝐶𝑇) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑅𝐹) = (𝑅𝑁)) ∧ ((𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐷 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵)) ∧ (𝐶 ≠ ( I ↾ 𝐵) ∧ (𝑅𝐺) ≠ (𝑅𝐶) ∧ (𝑅𝐶) ≠ (𝑅𝐹)) ∧ ((𝑅𝐷) ≠ (𝑅𝐹) ∧ (𝑅𝐺) ≠ (𝑅𝐷) ∧ (𝑅𝐶) ≠ (𝑅𝐷)))) → 𝐺 ≠ ( I ↾ 𝐵))
4317, 42, 193jca 1122 . . 3 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇𝐷𝑇) ∧ ((𝑁𝑇𝐺𝑇𝐶𝑇) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑅𝐹) = (𝑅𝑁)) ∧ ((𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐷 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵)) ∧ (𝐶 ≠ ( I ↾ 𝐵) ∧ (𝑅𝐺) ≠ (𝑅𝐶) ∧ (𝑅𝐶) ≠ (𝑅𝐹)) ∧ ((𝑅𝐷) ≠ (𝑅𝐹) ∧ (𝑅𝐺) ≠ (𝑅𝐷) ∧ (𝑅𝐶) ≠ (𝑅𝐷)))) → (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ 𝐶 ≠ ( I ↾ 𝐵)))
44 cdlemk2.v . . . 4 𝑉 = (𝑑𝑇 ↦ (𝑘𝑇 (𝑘𝑃) = ((𝑃 (𝑅𝑑)) ((𝑄𝑃) (𝑅‘(𝑑𝐶))))))
4525, 4, 5, 26, 6, 7, 8, 9, 27, 30, 44cdlemkuv2-2 36695 . . 3 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑅𝐹) = (𝑅𝑁) ∧ 𝐺𝑇) ∧ (𝐹𝑇𝐶𝑇𝑁𝑇) ∧ (((𝑅𝐶) ≠ (𝑅𝐹) ∧ (𝑅𝐶) ≠ (𝑅𝐺)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ 𝐶 ≠ ( I ↾ 𝐵)) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊))) → ((𝑉𝐺)‘𝑃) = ((𝑃 (𝑅𝐺)) ((𝑄𝑃) (𝑅‘(𝐺𝐶)))))
461, 16, 2, 38, 14, 13, 41, 43, 3, 45syl333anc 1508 . 2 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇𝐷𝑇) ∧ ((𝑁𝑇𝐺𝑇𝐶𝑇) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑅𝐹) = (𝑅𝑁)) ∧ ((𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐷 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵)) ∧ (𝐶 ≠ ( I ↾ 𝐵) ∧ (𝑅𝐺) ≠ (𝑅𝐶) ∧ (𝑅𝐶) ≠ (𝑅𝐹)) ∧ ((𝑅𝐷) ≠ (𝑅𝐹) ∧ (𝑅𝐺) ≠ (𝑅𝐷) ∧ (𝑅𝐶) ≠ (𝑅𝐷)))) → ((𝑉𝐺)‘𝑃) = ((𝑃 (𝑅𝐺)) ((𝑄𝑃) (𝑅‘(𝐺𝐶)))))
47 simp31 1251 . . . 4 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇𝐷𝑇) ∧ ((𝑁𝑇𝐺𝑇𝐶𝑇) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑅𝐹) = (𝑅𝑁)) ∧ ((𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐷 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵)) ∧ (𝐶 ≠ ( I ↾ 𝐵) ∧ (𝑅𝐺) ≠ (𝑅𝐶) ∧ (𝑅𝐶) ≠ (𝑅𝐹)) ∧ ((𝑅𝐷) ≠ (𝑅𝐹) ∧ (𝑅𝐺) ≠ (𝑅𝐷) ∧ (𝑅𝐶) ≠ (𝑅𝐷)))) → (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐷 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵)))
4819, 39jca 501 . . . 4 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇𝐷𝑇) ∧ ((𝑁𝑇𝐺𝑇𝐶𝑇) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑅𝐹) = (𝑅𝑁)) ∧ ((𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐷 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵)) ∧ (𝐶 ≠ ( I ↾ 𝐵) ∧ (𝑅𝐺) ≠ (𝑅𝐶) ∧ (𝑅𝐶) ≠ (𝑅𝐹)) ∧ ((𝑅𝐷) ≠ (𝑅𝐹) ∧ (𝑅𝐺) ≠ (𝑅𝐷) ∧ (𝑅𝐶) ≠ (𝑅𝐷)))) → (𝐶 ≠ ( I ↾ 𝐵) ∧ (𝑅𝐺) ≠ (𝑅𝐶)))
49 simp33 1253 . . . 4 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇𝐷𝑇) ∧ ((𝑁𝑇𝐺𝑇𝐶𝑇) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑅𝐹) = (𝑅𝑁)) ∧ ((𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐷 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵)) ∧ (𝐶 ≠ ( I ↾ 𝐵) ∧ (𝑅𝐺) ≠ (𝑅𝐶) ∧ (𝑅𝐶) ≠ (𝑅𝐹)) ∧ ((𝑅𝐷) ≠ (𝑅𝐹) ∧ (𝑅𝐺) ≠ (𝑅𝐷) ∧ (𝑅𝐶) ≠ (𝑅𝐷)))) → ((𝑅𝐷) ≠ (𝑅𝐹) ∧ (𝑅𝐺) ≠ (𝑅𝐷) ∧ (𝑅𝐶) ≠ (𝑅𝐷)))
5047, 48, 493jca 1122 . . 3 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇𝐷𝑇) ∧ ((𝑁𝑇𝐺𝑇𝐶𝑇) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑅𝐹) = (𝑅𝑁)) ∧ ((𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐷 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵)) ∧ (𝐶 ≠ ( I ↾ 𝐵) ∧ (𝑅𝐺) ≠ (𝑅𝐶) ∧ (𝑅𝐶) ≠ (𝑅𝐹)) ∧ ((𝑅𝐷) ≠ (𝑅𝐹) ∧ (𝑅𝐺) ≠ (𝑅𝐷) ∧ (𝑅𝐶) ≠ (𝑅𝐷)))) → ((𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐷 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵)) ∧ (𝐶 ≠ ( I ↾ 𝐵) ∧ (𝑅𝐺) ≠ (𝑅𝐶)) ∧ ((𝑅𝐷) ≠ (𝑅𝐹) ∧ (𝑅𝐺) ≠ (𝑅𝐷) ∧ (𝑅𝐶) ≠ (𝑅𝐷))))
5125, 4, 5, 26, 6, 7, 8, 9, 27, 28, 29cdlemk12u 36682 . . 3 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇𝐷𝑇) ∧ ((𝑁𝑇𝐺𝑇𝐶𝑇) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑅𝐹) = (𝑅𝑁)) ∧ ((𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐷 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵)) ∧ (𝐶 ≠ ( I ↾ 𝐵) ∧ (𝑅𝐺) ≠ (𝑅𝐶)) ∧ ((𝑅𝐷) ≠ (𝑅𝐹) ∧ (𝑅𝐺) ≠ (𝑅𝐷) ∧ (𝑅𝐶) ≠ (𝑅𝐷)))) → ((𝑈𝐺)‘𝑃) = ((𝑃 (𝐺𝑃)) (((𝑈𝐶)‘𝑃) (𝑅‘(𝐶𝐺)))))
5250, 51syld3an3 1515 . 2 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇𝐷𝑇) ∧ ((𝑁𝑇𝐺𝑇𝐶𝑇) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑅𝐹) = (𝑅𝑁)) ∧ ((𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐷 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵)) ∧ (𝐶 ≠ ( I ↾ 𝐵) ∧ (𝑅𝐺) ≠ (𝑅𝐶) ∧ (𝑅𝐶) ≠ (𝑅𝐹)) ∧ ((𝑅𝐷) ≠ (𝑅𝐹) ∧ (𝑅𝐺) ≠ (𝑅𝐷) ∧ (𝑅𝐶) ≠ (𝑅𝐷)))) → ((𝑈𝐺)‘𝑃) = ((𝑃 (𝐺𝑃)) (((𝑈𝐶)‘𝑃) (𝑅‘(𝐶𝐺)))))
5337, 46, 523eqtr4rd 2816 1 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇𝐷𝑇) ∧ ((𝑁𝑇𝐺𝑇𝐶𝑇) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑅𝐹) = (𝑅𝑁)) ∧ ((𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐷 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵)) ∧ (𝐶 ≠ ( I ↾ 𝐵) ∧ (𝑅𝐺) ≠ (𝑅𝐶) ∧ (𝑅𝐶) ≠ (𝑅𝐹)) ∧ ((𝑅𝐷) ≠ (𝑅𝐹) ∧ (𝑅𝐺) ≠ (𝑅𝐷) ∧ (𝑅𝐶) ≠ (𝑅𝐷)))) → ((𝑈𝐺)‘𝑃) = ((𝑉𝐺)‘𝑃))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 382   ∧ w3a 1071   = wceq 1631   ∈ wcel 2145   ≠ wne 2943   class class class wbr 4787   ↦ cmpt 4864   I cid 5157  ◡ccnv 5249   ↾ cres 5252   ∘ ccom 5254  ‘cfv 6030  ℩crio 6756  (class class class)co 6796  Basecbs 16064  lecple 16156  joincjn 17152  meetcmee 17153  Atomscatm 35072  HLchlt 35159  LHypclh 35793  LTrncltrn 35910  trLctrl 35968 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-rep 4905  ax-sep 4916  ax-nul 4924  ax-pow 4975  ax-pr 5035  ax-un 7100  ax-riotaBAD 34761 This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-3or 1072  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-nel 3047  df-ral 3066  df-rex 3067  df-reu 3068  df-rmo 3069  df-rab 3070  df-v 3353  df-sbc 3588  df-csb 3683  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-nul 4064  df-if 4227  df-pw 4300  df-sn 4318  df-pr 4320  df-op 4324  df-uni 4576  df-iun 4657  df-iin 4658  df-br 4788  df-opab 4848  df-mpt 4865  df-id 5158  df-xp 5256  df-rel 5257  df-cnv 5258  df-co 5259  df-dm 5260  df-rn 5261  df-res 5262  df-ima 5263  df-iota 5993  df-fun 6032  df-fn 6033  df-f 6034  df-f1 6035  df-fo 6036  df-f1o 6037  df-fv 6038  df-riota 6757  df-ov 6799  df-oprab 6800  df-mpt2 6801  df-1st 7319  df-2nd 7320  df-undef 7555  df-map 8015  df-preset 17136  df-poset 17154  df-plt 17166  df-lub 17182  df-glb 17183  df-join 17184  df-meet 17185  df-p0 17247  df-p1 17248  df-lat 17254  df-clat 17316  df-oposet 34985  df-ol 34987  df-oml 34988  df-covers 35075  df-ats 35076  df-atl 35107  df-cvlat 35131  df-hlat 35160  df-llines 35307  df-lplanes 35308  df-lvols 35309  df-lines 35310  df-psubsp 35312  df-pmap 35313  df-padd 35605  df-lhyp 35797  df-laut 35798  df-ldil 35913  df-ltrn 35914  df-trl 35969 This theorem is referenced by:  cdlemk22-3  36711
 Copyright terms: Public domain W3C validator