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 41401

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 1136	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ (𝑠 ∈ 𝐸 ∧ 𝑔 ∈ 𝑇)) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
2		simp3l 1202	. . . 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 40218	. . . . . 6 ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊))
8	1, 7	syl 17	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ (𝑠 ∈ 𝐸 ∧ 𝑔 ∈ 𝑇)) → (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊))
9		simp2l 1200	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ (𝑠 ∈ 𝐸 ∧ 𝑔 ∈ 𝑇)) → (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊))
10		cdlemn8.t	. . . . . 6 ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)
11		cdlemn8.f	. . . . . 6 ⊢ 𝐹 = (℩ℎ ∈ 𝑇 (ℎ‘𝑃) = 𝑄)
12	3, 4, 5, 10, 11	ltrniotacl 40778	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → 𝐹 ∈ 𝑇)
13	1, 8, 9, 12	syl3anc 1373	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ (𝑠 ∈ 𝐸 ∧ 𝑔 ∈ 𝑇)) → 𝐹 ∈ 𝑇)
14		cdlemn8.e	. . . . 5 ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊)
15	5, 10, 14	tendocl 40966	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑠 ∈ 𝐸 ∧ 𝐹 ∈ 𝑇) → (𝑠‘𝐹) ∈ 𝑇)
16	1, 2, 13, 15	syl3anc 1373	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ (𝑠 ∈ 𝐸 ∧ 𝑔 ∈ 𝑇)) → (𝑠‘𝐹) ∈ 𝑇)
17		simp3r 1203	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ (𝑠 ∈ 𝐸 ∧ 𝑔 ∈ 𝑇)) → 𝑔 ∈ 𝑇)
18		cdlemn8.b	. . . . 5 ⊢ 𝐵 = (Base‘𝐾)
19		cdlemn8.o	. . . . 5 ⊢ 𝑂 = (ℎ ∈ 𝑇 ↦ ( I ↾ 𝐵))
20	18, 5, 10, 14, 19	tendo0cl 40989	. . . 4 ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → 𝑂 ∈ 𝐸)
21	1, 20	syl 17	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ (𝑠 ∈ 𝐸 ∧ 𝑔 ∈ 𝑇)) → 𝑂 ∈ 𝐸)
22		cdlemn8.u	. . . 4 ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)
23		eqid 2734	. . . 4 ⊢ (Scalar‘𝑈) = (Scalar‘𝑈)
24		cdlemn8.s	. . . 4 ⊢ + = (+_g‘𝑈)
25		eqid 2734	. . . 4 ⊢ (+_g‘(Scalar‘𝑈)) = (+_g‘(Scalar‘𝑈))
26	5, 10, 14, 22, 23, 24, 25	dvhopvadd 41292	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑠‘𝐹) ∈ 𝑇 ∧ 𝑠 ∈ 𝐸) ∧ (𝑔 ∈ 𝑇 ∧ 𝑂 ∈ 𝐸)) → (⟨(𝑠‘𝐹), 𝑠⟩ + ⟨𝑔, 𝑂⟩) = ⟨((𝑠‘𝐹) ∘ 𝑔), (𝑠(+_g‘(Scalar‘𝑈))𝑂)⟩)
27	1, 16, 2, 17, 21, 26	syl122anc 1381	. 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ (𝑠 ∈ 𝐸 ∧ 𝑔 ∈ 𝑇)) → (⟨(𝑠‘𝐹), 𝑠⟩ + ⟨𝑔, 𝑂⟩) = ⟨((𝑠‘𝐹) ∘ 𝑔), (𝑠(+_g‘(Scalar‘𝑈))𝑂)⟩)
28		eqid 2734	. . . . . . 7 ⊢ (𝑡 ∈ 𝐸, 𝑢 ∈ 𝐸 ↦ (ℎ ∈ 𝑇 ↦ ((𝑡‘ℎ) ∘ (𝑢‘ℎ)))) = (𝑡 ∈ 𝐸, 𝑢 ∈ 𝐸 ↦ (ℎ ∈ 𝑇 ↦ ((𝑡‘ℎ) ∘ (𝑢‘ℎ))))
29	5, 10, 14, 22, 23, 28, 25	dvhfplusr 41283	. . . . . 6 ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → (+_g‘(Scalar‘𝑈)) = (𝑡 ∈ 𝐸, 𝑢 ∈ 𝐸 ↦ (ℎ ∈ 𝑇 ↦ ((𝑡‘ℎ) ∘ (𝑢‘ℎ)))))
30	1, 29	syl 17	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ (𝑠 ∈ 𝐸 ∧ 𝑔 ∈ 𝑇)) → (+_g‘(Scalar‘𝑈)) = (𝑡 ∈ 𝐸, 𝑢 ∈ 𝐸 ↦ (ℎ ∈ 𝑇 ↦ ((𝑡‘ℎ) ∘ (𝑢‘ℎ)))))
31	30	oveqd 7373	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ (𝑠 ∈ 𝐸 ∧ 𝑔 ∈ 𝑇)) → (𝑠(+_g‘(Scalar‘𝑈))𝑂) = (𝑠(𝑡 ∈ 𝐸, 𝑢 ∈ 𝐸 ↦ (ℎ ∈ 𝑇 ↦ ((𝑡‘ℎ) ∘ (𝑢‘ℎ))))𝑂))
32	18, 5, 10, 14, 19, 28	tendo0plr 40991	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑠 ∈ 𝐸) → (𝑠(𝑡 ∈ 𝐸, 𝑢 ∈ 𝐸 ↦ (ℎ ∈ 𝑇 ↦ ((𝑡‘ℎ) ∘ (𝑢‘ℎ))))𝑂) = 𝑠)
33	1, 2, 32	syl2anc 584	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ (𝑠 ∈ 𝐸 ∧ 𝑔 ∈ 𝑇)) → (𝑠(𝑡 ∈ 𝐸, 𝑢 ∈ 𝐸 ↦ (ℎ ∈ 𝑇 ↦ ((𝑡‘ℎ) ∘ (𝑢‘ℎ))))𝑂) = 𝑠)
34	31, 33	eqtrd 2769	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ (𝑠 ∈ 𝐸 ∧ 𝑔 ∈ 𝑇)) → (𝑠(+_g‘(Scalar‘𝑈))𝑂) = 𝑠)
35	34	opeq2d 4834	. 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ (𝑠 ∈ 𝐸 ∧ 𝑔 ∈ 𝑇)) → ⟨((𝑠‘𝐹) ∘ 𝑔), (𝑠(+_g‘(Scalar‘𝑈))𝑂)⟩ = ⟨((𝑠‘𝐹) ∘ 𝑔), 𝑠⟩)
36	27, 35	eqtrd 2769	1 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ (𝑠 ∈ 𝐸 ∧ 𝑔 ∈ 𝑇)) → (⟨(𝑠‘𝐹), 𝑠⟩ + ⟨𝑔, 𝑂⟩) = ⟨((𝑠‘𝐹) ∘ 𝑔), 𝑠⟩)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 395 ∧ w3a 1086 = wceq 1541 ∈ wcel 2113 ⟨cop 4584 class class class wbr 5096 ↦ cmpt 5177 I cid 5516 ↾ cres 5624 ∘ ccom 5626 ‘cfv 6490 ℩crio 7312 (class class class)co 7356 ∈ cmpo 7358 Basecbs 17134 +_gcplusg 17175 Scalarcsca 17178 lecple 17182 occoc 17183 Atomscatm 39462 HLchlt 39549 LHypclh 40183 LTrncltrn 40300 TEndoctendo 40951 DVecHcdvh 41277

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2115 ax-9 2123 ax-10 2146 ax-11 2162 ax-12 2182 ax-ext 2706 ax-rep 5222 ax-sep 5239 ax-nul 5249 ax-pow 5308 ax-pr 5375 ax-un 7678 ax-cnex 11080 ax-resscn 11081 ax-1cn 11082 ax-icn 11083 ax-addcl 11084 ax-addrcl 11085 ax-mulcl 11086 ax-mulrcl 11087 ax-mulcom 11088 ax-addass 11089 ax-mulass 11090 ax-distr 11091 ax-i2m1 11092 ax-1ne0 11093 ax-1rid 11094 ax-rnegex 11095 ax-rrecex 11096 ax-cnre 11097 ax-pre-lttri 11098 ax-pre-lttrn 11099 ax-pre-ltadd 11100 ax-pre-mulgt0 11101 ax-riotaBAD 39152

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2068 df-mo 2537 df-eu 2567 df-clab 2713 df-cleq 2726 df-clel 2809 df-nfc 2883 df-ne 2931 df-nel 3035 df-ral 3050 df-rex 3059 df-rmo 3348 df-reu 3349 df-rab 3398 df-v 3440 df-sbc 3739 df-csb 3848 df-dif 3902 df-un 3904 df-in 3906 df-ss 3916 df-pss 3919 df-nul 4284 df-if 4478 df-pw 4554 df-sn 4579 df-pr 4581 df-tp 4583 df-op 4585 df-uni 4862 df-iun 4946 df-iin 4947 df-br 5097 df-opab 5159 df-mpt 5178 df-tr 5204 df-id 5517 df-eprel 5522 df-po 5530 df-so 5531 df-fr 5575 df-we 5577 df-xp 5628 df-rel 5629 df-cnv 5630 df-co 5631 df-dm 5632 df-rn 5633 df-res 5634 df-ima 5635 df-pred 6257 df-ord 6318 df-on 6319 df-lim 6320 df-suc 6321 df-iota 6446 df-fun 6492 df-fn 6493 df-f 6494 df-f1 6495 df-fo 6496 df-f1o 6497 df-fv 6498 df-riota 7313 df-ov 7359 df-oprab 7360 df-mpo 7361 df-om 7807 df-1st 7931 df-2nd 7932 df-undef 8213 df-frecs 8221 df-wrecs 8252 df-recs 8301 df-rdg 8339 df-1o 8395 df-er 8633 df-map 8763 df-en 8882 df-dom 8883 df-sdom 8884 df-fin 8885 df-pnf 11166 df-mnf 11167 df-xr 11168 df-ltxr 11169 df-le 11170 df-sub 11364 df-neg 11365 df-nn 12144 df-2 12206 df-3 12207 df-4 12208 df-5 12209 df-6 12210 df-n0 12400 df-z 12487 df-uz 12750 df-fz 13422 df-struct 17072 df-slot 17107 df-ndx 17119 df-base 17135 df-plusg 17188 df-mulr 17189 df-sca 17191 df-vsca 17192 df-proset 18215 df-poset 18234 df-plt 18249 df-lub 18265 df-glb 18266 df-join 18267 df-meet 18268 df-p0 18344 df-p1 18345 df-lat 18353 df-clat 18420 df-oposet 39375 df-ol 39377 df-oml 39378 df-covers 39465 df-ats 39466 df-atl 39497 df-cvlat 39521 df-hlat 39550 df-llines 39697 df-lplanes 39698 df-lvols 39699 df-lines 39700 df-psubsp 39702 df-pmap 39703 df-padd 39995 df-lhyp 40187 df-laut 40188 df-ldil 40303 df-ltrn 40304 df-trl 40358 df-tendo 40954 df-edring 40956 df-dvech 41278

This theorem is referenced by: cdlemn7 41402 dihordlem6 41412

W3C validator