dia2dimlem13 - Mathbox for Norm Megill

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

Theorem dia2dimlem13 42014

Description: Lemma for dia2dim 42015. Eliminate 𝑈 ≠ 𝑉 condition. (Contributed by NM, 8-Sep-2014.)

**Hypotheses**
Ref	Expression
dia2dimlem12.l	⊢ ≤ = (le‘𝐾)
dia2dimlem12.j	⊢ ∨ = (join‘𝐾)
dia2dimlem12.m	⊢ ∧ = (meet‘𝐾)
dia2dimlem12.a	⊢ 𝐴 = (Atoms‘𝐾)
dia2dimlem12.h	⊢ 𝐻 = (LHyp‘𝐾)
dia2dimlem12.t	⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)
dia2dimlem12.r	⊢ 𝑅 = ((trL‘𝐾)‘𝑊)
dia2dimlem12.y	⊢ 𝑌 = ((DVecA‘𝐾)‘𝑊)
dia2dimlem12.s	⊢ 𝑆 = (LSubSp‘𝑌)
dia2dimlem12.pl	⊢ ⊕ = (LSSum‘𝑌)
dia2dimlem12.n	⊢ 𝑁 = (LSpan‘𝑌)
dia2dimlem12.i	⊢ 𝐼 = ((DIsoA‘𝐾)‘𝑊)
dia2dimlem12.k	⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
dia2dimlem12.u	⊢ (𝜑 → (𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊))
dia2dimlem12.v	⊢ (𝜑 → (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊))

**Assertion**
Ref	Expression
dia2dimlem13	⊢ (𝜑 → (𝐼‘(𝑈 ∨ 𝑉)) ⊆ ((𝐼‘𝑈) ⊕ (𝐼‘𝑉)))

**Proof of Theorem dia2dimlem13**
Step	Hyp	Ref	Expression
1		oveq2 7424	. . . . . . 7 ⊢ (𝑈 = 𝑉 → (𝑈 ∨ 𝑈) = (𝑈 ∨ 𝑉))
2	1	adantl 487	. . . . . 6 ⊢ ((𝜑 ∧ 𝑈 = 𝑉) → (𝑈 ∨ 𝑈) = (𝑈 ∨ 𝑉))
3		dia2dimlem12.k	. . . . . . . . 9 ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
4	3	simpld 500	. . . . . . . 8 ⊢ (𝜑 → 𝐾 ∈ HL)
5		dia2dimlem12.u	. . . . . . . . 9 ⊢ (𝜑 → (𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊))
6	5	simpld 500	. . . . . . . 8 ⊢ (𝜑 → 𝑈 ∈ 𝐴)
7		dia2dimlem12.j	. . . . . . . . 9 ⊢ ∨ = (join‘𝐾)
8		dia2dimlem12.a	. . . . . . . . 9 ⊢ 𝐴 = (Atoms‘𝐾)
9	7, 8	hlatjidm 40307	. . . . . . . 8 ⊢ ((𝐾 ∈ HL ∧ 𝑈 ∈ 𝐴) → (𝑈 ∨ 𝑈) = 𝑈)
10	4, 6, 9	syl2anc 596	. . . . . . 7 ⊢ (𝜑 → (𝑈 ∨ 𝑈) = 𝑈)
11	10	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝑈 = 𝑉) → (𝑈 ∨ 𝑈) = 𝑈)
12	2, 11	eqtr3d 2797	. . . . 5 ⊢ ((𝜑 ∧ 𝑈 = 𝑉) → (𝑈 ∨ 𝑉) = 𝑈)
13	12	fveq2d 6885	. . . 4 ⊢ ((𝜑 ∧ 𝑈 = 𝑉) → (𝐼‘(𝑈 ∨ 𝑉)) = (𝐼‘𝑈))
14		ssid 3953	. . . 4 ⊢ (𝐼‘𝑈) ⊆ (𝐼‘𝑈)
15	13, 14	eqsstrdi 3975	. . 3 ⊢ ((𝜑 ∧ 𝑈 = 𝑉) → (𝐼‘(𝑈 ∨ 𝑉)) ⊆ (𝐼‘𝑈))
16		dia2dimlem12.h	. . . . . . . 8 ⊢ 𝐻 = (LHyp‘𝐾)
17		dia2dimlem12.y	. . . . . . . 8 ⊢ 𝑌 = ((DVecA‘𝐾)‘𝑊)
18	16, 17	dvalvec 41964	. . . . . . 7 ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → 𝑌 ∈ LVec)
19		lveclmod 21320	. . . . . . 7 ⊢ (𝑌 ∈ LVec → 𝑌 ∈ LMod)
20	3, 18, 19	3syl 19	. . . . . 6 ⊢ (𝜑 → 𝑌 ∈ LMod)
21		eqid 2760	. . . . . . . . 9 ⊢ (Base‘𝐾) = (Base‘𝐾)
22	21, 8	atbase 40227	. . . . . . . 8 ⊢ (𝑈 ∈ 𝐴 → 𝑈 ∈ (Base‘𝐾))
23	6, 22	syl 18	. . . . . . 7 ⊢ (𝜑 → 𝑈 ∈ (Base‘𝐾))
24	5	simprd 501	. . . . . . 7 ⊢ (𝜑 → 𝑈 ≤ 𝑊)
25		dia2dimlem12.l	. . . . . . . 8 ⊢ ≤ = (le‘𝐾)
26		dia2dimlem12.i	. . . . . . . 8 ⊢ 𝐼 = ((DIsoA‘𝐾)‘𝑊)
27		dia2dimlem12.s	. . . . . . . 8 ⊢ 𝑆 = (LSubSp‘𝑌)
28	21, 25, 16, 17, 26, 27	dialss 41984	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑈 ∈ (Base‘𝐾) ∧ 𝑈 ≤ 𝑊)) → (𝐼‘𝑈) ∈ 𝑆)
29	3, 23, 24, 28	syl12anc 850	. . . . . 6 ⊢ (𝜑 → (𝐼‘𝑈) ∈ 𝑆)
30	27	lsssubg 21171	. . . . . 6 ⊢ ((𝑌 ∈ LMod ∧ (𝐼‘𝑈) ∈ 𝑆) → (𝐼‘𝑈) ∈ (SubGrp‘𝑌))
31	20, 29, 30	syl2anc 596	. . . . 5 ⊢ (𝜑 → (𝐼‘𝑈) ∈ (SubGrp‘𝑌))
32		dia2dimlem12.pl	. . . . . 6 ⊢ ⊕ = (LSSum‘𝑌)
33	32	lsmidm 19816	. . . . 5 ⊢ ((𝐼‘𝑈) ∈ (SubGrp‘𝑌) → ((𝐼‘𝑈) ⊕ (𝐼‘𝑈)) = (𝐼‘𝑈))
34	31, 33	syl 18	. . . 4 ⊢ (𝜑 → ((𝐼‘𝑈) ⊕ (𝐼‘𝑈)) = (𝐼‘𝑈))
35		fveq2 6881	. . . . 5 ⊢ (𝑈 = 𝑉 → (𝐼‘𝑈) = (𝐼‘𝑉))
36	35	oveq2d 7432	. . . 4 ⊢ (𝑈 = 𝑉 → ((𝐼‘𝑈) ⊕ (𝐼‘𝑈)) = ((𝐼‘𝑈) ⊕ (𝐼‘𝑉)))
37	34, 36	sylan9req 2816	. . 3 ⊢ ((𝜑 ∧ 𝑈 = 𝑉) → (𝐼‘𝑈) = ((𝐼‘𝑈) ⊕ (𝐼‘𝑉)))
38	15, 37	sseqtrd 3967	. 2 ⊢ ((𝜑 ∧ 𝑈 = 𝑉) → (𝐼‘(𝑈 ∨ 𝑉)) ⊆ ((𝐼‘𝑈) ⊕ (𝐼‘𝑉)))
39		dia2dimlem12.m	. . 3 ⊢ ∧ = (meet‘𝐾)
40		dia2dimlem12.t	. . 3 ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)
41		dia2dimlem12.r	. . 3 ⊢ 𝑅 = ((trL‘𝐾)‘𝑊)
42		dia2dimlem12.n	. . 3 ⊢ 𝑁 = (LSpan‘𝑌)
43	3	adantr 486	. . 3 ⊢ ((𝜑 ∧ 𝑈 ≠ 𝑉) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
44	5	adantr 486	. . 3 ⊢ ((𝜑 ∧ 𝑈 ≠ 𝑉) → (𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊))
45		dia2dimlem12.v	. . . 4 ⊢ (𝜑 → (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊))
46	45	adantr 486	. . 3 ⊢ ((𝜑 ∧ 𝑈 ≠ 𝑉) → (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊))
47		simpr 490	. . 3 ⊢ ((𝜑 ∧ 𝑈 ≠ 𝑉) → 𝑈 ≠ 𝑉)
48	25, 7, 39, 8, 16, 40, 41, 17, 27, 32, 42, 26, 43, 44, 46, 47	dia2dimlem12 42013	. 2 ⊢ ((𝜑 ∧ 𝑈 ≠ 𝑉) → (𝐼‘(𝑈 ∨ 𝑉)) ⊆ ((𝐼‘𝑈) ⊕ (𝐼‘𝑉)))
49	38, 48	pm2.61dane 3042	1 ⊢ (𝜑 → (𝐼‘(𝑈 ∨ 𝑉)) ⊆ ((𝐼‘𝑈) ⊕ (𝐼‘𝑉)))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ∧ wa 401 = wceq 1570 ∈ wcel 2145 ≠ wne 2955 ⊆ wss 3899 class class class wbr 5103 ‘cfv 6535 (class class class)co 7416 Basecbs 17326 lecple 17374 joincjn 18424 meetcmee 18425 SubGrpcsubg 19269 LSSumclsm 19787 LModclmod 21074 LSubSpclss 21145 LSpanclspn 21185 LVecclvec 21316 Atomscatm 40201 HLchlt 40288 LHypclh 40922 LTrncltrn 41039 trLctrl 41096 DVecAcdveca 41940 DIsoAcdia 41966

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2213 ax-ext 2732 ax-rep 5232 ax-sep 5251 ax-nul 5263 ax-pow 5330 ax-pr 5398 ax-un 7742 ax-cnex 11205 ax-resscn 11206 ax-1cn 11207 ax-icn 11208 ax-addcl 11209 ax-addrcl 11210 ax-mulcl 11211 ax-mulrcl 11212 ax-mulcom 11213 ax-addass 11214 ax-mulass 11215 ax-distr 11216 ax-i2m1 11217 ax-1ne0 11218 ax-1rid 11219 ax-rnegex 11220 ax-rrecex 11221 ax-cnre 11222 ax-pre-lttri 11223 ax-pre-lttrn 11224 ax-pre-ltadd 11225 ax-pre-mulgt0 11226 ax-riotaBAD 39891

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 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 3740 df-csb 3848 df-dif 3902 df-un 3904 df-in 3906 df-ss 3916 df-pss 3919 df-nul 4280 df-if 4483 df-pw 4559 df-sn 4585 df-pr 4587 df-tp 4589 df-op 4591 df-uni 4868 df-int 4908 df-iun 4953 df-iin 4954 df-br 5104 df-opab 5168 df-mpt 5187 df-tr 5213 df-id 5550 df-eprel 5555 df-po 5563 df-so 5564 df-fr 5608 df-we 5610 df-xp 5661 df-rel 5662 df-cnv 5663 df-co 5664 df-dm 5665 df-rn 5666 df-res 5667 df-ima 5668 df-pred 6301 df-ord 6362 df-on 6363 df-lim 6364 df-suc 6365 df-iota 6491 df-fun 6537 df-fn 6538 df-f 6539 df-f1 6540 df-fo 6541 df-f1o 6542 df-fv 6543 df-riota 7373 df-ov 7419 df-oprab 7420 df-mpo 7421 df-om 7869 df-1st 7992 df-2nd 7993 df-tpos 8229 df-undef 8276 df-frecs 8285 df-wrecs 8316 df-recs 8365 df-rdg 8404 df-1o 8462 df-er 8703 df-map 8835 df-en 8960 df-dom 8961 df-sdom 8962 df-fin 8963 df-pnf 11294 df-mnf 11295 df-xr 11296 df-ltxr 11297 df-le 11298 df-sub 11492 df-neg 11493 df-nn 12283 df-2 12352 df-3 12353 df-4 12354 df-5 12355 df-6 12356 df-n0 12554 df-z 12641 df-uz 12913 df-fz 13587 df-struct 17264 df-sets 17281 df-slot 17299 df-ndx 17311 df-base 17327 df-ress 17348 df-plusg 17380 df-mulr 17381 df-sca 17383 df-vsca 17384 df-0g 17551 df-proset 18407 df-poset 18426 df-plt 18441 df-lub 18457 df-glb 18458 df-join 18459 df-meet 18460 df-p0 18536 df-p1 18537 df-lat 18545 df-clat 18612 df-mgm 18755 df-sgrp 18847 df-mnd 18863 df-submnd 18918 df-grp 19086 df-minusg 19087 df-sbg 19088 df-subg 19272 df-cntz 19470 df-lsm 19789 df-cmn 19935 df-abl 19936 df-mgp 20300 df-rng 20314 df-ur 20347 df-ring 20400 df-oppr 20506 df-dvdsr 20526 df-unit 20527 df-invr 20557 df-dvr 20570 df-drng 20921 df-lmod 21076 df-lss 21146 df-lsp 21186 df-lvec 21317 df-oposet 40114 df-ol 40116 df-oml 40117 df-covers 40204 df-ats 40205 df-atl 40236 df-cvlat 40260 df-hlat 40289 df-llines 40436 df-lplanes 40437 df-lvols 40438 df-lines 40439 df-psubsp 40441 df-pmap 40442 df-padd 40734 df-lhyp 40926 df-laut 40927 df-ldil 41042 df-ltrn 41043 df-trl 41097 df-tgrp 41681 df-tendo 41693 df-edring 41695 df-dveca 41941 df-disoa 41967

This theorem is used by: dia2dim 42015

W3C validator