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 41913

Description: Lemma for dia2dim 41914. 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 7428	. . . . . . 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 40206	. . . . . . . 8 ⊢ ((𝐾 ∈ HL ∧ 𝑈 ∈ 𝐴) → (𝑈 ∨ 𝑈) = 𝑈)
10	4, 6, 9	syl2anc 596	. . . . . . 7 ⊢ (𝜑 → (𝑈 ∨ 𝑈) = 𝑈)
11	10	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝑈 = 𝑉) → (𝑈 ∨ 𝑈) = 𝑈)
12	2, 11	eqtr3d 2802	. . . . 5 ⊢ ((𝜑 ∧ 𝑈 = 𝑉) → (𝑈 ∨ 𝑉) = 𝑈)
13	12	fveq2d 6890	. . . 4 ⊢ ((𝜑 ∧ 𝑈 = 𝑉) → (𝐼‘(𝑈 ∨ 𝑉)) = (𝐼‘𝑈))
14		ssid 3960	. . . 4 ⊢ (𝐼‘𝑈) ⊆ (𝐼‘𝑈)
15	13, 14	eqsstrdi 3982	. . 3 ⊢ ((𝜑 ∧ 𝑈 = 𝑉) → (𝐼‘(𝑈 ∨ 𝑉)) ⊆ (𝐼‘𝑈))
16		dia2dimlem12.h	. . . . . . . 8 ⊢ 𝐻 = (LHyp‘𝐾)
17		dia2dimlem12.y	. . . . . . . 8 ⊢ 𝑌 = ((DVecA‘𝐾)‘𝑊)
18	16, 17	dvalvec 41863	. . . . . . 7 ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → 𝑌 ∈ LVec)
19		lveclmod 21282	. . . . . . 7 ⊢ (𝑌 ∈ LVec → 𝑌 ∈ LMod)
20	3, 18, 19	3syl 19	. . . . . 6 ⊢ (𝜑 → 𝑌 ∈ LMod)
21		eqid 2765	. . . . . . . . 9 ⊢ (Base‘𝐾) = (Base‘𝐾)
22	21, 8	atbase 40126	. . . . . . . 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 41883	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑈 ∈ (Base‘𝐾) ∧ 𝑈 ≤ 𝑊)) → (𝐼‘𝑈) ∈ 𝑆)
29	3, 23, 24, 28	syl12anc 850	. . . . . 6 ⊢ (𝜑 → (𝐼‘𝑈) ∈ 𝑆)
30	27	lsssubg 21133	. . . . . 6 ⊢ ((𝑌 ∈ LMod ∧ (𝐼‘𝑈) ∈ 𝑆) → (𝐼‘𝑈) ∈ (SubGrp‘𝑌))
31	20, 29, 30	syl2anc 596	. . . . 5 ⊢ (𝜑 → (𝐼‘𝑈) ∈ (SubGrp‘𝑌))
32		dia2dimlem12.pl	. . . . . 6 ⊢ ⊕ = (LSSum‘𝑌)
33	32	lsmidm 19782	. . . . 5 ⊢ ((𝐼‘𝑈) ∈ (SubGrp‘𝑌) → ((𝐼‘𝑈) ⊕ (𝐼‘𝑈)) = (𝐼‘𝑈))
34	31, 33	syl 18	. . . 4 ⊢ (𝜑 → ((𝐼‘𝑈) ⊕ (𝐼‘𝑈)) = (𝐼‘𝑈))
35		fveq2 6886	. . . . 5 ⊢ (𝑈 = 𝑉 → (𝐼‘𝑈) = (𝐼‘𝑉))
36	35	oveq2d 7436	. . . 4 ⊢ (𝑈 = 𝑉 → ((𝐼‘𝑈) ⊕ (𝐼‘𝑈)) = ((𝐼‘𝑈) ⊕ (𝐼‘𝑉)))
37	34, 36	sylan9req 2821	. . 3 ⊢ ((𝜑 ∧ 𝑈 = 𝑉) → (𝐼‘𝑈) = ((𝐼‘𝑈) ⊕ (𝐼‘𝑉)))
38	15, 37	sseqtrd 3974	. 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 41912	. 2 ⊢ ((𝜑 ∧ 𝑈 ≠ 𝑉) → (𝐼‘(𝑈 ∨ 𝑉)) ⊆ ((𝐼‘𝑈) ⊕ (𝐼‘𝑉)))
49	38, 48	pm2.61dane 3047	1 ⊢ (𝜑 → (𝐼‘(𝑈 ∨ 𝑉)) ⊆ ((𝐼‘𝑈) ⊕ (𝐼‘𝑉)))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ∧ wa 401 = wceq 1570 ∈ wcel 2146 ≠ wne 2960 ⊆ wss 3906 class class class wbr 5111 ‘cfv 6541 (class class class)co 7420 Basecbs 17296 lecple 17344 joincjn 18394 meetcmee 18395 SubGrpcsubg 19235 LSSumclsm 19753 LModclmod 21036 LSubSpclss 21107 LSpanclspn 21147 LVecclvec 21278 Atomscatm 40100 HLchlt 40187 LHypclh 40821 LTrncltrn 40938 trLctrl 40995 DVecAcdveca 41839 DIsoAcdia 41865

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 2148 ax-9 2156 ax-10 2179 ax-11 2195 ax-12 2216 ax-ext 2737 ax-rep 5240 ax-sep 5259 ax-nul 5271 ax-pow 5338 ax-pr 5406 ax-un 7743 ax-cnex 11176 ax-resscn 11177 ax-1cn 11178 ax-icn 11179 ax-addcl 11180 ax-addrcl 11181 ax-mulcl 11182 ax-mulrcl 11183 ax-mulcom 11184 ax-addass 11185 ax-mulass 11186 ax-distr 11187 ax-i2m1 11188 ax-1ne0 11189 ax-1rid 11190 ax-rnegex 11191 ax-rrecex 11192 ax-cnre 11193 ax-pre-lttri 11194 ax-pre-lttrn 11195 ax-pre-ltadd 11196 ax-pre-mulgt0 11197 ax-riotaBAD 39790

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 2569 df-eu 2599 df-clab 2744 df-cleq 2757 df-clel 2840 df-nfc 2914 df-ne 2961 df-nel 3067 df-ral 3082 df-rex 3092 df-rmo 3371 df-reu 3372 df-rab 3419 df-v 3459 df-sbc 3747 df-csb 3855 df-dif 3909 df-un 3911 df-in 3913 df-ss 3923 df-pss 3926 df-nul 4287 df-if 4490 df-pw 4566 df-sn 4592 df-pr 4594 df-tp 4596 df-op 4598 df-uni 4875 df-int 4915 df-iun 4960 df-iin 4961 df-br 5112 df-opab 5176 df-mpt 5195 df-tr 5221 df-id 5558 df-eprel 5563 df-po 5571 df-so 5572 df-fr 5616 df-we 5618 df-xp 5669 df-rel 5670 df-cnv 5671 df-co 5672 df-dm 5673 df-rn 5674 df-res 5675 df-ima 5676 df-pred 6307 df-ord 6368 df-on 6369 df-lim 6370 df-suc 6371 df-iota 6497 df-fun 6543 df-fn 6544 df-f 6545 df-f1 6546 df-fo 6547 df-f1o 6548 df-fv 6549 df-riota 7377 df-ov 7423 df-oprab 7424 df-mpo 7425 df-om 7870 df-1st 7993 df-2nd 7994 df-tpos 8229 df-undef 8276 df-frecs 8285 df-wrecs 8316 df-recs 8365 df-rdg 8404 df-1o 8460 df-er 8701 df-map 8833 df-en 8951 df-dom 8952 df-sdom 8953 df-fin 8954 df-pnf 11265 df-mnf 11266 df-xr 11267 df-ltxr 11268 df-le 11269 df-sub 11463 df-neg 11464 df-nn 12254 df-2 12323 df-3 12324 df-4 12325 df-5 12326 df-6 12327 df-n0 12525 df-z 12612 df-uz 12884 df-fz 13557 df-struct 17234 df-sets 17251 df-slot 17269 df-ndx 17281 df-base 17297 df-ress 17318 df-plusg 17350 df-mulr 17351 df-sca 17353 df-vsca 17354 df-0g 17521 df-proset 18377 df-poset 18396 df-plt 18411 df-lub 18427 df-glb 18428 df-join 18429 df-meet 18430 df-p0 18506 df-p1 18507 df-lat 18515 df-clat 18582 df-mgm 18725 df-sgrp 18814 df-mnd 18830 df-submnd 18884 df-grp 19052 df-minusg 19053 df-sbg 19054 df-subg 19238 df-cntz 19436 df-lsm 19755 df-cmn 19901 df-abl 19902 df-mgp 20266 df-rng 20280 df-ur 20313 df-ring 20366 df-oppr 20470 df-dvdsr 20490 df-unit 20491 df-invr 20521 df-dvr 20534 df-drng 20884 df-lmod 21038 df-lss 21108 df-lsp 21148 df-lvec 21279 df-oposet 40013 df-ol 40015 df-oml 40016 df-covers 40103 df-ats 40104 df-atl 40135 df-cvlat 40159 df-hlat 40188 df-llines 40335 df-lplanes 40336 df-lvols 40337 df-lines 40338 df-psubsp 40340 df-pmap 40341 df-padd 40633 df-lhyp 40825 df-laut 40826 df-ldil 40941 df-ltrn 40942 df-trl 40996 df-tgrp 41580 df-tendo 41592 df-edring 41594 df-dveca 41840 df-disoa 41866

This theorem is used by: dia2dim 41914

W3C validator