cdleme42g - Mathbox for Norm Megill

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

Theorem cdleme42g 41675

Description: Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 8-Mar-2013.)

**Hypotheses**
Ref	Expression
cdleme41.b	⊢ 𝐵 = (Base‘𝐾)
cdleme41.l	⊢ ≤ = (le‘𝐾)
cdleme41.j	⊢ ∨ = (join‘𝐾)
cdleme41.m	⊢ ∧ = (meet‘𝐾)
cdleme41.a	⊢ 𝐴 = (Atoms‘𝐾)
cdleme41.h	⊢ 𝐻 = (LHyp‘𝐾)
cdleme41.u	⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊)
cdleme41.d	⊢ 𝐷 = ((𝑠 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑠) ∧ 𝑊)))
cdleme41.e	⊢ 𝐸 = ((𝑡 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑡) ∧ 𝑊)))
cdleme41.g	⊢ 𝐺 = ((𝑃 ∨ 𝑄) ∧ (𝐸 ∨ ((𝑠 ∨ 𝑡) ∧ 𝑊)))
cdleme41.i	⊢ 𝐼 = (℩𝑦 ∈ 𝐵 ∀𝑡 ∈ 𝐴 ((¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) → 𝑦 = 𝐺))
cdleme41.n	⊢ 𝑁 = if(𝑠 ≤ (𝑃 ∨ 𝑄), 𝐼, 𝐷)
cdleme41.o	⊢ 𝑂 = (℩𝑧 ∈ 𝐵 ∀𝑠 ∈ 𝐴 ((¬ 𝑠 ≤ 𝑊 ∧ (𝑠 ∨ (𝑥 ∧ 𝑊)) = 𝑥) → 𝑧 = (𝑁 ∨ (𝑥 ∧ 𝑊))))
cdleme41.f	⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ if((𝑃 ≠ 𝑄 ∧ ¬ 𝑥 ≤ 𝑊), 𝑂, 𝑥))
cdleme34e.v	⊢ 𝑉 = ((𝑅 ∨ 𝑆) ∧ 𝑊)

**Assertion**
Ref	Expression
cdleme42g	⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊)) ∧ 𝑃 ≠ 𝑄) → (𝐹‘(𝑅 ∨ 𝑆)) = ((𝐹‘𝑅) ∨ 𝑉))

Distinct variable groups: 𝐴,𝑠 ∨ ,𝑠 ≤ ,𝑠 ∧ ,𝑠 𝑃,𝑠 𝑄,𝑠 𝑅,𝑠 𝑆,𝑠 𝑈,𝑠 𝑊,𝑠 𝑦,𝑡,𝐴,𝑠 𝐵,𝑠,𝑡,𝑦 𝑦,𝐷 𝑦,𝐺 𝐸,𝑠,𝑦 𝐻,𝑠,𝑡,𝑦 𝑡, ∨ ,𝑦 𝐾,𝑠,𝑡,𝑦 𝑡, ≤ ,𝑦 𝑡, ∧ ,𝑦 𝑡,𝑃,𝑦 𝑡,𝑄,𝑦 𝑡,𝑅,𝑦 𝑡,𝑆,𝑦 𝑡,𝑈,𝑦 𝑡,𝑊,𝑦 𝑥,𝑧,𝐴 𝑥,𝐵,𝑧 𝑧,𝐸,𝑠 𝑧,𝐻 𝑥, ∨ ,𝑧 𝑧,𝐾 𝑥, ≤ ,𝑧 𝑥, ∧ ,𝑧 𝑥,𝑁,𝑧 𝑥,𝑃,𝑧 𝑥,𝑄,𝑧 𝑥,𝑅,𝑧 𝑥,𝑆,𝑧 𝑥,𝑈,𝑧 𝑥,𝑊,𝑧,𝑠,𝑡,𝑦 𝑉,𝑠,𝑡,𝑥,𝑧 Allowed substitution hints: 𝐷(𝑥, 𝑧, 𝑡, 𝑠) 𝐸(𝑥, 𝑡) 𝐹(𝑥, 𝑦, 𝑧, 𝑡, 𝑠) 𝐺(𝑥, 𝑧, 𝑡, 𝑠) 𝐻(𝑥) 𝐼(𝑥, 𝑦, 𝑧, 𝑡, 𝑠) 𝐾(𝑥) 𝑁(𝑦, 𝑡, 𝑠) 𝑂(𝑥, 𝑦, 𝑧, 𝑡, 𝑠) 𝑉(𝑦)

**Proof of Theorem cdleme42g**
Step	Hyp	Ref	Expression
1		simp11 1222	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊)) ∧ 𝑃 ≠ 𝑄) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
2		simp2l 1218	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊)) ∧ 𝑃 ≠ 𝑄) → (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊))
3		simp2r 1219	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊)) ∧ 𝑃 ≠ 𝑄) → (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊))
4		cdleme41.b	. . . . 5 ⊢ 𝐵 = (Base‘𝐾)
5		cdleme41.l	. . . . 5 ⊢ ≤ = (le‘𝐾)
6		cdleme41.j	. . . . 5 ⊢ ∨ = (join‘𝐾)
7		cdleme41.m	. . . . 5 ⊢ ∧ = (meet‘𝐾)
8		cdleme41.a	. . . . 5 ⊢ 𝐴 = (Atoms‘𝐾)
9		cdleme41.h	. . . . 5 ⊢ 𝐻 = (LHyp‘𝐾)
10		cdleme34e.v	. . . . 5 ⊢ 𝑉 = ((𝑅 ∨ 𝑆) ∧ 𝑊)
11	4, 5, 6, 7, 8, 9, 10	cdleme42a 41665	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊)) → (𝑅 ∨ 𝑆) = (𝑅 ∨ 𝑉))
12	1, 2, 3, 11	syl3anc 1398	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊)) ∧ 𝑃 ≠ 𝑄) → (𝑅 ∨ 𝑆) = (𝑅 ∨ 𝑉))
13	12	fveq2d 6894	. 2 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊)) ∧ 𝑃 ≠ 𝑄) → (𝐹‘(𝑅 ∨ 𝑆)) = (𝐹‘(𝑅 ∨ 𝑉)))
14		cdleme41.u	. . 3 ⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊)
15		cdleme41.d	. . 3 ⊢ 𝐷 = ((𝑠 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑠) ∧ 𝑊)))
16		cdleme41.e	. . 3 ⊢ 𝐸 = ((𝑡 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑡) ∧ 𝑊)))
17		cdleme41.g	. . 3 ⊢ 𝐺 = ((𝑃 ∨ 𝑄) ∧ (𝐸 ∨ ((𝑠 ∨ 𝑡) ∧ 𝑊)))
18		cdleme41.i	. . 3 ⊢ 𝐼 = (℩𝑦 ∈ 𝐵 ∀𝑡 ∈ 𝐴 ((¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) → 𝑦 = 𝐺))
19		cdleme41.n	. . 3 ⊢ 𝑁 = if(𝑠 ≤ (𝑃 ∨ 𝑄), 𝐼, 𝐷)
20		cdleme41.o	. . 3 ⊢ 𝑂 = (℩𝑧 ∈ 𝐵 ∀𝑠 ∈ 𝐴 ((¬ 𝑠 ≤ 𝑊 ∧ (𝑠 ∨ (𝑥 ∧ 𝑊)) = 𝑥) → 𝑧 = (𝑁 ∨ (𝑥 ∧ 𝑊))))
21		cdleme41.f	. . 3 ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ if((𝑃 ≠ 𝑄 ∧ ¬ 𝑥 ≤ 𝑊), 𝑂, 𝑥))
22	4, 5, 6, 7, 8, 9, 14, 15, 16, 17, 18, 19, 20, 21, 10	cdleme42f 41674	. 2 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊)) ∧ 𝑃 ≠ 𝑄) → (𝐹‘(𝑅 ∨ 𝑉)) = ((𝐹‘𝑅) ∨ 𝑉))
23	13, 22	eqtrd 2795	1 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊)) ∧ 𝑃 ≠ 𝑄) → (𝐹‘(𝑅 ∨ 𝑆)) = ((𝐹‘𝑅) ∨ 𝑉))

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ∧ wa 401 ∧ w3a 1103 = wceq 1569 ∈ wcel 2144 ≠ wne 2955 ∀wral 3076 ifcif 4481 class class class wbr 5102 ↦ cmpt 5185 ‘cfv 6543 ℩crio 7380 (class class class)co 7424 Basecbs 17396 lecple 17444 joincjn 18494 meetcmee 18495 Atomscatm 40457 HLchlt 40544 LHypclh 41178

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1827 ax-4 1841 ax-5 1942 ax-6 1999 ax-7 2040 ax-8 2146 ax-9 2154 ax-10 2177 ax-11 2193 ax-12 2212 ax-ext 2732 ax-rep 5231 ax-sep 5248 ax-nul 5259 ax-pow 5327 ax-pr 5391 ax-un 7755 ax-riotaBAD 40147

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1572 df-fal 1582 df-ex 1812 df-nf 1816 df-sb 2099 df-mo 2564 df-eu 2594 df-clab 2739 df-cleq 2752 df-clel 2835 df-nfc 2909 df-ne 2956 df-ral 3077 df-rex 3087 df-rmo 3365 df-reu 3366 df-rab 3413 df-v 3452 df-sbc 3739 df-csb 3848 df-ss 3897 df-dif 4046 df-in 4090 df-un 4150 df-nul 4278 df-if 4482 df-pw 4558 df-sn 4585 df-pr 4587 df-op 4835 df-uni 4867 df-iun 4952 df-iin 4953 df-br 5103 df-opab 5167 df-mpt 5186 df-id 5546 df-xp 5657 df-rel 5658 df-cnv 5659 df-co 5660 df-dm 5661 df-rn 5662 df-res 5663 df-ima 5664 df-iota 6497 df-fun 6545 df-fn 6546 df-f 6547 df-f1 6548 df-fo 6549 df-f1o 6550 df-fv 6551 df-riota 7381 df-ov 7427 df-oprab 7428 df-mpo 7429 df-1st 8005 df-2nd 8006 df-undef 8298 df-proset 18477 df-poset 18496 df-plt 18511 df-lub 18527 df-glb 18528 df-join 18529 df-meet 18530 df-p0 18606 df-p1 18607 df-lat 18615 df-clat 18682 df-oposet 40370 df-ol 40372 df-oml 40373 df-covers 40460 df-ats 40461 df-atl 40492 df-cvlat 40516 df-hlat 40545 df-llines 40692 df-lplanes 40693 df-lvols 40694 df-lines 40695 df-psubsp 40697 df-pmap 40698 df-padd 40990 df-lhyp 41182

This theorem is used by: cdleme42h 41676 cdleme42mN 41681

W3C validator