cdlemn11b - Mathbox for Norm Megill

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

Theorem cdlemn11b 41207

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
cdlemn11b	⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ≤ 𝑊) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ (𝐽‘𝑁) ⊆ ((𝐽‘𝑄) ⊕ (𝐼‘𝑋))) → ⟨𝐺, ( I ↾ 𝑇)⟩ ∈ ((𝐽‘𝑄) ⊕ (𝐼‘𝑋)))

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

**Proof of Theorem cdlemn11b**
Step	Hyp	Ref	Expression
1		simp3 1138	. 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ≤ 𝑊) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ (𝐽‘𝑁) ⊆ ((𝐽‘𝑄) ⊕ (𝐼‘𝑋))) → (𝐽‘𝑁) ⊆ ((𝐽‘𝑄) ⊕ (𝐼‘𝑋)))
2		cdlemn11a.b	. . 3 ⊢ 𝐵 = (Base‘𝐾)
3		cdlemn11a.l	. . 3 ⊢ ≤ = (le‘𝐾)
4		cdlemn11a.j	. . 3 ⊢ ∨ = (join‘𝐾)
5		cdlemn11a.a	. . 3 ⊢ 𝐴 = (Atoms‘𝐾)
6		cdlemn11a.h	. . 3 ⊢ 𝐻 = (LHyp‘𝐾)
7		cdlemn11a.p	. . 3 ⊢ 𝑃 = ((oc‘𝐾)‘𝑊)
8		cdlemn11a.o	. . 3 ⊢ 𝑂 = (ℎ ∈ 𝑇 ↦ ( I ↾ 𝐵))
9		cdlemn11a.t	. . 3 ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)
10		cdlemn11a.r	. . 3 ⊢ 𝑅 = ((trL‘𝐾)‘𝑊)
11		cdlemn11a.e	. . 3 ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊)
12		cdlemn11a.i	. . 3 ⊢ 𝐼 = ((DIsoB‘𝐾)‘𝑊)
13		cdlemn11a.J	. . 3 ⊢ 𝐽 = ((DIsoC‘𝐾)‘𝑊)
14		cdlemn11a.u	. . 3 ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)
15		cdlemn11a.d	. . 3 ⊢ + = (+_g‘𝑈)
16		cdlemn11a.s	. . 3 ⊢ ⊕ = (LSSum‘𝑈)
17		cdlemn11a.f	. . 3 ⊢ 𝐹 = (℩ℎ ∈ 𝑇 (ℎ‘𝑃) = 𝑄)
18		cdlemn11a.g	. . 3 ⊢ 𝐺 = (℩ℎ ∈ 𝑇 (ℎ‘𝑃) = 𝑁)
19	2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18	cdlemn11a 41206	. 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ≤ 𝑊) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ (𝐽‘𝑁) ⊆ ((𝐽‘𝑄) ⊕ (𝐼‘𝑋))) → ⟨𝐺, ( I ↾ 𝑇)⟩ ∈ (𝐽‘𝑁))
20	1, 19	sseldd 3938	1 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ≤ 𝑊) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ (𝐽‘𝑁) ⊆ ((𝐽‘𝑄) ⊕ (𝐼‘𝑋))) → ⟨𝐺, ( I ↾ 𝑇)⟩ ∈ ((𝐽‘𝑄) ⊕ (𝐼‘𝑋)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 395 ∧ w3a 1086 = wceq 1540 ∈ wcel 2109 ⊆ wss 3905 ⟨cop 4585 class class class wbr 5095 ↦ cmpt 5176 I cid 5517 ↾ cres 5625 ‘cfv 6486 ℩crio 7309 (class class class)co 7353 Basecbs 17139 +_gcplusg 17180 lecple 17187 occoc 17188 joincjn 18236 LSSumclsm 19532 Atomscatm 39261 HLchlt 39348 LHypclh 39983 LTrncltrn 40100 trLctrl 40157 TEndoctendo 40751 DVecHcdvh 41077 DIsoBcdib 41137 DIsoCcdic 41171

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2701 ax-rep 5221 ax-sep 5238 ax-nul 5248 ax-pow 5307 ax-pr 5374 ax-un 7675 ax-riotaBAD 38951

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2533 df-eu 2562 df-clab 2708 df-cleq 2721 df-clel 2803 df-nfc 2878 df-ne 2926 df-ral 3045 df-rex 3054 df-rmo 3345 df-reu 3346 df-rab 3397 df-v 3440 df-sbc 3745 df-csb 3854 df-dif 3908 df-un 3910 df-in 3912 df-ss 3922 df-nul 4287 df-if 4479 df-pw 4555 df-sn 4580 df-pr 4582 df-op 4586 df-uni 4862 df-iun 4946 df-iin 4947 df-br 5096 df-opab 5158 df-mpt 5177 df-id 5518 df-xp 5629 df-rel 5630 df-cnv 5631 df-co 5632 df-dm 5633 df-rn 5634 df-res 5635 df-ima 5636 df-iota 6442 df-fun 6488 df-fn 6489 df-f 6490 df-f1 6491 df-fo 6492 df-f1o 6493 df-fv 6494 df-riota 7310 df-ov 7356 df-oprab 7357 df-mpo 7358 df-1st 7931 df-2nd 7932 df-undef 8213 df-map 8762 df-proset 18219 df-poset 18238 df-plt 18253 df-lub 18269 df-glb 18270 df-join 18271 df-meet 18272 df-p0 18348 df-p1 18349 df-lat 18357 df-clat 18424 df-oposet 39174 df-ol 39176 df-oml 39177 df-covers 39264 df-ats 39265 df-atl 39296 df-cvlat 39320 df-hlat 39349 df-llines 39497 df-lplanes 39498 df-lvols 39499 df-lines 39500 df-psubsp 39502 df-pmap 39503 df-padd 39795 df-lhyp 39987 df-laut 39988 df-ldil 40103 df-ltrn 40104 df-trl 40158 df-tendo 40754 df-dic 41172

This theorem is referenced by: cdlemn11c 41208

W3C validator