dvhvaddcl - Mathbox for Norm Megill

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

Theorem dvhvaddcl 41084

Description: Closure of the vector sum operation for the constructed full vector space H. (Contributed by NM, 26-Oct-2013.) (Revised by Mario Carneiro, 23-Jun-2014.)

**Hypotheses**
Ref	Expression
dvhvaddcl.h	⊢ 𝐻 = (LHyp‘𝐾)
dvhvaddcl.t	⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)
dvhvaddcl.e	⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊)
dvhvaddcl.u	⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)
dvhvaddcl.d	⊢ 𝐷 = (Scalar‘𝑈)
dvhvaddcl.p	⊢ ⨣ = (+_g‘𝐷)
dvhvaddcl.a	⊢ + = (+_g‘𝑈)

**Assertion**
Ref	Expression
dvhvaddcl	⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ (𝑇 × 𝐸) ∧ 𝐺 ∈ (𝑇 × 𝐸))) → (𝐹 + 𝐺) ∈ (𝑇 × 𝐸))

Proof of Theorem dvhvaddcl Dummy variables 𝑎 𝑏 𝑐 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		dvhvaddcl.h	. . 3 ⊢ 𝐻 = (LHyp‘𝐾)
2		dvhvaddcl.t	. . 3 ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)
3		dvhvaddcl.e	. . 3 ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊)
4		dvhvaddcl.u	. . 3 ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)
5		dvhvaddcl.d	. . 3 ⊢ 𝐷 = (Scalar‘𝑈)
6		dvhvaddcl.a	. . 3 ⊢ + = (+_g‘𝑈)
7		dvhvaddcl.p	. . 3 ⊢ ⨣ = (+_g‘𝐷)
8	1, 2, 3, 4, 5, 6, 7	dvhvadd 41081	. 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ (𝑇 × 𝐸) ∧ 𝐺 ∈ (𝑇 × 𝐸))) → (𝐹 + 𝐺) = ⟨((1^st ‘𝐹) ∘ (1^st ‘𝐺)), ((2^nd ‘𝐹) ⨣ (2^nd ‘𝐺))⟩)
9		simpl 482	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ (𝑇 × 𝐸) ∧ 𝐺 ∈ (𝑇 × 𝐸))) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
10		xp1st 7956	. . . . 5 ⊢ (𝐹 ∈ (𝑇 × 𝐸) → (1^st ‘𝐹) ∈ 𝑇)
11	10	ad2antrl 728	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ (𝑇 × 𝐸) ∧ 𝐺 ∈ (𝑇 × 𝐸))) → (1^st ‘𝐹) ∈ 𝑇)
12		xp1st 7956	. . . . 5 ⊢ (𝐺 ∈ (𝑇 × 𝐸) → (1^st ‘𝐺) ∈ 𝑇)
13	12	ad2antll 729	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ (𝑇 × 𝐸) ∧ 𝐺 ∈ (𝑇 × 𝐸))) → (1^st ‘𝐺) ∈ 𝑇)
14	1, 2	ltrnco 40708	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (1^st ‘𝐹) ∈ 𝑇 ∧ (1^st ‘𝐺) ∈ 𝑇) → ((1^st ‘𝐹) ∘ (1^st ‘𝐺)) ∈ 𝑇)
15	9, 11, 13, 14	syl3anc 1373	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ (𝑇 × 𝐸) ∧ 𝐺 ∈ (𝑇 × 𝐸))) → ((1^st ‘𝐹) ∘ (1^st ‘𝐺)) ∈ 𝑇)
16		eqid 2729	. . . . . . 7 ⊢ (𝑎 ∈ 𝐸, 𝑏 ∈ 𝐸 ↦ (𝑐 ∈ 𝑇 ↦ ((𝑎‘𝑐) ∘ (𝑏‘𝑐)))) = (𝑎 ∈ 𝐸, 𝑏 ∈ 𝐸 ↦ (𝑐 ∈ 𝑇 ↦ ((𝑎‘𝑐) ∘ (𝑏‘𝑐))))
17	1, 2, 3, 4, 5, 16, 7	dvhfplusr 41073	. . . . . 6 ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → ⨣ = (𝑎 ∈ 𝐸, 𝑏 ∈ 𝐸 ↦ (𝑐 ∈ 𝑇 ↦ ((𝑎‘𝑐) ∘ (𝑏‘𝑐)))))
18	17	adantr 480	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ (𝑇 × 𝐸) ∧ 𝐺 ∈ (𝑇 × 𝐸))) → ⨣ = (𝑎 ∈ 𝐸, 𝑏 ∈ 𝐸 ↦ (𝑐 ∈ 𝑇 ↦ ((𝑎‘𝑐) ∘ (𝑏‘𝑐)))))
19	18	oveqd 7366	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ (𝑇 × 𝐸) ∧ 𝐺 ∈ (𝑇 × 𝐸))) → ((2^nd ‘𝐹) ⨣ (2^nd ‘𝐺)) = ((2^nd ‘𝐹)(𝑎 ∈ 𝐸, 𝑏 ∈ 𝐸 ↦ (𝑐 ∈ 𝑇 ↦ ((𝑎‘𝑐) ∘ (𝑏‘𝑐))))(2^nd ‘𝐺)))
20		xp2nd 7957	. . . . . 6 ⊢ (𝐹 ∈ (𝑇 × 𝐸) → (2^nd ‘𝐹) ∈ 𝐸)
21	20	ad2antrl 728	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ (𝑇 × 𝐸) ∧ 𝐺 ∈ (𝑇 × 𝐸))) → (2^nd ‘𝐹) ∈ 𝐸)
22		xp2nd 7957	. . . . . 6 ⊢ (𝐺 ∈ (𝑇 × 𝐸) → (2^nd ‘𝐺) ∈ 𝐸)
23	22	ad2antll 729	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ (𝑇 × 𝐸) ∧ 𝐺 ∈ (𝑇 × 𝐸))) → (2^nd ‘𝐺) ∈ 𝐸)
24	1, 2, 3, 16	tendoplcl 40770	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (2^nd ‘𝐹) ∈ 𝐸 ∧ (2^nd ‘𝐺) ∈ 𝐸) → ((2^nd ‘𝐹)(𝑎 ∈ 𝐸, 𝑏 ∈ 𝐸 ↦ (𝑐 ∈ 𝑇 ↦ ((𝑎‘𝑐) ∘ (𝑏‘𝑐))))(2^nd ‘𝐺)) ∈ 𝐸)
25	9, 21, 23, 24	syl3anc 1373	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ (𝑇 × 𝐸) ∧ 𝐺 ∈ (𝑇 × 𝐸))) → ((2^nd ‘𝐹)(𝑎 ∈ 𝐸, 𝑏 ∈ 𝐸 ↦ (𝑐 ∈ 𝑇 ↦ ((𝑎‘𝑐) ∘ (𝑏‘𝑐))))(2^nd ‘𝐺)) ∈ 𝐸)
26	19, 25	eqeltrd 2828	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ (𝑇 × 𝐸) ∧ 𝐺 ∈ (𝑇 × 𝐸))) → ((2^nd ‘𝐹) ⨣ (2^nd ‘𝐺)) ∈ 𝐸)
27		opelxpi 5656	. . 3 ⊢ ((((1^st ‘𝐹) ∘ (1^st ‘𝐺)) ∈ 𝑇 ∧ ((2^nd ‘𝐹) ⨣ (2^nd ‘𝐺)) ∈ 𝐸) → ⟨((1^st ‘𝐹) ∘ (1^st ‘𝐺)), ((2^nd ‘𝐹) ⨣ (2^nd ‘𝐺))⟩ ∈ (𝑇 × 𝐸))
28	15, 26, 27	syl2anc 584	. 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ (𝑇 × 𝐸) ∧ 𝐺 ∈ (𝑇 × 𝐸))) → ⟨((1^st ‘𝐹) ∘ (1^st ‘𝐺)), ((2^nd ‘𝐹) ⨣ (2^nd ‘𝐺))⟩ ∈ (𝑇 × 𝐸))
29	8, 28	eqeltrd 2828	1 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ (𝑇 × 𝐸) ∧ 𝐺 ∈ (𝑇 × 𝐸))) → (𝐹 + 𝐺) ∈ (𝑇 × 𝐸))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 395 = wceq 1540 ∈ wcel 2109 ⟨cop 4583 ↦ cmpt 5173 × cxp 5617 ∘ ccom 5623 ‘cfv 6482 (class class class)co 7349 ∈ cmpo 7351 1^st c1st 7922 2^nd c2nd 7923 +_gcplusg 17161 Scalarcsca 17164 HLchlt 39339 LHypclh 39973 LTrncltrn 40090 TEndoctendo 40741 DVecHcdvh 41067

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 5218 ax-sep 5235 ax-nul 5245 ax-pow 5304 ax-pr 5371 ax-un 7671 ax-cnex 11065 ax-resscn 11066 ax-1cn 11067 ax-icn 11068 ax-addcl 11069 ax-addrcl 11070 ax-mulcl 11071 ax-mulrcl 11072 ax-mulcom 11073 ax-addass 11074 ax-mulass 11075 ax-distr 11076 ax-i2m1 11077 ax-1ne0 11078 ax-1rid 11079 ax-rnegex 11080 ax-rrecex 11081 ax-cnre 11082 ax-pre-lttri 11083 ax-pre-lttrn 11084 ax-pre-ltadd 11085 ax-pre-mulgt0 11086 ax-riotaBAD 38942

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-nel 3030 df-ral 3045 df-rex 3054 df-rmo 3343 df-reu 3344 df-rab 3395 df-v 3438 df-sbc 3743 df-csb 3852 df-dif 3906 df-un 3908 df-in 3910 df-ss 3920 df-pss 3923 df-nul 4285 df-if 4477 df-pw 4553 df-sn 4578 df-pr 4580 df-tp 4582 df-op 4584 df-uni 4859 df-iun 4943 df-iin 4944 df-br 5093 df-opab 5155 df-mpt 5174 df-tr 5200 df-id 5514 df-eprel 5519 df-po 5527 df-so 5528 df-fr 5572 df-we 5574 df-xp 5625 df-rel 5626 df-cnv 5627 df-co 5628 df-dm 5629 df-rn 5630 df-res 5631 df-ima 5632 df-pred 6249 df-ord 6310 df-on 6311 df-lim 6312 df-suc 6313 df-iota 6438 df-fun 6484 df-fn 6485 df-f 6486 df-f1 6487 df-fo 6488 df-f1o 6489 df-fv 6490 df-riota 7306 df-ov 7352 df-oprab 7353 df-mpo 7354 df-om 7800 df-1st 7924 df-2nd 7925 df-undef 8206 df-frecs 8214 df-wrecs 8245 df-recs 8294 df-rdg 8332 df-1o 8388 df-er 8625 df-map 8755 df-en 8873 df-dom 8874 df-sdom 8875 df-fin 8876 df-pnf 11151 df-mnf 11152 df-xr 11153 df-ltxr 11154 df-le 11155 df-sub 11349 df-neg 11350 df-nn 12129 df-2 12191 df-3 12192 df-4 12193 df-5 12194 df-6 12195 df-n0 12385 df-z 12472 df-uz 12736 df-fz 13411 df-struct 17058 df-slot 17093 df-ndx 17105 df-base 17121 df-plusg 17174 df-mulr 17175 df-sca 17177 df-vsca 17178 df-proset 18200 df-poset 18219 df-plt 18234 df-lub 18250 df-glb 18251 df-join 18252 df-meet 18253 df-p0 18329 df-p1 18330 df-lat 18338 df-clat 18405 df-oposet 39165 df-ol 39167 df-oml 39168 df-covers 39255 df-ats 39256 df-atl 39287 df-cvlat 39311 df-hlat 39340 df-llines 39487 df-lplanes 39488 df-lvols 39489 df-lines 39490 df-psubsp 39492 df-pmap 39493 df-padd 39785 df-lhyp 39977 df-laut 39978 df-ldil 40093 df-ltrn 40094 df-trl 40148 df-tendo 40744 df-edring 40746 df-dvech 41068

This theorem is referenced by: dvhvaddass 41086 dvhgrp 41096 dvhlveclem 41097

W3C validator