cdlemn11a - Mathbox for Norm Megill

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

Theorem cdlemn11a 42358

Description: Part of proof of Lemma N of [Crawley] p. 121 line 37. (Contributed by NM, 27-Feb-2014.)

**Hypotheses**
Ref	Expression
cdlemn11a.b	⊢ 𝐵 = (Base‘𝐾)
cdlemn11a.l	⊢ ≤ = (le‘𝐾)
cdlemn11a.j	⊢ ∨ = (join‘𝐾)
cdlemn11a.a	⊢ 𝐴 = (Atoms‘𝐾)
cdlemn11a.h	⊢ 𝐻 = (LHyp‘𝐾)
cdlemn11a.p	⊢ 𝑃 = ((oc‘𝐾)‘𝑊)
cdlemn11a.o	⊢ 𝑂 = (ℎ ∈ 𝑇 ↦ ( I ↾ 𝐵))
cdlemn11a.t	⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)
cdlemn11a.r	⊢ 𝑅 = ((trL‘𝐾)‘𝑊)
cdlemn11a.e	⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊)
cdlemn11a.i	⊢ 𝐼 = ((DIsoB‘𝐾)‘𝑊)
cdlemn11a.J	⊢ 𝐽 = ((DIsoC‘𝐾)‘𝑊)
cdlemn11a.u	⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)
cdlemn11a.d	⊢ + = (+_g‘𝑈)
cdlemn11a.s	⊢ ⊕ = (LSSum‘𝑈)
cdlemn11a.f	⊢ 𝐹 = (℩ℎ ∈ 𝑇 (ℎ‘𝑃) = 𝑄)
cdlemn11a.g	⊢ 𝐺 = (℩ℎ ∈ 𝑇 (ℎ‘𝑃) = 𝑁)

**Assertion**
Ref	Expression
cdlemn11a	⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ≤ 𝑊) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ (𝐽‘𝑁) ⊆ ((𝐽‘𝑄) ⊕ (𝐼‘𝑋))) → ⟨𝐺, ( I ↾ 𝑇)⟩ ∈ (𝐽‘𝑁))

Distinct variable groups: ≤ ,ℎ 𝐴,ℎ 𝐵,ℎ ℎ,𝐻 ℎ,𝐾 ℎ,𝑁 𝑃,ℎ 𝑄,ℎ 𝑇,ℎ ℎ,𝑊 Allowed substitution hints: + (ℎ) ⊕ (ℎ) 𝑅(ℎ) 𝑈(ℎ) 𝐸(ℎ) 𝐹(ℎ) 𝐺(ℎ) 𝐼(ℎ) 𝐽(ℎ) ∨ (ℎ) 𝑂(ℎ) 𝑋(ℎ)

**Proof of Theorem cdlemn11a**
Step	Hyp	Ref	Expression
1		simp1 1154	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ≤ 𝑊) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ (𝐽‘𝑁) ⊆ ((𝐽‘𝑄) ⊕ (𝐼‘𝑋))) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
2		cdlemn11a.l	. . . . . . 7 ⊢ ≤ = (le‘𝐾)
3		cdlemn11a.a	. . . . . . 7 ⊢ 𝐴 = (Atoms‘𝐾)
4		cdlemn11a.h	. . . . . . 7 ⊢ 𝐻 = (LHyp‘𝐾)
5		cdlemn11a.p	. . . . . . 7 ⊢ 𝑃 = ((oc‘𝐾)‘𝑊)
6	2, 3, 4, 5	lhpocnel2 41170	. . . . . 6 ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊))
7	6	3ad2ant1 1151	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ≤ 𝑊) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ (𝐽‘𝑁) ⊆ ((𝐽‘𝑄) ⊕ (𝐼‘𝑋))) → (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊))
8		simp22 1226	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ≤ 𝑊) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ (𝐽‘𝑁) ⊆ ((𝐽‘𝑄) ⊕ (𝐼‘𝑋))) → (𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ≤ 𝑊))
9		cdlemn11a.t	. . . . . 6 ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)
10		cdlemn11a.g	. . . . . 6 ⊢ 𝐺 = (℩ℎ ∈ 𝑇 (ℎ‘𝑃) = 𝑁)
11	2, 3, 4, 9, 10	ltrniotacl 41730	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ≤ 𝑊)) → 𝐺 ∈ 𝑇)
12	1, 7, 8, 11	syl3anc 1398	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ≤ 𝑊) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ (𝐽‘𝑁) ⊆ ((𝐽‘𝑄) ⊕ (𝐼‘𝑋))) → 𝐺 ∈ 𝑇)
13		fvresi 7179	. . . 4 ⊢ (𝐺 ∈ 𝑇 → (( I ↾ 𝑇)‘𝐺) = 𝐺)
14	12, 13	syl 18	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ≤ 𝑊) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ (𝐽‘𝑁) ⊆ ((𝐽‘𝑄) ⊕ (𝐼‘𝑋))) → (( I ↾ 𝑇)‘𝐺) = 𝐺)
15	14	eqcomd 2766	. 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ≤ 𝑊) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ (𝐽‘𝑁) ⊆ ((𝐽‘𝑄) ⊕ (𝐼‘𝑋))) → 𝐺 = (( I ↾ 𝑇)‘𝐺))
16		cdlemn11a.e	. . . 4 ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊)
17	4, 9, 16	tendoidcl 41920	. . 3 ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → ( I ↾ 𝑇) ∈ 𝐸)
18	17	3ad2ant1 1151	. 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ≤ 𝑊) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ (𝐽‘𝑁) ⊆ ((𝐽‘𝑄) ⊕ (𝐼‘𝑋))) → ( I ↾ 𝑇) ∈ 𝐸)
19		cdlemn11a.J	. . . 4 ⊢ 𝐽 = ((DIsoC‘𝐾)‘𝑊)
20		riotaex 7382	. . . . 5 ⊢ (℩ℎ ∈ 𝑇 (ℎ‘𝑃) = 𝑁) ∈ V
21	10, 20	eqeltri 2856	. . . 4 ⊢ 𝐺 ∈ V
22	9	fvexi 6900	. . . . 5 ⊢ 𝑇 ∈ V
23		resiexg 7925	. . . . 5 ⊢ (𝑇 ∈ V → ( I ↾ 𝑇) ∈ V)
24	22, 23	ax-mp 5	. . . 4 ⊢ ( I ↾ 𝑇) ∈ V
25	2, 3, 4, 5, 9, 16, 19, 10, 21, 24	dicopelval2 42332	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ≤ 𝑊)) → (⟨𝐺, ( I ↾ 𝑇)⟩ ∈ (𝐽‘𝑁) ↔ (𝐺 = (( I ↾ 𝑇)‘𝐺) ∧ ( I ↾ 𝑇) ∈ 𝐸)))
26	1, 8, 25	syl2anc 596	. 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ≤ 𝑊) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ (𝐽‘𝑁) ⊆ ((𝐽‘𝑄) ⊕ (𝐼‘𝑋))) → (⟨𝐺, ( I ↾ 𝑇)⟩ ∈ (𝐽‘𝑁) ↔ (𝐺 = (( I ↾ 𝑇)‘𝐺) ∧ ( I ↾ 𝑇) ∈ 𝐸)))
27	15, 18, 26	mpbir2and 726	1 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ≤ 𝑊) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ (𝐽‘𝑁) ⊆ ((𝐽‘𝑄) ⊕ (𝐼‘𝑋))) → ⟨𝐺, ( I ↾ 𝑇)⟩ ∈ (𝐽‘𝑁))

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 401 ∧ w3a 1103 = wceq 1569 ∈ wcel 2144 Vcvv 3450 ⊆ wss 3895 ⟨cop 4834 class class class wbr 5102 ↦ cmpt 5185 I cid 5544 ↾ cres 5652 ‘cfv 6539 ℩crio 7377 (class class class)co 7421 Basecbs 17393 +_gcplusg 17434 lecple 17441 occoc 17442 joincjn 18491 LSSumclsm 19854 Atomscatm 40414 HLchlt 40501 LHypclh 41135 LTrncltrn 41252 trLctrl 41309 TEndoctendo 41903 DVecHcdvh 42229 DIsoBcdib 42289 DIsoCcdic 42323

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 5326 ax-pr 5390 ax-un 7752 ax-riotaBAD 40104

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 3847 df-ss 3896 df-dif 4047 df-in 4091 df-un 4151 df-nul 4279 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 5545 df-xp 5656 df-rel 5657 df-cnv 5658 df-co 5659 df-dm 5660 df-rn 5661 df-res 5662 df-ima 5663 df-iota 6494 df-fun 6541 df-fn 6542 df-f 6543 df-f1 6544 df-fo 6545 df-f1o 6546 df-fv 6547 df-riota 7378 df-ov 7424 df-oprab 7425 df-mpo 7426 df-1st 8002 df-2nd 8003 df-undef 8294 df-map 8853 df-proset 18474 df-poset 18493 df-plt 18508 df-lub 18524 df-glb 18525 df-join 18526 df-meet 18527 df-p0 18603 df-p1 18604 df-lat 18612 df-clat 18679 df-oposet 40327 df-ol 40329 df-oml 40330 df-covers 40417 df-ats 40418 df-atl 40449 df-cvlat 40473 df-hlat 40502 df-llines 40649 df-lplanes 40650 df-lvols 40651 df-lines 40652 df-psubsp 40654 df-pmap 40655 df-padd 40947 df-lhyp 41139 df-laut 41140 df-ldil 41255 df-ltrn 41256 df-trl 41310 df-tendo 41906 df-dic 42324

This theorem is used by: cdlemn11b 42359

W3C validator