cdlemn6 - Mathbox for Norm Megill

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

Theorem cdlemn6 42368

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

**Hypotheses**
Ref	Expression
cdlemn8.b	⊢ 𝐵 = (Base‘𝐾)
cdlemn8.l	⊢ ≤ = (le‘𝐾)
cdlemn8.a	⊢ 𝐴 = (Atoms‘𝐾)
cdlemn8.h	⊢ 𝐻 = (LHyp‘𝐾)
cdlemn8.p	⊢ 𝑃 = ((oc‘𝐾)‘𝑊)
cdlemn8.o	⊢ 𝑂 = (ℎ ∈ 𝑇 ↦ ( I ↾ 𝐵))
cdlemn8.t	⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)
cdlemn8.e	⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊)
cdlemn8.u	⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)
cdlemn8.s	⊢ + = (+_g‘𝑈)
cdlemn8.f	⊢ 𝐹 = (℩ℎ ∈ 𝑇 (ℎ‘𝑃) = 𝑄)

**Assertion**
Ref	Expression
cdlemn6	⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ (𝑠 ∈ 𝐸 ∧ 𝑔 ∈ 𝑇)) → (⟨(𝑠‘𝐹), 𝑠⟩ + ⟨𝑔, 𝑂⟩) = ⟨((𝑠‘𝐹) ∘ 𝑔), 𝑠⟩)

Distinct variable groups: ≤ ,ℎ 𝐴,ℎ 𝐵,ℎ ℎ,𝐻 ℎ,𝐾 𝑇,ℎ 𝑃,ℎ 𝑄,ℎ ℎ,𝑊 Allowed substitution hints: 𝐴(𝑔, 𝑠) 𝐵(𝑔, 𝑠) 𝑃(𝑔, 𝑠) + (𝑔, ℎ, 𝑠) 𝑄(𝑔, 𝑠) 𝑅(𝑔, ℎ, 𝑠) 𝑇(𝑔, 𝑠) 𝑈(𝑔, ℎ, 𝑠) 𝐸(𝑔, ℎ, 𝑠) 𝐹(𝑔, ℎ, 𝑠) 𝐻(𝑔, 𝑠) 𝐾(𝑔, 𝑠) ≤ (𝑔, 𝑠) 𝑂(𝑔, ℎ, 𝑠) 𝑊(𝑔, 𝑠)

Proof of Theorem cdlemn6 Dummy variables 𝑡 𝑢 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		simp1 1154	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ (𝑠 ∈ 𝐸 ∧ 𝑔 ∈ 𝑇)) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
2		simp3l 1220	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ (𝑠 ∈ 𝐸 ∧ 𝑔 ∈ 𝑇)) → 𝑠 ∈ 𝐸)
3		cdlemn8.l	. . . . . . 7 ⊢ ≤ = (le‘𝐾)
4		cdlemn8.a	. . . . . . 7 ⊢ 𝐴 = (Atoms‘𝐾)
5		cdlemn8.h	. . . . . . 7 ⊢ 𝐻 = (LHyp‘𝐾)
6		cdlemn8.p	. . . . . . 7 ⊢ 𝑃 = ((oc‘𝐾)‘𝑊)
7	3, 4, 5, 6	lhpocnel2 41185	. . . . . 6 ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊))
8	1, 7	syl 18	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ (𝑠 ∈ 𝐸 ∧ 𝑔 ∈ 𝑇)) → (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊))
9		simp2l 1218	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ (𝑠 ∈ 𝐸 ∧ 𝑔 ∈ 𝑇)) → (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊))
10		cdlemn8.t	. . . . . 6 ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)
11		cdlemn8.f	. . . . . 6 ⊢ 𝐹 = (℩ℎ ∈ 𝑇 (ℎ‘𝑃) = 𝑄)
12	3, 4, 5, 10, 11	ltrniotacl 41745	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → 𝐹 ∈ 𝑇)
13	1, 8, 9, 12	syl3anc 1398	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ (𝑠 ∈ 𝐸 ∧ 𝑔 ∈ 𝑇)) → 𝐹 ∈ 𝑇)
14		cdlemn8.e	. . . . 5 ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊)
15	5, 10, 14	tendocl 41933	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑠 ∈ 𝐸 ∧ 𝐹 ∈ 𝑇) → (𝑠‘𝐹) ∈ 𝑇)
16	1, 2, 13, 15	syl3anc 1398	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ (𝑠 ∈ 𝐸 ∧ 𝑔 ∈ 𝑇)) → (𝑠‘𝐹) ∈ 𝑇)
17		simp3r 1221	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ (𝑠 ∈ 𝐸 ∧ 𝑔 ∈ 𝑇)) → 𝑔 ∈ 𝑇)
18		cdlemn8.b	. . . . 5 ⊢ 𝐵 = (Base‘𝐾)
19		cdlemn8.o	. . . . 5 ⊢ 𝑂 = (ℎ ∈ 𝑇 ↦ ( I ↾ 𝐵))
20	18, 5, 10, 14, 19	tendo0cl 41956	. . . 4 ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → 𝑂 ∈ 𝐸)
21	1, 20	syl 18	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ (𝑠 ∈ 𝐸 ∧ 𝑔 ∈ 𝑇)) → 𝑂 ∈ 𝐸)
22		cdlemn8.u	. . . 4 ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)
23		eqid 2760	. . . 4 ⊢ (Scalar‘𝑈) = (Scalar‘𝑈)
24		cdlemn8.s	. . . 4 ⊢ + = (+_g‘𝑈)
25		eqid 2760	. . . 4 ⊢ (+_g‘(Scalar‘𝑈)) = (+_g‘(Scalar‘𝑈))
26	5, 10, 14, 22, 23, 24, 25	dvhopvadd 42259	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑠‘𝐹) ∈ 𝑇 ∧ 𝑠 ∈ 𝐸) ∧ (𝑔 ∈ 𝑇 ∧ 𝑂 ∈ 𝐸)) → (⟨(𝑠‘𝐹), 𝑠⟩ + ⟨𝑔, 𝑂⟩) = ⟨((𝑠‘𝐹) ∘ 𝑔), (𝑠(+_g‘(Scalar‘𝑈))𝑂)⟩)
27	1, 16, 2, 17, 21, 26	syl122anc 1406	. 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ (𝑠 ∈ 𝐸 ∧ 𝑔 ∈ 𝑇)) → (⟨(𝑠‘𝐹), 𝑠⟩ + ⟨𝑔, 𝑂⟩) = ⟨((𝑠‘𝐹) ∘ 𝑔), (𝑠(+_g‘(Scalar‘𝑈))𝑂)⟩)
28		eqid 2760	. . . . . . 7 ⊢ (𝑡 ∈ 𝐸, 𝑢 ∈ 𝐸 ↦ (ℎ ∈ 𝑇 ↦ ((𝑡‘ℎ) ∘ (𝑢‘ℎ)))) = (𝑡 ∈ 𝐸, 𝑢 ∈ 𝐸 ↦ (ℎ ∈ 𝑇 ↦ ((𝑡‘ℎ) ∘ (𝑢‘ℎ))))
29	5, 10, 14, 22, 23, 28, 25	dvhfplusr 42250	. . . . . 6 ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → (+_g‘(Scalar‘𝑈)) = (𝑡 ∈ 𝐸, 𝑢 ∈ 𝐸 ↦ (ℎ ∈ 𝑇 ↦ ((𝑡‘ℎ) ∘ (𝑢‘ℎ)))))
30	1, 29	syl 18	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ (𝑠 ∈ 𝐸 ∧ 𝑔 ∈ 𝑇)) → (+_g‘(Scalar‘𝑈)) = (𝑡 ∈ 𝐸, 𝑢 ∈ 𝐸 ↦ (ℎ ∈ 𝑇 ↦ ((𝑡‘ℎ) ∘ (𝑢‘ℎ)))))
31	30	oveqd 7441	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ (𝑠 ∈ 𝐸 ∧ 𝑔 ∈ 𝑇)) → (𝑠(+_g‘(Scalar‘𝑈))𝑂) = (𝑠(𝑡 ∈ 𝐸, 𝑢 ∈ 𝐸 ↦ (ℎ ∈ 𝑇 ↦ ((𝑡‘ℎ) ∘ (𝑢‘ℎ))))𝑂))
32	18, 5, 10, 14, 19, 28	tendo0plr 41958	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑠 ∈ 𝐸) → (𝑠(𝑡 ∈ 𝐸, 𝑢 ∈ 𝐸 ↦ (ℎ ∈ 𝑇 ↦ ((𝑡‘ℎ) ∘ (𝑢‘ℎ))))𝑂) = 𝑠)
33	1, 2, 32	syl2anc 596	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ (𝑠 ∈ 𝐸 ∧ 𝑔 ∈ 𝑇)) → (𝑠(𝑡 ∈ 𝐸, 𝑢 ∈ 𝐸 ↦ (ℎ ∈ 𝑇 ↦ ((𝑡‘ℎ) ∘ (𝑢‘ℎ))))𝑂) = 𝑠)
34	31, 33	eqtrd 2795	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ (𝑠 ∈ 𝐸 ∧ 𝑔 ∈ 𝑇)) → (𝑠(+_g‘(Scalar‘𝑈))𝑂) = 𝑠)
35	34	opeq2d 4846	. 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ (𝑠 ∈ 𝐸 ∧ 𝑔 ∈ 𝑇)) → ⟨((𝑠‘𝐹) ∘ 𝑔), (𝑠(+_g‘(Scalar‘𝑈))𝑂)⟩ = ⟨((𝑠‘𝐹) ∘ 𝑔), 𝑠⟩)
36	27, 35	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 ⟨cop 4834 class class class wbr 5102 ↦ cmpt 5185 I cid 5545 ↾ cres 5653 ∘ ccom 5655 ‘cfv 6543 ℩crio 7380 (class class class)co 7424 ∈ cmpo 7426 Basecbs 17396 +_gcplusg 17437 Scalarcsca 17440 lecple 17444 occoc 17445 Atomscatm 40429 HLchlt 40516 LHypclh 41150 LTrncltrn 41267 TEndoctendo 41918 DVecHcdvh 42244

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-cnex 11263 ax-resscn 11264 ax-1cn 11265 ax-icn 11266 ax-addcl 11267 ax-addrcl 11268 ax-mulcl 11269 ax-mulrcl 11270 ax-mulcom 11271 ax-addass 11272 ax-mulass 11273 ax-distr 11274 ax-i2m1 11275 ax-1ne0 11276 ax-1rid 11277 ax-rnegex 11278 ax-rrecex 11279 ax-cnre 11280 ax-pre-lttri 11281 ax-pre-lttrn 11282 ax-pre-ltadd 11283 ax-pre-mulgt0 11284 ax-riotaBAD 40119

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-nel 3062 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-pss 4013 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-tp 4589 df-op 4835 df-uni 4867 df-iun 4952 df-iin 4953 df-br 5103 df-opab 5167 df-mpt 5186 df-tr 5212 df-id 5546 df-eprel 5551 df-po 5559 df-so 5560 df-fr 5604 df-we 5606 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-pred 6307 df-ord 6368 df-on 6369 df-lim 6370 df-suc 6371 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-om 7882 df-1st 8005 df-2nd 8006 df-undef 8297 df-frecs 8306 df-wrecs 8337 df-recs 8386 df-rdg 8425 df-1o 8483 df-er 8724 df-map 8856 df-en 8981 df-dom 8982 df-sdom 8983 df-fin 8984 df-pnf 11352 df-mnf 11353 df-xr 11354 df-ltxr 11355 df-le 11356 df-sub 11550 df-neg 11551 df-nn 12343 df-2 12412 df-3 12413 df-4 12414 df-5 12415 df-6 12416 df-n0 12614 df-z 12701 df-uz 12973 df-fz 13647 df-struct 17334 df-slot 17369 df-ndx 17381 df-base 17397 df-plusg 17450 df-mulr 17451 df-sca 17453 df-vsca 17454 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 40342 df-ol 40344 df-oml 40345 df-covers 40432 df-ats 40433 df-atl 40464 df-cvlat 40488 df-hlat 40517 df-llines 40664 df-lplanes 40665 df-lvols 40666 df-lines 40667 df-psubsp 40669 df-pmap 40670 df-padd 40962 df-lhyp 41154 df-laut 41155 df-ldil 41270 df-ltrn 41271 df-trl 41325 df-tendo 41921 df-edring 41923 df-dvech 42245

This theorem is used by: cdlemn7 42369 dihordlem6 42379

W3C validator