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 41188

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 1139	. 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 41187	. 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ≤ 𝑊) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ (𝐽‘𝑁) ⊆ ((𝐽‘𝑄) ⊕ (𝐼‘𝑋))) → ⟨𝐺, ( I ↾ 𝑇)⟩ ∈ (𝐽‘𝑁))
20	1, 19	sseldd 3983	1 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ≤ 𝑊) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ (𝐽‘𝑁) ⊆ ((𝐽‘𝑄) ⊕ (𝐼‘𝑋))) → ⟨𝐺, ( I ↾ 𝑇)⟩ ∈ ((𝐽‘𝑄) ⊕ (𝐼‘𝑋)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 395 ∧ w3a 1087 = wceq 1540 ∈ wcel 2108 ⊆ wss 3950 ⟨cop 4630 class class class wbr 5141 ↦ cmpt 5223 I cid 5575 ↾ cres 5685 ‘cfv 6559 ℩crio 7385 (class class class)co 7429 Basecbs 17243 +_gcplusg 17293 lecple 17300 occoc 17301 joincjn 18353 LSSumclsm 19648 Atomscatm 39242 HLchlt 39329 LHypclh 39964 LTrncltrn 40081 trLctrl 40138 TEndoctendo 40732 DVecHcdvh 41058 DIsoBcdib 41118 DIsoCcdic 41152

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 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2157 ax-12 2177 ax-ext 2707 ax-rep 5277 ax-sep 5294 ax-nul 5304 ax-pow 5363 ax-pr 5430 ax-un 7751 ax-riotaBAD 38932

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2065 df-mo 2539 df-eu 2568 df-clab 2714 df-cleq 2728 df-clel 2815 df-nfc 2891 df-ne 2940 df-ral 3061 df-rex 3070 df-rmo 3379 df-reu 3380 df-rab 3436 df-v 3481 df-sbc 3788 df-csb 3899 df-dif 3953 df-un 3955 df-in 3957 df-ss 3967 df-nul 4333 df-if 4525 df-pw 4600 df-sn 4625 df-pr 4627 df-op 4631 df-uni 4906 df-iun 4991 df-iin 4992 df-br 5142 df-opab 5204 df-mpt 5224 df-id 5576 df-xp 5689 df-rel 5690 df-cnv 5691 df-co 5692 df-dm 5693 df-rn 5694 df-res 5695 df-ima 5696 df-iota 6512 df-fun 6561 df-fn 6562 df-f 6563 df-f1 6564 df-fo 6565 df-f1o 6566 df-fv 6567 df-riota 7386 df-ov 7432 df-oprab 7433 df-mpo 7434 df-1st 8010 df-2nd 8011 df-undef 8294 df-map 8864 df-proset 18336 df-poset 18355 df-plt 18371 df-lub 18387 df-glb 18388 df-join 18389 df-meet 18390 df-p0 18466 df-p1 18467 df-lat 18473 df-clat 18540 df-oposet 39155 df-ol 39157 df-oml 39158 df-covers 39245 df-ats 39246 df-atl 39277 df-cvlat 39301 df-hlat 39330 df-llines 39478 df-lplanes 39479 df-lvols 39480 df-lines 39481 df-psubsp 39483 df-pmap 39484 df-padd 39776 df-lhyp 39968 df-laut 39969 df-ldil 40084 df-ltrn 40085 df-trl 40139 df-tendo 40735 df-dic 41153

This theorem is referenced by: cdlemn11c 41189

W3C validator