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 41878

Description: Lemma for dia2dim 41879. 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 7418	. . . . . . 7 ⊢ (𝑈 = 𝑉 → (𝑈 ∨ 𝑈) = (𝑈 ∨ 𝑉))
2	1	adantl 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝑈 = 𝑉) → (𝑈 ∨ 𝑈) = (𝑈 ∨ 𝑉))
3		dia2dimlem12.k	. . . . . . . . 9 ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
4	3	simpld 499	. . . . . . . 8 ⊢ (𝜑 → 𝐾 ∈ HL)
5		dia2dimlem12.u	. . . . . . . . 9 ⊢ (𝜑 → (𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊))
6	5	simpld 499	. . . . . . . 8 ⊢ (𝜑 → 𝑈 ∈ 𝐴)
7		dia2dimlem12.j	. . . . . . . . 9 ⊢ ∨ = (join‘𝐾)
8		dia2dimlem12.a	. . . . . . . . 9 ⊢ 𝐴 = (Atoms‘𝐾)
9	7, 8	hlatjidm 40171	. . . . . . . 8 ⊢ ((𝐾 ∈ HL ∧ 𝑈 ∈ 𝐴) → (𝑈 ∨ 𝑈) = 𝑈)
10	4, 6, 9	syl2anc 595	. . . . . . 7 ⊢ (𝜑 → (𝑈 ∨ 𝑈) = 𝑈)
11	10	adantr 485	. . . . . 6 ⊢ ((𝜑 ∧ 𝑈 = 𝑉) → (𝑈 ∨ 𝑈) = 𝑈)
12	2, 11	eqtr3d 2800	. . . . 5 ⊢ ((𝜑 ∧ 𝑈 = 𝑉) → (𝑈 ∨ 𝑉) = 𝑈)
13	12	fveq2d 6885	. . . 4 ⊢ ((𝜑 ∧ 𝑈 = 𝑉) → (𝐼‘(𝑈 ∨ 𝑉)) = (𝐼‘𝑈))
14		ssid 3959	. . . 4 ⊢ (𝐼‘𝑈) ⊆ (𝐼‘𝑈)
15	13, 14	eqsstrdi 3981	. . 3 ⊢ ((𝜑 ∧ 𝑈 = 𝑉) → (𝐼‘(𝑈 ∨ 𝑉)) ⊆ (𝐼‘𝑈))
16		dia2dimlem12.h	. . . . . . . 8 ⊢ 𝐻 = (LHyp‘𝐾)
17		dia2dimlem12.y	. . . . . . . 8 ⊢ 𝑌 = ((DVecA‘𝐾)‘𝑊)
18	16, 17	dvalvec 41828	. . . . . . 7 ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → 𝑌 ∈ LVec)
19		lveclmod 21236	. . . . . . 7 ⊢ (𝑌 ∈ LVec → 𝑌 ∈ LMod)
20	3, 18, 19	3syl 19	. . . . . 6 ⊢ (𝜑 → 𝑌 ∈ LMod)
21		eqid 2763	. . . . . . . . 9 ⊢ (Base‘𝐾) = (Base‘𝐾)
22	21, 8	atbase 40091	. . . . . . . 8 ⊢ (𝑈 ∈ 𝐴 → 𝑈 ∈ (Base‘𝐾))
23	6, 22	syl 18	. . . . . . 7 ⊢ (𝜑 → 𝑈 ∈ (Base‘𝐾))
24	5	simprd 500	. . . . . . 7 ⊢ (𝜑 → 𝑈 ≤ 𝑊)
25		dia2dimlem12.l	. . . . . . . 8 ⊢ ≤ = (le‘𝐾)
26		dia2dimlem12.i	. . . . . . . 8 ⊢ 𝐼 = ((DIsoA‘𝐾)‘𝑊)
27		dia2dimlem12.s	. . . . . . . 8 ⊢ 𝑆 = (LSubSp‘𝑌)
28	21, 25, 16, 17, 26, 27	dialss 41848	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑈 ∈ (Base‘𝐾) ∧ 𝑈 ≤ 𝑊)) → (𝐼‘𝑈) ∈ 𝑆)
29	3, 23, 24, 28	syl12anc 849	. . . . . 6 ⊢ (𝜑 → (𝐼‘𝑈) ∈ 𝑆)
30	27	lsssubg 21087	. . . . . 6 ⊢ ((𝑌 ∈ LMod ∧ (𝐼‘𝑈) ∈ 𝑆) → (𝐼‘𝑈) ∈ (SubGrp‘𝑌))
31	20, 29, 30	syl2anc 595	. . . . 5 ⊢ (𝜑 → (𝐼‘𝑈) ∈ (SubGrp‘𝑌))
32		dia2dimlem12.pl	. . . . . 6 ⊢ ⊕ = (LSSum‘𝑌)
33	32	lsmidm 19737	. . . . 5 ⊢ ((𝐼‘𝑈) ∈ (SubGrp‘𝑌) → ((𝐼‘𝑈) ⊕ (𝐼‘𝑈)) = (𝐼‘𝑈))
34	31, 33	syl 18	. . . 4 ⊢ (𝜑 → ((𝐼‘𝑈) ⊕ (𝐼‘𝑈)) = (𝐼‘𝑈))
35		fveq2 6881	. . . . 5 ⊢ (𝑈 = 𝑉 → (𝐼‘𝑈) = (𝐼‘𝑉))
36	35	oveq2d 7426	. . . 4 ⊢ (𝑈 = 𝑉 → ((𝐼‘𝑈) ⊕ (𝐼‘𝑈)) = ((𝐼‘𝑈) ⊕ (𝐼‘𝑉)))
37	34, 36	sylan9req 2819	. . 3 ⊢ ((𝜑 ∧ 𝑈 = 𝑉) → (𝐼‘𝑈) = ((𝐼‘𝑈) ⊕ (𝐼‘𝑉)))
38	15, 37	sseqtrd 3973	. 2 ⊢ ((𝜑 ∧ 𝑈 = 𝑉) → (𝐼‘(𝑈 ∨ 𝑉)) ⊆ ((𝐼‘𝑈) ⊕ (𝐼‘𝑉)))
39		dia2dimlem12.m	. . 3 ⊢ ∧ = (meet‘𝐾)
40		dia2dimlem12.t	. . 3 ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)
41		dia2dimlem12.r	. . 3 ⊢ 𝑅 = ((trL‘𝐾)‘𝑊)
42		dia2dimlem12.n	. . 3 ⊢ 𝑁 = (LSpan‘𝑌)
43	3	adantr 485	. . 3 ⊢ ((𝜑 ∧ 𝑈 ≠ 𝑉) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
44	5	adantr 485	. . 3 ⊢ ((𝜑 ∧ 𝑈 ≠ 𝑉) → (𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊))
45		dia2dimlem12.v	. . . 4 ⊢ (𝜑 → (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊))
46	45	adantr 485	. . 3 ⊢ ((𝜑 ∧ 𝑈 ≠ 𝑉) → (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊))
47		simpr 489	. . 3 ⊢ ((𝜑 ∧ 𝑈 ≠ 𝑉) → 𝑈 ≠ 𝑉)
48	25, 7, 39, 8, 16, 40, 41, 17, 27, 32, 42, 26, 43, 44, 46, 47	dia2dimlem12 41877	. 2 ⊢ ((𝜑 ∧ 𝑈 ≠ 𝑉) → (𝐼‘(𝑈 ∨ 𝑉)) ⊆ ((𝐼‘𝑈) ⊕ (𝐼‘𝑉)))
49	38, 48	pm2.61dane 3045	1 ⊢ (𝜑 → (𝐼‘(𝑈 ∨ 𝑉)) ⊆ ((𝐼‘𝑈) ⊕ (𝐼‘𝑉)))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ∧ wa 400 = wceq 1570 ∈ wcel 2143 ≠ wne 2958 ⊆ wss 3905 class class class wbr 5109 ‘cfv 6536 (class class class)co 7410 Basecbs 17273 lecple 17321 joincjn 18371 meetcmee 18372 SubGrpcsubg 19190 LSSumclsm 19708 LModclmod 20990 LSubSpclss 21061 LSpanclspn 21101 LVecclvec 21232 Atomscatm 40065 HLchlt 40152 LHypclh 40786 LTrncltrn 40903 trLctrl 40960 DVecAcdveca 41804 DIsoAcdia 41830

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1825 ax-4 1839 ax-5 1940 ax-6 1997 ax-7 2038 ax-8 2145 ax-9 2153 ax-10 2176 ax-11 2192 ax-12 2213 ax-ext 2735 ax-rep 5238 ax-sep 5257 ax-nul 5269 ax-pow 5336 ax-pr 5404 ax-un 7732 ax-cnex 11160 ax-resscn 11161 ax-1cn 11162 ax-icn 11163 ax-addcl 11164 ax-addrcl 11165 ax-mulcl 11166 ax-mulrcl 11167 ax-mulcom 11168 ax-addass 11169 ax-mulass 11170 ax-distr 11171 ax-i2m1 11172 ax-1ne0 11173 ax-1rid 11174 ax-rnegex 11175 ax-rrecex 11176 ax-cnre 11177 ax-pre-lttri 11178 ax-pre-lttrn 11179 ax-pre-ltadd 11180 ax-pre-mulgt0 11181 ax-riotaBAD 39755

This proof depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1810 df-nf 1814 df-sb 2097 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2838 df-nfc 2912 df-ne 2959 df-nel 3065 df-ral 3080 df-rex 3090 df-rmo 3369 df-reu 3370 df-rab 3417 df-v 3457 df-sbc 3745 df-csb 3854 df-dif 3908 df-un 3910 df-in 3912 df-ss 3922 df-pss 3925 df-nul 4287 df-if 4488 df-pw 4564 df-sn 4590 df-pr 4592 df-tp 4594 df-op 4596 df-uni 4873 df-int 4913 df-iun 4958 df-iin 4959 df-br 5110 df-opab 5174 df-mpt 5193 df-tr 5219 df-id 5556 df-eprel 5561 df-po 5569 df-so 5570 df-fr 5614 df-we 5616 df-xp 5667 df-rel 5668 df-cnv 5669 df-co 5670 df-dm 5671 df-rn 5672 df-res 5673 df-ima 5674 df-pred 6302 df-ord 6363 df-on 6364 df-lim 6365 df-suc 6366 df-iota 6492 df-fun 6538 df-fn 6539 df-f 6540 df-f1 6541 df-fo 6542 df-f1o 6543 df-fv 6544 df-riota 7367 df-ov 7413 df-oprab 7414 df-mpo 7415 df-om 7859 df-1st 7982 df-2nd 7983 df-tpos 8218 df-undef 8265 df-frecs 8274 df-wrecs 8305 df-recs 8354 df-rdg 8393 df-1o 8449 df-er 8690 df-map 8822 df-en 8940 df-dom 8941 df-sdom 8942 df-fin 8943 df-pnf 11249 df-mnf 11250 df-xr 11251 df-ltxr 11252 df-le 11253 df-sub 11447 df-neg 11448 df-nn 12238 df-2 12307 df-3 12308 df-4 12309 df-5 12310 df-6 12311 df-n0 12509 df-z 12596 df-uz 12867 df-fz 13540 df-struct 17211 df-sets 17228 df-slot 17246 df-ndx 17258 df-base 17274 df-ress 17295 df-plusg 17327 df-mulr 17328 df-sca 17330 df-vsca 17331 df-0g 17498 df-proset 18354 df-poset 18373 df-plt 18388 df-lub 18404 df-glb 18405 df-join 18406 df-meet 18407 df-p0 18483 df-p1 18484 df-lat 18492 df-clat 18559 df-mgm 18702 df-sgrp 18781 df-mnd 18797 df-submnd 18846 df-grp 19007 df-minusg 19008 df-sbg 19009 df-subg 19193 df-cntz 19391 df-lsm 19710 df-cmn 19856 df-abl 19857 df-mgp 20221 df-rng 20235 df-ur 20268 df-ring 20321 df-oppr 20424 df-dvdsr 20444 df-unit 20445 df-invr 20475 df-dvr 20488 df-drng 20838 df-lmod 20992 df-lss 21062 df-lsp 21102 df-lvec 21233 df-oposet 39978 df-ol 39980 df-oml 39981 df-covers 40068 df-ats 40069 df-atl 40100 df-cvlat 40124 df-hlat 40153 df-llines 40300 df-lplanes 40301 df-lvols 40302 df-lines 40303 df-psubsp 40305 df-pmap 40306 df-padd 40598 df-lhyp 40790 df-laut 40791 df-ldil 40906 df-ltrn 40907 df-trl 40961 df-tgrp 41545 df-tendo 41557 df-edring 41559 df-dveca 41805 df-disoa 41831

This theorem is used by: dia2dim 41879

W3C validator