cdlemk56w - Mathbox for Norm Megill

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

Theorem cdlemk56w 40940

Description: Use a fixed element to eliminate 𝑃 in cdlemk56 40938. (Contributed by NM, 1-Aug-2013.)

**Hypotheses**
Ref	Expression
cdlemk6.b	⊢ 𝐵 = (Base‘𝐾)
cdlemk6.j	⊢ ∨ = (join‘𝐾)
cdlemk6.m	⊢ ∧ = (meet‘𝐾)
cdlemk6.o	⊢ ⊥ = (oc‘𝐾)
cdlemk6.a	⊢ 𝐴 = (Atoms‘𝐾)
cdlemk6.h	⊢ 𝐻 = (LHyp‘𝐾)
cdlemk6.t	⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)
cdlemk6.r	⊢ 𝑅 = ((trL‘𝐾)‘𝑊)
cdlemk6.p	⊢ 𝑃 = ( ⊥ ‘𝑊)
cdlemk6.z	⊢ 𝑍 = ((𝑃 ∨ (𝑅‘𝑏)) ∧ ((𝑁‘𝑃) ∨ (𝑅‘(𝑏 ∘ ^◡𝐹))))
cdlemk6.y	⊢ 𝑌 = ((𝑃 ∨ (𝑅‘𝑔)) ∧ (𝑍 ∨ (𝑅‘(𝑔 ∘ ^◡𝑏))))
cdlemk6.x	⊢ 𝑋 = (℩𝑧 ∈ 𝑇 ∀𝑏 ∈ 𝑇 ((𝑏 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝑏) ≠ (𝑅‘𝐹) ∧ (𝑅‘𝑏) ≠ (𝑅‘𝑔)) → (𝑧‘𝑃) = 𝑌))
cdlemk6.u	⊢ 𝑈 = (𝑔 ∈ 𝑇 ↦ if(𝐹 = 𝑁, 𝑔, 𝑋))
cdlemk6.e	⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊)

**Assertion**
Ref	Expression
cdlemk56w	⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) → (𝑈 ∈ 𝐸 ∧ (𝑈‘𝐹) = 𝑁))

Distinct variable groups: 𝑔,𝑏,𝑧, ∧ ∨ ,𝑏,𝑔,𝑧 𝐴,𝑏,𝑔,𝑧 𝐵,𝑏,𝑔,𝑧 𝐹,𝑏,𝑔,𝑧 𝐻,𝑏,𝑔,𝑧 𝐾,𝑏,𝑔,𝑧 𝑁,𝑏,𝑔,𝑧 𝑃,𝑏,𝑔,𝑧 𝑅,𝑏,𝑔,𝑧 𝑇,𝑏,𝑔,𝑧 𝑊,𝑏,𝑔,𝑧 𝑧,𝑌 𝑔,𝑍 Allowed substitution hints: 𝑈(𝑧,𝑔,𝑏) 𝐸(𝑧,𝑔,𝑏) ⊥ (𝑧,𝑔,𝑏) 𝑋(𝑧,𝑔,𝑏) 𝑌(𝑔,𝑏) 𝑍(𝑧,𝑏)

**Proof of Theorem cdlemk56w**
Step	Hyp	Ref	Expression
1		simp1 1136	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
2		simp2l 1200	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) → 𝐹 ∈ 𝑇)
3		simp2r 1201	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) → 𝑁 ∈ 𝑇)
4		simp3 1138	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) → (𝑅‘𝐹) = (𝑅‘𝑁))
5		eqid 2729	. . . . 5 ⊢ (le‘𝐾) = (le‘𝐾)
6		cdlemk6.a	. . . . 5 ⊢ 𝐴 = (Atoms‘𝐾)
7		cdlemk6.h	. . . . 5 ⊢ 𝐻 = (LHyp‘𝐾)
8		cdlemk6.p	. . . . . 6 ⊢ 𝑃 = ( ⊥ ‘𝑊)
9		cdlemk6.o	. . . . . . 7 ⊢ ⊥ = (oc‘𝐾)
10	9	fveq1i 6841	. . . . . 6 ⊢ ( ⊥ ‘𝑊) = ((oc‘𝐾)‘𝑊)
11	8, 10	eqtri 2752	. . . . 5 ⊢ 𝑃 = ((oc‘𝐾)‘𝑊)
12	5, 6, 7, 11	lhpocnel2 39986	. . . 4 ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → (𝑃 ∈ 𝐴 ∧ ¬ 𝑃(le‘𝐾)𝑊))
13	12	3ad2ant1 1133	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) → (𝑃 ∈ 𝐴 ∧ ¬ 𝑃(le‘𝐾)𝑊))
14		cdlemk6.b	. . . 4 ⊢ 𝐵 = (Base‘𝐾)
15		cdlemk6.j	. . . 4 ⊢ ∨ = (join‘𝐾)
16		cdlemk6.m	. . . 4 ⊢ ∧ = (meet‘𝐾)
17		cdlemk6.t	. . . 4 ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)
18		cdlemk6.r	. . . 4 ⊢ 𝑅 = ((trL‘𝐾)‘𝑊)
19		cdlemk6.z	. . . 4 ⊢ 𝑍 = ((𝑃 ∨ (𝑅‘𝑏)) ∧ ((𝑁‘𝑃) ∨ (𝑅‘(𝑏 ∘ ^◡𝐹))))
20		cdlemk6.y	. . . 4 ⊢ 𝑌 = ((𝑃 ∨ (𝑅‘𝑔)) ∧ (𝑍 ∨ (𝑅‘(𝑔 ∘ ^◡𝑏))))
21		cdlemk6.x	. . . 4 ⊢ 𝑋 = (℩𝑧 ∈ 𝑇 ∀𝑏 ∈ 𝑇 ((𝑏 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝑏) ≠ (𝑅‘𝐹) ∧ (𝑅‘𝑏) ≠ (𝑅‘𝑔)) → (𝑧‘𝑃) = 𝑌))
22		cdlemk6.u	. . . 4 ⊢ 𝑈 = (𝑔 ∈ 𝑇 ↦ if(𝐹 = 𝑁, 𝑔, 𝑋))
23		cdlemk6.e	. . . 4 ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊)
24	14, 5, 15, 16, 6, 7, 17, 18, 19, 20, 21, 22, 23	cdlemk56 40938	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇) ∧ (𝑅‘𝐹) = (𝑅‘𝑁) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃(le‘𝐾)𝑊)) → 𝑈 ∈ 𝐸)
25	1, 2, 3, 4, 13, 24	syl311anc 1386	. 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) → 𝑈 ∈ 𝐸)
26	14, 15, 16, 9, 6, 7, 17, 18, 8, 19, 20, 21, 22	cdlemk19w 40939	. 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) → (𝑈‘𝐹) = 𝑁)
27	25, 26	jca 511	1 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) → (𝑈 ∈ 𝐸 ∧ (𝑈‘𝐹) = 𝑁))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 395 ∧ w3a 1086 = wceq 1540 ∈ wcel 2109 ≠ wne 2925 ∀wral 3044 ifcif 4484 class class class wbr 5102 ↦ cmpt 5183 I cid 5525 ^◡ccnv 5630 ↾ cres 5633 ∘ ccom 5635 ‘cfv 6499 ℩crio 7325 (class class class)co 7369 Basecbs 17155 lecple 17203 occoc 17204 joincjn 18248 meetcmee 18249 Atomscatm 39229 HLchlt 39316 LHypclh 39951 LTrncltrn 40068 trLctrl 40125 TEndoctendo 40719

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2701 ax-rep 5229 ax-sep 5246 ax-nul 5256 ax-pow 5315 ax-pr 5382 ax-un 7691 ax-riotaBAD 38919

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2533 df-eu 2562 df-clab 2708 df-cleq 2721 df-clel 2803 df-nfc 2878 df-ne 2926 df-ral 3045 df-rex 3054 df-rmo 3351 df-reu 3352 df-rab 3403 df-v 3446 df-sbc 3751 df-csb 3860 df-dif 3914 df-un 3916 df-in 3918 df-ss 3928 df-nul 4293 df-if 4485 df-pw 4561 df-sn 4586 df-pr 4588 df-op 4592 df-uni 4868 df-iun 4953 df-iin 4954 df-br 5103 df-opab 5165 df-mpt 5184 df-id 5526 df-xp 5637 df-rel 5638 df-cnv 5639 df-co 5640 df-dm 5641 df-rn 5642 df-res 5643 df-ima 5644 df-iota 6452 df-fun 6501 df-fn 6502 df-f 6503 df-f1 6504 df-fo 6505 df-f1o 6506 df-fv 6507 df-riota 7326 df-ov 7372 df-oprab 7373 df-mpo 7374 df-1st 7947 df-2nd 7948 df-undef 8229 df-map 8778 df-proset 18231 df-poset 18250 df-plt 18265 df-lub 18281 df-glb 18282 df-join 18283 df-meet 18284 df-p0 18360 df-p1 18361 df-lat 18367 df-clat 18434 df-oposet 39142 df-ol 39144 df-oml 39145 df-covers 39232 df-ats 39233 df-atl 39264 df-cvlat 39288 df-hlat 39317 df-llines 39465 df-lplanes 39466 df-lvols 39467 df-lines 39468 df-psubsp 39470 df-pmap 39471 df-padd 39763 df-lhyp 39955 df-laut 39956 df-ldil 40071 df-ltrn 40072 df-trl 40126 df-tendo 40722

This theorem is referenced by: cdlemk 40941 cdleml6 40948

W3C validator