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 41481

Description: Lemma for dia2dim 41482. 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 7378	. . . . . . 7 ⊢ (𝑈 = 𝑉 → (𝑈 ∨ 𝑈) = (𝑈 ∨ 𝑉))
2	1	adantl 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑈 = 𝑉) → (𝑈 ∨ 𝑈) = (𝑈 ∨ 𝑉))
3		dia2dimlem12.k	. . . . . . . . 9 ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
4	3	simpld 494	. . . . . . . 8 ⊢ (𝜑 → 𝐾 ∈ HL)
5		dia2dimlem12.u	. . . . . . . . 9 ⊢ (𝜑 → (𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊))
6	5	simpld 494	. . . . . . . 8 ⊢ (𝜑 → 𝑈 ∈ 𝐴)
7		dia2dimlem12.j	. . . . . . . . 9 ⊢ ∨ = (join‘𝐾)
8		dia2dimlem12.a	. . . . . . . . 9 ⊢ 𝐴 = (Atoms‘𝐾)
9	7, 8	hlatjidm 39774	. . . . . . . 8 ⊢ ((𝐾 ∈ HL ∧ 𝑈 ∈ 𝐴) → (𝑈 ∨ 𝑈) = 𝑈)
10	4, 6, 9	syl2anc 585	. . . . . . 7 ⊢ (𝜑 → (𝑈 ∨ 𝑈) = 𝑈)
11	10	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑈 = 𝑉) → (𝑈 ∨ 𝑈) = 𝑈)
12	2, 11	eqtr3d 2774	. . . . 5 ⊢ ((𝜑 ∧ 𝑈 = 𝑉) → (𝑈 ∨ 𝑉) = 𝑈)
13	12	fveq2d 6848	. . . 4 ⊢ ((𝜑 ∧ 𝑈 = 𝑉) → (𝐼‘(𝑈 ∨ 𝑉)) = (𝐼‘𝑈))
14		ssid 3958	. . . 4 ⊢ (𝐼‘𝑈) ⊆ (𝐼‘𝑈)
15	13, 14	eqsstrdi 3980	. . 3 ⊢ ((𝜑 ∧ 𝑈 = 𝑉) → (𝐼‘(𝑈 ∨ 𝑉)) ⊆ (𝐼‘𝑈))
16		dia2dimlem12.h	. . . . . . . 8 ⊢ 𝐻 = (LHyp‘𝐾)
17		dia2dimlem12.y	. . . . . . . 8 ⊢ 𝑌 = ((DVecA‘𝐾)‘𝑊)
18	16, 17	dvalvec 41431	. . . . . . 7 ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → 𝑌 ∈ LVec)
19		lveclmod 21075	. . . . . . 7 ⊢ (𝑌 ∈ LVec → 𝑌 ∈ LMod)
20	3, 18, 19	3syl 18	. . . . . 6 ⊢ (𝜑 → 𝑌 ∈ LMod)
21		eqid 2737	. . . . . . . . 9 ⊢ (Base‘𝐾) = (Base‘𝐾)
22	21, 8	atbase 39694	. . . . . . . 8 ⊢ (𝑈 ∈ 𝐴 → 𝑈 ∈ (Base‘𝐾))
23	6, 22	syl 17	. . . . . . 7 ⊢ (𝜑 → 𝑈 ∈ (Base‘𝐾))
24	5	simprd 495	. . . . . . 7 ⊢ (𝜑 → 𝑈 ≤ 𝑊)
25		dia2dimlem12.l	. . . . . . . 8 ⊢ ≤ = (le‘𝐾)
26		dia2dimlem12.i	. . . . . . . 8 ⊢ 𝐼 = ((DIsoA‘𝐾)‘𝑊)
27		dia2dimlem12.s	. . . . . . . 8 ⊢ 𝑆 = (LSubSp‘𝑌)
28	21, 25, 16, 17, 26, 27	dialss 41451	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑈 ∈ (Base‘𝐾) ∧ 𝑈 ≤ 𝑊)) → (𝐼‘𝑈) ∈ 𝑆)
29	3, 23, 24, 28	syl12anc 837	. . . . . 6 ⊢ (𝜑 → (𝐼‘𝑈) ∈ 𝑆)
30	27	lsssubg 20925	. . . . . 6 ⊢ ((𝑌 ∈ LMod ∧ (𝐼‘𝑈) ∈ 𝑆) → (𝐼‘𝑈) ∈ (SubGrp‘𝑌))
31	20, 29, 30	syl2anc 585	. . . . 5 ⊢ (𝜑 → (𝐼‘𝑈) ∈ (SubGrp‘𝑌))
32		dia2dimlem12.pl	. . . . . 6 ⊢ ⊕ = (LSSum‘𝑌)
33	32	lsmidm 19609	. . . . 5 ⊢ ((𝐼‘𝑈) ∈ (SubGrp‘𝑌) → ((𝐼‘𝑈) ⊕ (𝐼‘𝑈)) = (𝐼‘𝑈))
34	31, 33	syl 17	. . . 4 ⊢ (𝜑 → ((𝐼‘𝑈) ⊕ (𝐼‘𝑈)) = (𝐼‘𝑈))
35		fveq2 6844	. . . . 5 ⊢ (𝑈 = 𝑉 → (𝐼‘𝑈) = (𝐼‘𝑉))
36	35	oveq2d 7386	. . . 4 ⊢ (𝑈 = 𝑉 → ((𝐼‘𝑈) ⊕ (𝐼‘𝑈)) = ((𝐼‘𝑈) ⊕ (𝐼‘𝑉)))
37	34, 36	sylan9req 2793	. . 3 ⊢ ((𝜑 ∧ 𝑈 = 𝑉) → (𝐼‘𝑈) = ((𝐼‘𝑈) ⊕ (𝐼‘𝑉)))
38	15, 37	sseqtrd 3972	. 2 ⊢ ((𝜑 ∧ 𝑈 = 𝑉) → (𝐼‘(𝑈 ∨ 𝑉)) ⊆ ((𝐼‘𝑈) ⊕ (𝐼‘𝑉)))
39		dia2dimlem12.m	. . 3 ⊢ ∧ = (meet‘𝐾)
40		dia2dimlem12.t	. . 3 ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)
41		dia2dimlem12.r	. . 3 ⊢ 𝑅 = ((trL‘𝐾)‘𝑊)
42		dia2dimlem12.n	. . 3 ⊢ 𝑁 = (LSpan‘𝑌)
43	3	adantr 480	. . 3 ⊢ ((𝜑 ∧ 𝑈 ≠ 𝑉) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
44	5	adantr 480	. . 3 ⊢ ((𝜑 ∧ 𝑈 ≠ 𝑉) → (𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊))
45		dia2dimlem12.v	. . . 4 ⊢ (𝜑 → (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊))
46	45	adantr 480	. . 3 ⊢ ((𝜑 ∧ 𝑈 ≠ 𝑉) → (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊))
47		simpr 484	. . 3 ⊢ ((𝜑 ∧ 𝑈 ≠ 𝑉) → 𝑈 ≠ 𝑉)
48	25, 7, 39, 8, 16, 40, 41, 17, 27, 32, 42, 26, 43, 44, 46, 47	dia2dimlem12 41480	. 2 ⊢ ((𝜑 ∧ 𝑈 ≠ 𝑉) → (𝐼‘(𝑈 ∨ 𝑉)) ⊆ ((𝐼‘𝑈) ⊕ (𝐼‘𝑉)))
49	38, 48	pm2.61dane 3020	1 ⊢ (𝜑 → (𝐼‘(𝑈 ∨ 𝑉)) ⊆ ((𝐼‘𝑈) ⊕ (𝐼‘𝑉)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 395 = wceq 1542 ∈ wcel 2114 ≠ wne 2933 ⊆ wss 3903 class class class wbr 5100 ‘cfv 6502 (class class class)co 7370 Basecbs 17150 lecple 17198 joincjn 18248 meetcmee 18249 SubGrpcsubg 19067 LSSumclsm 19580 LModclmod 20828 LSubSpclss 20899 LSpanclspn 20939 LVecclvec 21071 Atomscatm 39668 HLchlt 39755 LHypclh 40389 LTrncltrn 40506 trLctrl 40563 DVecAcdveca 41407 DIsoAcdia 41433

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2709 ax-rep 5226 ax-sep 5245 ax-nul 5255 ax-pow 5314 ax-pr 5381 ax-un 7692 ax-cnex 11096 ax-resscn 11097 ax-1cn 11098 ax-icn 11099 ax-addcl 11100 ax-addrcl 11101 ax-mulcl 11102 ax-mulrcl 11103 ax-mulcom 11104 ax-addass 11105 ax-mulass 11106 ax-distr 11107 ax-i2m1 11108 ax-1ne0 11109 ax-1rid 11110 ax-rnegex 11111 ax-rrecex 11112 ax-cnre 11113 ax-pre-lttri 11114 ax-pre-lttrn 11115 ax-pre-ltadd 11116 ax-pre-mulgt0 11117 ax-riotaBAD 39358

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2540 df-eu 2570 df-clab 2716 df-cleq 2729 df-clel 2812 df-nfc 2886 df-ne 2934 df-nel 3038 df-ral 3053 df-rex 3063 df-rmo 3352 df-reu 3353 df-rab 3402 df-v 3444 df-sbc 3743 df-csb 3852 df-dif 3906 df-un 3908 df-in 3910 df-ss 3920 df-pss 3923 df-nul 4288 df-if 4482 df-pw 4558 df-sn 4583 df-pr 4585 df-tp 4587 df-op 4589 df-uni 4866 df-int 4905 df-iun 4950 df-iin 4951 df-br 5101 df-opab 5163 df-mpt 5182 df-tr 5208 df-id 5529 df-eprel 5534 df-po 5542 df-so 5543 df-fr 5587 df-we 5589 df-xp 5640 df-rel 5641 df-cnv 5642 df-co 5643 df-dm 5644 df-rn 5645 df-res 5646 df-ima 5647 df-pred 6269 df-ord 6330 df-on 6331 df-lim 6332 df-suc 6333 df-iota 6458 df-fun 6504 df-fn 6505 df-f 6506 df-f1 6507 df-fo 6508 df-f1o 6509 df-fv 6510 df-riota 7327 df-ov 7373 df-oprab 7374 df-mpo 7375 df-om 7821 df-1st 7945 df-2nd 7946 df-tpos 8180 df-undef 8227 df-frecs 8235 df-wrecs 8266 df-recs 8315 df-rdg 8353 df-1o 8409 df-er 8647 df-map 8779 df-en 8898 df-dom 8899 df-sdom 8900 df-fin 8901 df-pnf 11182 df-mnf 11183 df-xr 11184 df-ltxr 11185 df-le 11186 df-sub 11380 df-neg 11381 df-nn 12160 df-2 12222 df-3 12223 df-4 12224 df-5 12225 df-6 12226 df-n0 12416 df-z 12503 df-uz 12766 df-fz 13438 df-struct 17088 df-sets 17105 df-slot 17123 df-ndx 17135 df-base 17151 df-ress 17172 df-plusg 17204 df-mulr 17205 df-sca 17207 df-vsca 17208 df-0g 17375 df-proset 18231 df-poset 18250 df-plt 18265 df-lub 18281 df-glb 18282 df-join 18283 df-meet 18284 df-p0 18360 df-p1 18361 df-lat 18369 df-clat 18436 df-mgm 18579 df-sgrp 18658 df-mnd 18674 df-submnd 18723 df-grp 18883 df-minusg 18884 df-sbg 18885 df-subg 19070 df-cntz 19263 df-lsm 19582 df-cmn 19728 df-abl 19729 df-mgp 20093 df-rng 20105 df-ur 20134 df-ring 20187 df-oppr 20290 df-dvdsr 20310 df-unit 20311 df-invr 20341 df-dvr 20354 df-drng 20681 df-lmod 20830 df-lss 20900 df-lsp 20940 df-lvec 21072 df-oposet 39581 df-ol 39583 df-oml 39584 df-covers 39671 df-ats 39672 df-atl 39703 df-cvlat 39727 df-hlat 39756 df-llines 39903 df-lplanes 39904 df-lvols 39905 df-lines 39906 df-psubsp 39908 df-pmap 39909 df-padd 40201 df-lhyp 40393 df-laut 40394 df-ldil 40509 df-ltrn 40510 df-trl 40564 df-tgrp 41148 df-tendo 41160 df-edring 41162 df-dveca 41408 df-disoa 41434

This theorem is referenced by: dia2dim 41482

W3C validator