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 40970

Description: Use a fixed element to eliminate 𝑃 in cdlemk56 40968. (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 1137	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
2		simp2l 1200	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) → 𝐹 ∈ 𝑇)
3		simp2r 1201	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) → 𝑁 ∈ 𝑇)
4		simp3 1139	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) → (𝑅‘𝐹) = (𝑅‘𝑁))
5		eqid 2737	. . . . 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 6915	. . . . . 6 ⊢ ( ⊥ ‘𝑊) = ((oc‘𝐾)‘𝑊)
11	8, 10	eqtri 2765	. . . . 5 ⊢ 𝑃 = ((oc‘𝐾)‘𝑊)
12	5, 6, 7, 11	lhpocnel2 40016	. . . 4 ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → (𝑃 ∈ 𝐴 ∧ ¬ 𝑃(le‘𝐾)𝑊))
13	12	3ad2ant1 1134	. . 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 40968	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇) ∧ (𝑅‘𝐹) = (𝑅‘𝑁) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃(le‘𝐾)𝑊)) → 𝑈 ∈ 𝐸)
25	1, 2, 3, 4, 13, 24	syl311anc 1385	. 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) → 𝑈 ∈ 𝐸)
26	14, 15, 16, 9, 6, 7, 17, 18, 8, 19, 20, 21, 22	cdlemk19w 40969	. 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) → (𝑈‘𝐹) = 𝑁)
27	25, 26	jca 511	1 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) → (𝑈 ∈ 𝐸 ∧ (𝑈‘𝐹) = 𝑁))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 395 ∧ w3a 1087 = wceq 1539 ∈ wcel 2108 ≠ wne 2940 ∀wral 3061 ifcif 4534 class class class wbr 5151 ↦ cmpt 5234 I cid 5586 ^◡ccnv 5692 ↾ cres 5695 ∘ ccom 5697 ‘cfv 6569 ℩crio 7394 (class class class)co 7438 Basecbs 17254 lecple 17314 occoc 17315 joincjn 18378 meetcmee 18379 Atomscatm 39259 HLchlt 39346 LHypclh 39981 LTrncltrn 40098 trLctrl 40155 TEndoctendo 40749

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2157 ax-12 2177 ax-ext 2708 ax-rep 5288 ax-sep 5305 ax-nul 5315 ax-pow 5374 ax-pr 5441 ax-un 7761 ax-riotaBAD 38949

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1542 df-fal 1552 df-ex 1779 df-nf 1783 df-sb 2065 df-mo 2540 df-eu 2569 df-clab 2715 df-cleq 2729 df-clel 2816 df-nfc 2892 df-ne 2941 df-ral 3062 df-rex 3071 df-rmo 3380 df-reu 3381 df-rab 3437 df-v 3483 df-sbc 3795 df-csb 3912 df-dif 3969 df-un 3971 df-in 3973 df-ss 3983 df-nul 4343 df-if 4535 df-pw 4610 df-sn 4635 df-pr 4637 df-op 4641 df-uni 4916 df-iun 5001 df-iin 5002 df-br 5152 df-opab 5214 df-mpt 5235 df-id 5587 df-xp 5699 df-rel 5700 df-cnv 5701 df-co 5702 df-dm 5703 df-rn 5704 df-res 5705 df-ima 5706 df-iota 6522 df-fun 6571 df-fn 6572 df-f 6573 df-f1 6574 df-fo 6575 df-f1o 6576 df-fv 6577 df-riota 7395 df-ov 7441 df-oprab 7442 df-mpo 7443 df-1st 8022 df-2nd 8023 df-undef 8306 df-map 8876 df-proset 18361 df-poset 18380 df-plt 18397 df-lub 18413 df-glb 18414 df-join 18415 df-meet 18416 df-p0 18492 df-p1 18493 df-lat 18499 df-clat 18566 df-oposet 39172 df-ol 39174 df-oml 39175 df-covers 39262 df-ats 39263 df-atl 39294 df-cvlat 39318 df-hlat 39347 df-llines 39495 df-lplanes 39496 df-lvols 39497 df-lines 39498 df-psubsp 39500 df-pmap 39501 df-padd 39793 df-lhyp 39985 df-laut 39986 df-ldil 40101 df-ltrn 40102 df-trl 40156 df-tendo 40752

This theorem is referenced by: cdlemk 40971 cdleml6 40978

W3C validator