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 39298

Description: Lemma for dia2dim 39303. 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 39252	. . . . . . 7 ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → 𝑌 ∈ LVec)
5		lveclmod 20439	. . . . . . 7 ⊢ (𝑌 ∈ LVec → 𝑌 ∈ LMod)
6		dia2dimlem9.s	. . . . . . . 8 ⊢ 𝑆 = (LSubSp‘𝑌)
7	6	lsssssubg 20291	. . . . . . 7 ⊢ (𝑌 ∈ LMod → 𝑆 ⊆ (SubGrp‘𝑌))
8	1, 4, 5, 7	4syl 19	. . . . . 6 ⊢ (𝜑 → 𝑆 ⊆ (SubGrp‘𝑌))
9		dia2dimlem9.u	. . . . . . . . 9 ⊢ (𝜑 → (𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊))
10	9	simpld 495	. . . . . . . 8 ⊢ (𝜑 → 𝑈 ∈ 𝐴)
11		eqid 2737	. . . . . . . . 9 ⊢ (Base‘𝐾) = (Base‘𝐾)
12		dia2dimlem9.a	. . . . . . . . 9 ⊢ 𝐴 = (Atoms‘𝐾)
13	11, 12	atbase 37515	. . . . . . . 8 ⊢ (𝑈 ∈ 𝐴 → 𝑈 ∈ (Base‘𝐾))
14	10, 13	syl 17	. . . . . . 7 ⊢ (𝜑 → 𝑈 ∈ (Base‘𝐾))
15	9	simprd 496	. . . . . . 7 ⊢ (𝜑 → 𝑈 ≤ 𝑊)
16		dia2dimlem9.l	. . . . . . . 8 ⊢ ≤ = (le‘𝐾)
17		dia2dimlem9.i	. . . . . . . 8 ⊢ 𝐼 = ((DIsoA‘𝐾)‘𝑊)
18	11, 16, 2, 3, 17, 6	dialss 39272	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑈 ∈ (Base‘𝐾) ∧ 𝑈 ≤ 𝑊)) → (𝐼‘𝑈) ∈ 𝑆)
19	1, 14, 15, 18	syl12anc 834	. . . . . 6 ⊢ (𝜑 → (𝐼‘𝑈) ∈ 𝑆)
20	8, 19	sseldd 3931	. . . . 5 ⊢ (𝜑 → (𝐼‘𝑈) ∈ (SubGrp‘𝑌))
21		dia2dimlem9.v	. . . . . . . . 9 ⊢ (𝜑 → (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊))
22	21	simpld 495	. . . . . . . 8 ⊢ (𝜑 → 𝑉 ∈ 𝐴)
23	11, 12	atbase 37515	. . . . . . . 8 ⊢ (𝑉 ∈ 𝐴 → 𝑉 ∈ (Base‘𝐾))
24	22, 23	syl 17	. . . . . . 7 ⊢ (𝜑 → 𝑉 ∈ (Base‘𝐾))
25	21	simprd 496	. . . . . . 7 ⊢ (𝜑 → 𝑉 ≤ 𝑊)
26	11, 16, 2, 3, 17, 6	dialss 39272	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑉 ∈ (Base‘𝐾) ∧ 𝑉 ≤ 𝑊)) → (𝐼‘𝑉) ∈ 𝑆)
27	1, 24, 25, 26	syl12anc 834	. . . . . 6 ⊢ (𝜑 → (𝐼‘𝑉) ∈ 𝑆)
28	8, 27	sseldd 3931	. . . . 5 ⊢ (𝜑 → (𝐼‘𝑉) ∈ (SubGrp‘𝑌))
29		dia2dimlem9.pl	. . . . . 6 ⊢ ⊕ = (LSSum‘𝑌)
30	29	lsmub1 19329	. . . . 5 ⊢ (((𝐼‘𝑈) ∈ (SubGrp‘𝑌) ∧ (𝐼‘𝑉) ∈ (SubGrp‘𝑌)) → (𝐼‘𝑈) ⊆ ((𝐼‘𝑈) ⊕ (𝐼‘𝑉)))
31	20, 28, 30	syl2anc 584	. . . 4 ⊢ (𝜑 → (𝐼‘𝑈) ⊆ ((𝐼‘𝑈) ⊕ (𝐼‘𝑉)))
32	31	adantr 481	. . 3 ⊢ ((𝜑 ∧ (𝑅‘𝐹) = 𝑈) → (𝐼‘𝑈) ⊆ ((𝐼‘𝑈) ⊕ (𝐼‘𝑉)))
33		dia2dimlem9.f	. . . . . 6 ⊢ (𝜑 → 𝐹 ∈ 𝑇)
34		dia2dimlem9.t	. . . . . . 7 ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)
35		dia2dimlem9.r	. . . . . . 7 ⊢ 𝑅 = ((trL‘𝐾)‘𝑊)
36	2, 34, 35, 17	dia1dimid 39289	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) → 𝐹 ∈ (𝐼‘(𝑅‘𝐹)))
37	1, 33, 36	syl2anc 584	. . . . 5 ⊢ (𝜑 → 𝐹 ∈ (𝐼‘(𝑅‘𝐹)))
38	37	adantr 481	. . . 4 ⊢ ((𝜑 ∧ (𝑅‘𝐹) = 𝑈) → 𝐹 ∈ (𝐼‘(𝑅‘𝐹)))
39		fveq2 6809	. . . . 5 ⊢ ((𝑅‘𝐹) = 𝑈 → (𝐼‘(𝑅‘𝐹)) = (𝐼‘𝑈))
40	39	adantl 482	. . . 4 ⊢ ((𝜑 ∧ (𝑅‘𝐹) = 𝑈) → (𝐼‘(𝑅‘𝐹)) = (𝐼‘𝑈))
41	38, 40	eleqtrd 2840	. . 3 ⊢ ((𝜑 ∧ (𝑅‘𝐹) = 𝑈) → 𝐹 ∈ (𝐼‘𝑈))
42	32, 41	sseldd 3931	. 2 ⊢ ((𝜑 ∧ (𝑅‘𝐹) = 𝑈) → 𝐹 ∈ ((𝐼‘𝑈) ⊕ (𝐼‘𝑉)))
43	20	adantr 481	. . . 4 ⊢ ((𝜑 ∧ (𝑅‘𝐹) = 𝑉) → (𝐼‘𝑈) ∈ (SubGrp‘𝑌))
44	28	adantr 481	. . . 4 ⊢ ((𝜑 ∧ (𝑅‘𝐹) = 𝑉) → (𝐼‘𝑉) ∈ (SubGrp‘𝑌))
45	29	lsmub2 19330	. . . 4 ⊢ (((𝐼‘𝑈) ∈ (SubGrp‘𝑌) ∧ (𝐼‘𝑉) ∈ (SubGrp‘𝑌)) → (𝐼‘𝑉) ⊆ ((𝐼‘𝑈) ⊕ (𝐼‘𝑉)))
46	43, 44, 45	syl2anc 584	. . 3 ⊢ ((𝜑 ∧ (𝑅‘𝐹) = 𝑉) → (𝐼‘𝑉) ⊆ ((𝐼‘𝑈) ⊕ (𝐼‘𝑉)))
47	37	adantr 481	. . . 4 ⊢ ((𝜑 ∧ (𝑅‘𝐹) = 𝑉) → 𝐹 ∈ (𝐼‘(𝑅‘𝐹)))
48		fveq2 6809	. . . . 5 ⊢ ((𝑅‘𝐹) = 𝑉 → (𝐼‘(𝑅‘𝐹)) = (𝐼‘𝑉))
49	48	adantl 482	. . . 4 ⊢ ((𝜑 ∧ (𝑅‘𝐹) = 𝑉) → (𝐼‘(𝑅‘𝐹)) = (𝐼‘𝑉))
50	47, 49	eleqtrd 2840	. . 3 ⊢ ((𝜑 ∧ (𝑅‘𝐹) = 𝑉) → 𝐹 ∈ (𝐼‘𝑉))
51	46, 50	sseldd 3931	. 2 ⊢ ((𝜑 ∧ (𝑅‘𝐹) = 𝑉) → 𝐹 ∈ ((𝐼‘𝑈) ⊕ (𝐼‘𝑉)))
52		dia2dimlem9.j	. . 3 ⊢ ∨ = (join‘𝐾)
53		dia2dimlem9.m	. . 3 ⊢ ∧ = (meet‘𝐾)
54		dia2dimlem9.n	. . 3 ⊢ 𝑁 = (LSpan‘𝑌)
55	1	adantr 481	. . 3 ⊢ ((𝜑 ∧ ((𝑅‘𝐹) ≠ 𝑈 ∧ (𝑅‘𝐹) ≠ 𝑉)) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
56	9	adantr 481	. . 3 ⊢ ((𝜑 ∧ ((𝑅‘𝐹) ≠ 𝑈 ∧ (𝑅‘𝐹) ≠ 𝑉)) → (𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊))
57	21	adantr 481	. . 3 ⊢ ((𝜑 ∧ ((𝑅‘𝐹) ≠ 𝑈 ∧ (𝑅‘𝐹) ≠ 𝑉)) → (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊))
58	33	adantr 481	. . 3 ⊢ ((𝜑 ∧ ((𝑅‘𝐹) ≠ 𝑈 ∧ (𝑅‘𝐹) ≠ 𝑉)) → 𝐹 ∈ 𝑇)
59		dia2dimlem9.rf	. . . 4 ⊢ (𝜑 → (𝑅‘𝐹) ≤ (𝑈 ∨ 𝑉))
60	59	adantr 481	. . 3 ⊢ ((𝜑 ∧ ((𝑅‘𝐹) ≠ 𝑈 ∧ (𝑅‘𝐹) ≠ 𝑉)) → (𝑅‘𝐹) ≤ (𝑈 ∨ 𝑉))
61		dia2dimlem9.uv	. . . 4 ⊢ (𝜑 → 𝑈 ≠ 𝑉)
62	61	adantr 481	. . 3 ⊢ ((𝜑 ∧ ((𝑅‘𝐹) ≠ 𝑈 ∧ (𝑅‘𝐹) ≠ 𝑉)) → 𝑈 ≠ 𝑉)
63		simprl 768	. . 3 ⊢ ((𝜑 ∧ ((𝑅‘𝐹) ≠ 𝑈 ∧ (𝑅‘𝐹) ≠ 𝑉)) → (𝑅‘𝐹) ≠ 𝑈)
64		simprr 770	. . 3 ⊢ ((𝜑 ∧ ((𝑅‘𝐹) ≠ 𝑈 ∧ (𝑅‘𝐹) ≠ 𝑉)) → (𝑅‘𝐹) ≠ 𝑉)
65	16, 52, 53, 12, 2, 34, 35, 3, 6, 29, 54, 17, 55, 56, 57, 58, 60, 62, 63, 64	dia2dimlem8 39297	. 2 ⊢ ((𝜑 ∧ ((𝑅‘𝐹) ≠ 𝑈 ∧ (𝑅‘𝐹) ≠ 𝑉)) → 𝐹 ∈ ((𝐼‘𝑈) ⊕ (𝐼‘𝑉)))
66	42, 51, 65	pm2.61da2ne 3031	1 ⊢ (𝜑 → 𝐹 ∈ ((𝐼‘𝑈) ⊕ (𝐼‘𝑉)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 396 = wceq 1540 ∈ wcel 2105 ≠ wne 2941 ⊆ wss 3896 class class class wbr 5085 ‘cfv 6463 (class class class)co 7313 Basecbs 16979 lecple 17036 joincjn 18096 meetcmee 18097 SubGrpcsubg 18816 LSSumclsm 19306 LModclmod 20194 LSubSpclss 20264 LSpanclspn 20304 LVecclvec 20435 Atomscatm 37489 HLchlt 37576 LHypclh 38210 LTrncltrn 38327 trLctrl 38384 DVecAcdveca 39228 DIsoAcdia 39254

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 1912 ax-6 1970 ax-7 2010 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2153 ax-12 2170 ax-ext 2708 ax-rep 5222 ax-sep 5236 ax-nul 5243 ax-pow 5301 ax-pr 5365 ax-un 7626 ax-cnex 10997 ax-resscn 10998 ax-1cn 10999 ax-icn 11000 ax-addcl 11001 ax-addrcl 11002 ax-mulcl 11003 ax-mulrcl 11004 ax-mulcom 11005 ax-addass 11006 ax-mulass 11007 ax-distr 11008 ax-i2m1 11009 ax-1ne0 11010 ax-1rid 11011 ax-rnegex 11012 ax-rrecex 11013 ax-cnre 11014 ax-pre-lttri 11015 ax-pre-lttrn 11016 ax-pre-ltadd 11017 ax-pre-mulgt0 11018 ax-riotaBAD 37179

This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1781 df-nf 1785 df-sb 2067 df-mo 2539 df-eu 2568 df-clab 2715 df-cleq 2729 df-clel 2815 df-nfc 2887 df-ne 2942 df-nel 3048 df-ral 3063 df-rex 3072 df-rmo 3350 df-reu 3351 df-rab 3405 df-v 3443 df-sbc 3726 df-csb 3842 df-dif 3899 df-un 3901 df-in 3903 df-ss 3913 df-pss 3915 df-nul 4267 df-if 4470 df-pw 4545 df-sn 4570 df-pr 4572 df-tp 4574 df-op 4576 df-uni 4849 df-int 4891 df-iun 4937 df-iin 4938 df-br 5086 df-opab 5148 df-mpt 5169 df-tr 5203 df-id 5505 df-eprel 5511 df-po 5519 df-so 5520 df-fr 5560 df-we 5562 df-xp 5611 df-rel 5612 df-cnv 5613 df-co 5614 df-dm 5615 df-rn 5616 df-res 5617 df-ima 5618 df-pred 6222 df-ord 6289 df-on 6290 df-lim 6291 df-suc 6292 df-iota 6415 df-fun 6465 df-fn 6466 df-f 6467 df-f1 6468 df-fo 6469 df-f1o 6470 df-fv 6471 df-riota 7270 df-ov 7316 df-oprab 7317 df-mpo 7318 df-om 7756 df-1st 7874 df-2nd 7875 df-tpos 8087 df-undef 8134 df-frecs 8142 df-wrecs 8173 df-recs 8247 df-rdg 8286 df-1o 8342 df-er 8544 df-map 8663 df-en 8780 df-dom 8781 df-sdom 8782 df-fin 8783 df-pnf 11081 df-mnf 11082 df-xr 11083 df-ltxr 11084 df-le 11085 df-sub 11277 df-neg 11278 df-nn 12044 df-2 12106 df-3 12107 df-4 12108 df-5 12109 df-6 12110 df-n0 12304 df-z 12390 df-uz 12653 df-fz 13310 df-struct 16915 df-sets 16932 df-slot 16950 df-ndx 16962 df-base 16980 df-ress 17009 df-plusg 17042 df-mulr 17043 df-sca 17045 df-vsca 17046 df-0g 17219 df-proset 18080 df-poset 18098 df-plt 18115 df-lub 18131 df-glb 18132 df-join 18133 df-meet 18134 df-p0 18210 df-p1 18211 df-lat 18217 df-clat 18284 df-mgm 18393 df-sgrp 18442 df-mnd 18453 df-submnd 18498 df-grp 18647 df-minusg 18648 df-sbg 18649 df-subg 18819 df-cntz 18990 df-lsm 19308 df-cmn 19455 df-abl 19456 df-mgp 19788 df-ur 19805 df-ring 19852 df-oppr 19929 df-dvdsr 19950 df-unit 19951 df-invr 19981 df-dvr 19992 df-drng 20064 df-lmod 20196 df-lss 20265 df-lsp 20305 df-lvec 20436 df-oposet 37402 df-ol 37404 df-oml 37405 df-covers 37492 df-ats 37493 df-atl 37524 df-cvlat 37548 df-hlat 37577 df-llines 37724 df-lplanes 37725 df-lvols 37726 df-lines 37727 df-psubsp 37729 df-pmap 37730 df-padd 38022 df-lhyp 38214 df-laut 38215 df-ldil 38330 df-ltrn 38331 df-trl 38385 df-tgrp 38969 df-tendo 38981 df-edring 38983 df-dveca 39229 df-disoa 39255

This theorem is referenced by: dia2dimlem11 39300

W3C validator