dia2dimlem9 - Mathbox for Norm Megill

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

Theorem dia2dimlem9 41354

Description: Lemma for dia2dim 41359. Eliminate (𝑅‘𝐹) ≠ 𝑈, 𝑉 conditions. (Contributed by NM, 8-Sep-2014.)

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

**Assertion**
Ref	Expression
dia2dimlem9	⊢ (𝜑 → 𝐹 ∈ ((𝐼‘𝑈) ⊕ (𝐼‘𝑉)))

**Proof of Theorem dia2dimlem9**
Step	Hyp	Ref	Expression
1		dia2dimlem9.k	. . . . . . 7 ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
2		dia2dimlem9.h	. . . . . . . 8 ⊢ 𝐻 = (LHyp‘𝐾)
3		dia2dimlem9.y	. . . . . . . 8 ⊢ 𝑌 = ((DVecA‘𝐾)‘𝑊)
4	2, 3	dvalvec 41308	. . . . . . 7 ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → 𝑌 ∈ LVec)
5		lveclmod 21060	. . . . . . 7 ⊢ (𝑌 ∈ LVec → 𝑌 ∈ LMod)
6		dia2dimlem9.s	. . . . . . . 8 ⊢ 𝑆 = (LSubSp‘𝑌)
7	6	lsssssubg 20911	. . . . . . 7 ⊢ (𝑌 ∈ LMod → 𝑆 ⊆ (SubGrp‘𝑌))
8	1, 4, 5, 7	4syl 19	. . . . . 6 ⊢ (𝜑 → 𝑆 ⊆ (SubGrp‘𝑌))
9		dia2dimlem9.u	. . . . . . . . 9 ⊢ (𝜑 → (𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊))
10	9	simpld 494	. . . . . . . 8 ⊢ (𝜑 → 𝑈 ∈ 𝐴)
11		eqid 2736	. . . . . . . . 9 ⊢ (Base‘𝐾) = (Base‘𝐾)
12		dia2dimlem9.a	. . . . . . . . 9 ⊢ 𝐴 = (Atoms‘𝐾)
13	11, 12	atbase 39571	. . . . . . . 8 ⊢ (𝑈 ∈ 𝐴 → 𝑈 ∈ (Base‘𝐾))
14	10, 13	syl 17	. . . . . . 7 ⊢ (𝜑 → 𝑈 ∈ (Base‘𝐾))
15	9	simprd 495	. . . . . . 7 ⊢ (𝜑 → 𝑈 ≤ 𝑊)
16		dia2dimlem9.l	. . . . . . . 8 ⊢ ≤ = (le‘𝐾)
17		dia2dimlem9.i	. . . . . . . 8 ⊢ 𝐼 = ((DIsoA‘𝐾)‘𝑊)
18	11, 16, 2, 3, 17, 6	dialss 41328	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑈 ∈ (Base‘𝐾) ∧ 𝑈 ≤ 𝑊)) → (𝐼‘𝑈) ∈ 𝑆)
19	1, 14, 15, 18	syl12anc 836	. . . . . 6 ⊢ (𝜑 → (𝐼‘𝑈) ∈ 𝑆)
20	8, 19	sseldd 3934	. . . . 5 ⊢ (𝜑 → (𝐼‘𝑈) ∈ (SubGrp‘𝑌))
21		dia2dimlem9.v	. . . . . . . . 9 ⊢ (𝜑 → (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊))
22	21	simpld 494	. . . . . . . 8 ⊢ (𝜑 → 𝑉 ∈ 𝐴)
23	11, 12	atbase 39571	. . . . . . . 8 ⊢ (𝑉 ∈ 𝐴 → 𝑉 ∈ (Base‘𝐾))
24	22, 23	syl 17	. . . . . . 7 ⊢ (𝜑 → 𝑉 ∈ (Base‘𝐾))
25	21	simprd 495	. . . . . . 7 ⊢ (𝜑 → 𝑉 ≤ 𝑊)
26	11, 16, 2, 3, 17, 6	dialss 41328	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑉 ∈ (Base‘𝐾) ∧ 𝑉 ≤ 𝑊)) → (𝐼‘𝑉) ∈ 𝑆)
27	1, 24, 25, 26	syl12anc 836	. . . . . 6 ⊢ (𝜑 → (𝐼‘𝑉) ∈ 𝑆)
28	8, 27	sseldd 3934	. . . . 5 ⊢ (𝜑 → (𝐼‘𝑉) ∈ (SubGrp‘𝑌))
29		dia2dimlem9.pl	. . . . . 6 ⊢ ⊕ = (LSSum‘𝑌)
30	29	lsmub1 19588	. . . . 5 ⊢ (((𝐼‘𝑈) ∈ (SubGrp‘𝑌) ∧ (𝐼‘𝑉) ∈ (SubGrp‘𝑌)) → (𝐼‘𝑈) ⊆ ((𝐼‘𝑈) ⊕ (𝐼‘𝑉)))
31	20, 28, 30	syl2anc 584	. . . 4 ⊢ (𝜑 → (𝐼‘𝑈) ⊆ ((𝐼‘𝑈) ⊕ (𝐼‘𝑉)))
32	31	adantr 480	. . 3 ⊢ ((𝜑 ∧ (𝑅‘𝐹) = 𝑈) → (𝐼‘𝑈) ⊆ ((𝐼‘𝑈) ⊕ (𝐼‘𝑉)))
33		dia2dimlem9.f	. . . . . 6 ⊢ (𝜑 → 𝐹 ∈ 𝑇)
34		dia2dimlem9.t	. . . . . . 7 ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)
35		dia2dimlem9.r	. . . . . . 7 ⊢ 𝑅 = ((trL‘𝐾)‘𝑊)
36	2, 34, 35, 17	dia1dimid 41345	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) → 𝐹 ∈ (𝐼‘(𝑅‘𝐹)))
37	1, 33, 36	syl2anc 584	. . . . 5 ⊢ (𝜑 → 𝐹 ∈ (𝐼‘(𝑅‘𝐹)))
38	37	adantr 480	. . . 4 ⊢ ((𝜑 ∧ (𝑅‘𝐹) = 𝑈) → 𝐹 ∈ (𝐼‘(𝑅‘𝐹)))
39		fveq2 6834	. . . . 5 ⊢ ((𝑅‘𝐹) = 𝑈 → (𝐼‘(𝑅‘𝐹)) = (𝐼‘𝑈))
40	39	adantl 481	. . . 4 ⊢ ((𝜑 ∧ (𝑅‘𝐹) = 𝑈) → (𝐼‘(𝑅‘𝐹)) = (𝐼‘𝑈))
41	38, 40	eleqtrd 2838	. . 3 ⊢ ((𝜑 ∧ (𝑅‘𝐹) = 𝑈) → 𝐹 ∈ (𝐼‘𝑈))
42	32, 41	sseldd 3934	. 2 ⊢ ((𝜑 ∧ (𝑅‘𝐹) = 𝑈) → 𝐹 ∈ ((𝐼‘𝑈) ⊕ (𝐼‘𝑉)))
43	20	adantr 480	. . . 4 ⊢ ((𝜑 ∧ (𝑅‘𝐹) = 𝑉) → (𝐼‘𝑈) ∈ (SubGrp‘𝑌))
44	28	adantr 480	. . . 4 ⊢ ((𝜑 ∧ (𝑅‘𝐹) = 𝑉) → (𝐼‘𝑉) ∈ (SubGrp‘𝑌))
45	29	lsmub2 19589	. . . 4 ⊢ (((𝐼‘𝑈) ∈ (SubGrp‘𝑌) ∧ (𝐼‘𝑉) ∈ (SubGrp‘𝑌)) → (𝐼‘𝑉) ⊆ ((𝐼‘𝑈) ⊕ (𝐼‘𝑉)))
46	43, 44, 45	syl2anc 584	. . 3 ⊢ ((𝜑 ∧ (𝑅‘𝐹) = 𝑉) → (𝐼‘𝑉) ⊆ ((𝐼‘𝑈) ⊕ (𝐼‘𝑉)))
47	37	adantr 480	. . . 4 ⊢ ((𝜑 ∧ (𝑅‘𝐹) = 𝑉) → 𝐹 ∈ (𝐼‘(𝑅‘𝐹)))
48		fveq2 6834	. . . . 5 ⊢ ((𝑅‘𝐹) = 𝑉 → (𝐼‘(𝑅‘𝐹)) = (𝐼‘𝑉))
49	48	adantl 481	. . . 4 ⊢ ((𝜑 ∧ (𝑅‘𝐹) = 𝑉) → (𝐼‘(𝑅‘𝐹)) = (𝐼‘𝑉))
50	47, 49	eleqtrd 2838	. . 3 ⊢ ((𝜑 ∧ (𝑅‘𝐹) = 𝑉) → 𝐹 ∈ (𝐼‘𝑉))
51	46, 50	sseldd 3934	. 2 ⊢ ((𝜑 ∧ (𝑅‘𝐹) = 𝑉) → 𝐹 ∈ ((𝐼‘𝑈) ⊕ (𝐼‘𝑉)))
52		dia2dimlem9.j	. . 3 ⊢ ∨ = (join‘𝐾)
53		dia2dimlem9.m	. . 3 ⊢ ∧ = (meet‘𝐾)
54		dia2dimlem9.n	. . 3 ⊢ 𝑁 = (LSpan‘𝑌)
55	1	adantr 480	. . 3 ⊢ ((𝜑 ∧ ((𝑅‘𝐹) ≠ 𝑈 ∧ (𝑅‘𝐹) ≠ 𝑉)) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
56	9	adantr 480	. . 3 ⊢ ((𝜑 ∧ ((𝑅‘𝐹) ≠ 𝑈 ∧ (𝑅‘𝐹) ≠ 𝑉)) → (𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊))
57	21	adantr 480	. . 3 ⊢ ((𝜑 ∧ ((𝑅‘𝐹) ≠ 𝑈 ∧ (𝑅‘𝐹) ≠ 𝑉)) → (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊))
58	33	adantr 480	. . 3 ⊢ ((𝜑 ∧ ((𝑅‘𝐹) ≠ 𝑈 ∧ (𝑅‘𝐹) ≠ 𝑉)) → 𝐹 ∈ 𝑇)
59		dia2dimlem9.rf	. . . 4 ⊢ (𝜑 → (𝑅‘𝐹) ≤ (𝑈 ∨ 𝑉))
60	59	adantr 480	. . 3 ⊢ ((𝜑 ∧ ((𝑅‘𝐹) ≠ 𝑈 ∧ (𝑅‘𝐹) ≠ 𝑉)) → (𝑅‘𝐹) ≤ (𝑈 ∨ 𝑉))
61		dia2dimlem9.uv	. . . 4 ⊢ (𝜑 → 𝑈 ≠ 𝑉)
62	61	adantr 480	. . 3 ⊢ ((𝜑 ∧ ((𝑅‘𝐹) ≠ 𝑈 ∧ (𝑅‘𝐹) ≠ 𝑉)) → 𝑈 ≠ 𝑉)
63		simprl 770	. . 3 ⊢ ((𝜑 ∧ ((𝑅‘𝐹) ≠ 𝑈 ∧ (𝑅‘𝐹) ≠ 𝑉)) → (𝑅‘𝐹) ≠ 𝑈)
64		simprr 772	. . 3 ⊢ ((𝜑 ∧ ((𝑅‘𝐹) ≠ 𝑈 ∧ (𝑅‘𝐹) ≠ 𝑉)) → (𝑅‘𝐹) ≠ 𝑉)
65	16, 52, 53, 12, 2, 34, 35, 3, 6, 29, 54, 17, 55, 56, 57, 58, 60, 62, 63, 64	dia2dimlem8 41353	. 2 ⊢ ((𝜑 ∧ ((𝑅‘𝐹) ≠ 𝑈 ∧ (𝑅‘𝐹) ≠ 𝑉)) → 𝐹 ∈ ((𝐼‘𝑈) ⊕ (𝐼‘𝑉)))
66	42, 51, 65	pm2.61da2ne 3020	1 ⊢ (𝜑 → 𝐹 ∈ ((𝐼‘𝑈) ⊕ (𝐼‘𝑉)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 395 = wceq 1541 ∈ wcel 2113 ≠ wne 2932 ⊆ wss 3901 class class class wbr 5098 ‘cfv 6492 (class class class)co 7358 Basecbs 17138 lecple 17186 joincjn 18236 meetcmee 18237 SubGrpcsubg 19052 LSSumclsm 19565 LModclmod 20813 LSubSpclss 20884 LSpanclspn 20924 LVecclvec 21056 Atomscatm 39545 HLchlt 39632 LHypclh 40266 LTrncltrn 40383 trLctrl 40440 DVecAcdveca 41284 DIsoAcdia 41310

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2115 ax-9 2123 ax-10 2146 ax-11 2162 ax-12 2184 ax-ext 2708 ax-rep 5224 ax-sep 5241 ax-nul 5251 ax-pow 5310 ax-pr 5377 ax-un 7680 ax-cnex 11084 ax-resscn 11085 ax-1cn 11086 ax-icn 11087 ax-addcl 11088 ax-addrcl 11089 ax-mulcl 11090 ax-mulrcl 11091 ax-mulcom 11092 ax-addass 11093 ax-mulass 11094 ax-distr 11095 ax-i2m1 11096 ax-1ne0 11097 ax-1rid 11098 ax-rnegex 11099 ax-rrecex 11100 ax-cnre 11101 ax-pre-lttri 11102 ax-pre-lttrn 11103 ax-pre-ltadd 11104 ax-pre-mulgt0 11105 ax-riotaBAD 39235

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2068 df-mo 2539 df-eu 2569 df-clab 2715 df-cleq 2728 df-clel 2811 df-nfc 2885 df-ne 2933 df-nel 3037 df-ral 3052 df-rex 3061 df-rmo 3350 df-reu 3351 df-rab 3400 df-v 3442 df-sbc 3741 df-csb 3850 df-dif 3904 df-un 3906 df-in 3908 df-ss 3918 df-pss 3921 df-nul 4286 df-if 4480 df-pw 4556 df-sn 4581 df-pr 4583 df-tp 4585 df-op 4587 df-uni 4864 df-int 4903 df-iun 4948 df-iin 4949 df-br 5099 df-opab 5161 df-mpt 5180 df-tr 5206 df-id 5519 df-eprel 5524 df-po 5532 df-so 5533 df-fr 5577 df-we 5579 df-xp 5630 df-rel 5631 df-cnv 5632 df-co 5633 df-dm 5634 df-rn 5635 df-res 5636 df-ima 5637 df-pred 6259 df-ord 6320 df-on 6321 df-lim 6322 df-suc 6323 df-iota 6448 df-fun 6494 df-fn 6495 df-f 6496 df-f1 6497 df-fo 6498 df-f1o 6499 df-fv 6500 df-riota 7315 df-ov 7361 df-oprab 7362 df-mpo 7363 df-om 7809 df-1st 7933 df-2nd 7934 df-tpos 8168 df-undef 8215 df-frecs 8223 df-wrecs 8254 df-recs 8303 df-rdg 8341 df-1o 8397 df-er 8635 df-map 8767 df-en 8886 df-dom 8887 df-sdom 8888 df-fin 8889 df-pnf 11170 df-mnf 11171 df-xr 11172 df-ltxr 11173 df-le 11174 df-sub 11368 df-neg 11369 df-nn 12148 df-2 12210 df-3 12211 df-4 12212 df-5 12213 df-6 12214 df-n0 12404 df-z 12491 df-uz 12754 df-fz 13426 df-struct 17076 df-sets 17093 df-slot 17111 df-ndx 17123 df-base 17139 df-ress 17160 df-plusg 17192 df-mulr 17193 df-sca 17195 df-vsca 17196 df-0g 17363 df-proset 18219 df-poset 18238 df-plt 18253 df-lub 18269 df-glb 18270 df-join 18271 df-meet 18272 df-p0 18348 df-p1 18349 df-lat 18357 df-clat 18424 df-mgm 18567 df-sgrp 18646 df-mnd 18662 df-submnd 18711 df-grp 18868 df-minusg 18869 df-sbg 18870 df-subg 19055 df-cntz 19248 df-lsm 19567 df-cmn 19713 df-abl 19714 df-mgp 20078 df-rng 20090 df-ur 20119 df-ring 20172 df-oppr 20275 df-dvdsr 20295 df-unit 20296 df-invr 20326 df-dvr 20339 df-drng 20666 df-lmod 20815 df-lss 20885 df-lsp 20925 df-lvec 21057 df-oposet 39458 df-ol 39460 df-oml 39461 df-covers 39548 df-ats 39549 df-atl 39580 df-cvlat 39604 df-hlat 39633 df-llines 39780 df-lplanes 39781 df-lvols 39782 df-lines 39783 df-psubsp 39785 df-pmap 39786 df-padd 40078 df-lhyp 40270 df-laut 40271 df-ldil 40386 df-ltrn 40387 df-trl 40441 df-tgrp 41025 df-tendo 41037 df-edring 41039 df-dveca 41285 df-disoa 41311

This theorem is referenced by: dia2dimlem11 41356

W3C validator