cdlemkfid2N - Mathbox for Norm Megill

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

Theorem cdlemkfid2N 41383

Description: Lemma for cdlemkfid3N 41385. (Contributed by NM, 29-Jul-2013.) (New usage is discouraged.)

**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	⊢ 𝑍 = ((𝑃 ∨ (𝑅‘𝑏)) ∧ ((𝑁‘𝑃) ∨ (𝑅‘(𝑏 ∘ ^◡𝐹))))

**Assertion**
Ref	Expression
cdlemkfid2N	⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 = 𝑁) ∧ (𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵) ∧ 𝑏 ∈ 𝑇) ∧ ((𝑅‘𝑏) ≠ (𝑅‘𝐹) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊))) → 𝑍 = (𝑏‘𝑃))

**Proof of Theorem cdlemkfid2N**
Step	Hyp	Ref	Expression
1		cdlemk5.z	. 2 ⊢ 𝑍 = ((𝑃 ∨ (𝑅‘𝑏)) ∧ ((𝑁‘𝑃) ∨ (𝑅‘(𝑏 ∘ ^◡𝐹))))
2		simp1r 1200	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 = 𝑁) ∧ (𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵) ∧ 𝑏 ∈ 𝑇) ∧ ((𝑅‘𝑏) ≠ (𝑅‘𝐹) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊))) → 𝐹 = 𝑁)
3	2	fveq1d 6836	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 = 𝑁) ∧ (𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵) ∧ 𝑏 ∈ 𝑇) ∧ ((𝑅‘𝑏) ≠ (𝑅‘𝐹) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊))) → (𝐹‘𝑃) = (𝑁‘𝑃))
4	3	oveq1d 7375	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 = 𝑁) ∧ (𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵) ∧ 𝑏 ∈ 𝑇) ∧ ((𝑅‘𝑏) ≠ (𝑅‘𝐹) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊))) → ((𝐹‘𝑃) ∨ (𝑅‘(𝑏 ∘ ^◡𝐹))) = ((𝑁‘𝑃) ∨ (𝑅‘(𝑏 ∘ ^◡𝐹))))
5	4	oveq2d 7376	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 = 𝑁) ∧ (𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵) ∧ 𝑏 ∈ 𝑇) ∧ ((𝑅‘𝑏) ≠ (𝑅‘𝐹) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊))) → ((𝑃 ∨ (𝑅‘𝑏)) ∧ ((𝐹‘𝑃) ∨ (𝑅‘(𝑏 ∘ ^◡𝐹)))) = ((𝑃 ∨ (𝑅‘𝑏)) ∧ ((𝑁‘𝑃) ∨ (𝑅‘(𝑏 ∘ ^◡𝐹)))))
6		cdlemk5.b	. . . . 5 ⊢ 𝐵 = (Base‘𝐾)
7		cdlemk5.l	. . . . 5 ⊢ ≤ = (le‘𝐾)
8		cdlemk5.j	. . . . 5 ⊢ ∨ = (join‘𝐾)
9		cdlemk5.m	. . . . 5 ⊢ ∧ = (meet‘𝐾)
10		cdlemk5.a	. . . . 5 ⊢ 𝐴 = (Atoms‘𝐾)
11		cdlemk5.h	. . . . 5 ⊢ 𝐻 = (LHyp‘𝐾)
12		cdlemk5.t	. . . . 5 ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)
13		cdlemk5.r	. . . . 5 ⊢ 𝑅 = ((trL‘𝐾)‘𝑊)
14	6, 7, 8, 9, 10, 11, 12, 13	cdlemkfid1N 41381	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵) ∧ 𝑏 ∈ 𝑇) ∧ ((𝑅‘𝑏) ≠ (𝑅‘𝐹) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊))) → ((𝑃 ∨ (𝑅‘𝑏)) ∧ ((𝐹‘𝑃) ∨ (𝑅‘(𝑏 ∘ ^◡𝐹)))) = (𝑏‘𝑃))
15	14	3adant1r 1179	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 = 𝑁) ∧ (𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵) ∧ 𝑏 ∈ 𝑇) ∧ ((𝑅‘𝑏) ≠ (𝑅‘𝐹) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊))) → ((𝑃 ∨ (𝑅‘𝑏)) ∧ ((𝐹‘𝑃) ∨ (𝑅‘(𝑏 ∘ ^◡𝐹)))) = (𝑏‘𝑃))
16	5, 15	eqtr3d 2774	. 2 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 = 𝑁) ∧ (𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵) ∧ 𝑏 ∈ 𝑇) ∧ ((𝑅‘𝑏) ≠ (𝑅‘𝐹) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊))) → ((𝑃 ∨ (𝑅‘𝑏)) ∧ ((𝑁‘𝑃) ∨ (𝑅‘(𝑏 ∘ ^◡𝐹)))) = (𝑏‘𝑃))
17	1, 16	eqtrid 2784	1 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 = 𝑁) ∧ (𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵) ∧ 𝑏 ∈ 𝑇) ∧ ((𝑅‘𝑏) ≠ (𝑅‘𝐹) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊))) → 𝑍 = (𝑏‘𝑃))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 395 ∧ w3a 1087 = wceq 1542 ∈ wcel 2114 ≠ wne 2933 class class class wbr 5086 I cid 5518 ^◡ccnv 5623 ↾ cres 5626 ∘ ccom 5628 ‘cfv 6492 (class class class)co 7360 Basecbs 17170 lecple 17218 joincjn 18268 meetcmee 18269 Atomscatm 39723 HLchlt 39810 LHypclh 40444 LTrncltrn 40561 trLctrl 40618

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2709 ax-rep 5212 ax-sep 5231 ax-nul 5241 ax-pow 5302 ax-pr 5370 ax-un 7682 ax-riotaBAD 39413

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2540 df-eu 2570 df-clab 2716 df-cleq 2729 df-clel 2812 df-nfc 2886 df-ne 2934 df-ral 3053 df-rex 3063 df-rmo 3343 df-reu 3344 df-rab 3391 df-v 3432 df-sbc 3730 df-csb 3839 df-dif 3893 df-un 3895 df-in 3897 df-ss 3907 df-nul 4275 df-if 4468 df-pw 4544 df-sn 4569 df-pr 4571 df-op 4575 df-uni 4852 df-iun 4936 df-iin 4937 df-br 5087 df-opab 5149 df-mpt 5168 df-id 5519 df-xp 5630 df-rel 5631 df-cnv 5632 df-co 5633 df-dm 5634 df-rn 5635 df-res 5636 df-ima 5637 df-iota 6448 df-fun 6494 df-fn 6495 df-f 6496 df-f1 6497 df-fo 6498 df-f1o 6499 df-fv 6500 df-riota 7317 df-ov 7363 df-oprab 7364 df-mpo 7365 df-1st 7935 df-2nd 7936 df-undef 8216 df-map 8768 df-proset 18251 df-poset 18270 df-plt 18285 df-lub 18301 df-glb 18302 df-join 18303 df-meet 18304 df-p0 18380 df-p1 18381 df-lat 18389 df-clat 18456 df-oposet 39636 df-ol 39638 df-oml 39639 df-covers 39726 df-ats 39727 df-atl 39758 df-cvlat 39782 df-hlat 39811 df-llines 39958 df-lplanes 39959 df-lvols 39960 df-lines 39961 df-psubsp 39963 df-pmap 39964 df-padd 40256 df-lhyp 40448 df-laut 40449 df-ldil 40564 df-ltrn 40565 df-trl 40619

This theorem is referenced by: cdlemkfid3N 41385

W3C validator