cdlemg40 - Mathbox for Norm Megill

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

Theorem cdlemg40 36424

Description: Eliminate 𝑃 ≠ 𝑄 conditions from cdlemg39 36423. TODO: Fix comment. (Contributed by NM, 31-May-2013.)

**Hypotheses**
Ref	Expression
cdlemg35.l	⊢ ≤ = (le‘𝐾)
cdlemg35.j	⊢ ∨ = (join‘𝐾)
cdlemg35.m	⊢ ∧ = (meet‘𝐾)
cdlemg35.a	⊢ 𝐴 = (Atoms‘𝐾)
cdlemg35.h	⊢ 𝐻 = (LHyp‘𝐾)
cdlemg35.t	⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)

**Assertion**
Ref	Expression
cdlemg40	⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇)) → ((𝑃 ∨ (𝐹‘(𝐺‘𝑃))) ∧ 𝑊) = ((𝑄 ∨ (𝐹‘(𝐺‘𝑄))) ∧ 𝑊))

**Proof of Theorem cdlemg40**
Step	Hyp	Ref	Expression
1		id 22	. . . . 5 ⊢ (𝑃 = 𝑄 → 𝑃 = 𝑄)
2		fveq2 6304	. . . . . 6 ⊢ (𝑃 = 𝑄 → (𝐺‘𝑃) = (𝐺‘𝑄))
3	2	fveq2d 6308	. . . . 5 ⊢ (𝑃 = 𝑄 → (𝐹‘(𝐺‘𝑃)) = (𝐹‘(𝐺‘𝑄)))
4	1, 3	oveq12d 6783	. . . 4 ⊢ (𝑃 = 𝑄 → (𝑃 ∨ (𝐹‘(𝐺‘𝑃))) = (𝑄 ∨ (𝐹‘(𝐺‘𝑄))))
5	4	oveq1d 6780	. . 3 ⊢ (𝑃 = 𝑄 → ((𝑃 ∨ (𝐹‘(𝐺‘𝑃))) ∧ 𝑊) = ((𝑄 ∨ (𝐹‘(𝐺‘𝑄))) ∧ 𝑊))
6	5	adantl 473	. 2 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇)) ∧ 𝑃 = 𝑄) → ((𝑃 ∨ (𝐹‘(𝐺‘𝑃))) ∧ 𝑊) = ((𝑄 ∨ (𝐹‘(𝐺‘𝑄))) ∧ 𝑊))
7		simpl1 1204	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇)) ∧ 𝑃 ≠ 𝑄) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
8		simpl2 1206	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇)) ∧ 𝑃 ≠ 𝑄) → ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)))
9		simpl3l 1263	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇)) ∧ 𝑃 ≠ 𝑄) → 𝐹 ∈ 𝑇)
10		simpl3r 1265	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇)) ∧ 𝑃 ≠ 𝑄) → 𝐺 ∈ 𝑇)
11		simpr 479	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇)) ∧ 𝑃 ≠ 𝑄) → 𝑃 ≠ 𝑄)
12		cdlemg35.l	. . . 4 ⊢ ≤ = (le‘𝐾)
13		cdlemg35.j	. . . 4 ⊢ ∨ = (join‘𝐾)
14		cdlemg35.m	. . . 4 ⊢ ∧ = (meet‘𝐾)
15		cdlemg35.a	. . . 4 ⊢ 𝐴 = (Atoms‘𝐾)
16		cdlemg35.h	. . . 4 ⊢ 𝐻 = (LHyp‘𝐾)
17		cdlemg35.t	. . . 4 ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)
18		eqid 2724	. . . 4 ⊢ ((trL‘𝐾)‘𝑊) = ((trL‘𝐾)‘𝑊)
19	12, 13, 14, 15, 16, 17, 18	cdlemg39 36423	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄)) → ((𝑃 ∨ (𝐹‘(𝐺‘𝑃))) ∧ 𝑊) = ((𝑄 ∨ (𝐹‘(𝐺‘𝑄))) ∧ 𝑊))
20	7, 8, 9, 10, 11, 19	syl113anc 1451	. 2 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇)) ∧ 𝑃 ≠ 𝑄) → ((𝑃 ∨ (𝐹‘(𝐺‘𝑃))) ∧ 𝑊) = ((𝑄 ∨ (𝐹‘(𝐺‘𝑄))) ∧ 𝑊))
21	6, 20	pm2.61dane 2983	1 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇)) → ((𝑃 ∨ (𝐹‘(𝐺‘𝑃))) ∧ 𝑊) = ((𝑄 ∨ (𝐹‘(𝐺‘𝑄))) ∧ 𝑊))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 383 ∧ w3a 1072 = wceq 1596 ∈ wcel 2103 ≠ wne 2896 class class class wbr 4760 ‘cfv 6001 (class class class)co 6765 lecple 16071 joincjn 17066 meetcmee 17067 Atomscatm 34970 HLchlt 35057 LHypclh 35690 LTrncltrn 35807 trLctrl 35865

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1835 ax-4 1850 ax-5 1952 ax-6 2018 ax-7 2054 ax-8 2105 ax-9 2112 ax-10 2132 ax-11 2147 ax-12 2160 ax-13 2355 ax-ext 2704 ax-rep 4879 ax-sep 4889 ax-nul 4897 ax-pow 4948 ax-pr 5011 ax-un 7066 ax-riotaBAD 34659

This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-3or 1073 df-3an 1074 df-tru 1599 df-ex 1818 df-nf 1823 df-sb 2011 df-eu 2575 df-mo 2576 df-clab 2711 df-cleq 2717 df-clel 2720 df-nfc 2855 df-ne 2897 df-nel 3000 df-ral 3019 df-rex 3020 df-reu 3021 df-rmo 3022 df-rab 3023 df-v 3306 df-sbc 3542 df-csb 3640 df-dif 3683 df-un 3685 df-in 3687 df-ss 3694 df-nul 4024 df-if 4195 df-pw 4268 df-sn 4286 df-pr 4288 df-op 4292 df-uni 4545 df-iun 4630 df-iin 4631 df-br 4761 df-opab 4821 df-mpt 4838 df-id 5128 df-xp 5224 df-rel 5225 df-cnv 5226 df-co 5227 df-dm 5228 df-rn 5229 df-res 5230 df-ima 5231 df-iota 5964 df-fun 6003 df-fn 6004 df-f 6005 df-f1 6006 df-fo 6007 df-f1o 6008 df-fv 6009 df-riota 6726 df-ov 6768 df-oprab 6769 df-mpt2 6770 df-1st 7285 df-2nd 7286 df-undef 7519 df-map 7976 df-preset 17050 df-poset 17068 df-plt 17080 df-lub 17096 df-glb 17097 df-join 17098 df-meet 17099 df-p0 17161 df-p1 17162 df-lat 17168 df-clat 17230 df-oposet 34883 df-ol 34885 df-oml 34886 df-covers 34973 df-ats 34974 df-atl 35005 df-cvlat 35029 df-hlat 35058 df-llines 35204 df-lplanes 35205 df-lvols 35206 df-lines 35207 df-psubsp 35209 df-pmap 35210 df-padd 35502 df-lhyp 35694 df-laut 35695 df-ldil 35810 df-ltrn 35811 df-trl 35866

This theorem is referenced by: cdlemg41 36425

W3C validator