Theorem cdlemk19u 39779

Description: Part of Lemma K of [Crawley] p. 118. Line 12, p. 120, "f (exponent) tau = k". We represent f, k, tau with 𝐹, 𝑁, 𝑈. (Contributed by NM, 31-Jul-2013.)

Hypotheses

Ref	Expression
cdlemk5.b	⊢ 𝐵 = (Base‘𝐾)
cdlemk5.l	⊢ ≤ = (le‘𝐾)
cdlemk5.j	⊢ ∨ = (join‘𝐾)
cdlemk5.m	⊢ ∧ = (meet‘𝐾)
cdlemk5.a	⊢ 𝐴 = (Atoms‘𝐾)
cdlemk5.h	⊢ 𝐻 = (LHyp‘𝐾)
cdlemk5.t	⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)
cdlemk5.r	⊢ 𝑅 = ((trL‘𝐾)‘𝑊)
cdlemk5.z	⊢ 𝑍 = ((𝑃 ∨ (𝑅‘𝑏)) ∧ ((𝑁‘𝑃) ∨ (𝑅‘(𝑏 ∘ ◡𝐹))))
cdlemk5.y	⊢ 𝑌 = ((𝑃 ∨ (𝑅‘𝑔)) ∧ (𝑍 ∨ (𝑅‘(𝑔 ∘ ◡𝑏))))
cdlemk5.x	⊢ 𝑋 = (℩𝑧 ∈ 𝑇 ∀𝑏 ∈ 𝑇 ((𝑏 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝑏) ≠ (𝑅‘𝐹) ∧ (𝑅‘𝑏) ≠ (𝑅‘𝑔)) → (𝑧‘𝑃) = 𝑌))
cdlemk5.u	⊢ 𝑈 = (𝑔 ∈ 𝑇 ↦ if(𝐹 = 𝑁, 𝑔, 𝑋))

Assertion

Ref	Expression
cdlemk19u	⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝑈‘𝐹) = 𝑁)

Distinct variable groups:   ∧ ,𝑔   ∨ ,𝑔   𝐵,𝑔   𝑃,𝑔   𝑅,𝑔   𝑇,𝑔   𝑔,𝑍   𝑔,𝑏,𝑧, ∧   ≤ ,𝑏   𝑧,𝑔, ≤   ∨ ,𝑏,𝑧   𝐴,𝑏,𝑔,𝑧   𝐵,𝑏,𝑧   𝐹,𝑏,𝑔,𝑧   𝐻,𝑏,𝑔,𝑧   𝐾,𝑏,𝑔,𝑧   𝑁,𝑏,𝑔,𝑧   𝑃,𝑏,𝑧   𝑅,𝑏,𝑧   𝑇,𝑏,𝑧   𝑊,𝑏,𝑔,𝑧   𝑧,𝑌

Allowed substitution hints:   𝑈(𝑧,𝑔,𝑏)   𝑋(𝑧,𝑔,𝑏)   𝑌(𝑔,𝑏)   𝑍(𝑧,𝑏)

Proof of Theorem cdlemk19u

Step	Hyp	Ref	Expression
1		simp1l 1198	. 2 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
2		simp1 1137	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)))
3		simp2l 1200	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → 𝐹 ∈ 𝑇)
4		simp2r 1201	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → 𝑁 ∈ 𝑇)
5		simp3 1139	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊))
6		cdlemk5.b	. . . 4 ⊢ 𝐵 = (Base‘𝐾)
7		cdlemk5.l	. . . 4 ⊢ ≤ = (le‘𝐾)
8		cdlemk5.j	. . . 4 ⊢ ∨ = (join‘𝐾)
9		cdlemk5.m	. . . 4 ⊢ ∧ = (meet‘𝐾)
10		cdlemk5.a	. . . 4 ⊢ 𝐴 = (Atoms‘𝐾)
11		cdlemk5.h	. . . 4 ⊢ 𝐻 = (LHyp‘𝐾)
12		cdlemk5.t	. . . 4 ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)
13		cdlemk5.r	. . . 4 ⊢ 𝑅 = ((trL‘𝐾)‘𝑊)
14		cdlemk5.z	. . . 4 ⊢ 𝑍 = ((𝑃 ∨ (𝑅‘𝑏)) ∧ ((𝑁‘𝑃) ∨ (𝑅‘(𝑏 ∘ ◡𝐹))))
15		cdlemk5.y	. . . 4 ⊢ 𝑌 = ((𝑃 ∨ (𝑅‘𝑔)) ∧ (𝑍 ∨ (𝑅‘(𝑔 ∘ ◡𝑏))))
16		cdlemk5.x	. . . 4 ⊢ 𝑋 = (℩𝑧 ∈ 𝑇 ∀𝑏 ∈ 𝑇 ((𝑏 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝑏) ≠ (𝑅‘𝐹) ∧ (𝑅‘𝑏) ≠ (𝑅‘𝑔)) → (𝑧‘𝑃) = 𝑌))
17		cdlemk5.u	. . . 4 ⊢ 𝑈 = (𝑔 ∈ 𝑇 ↦ if(𝐹 = 𝑁, 𝑔, 𝑋))
18	6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17	cdlemk35u 39773	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ 𝐹 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝑈‘𝐹) ∈ 𝑇)
19	2, 3, 4, 3, 5, 18	syl131anc 1384	. 2 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝑈‘𝐹) ∈ 𝑇)
20		simpr 486	. . . . . 6 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) ∧ 𝐹 = 𝑁) → 𝐹 = 𝑁)
21		simpl2l 1227	. . . . . 6 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) ∧ 𝐹 = 𝑁) → 𝐹 ∈ 𝑇)
22	16, 17	cdlemk40t 39727	. . . . . 6 ⊢ ((𝐹 = 𝑁 ∧ 𝐹 ∈ 𝑇) → (𝑈‘𝐹) = 𝐹)
23	20, 21, 22	syl2anc 585	. . . . 5 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) ∧ 𝐹 = 𝑁) → (𝑈‘𝐹) = 𝐹)
24	23	fveq1d 6890	. . . 4 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) ∧ 𝐹 = 𝑁) → ((𝑈‘𝐹)‘𝑃) = (𝐹‘𝑃))
25		fveq1 6887	. . . . 5 ⊢ (𝐹 = 𝑁 → (𝐹‘𝑃) = (𝑁‘𝑃))
26	25	adantl 483	. . . 4 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) ∧ 𝐹 = 𝑁) → (𝐹‘𝑃) = (𝑁‘𝑃))
27	24, 26	eqtrd 2773	. . 3 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) ∧ 𝐹 = 𝑁) → ((𝑈‘𝐹)‘𝑃) = (𝑁‘𝑃))
28		simpl1 1192	. . . 4 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) ∧ 𝐹 ≠ 𝑁) → ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)))
29		simpl2l 1227	. . . 4 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) ∧ 𝐹 ≠ 𝑁) → 𝐹 ∈ 𝑇)
30		simpr 486	. . . 4 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) ∧ 𝐹 ≠ 𝑁) → 𝐹 ≠ 𝑁)
31		simpl2r 1228	. . . 4 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) ∧ 𝐹 ≠ 𝑁) → 𝑁 ∈ 𝑇)
32		simpl3 1194	. . . 4 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) ∧ 𝐹 ≠ 𝑁) → (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊))
33	6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17	cdlemk19u1 39778	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ (𝐹 ∈ 𝑇 ∧ 𝐹 ≠ 𝑁 ∧ 𝑁 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → ((𝑈‘𝐹)‘𝑃) = (𝑁‘𝑃))
34	28, 29, 30, 31, 32, 33	syl131anc 1384	. . 3 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) ∧ 𝐹 ≠ 𝑁) → ((𝑈‘𝐹)‘𝑃) = (𝑁‘𝑃))
35	27, 34	pm2.61dane 3030	. 2 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → ((𝑈‘𝐹)‘𝑃) = (𝑁‘𝑃))
36	7, 10, 11, 12	cdlemd 39016	. 2 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑈‘𝐹) ∈ 𝑇 ∧ 𝑁 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ ((𝑈‘𝐹)‘𝑃) = (𝑁‘𝑃)) → (𝑈‘𝐹) = 𝑁)
37	1, 19, 4, 5, 35, 36	syl311anc 1385	1 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝑈‘𝐹) = 𝑁)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 397   ∧ w3a 1088   = wceq 1542   ∈ wcel 2107   ≠ wne 2941  ∀wral 3062  ifcif 4527   class class class wbr 5147   ↦ cmpt 5230   I cid 5572  ^◡ccnv 5674   ↾ cres 5677   ∘ ccom 5679  ‘cfv 6540  ℩crio 7359  (class class class)co 7404  Basecbs 17140  lecple 17200  joincjn 18260  meetcmee 18261  Atomscatm 38071  HLchlt 38158  LHypclh 38793  LTrncltrn 38910  trLctrl 38967

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 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5284  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7720  ax-riotaBAD 37761

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-ral 3063  df-rex 3072  df-rmo 3377  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-iun 4998  df-iin 4999  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5573  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-iota 6492  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-riota 7360  df-ov 7407  df-oprab 7408  df-mpo 7409  df-1st 7970  df-2nd 7971  df-undef 8253  df-map 8818  df-proset 18244  df-poset 18262  df-plt 18279  df-lub 18295  df-glb 18296  df-join 18297  df-meet 18298  df-p0 18374  df-p1 18375  df-lat 18381  df-clat 18448  df-oposet 37984  df-ol 37986  df-oml 37987  df-covers 38074  df-ats 38075  df-atl 38106  df-cvlat 38130  df-hlat 38159  df-llines 38307  df-lplanes 38308  df-lvols 38309  df-lines 38310  df-psubsp 38312  df-pmap 38313  df-padd 38605  df-lhyp 38797  df-laut 38798  df-ldil 38913  df-ltrn 38914  df-trl 38968

This theorem is referenced by:  cdlemk19w  39781