dia2dimlem7 - Mathbox for Norm Megill

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

Theorem dia2dimlem7 36880

Description: Lemma for dia2dim 36887. Eliminate (𝐹‘𝑃) ≠ 𝑃 condition. (Contributed by NM, 8-Sep-2014.)

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

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

**Proof of Theorem dia2dimlem7**
Step	Hyp	Ref	Expression
1		dia2dimlem7.k	. . . . 5 ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
2		dia2dimlem7.f	. . . . 5 ⊢ (𝜑 → 𝐹 ∈ 𝑇)
3		dia2dimlem7.p	. . . . 5 ⊢ (𝜑 → (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊))
4		eqid 2761	. . . . . 6 ⊢ (Base‘𝐾) = (Base‘𝐾)
5		dia2dimlem7.l	. . . . . 6 ⊢ ≤ = (le‘𝐾)
6		dia2dimlem7.a	. . . . . 6 ⊢ 𝐴 = (Atoms‘𝐾)
7		dia2dimlem7.h	. . . . . 6 ⊢ 𝐻 = (LHyp‘𝐾)
8		dia2dimlem7.t	. . . . . 6 ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)
9	4, 5, 6, 7, 8	ltrnideq 35984	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝐹 = ( I ↾ (Base‘𝐾)) ↔ (𝐹‘𝑃) = 𝑃))
10	1, 2, 3, 9	syl3anc 1477	. . . 4 ⊢ (𝜑 → (𝐹 = ( I ↾ (Base‘𝐾)) ↔ (𝐹‘𝑃) = 𝑃))
11		dia2dimlem7.y	. . . . . . . 8 ⊢ 𝑌 = ((DVecA‘𝐾)‘𝑊)
12		eqid 2761	. . . . . . . 8 ⊢ (0_g‘𝑌) = (0_g‘𝑌)
13	4, 7, 8, 11, 12	dva0g 36837	. . . . . . 7 ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → (0_g‘𝑌) = ( I ↾ (Base‘𝐾)))
14	1, 13	syl 17	. . . . . 6 ⊢ (𝜑 → (0_g‘𝑌) = ( I ↾ (Base‘𝐾)))
15	7, 11	dvalvec 36836	. . . . . . . 8 ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → 𝑌 ∈ LVec)
16		lveclmod 19329	. . . . . . . 8 ⊢ (𝑌 ∈ LVec → 𝑌 ∈ LMod)
17	1, 15, 16	3syl 18	. . . . . . 7 ⊢ (𝜑 → 𝑌 ∈ LMod)
18		dia2dimlem7.u	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊))
19	18	simpld 477	. . . . . . . . . 10 ⊢ (𝜑 → 𝑈 ∈ 𝐴)
20	4, 6	atbase 35098	. . . . . . . . . 10 ⊢ (𝑈 ∈ 𝐴 → 𝑈 ∈ (Base‘𝐾))
21	19, 20	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝑈 ∈ (Base‘𝐾))
22	18	simprd 482	. . . . . . . . 9 ⊢ (𝜑 → 𝑈 ≤ 𝑊)
23		dia2dimlem7.i	. . . . . . . . . 10 ⊢ 𝐼 = ((DIsoA‘𝐾)‘𝑊)
24		dia2dimlem7.s	. . . . . . . . . 10 ⊢ 𝑆 = (LSubSp‘𝑌)
25	4, 5, 7, 11, 23, 24	dialss 36856	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑈 ∈ (Base‘𝐾) ∧ 𝑈 ≤ 𝑊)) → (𝐼‘𝑈) ∈ 𝑆)
26	1, 21, 22, 25	syl12anc 1475	. . . . . . . 8 ⊢ (𝜑 → (𝐼‘𝑈) ∈ 𝑆)
27		dia2dimlem7.v	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊))
28	27	simpld 477	. . . . . . . . . 10 ⊢ (𝜑 → 𝑉 ∈ 𝐴)
29	4, 6	atbase 35098	. . . . . . . . . 10 ⊢ (𝑉 ∈ 𝐴 → 𝑉 ∈ (Base‘𝐾))
30	28, 29	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝑉 ∈ (Base‘𝐾))
31	27	simprd 482	. . . . . . . . 9 ⊢ (𝜑 → 𝑉 ≤ 𝑊)
32	4, 5, 7, 11, 23, 24	dialss 36856	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑉 ∈ (Base‘𝐾) ∧ 𝑉 ≤ 𝑊)) → (𝐼‘𝑉) ∈ 𝑆)
33	1, 30, 31, 32	syl12anc 1475	. . . . . . . 8 ⊢ (𝜑 → (𝐼‘𝑉) ∈ 𝑆)
34		dia2dimlem7.pl	. . . . . . . . 9 ⊢ ⊕ = (LSSum‘𝑌)
35	24, 34	lsmcl 19306	. . . . . . . 8 ⊢ ((𝑌 ∈ LMod ∧ (𝐼‘𝑈) ∈ 𝑆 ∧ (𝐼‘𝑉) ∈ 𝑆) → ((𝐼‘𝑈) ⊕ (𝐼‘𝑉)) ∈ 𝑆)
36	17, 26, 33, 35	syl3anc 1477	. . . . . . 7 ⊢ (𝜑 → ((𝐼‘𝑈) ⊕ (𝐼‘𝑉)) ∈ 𝑆)
37	12, 24	lss0cl 19170	. . . . . . 7 ⊢ ((𝑌 ∈ LMod ∧ ((𝐼‘𝑈) ⊕ (𝐼‘𝑉)) ∈ 𝑆) → (0_g‘𝑌) ∈ ((𝐼‘𝑈) ⊕ (𝐼‘𝑉)))
38	17, 36, 37	syl2anc 696	. . . . . 6 ⊢ (𝜑 → (0_g‘𝑌) ∈ ((𝐼‘𝑈) ⊕ (𝐼‘𝑉)))
39	14, 38	eqeltrrd 2841	. . . . 5 ⊢ (𝜑 → ( I ↾ (Base‘𝐾)) ∈ ((𝐼‘𝑈) ⊕ (𝐼‘𝑉)))
40		eleq1a 2835	. . . . 5 ⊢ (( I ↾ (Base‘𝐾)) ∈ ((𝐼‘𝑈) ⊕ (𝐼‘𝑉)) → (𝐹 = ( I ↾ (Base‘𝐾)) → 𝐹 ∈ ((𝐼‘𝑈) ⊕ (𝐼‘𝑉))))
41	39, 40	syl 17	. . . 4 ⊢ (𝜑 → (𝐹 = ( I ↾ (Base‘𝐾)) → 𝐹 ∈ ((𝐼‘𝑈) ⊕ (𝐼‘𝑉))))
42	10, 41	sylbird 250	. . 3 ⊢ (𝜑 → ((𝐹‘𝑃) = 𝑃 → 𝐹 ∈ ((𝐼‘𝑈) ⊕ (𝐼‘𝑉))))
43	42	imp 444	. 2 ⊢ ((𝜑 ∧ (𝐹‘𝑃) = 𝑃) → 𝐹 ∈ ((𝐼‘𝑈) ⊕ (𝐼‘𝑉)))
44		dia2dimlem7.j	. . 3 ⊢ ∨ = (join‘𝐾)
45		dia2dimlem7.m	. . 3 ⊢ ∧ = (meet‘𝐾)
46		dia2dimlem7.r	. . 3 ⊢ 𝑅 = ((trL‘𝐾)‘𝑊)
47		dia2dimlem7.n	. . 3 ⊢ 𝑁 = (LSpan‘𝑌)
48		dia2dimlem7.q	. . 3 ⊢ 𝑄 = ((𝑃 ∨ 𝑈) ∧ ((𝐹‘𝑃) ∨ 𝑉))
49	1	adantr 472	. . 3 ⊢ ((𝜑 ∧ (𝐹‘𝑃) ≠ 𝑃) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
50	18	adantr 472	. . 3 ⊢ ((𝜑 ∧ (𝐹‘𝑃) ≠ 𝑃) → (𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊))
51	27	adantr 472	. . 3 ⊢ ((𝜑 ∧ (𝐹‘𝑃) ≠ 𝑃) → (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊))
52	3	adantr 472	. . 3 ⊢ ((𝜑 ∧ (𝐹‘𝑃) ≠ 𝑃) → (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊))
53	2	anim1i 593	. . 3 ⊢ ((𝜑 ∧ (𝐹‘𝑃) ≠ 𝑃) → (𝐹 ∈ 𝑇 ∧ (𝐹‘𝑃) ≠ 𝑃))
54		dia2dimlem7.rf	. . . 4 ⊢ (𝜑 → (𝑅‘𝐹) ≤ (𝑈 ∨ 𝑉))
55	54	adantr 472	. . 3 ⊢ ((𝜑 ∧ (𝐹‘𝑃) ≠ 𝑃) → (𝑅‘𝐹) ≤ (𝑈 ∨ 𝑉))
56		dia2dimlem7.uv	. . . 4 ⊢ (𝜑 → 𝑈 ≠ 𝑉)
57	56	adantr 472	. . 3 ⊢ ((𝜑 ∧ (𝐹‘𝑃) ≠ 𝑃) → 𝑈 ≠ 𝑉)
58		dia2dimlem7.ru	. . . 4 ⊢ (𝜑 → (𝑅‘𝐹) ≠ 𝑈)
59	58	adantr 472	. . 3 ⊢ ((𝜑 ∧ (𝐹‘𝑃) ≠ 𝑃) → (𝑅‘𝐹) ≠ 𝑈)
60		dia2dimlem7.rv	. . . 4 ⊢ (𝜑 → (𝑅‘𝐹) ≠ 𝑉)
61	60	adantr 472	. . 3 ⊢ ((𝜑 ∧ (𝐹‘𝑃) ≠ 𝑃) → (𝑅‘𝐹) ≠ 𝑉)
62	5, 44, 45, 6, 7, 8, 46, 11, 24, 34, 47, 23, 48, 49, 50, 51, 52, 53, 55, 57, 59, 61	dia2dimlem6 36879	. 2 ⊢ ((𝜑 ∧ (𝐹‘𝑃) ≠ 𝑃) → 𝐹 ∈ ((𝐼‘𝑈) ⊕ (𝐼‘𝑉)))
63	43, 62	pm2.61dane 3020	1 ⊢ (𝜑 → 𝐹 ∈ ((𝐼‘𝑈) ⊕ (𝐼‘𝑉)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 196 ∧ wa 383 = wceq 1632 ∈ wcel 2140 ≠ wne 2933 class class class wbr 4805 I cid 5174 ↾ cres 5269 ‘cfv 6050 (class class class)co 6815 Basecbs 16080 lecple 16171 0_gc0g 16323 joincjn 17166 meetcmee 17167 LSSumclsm 18270 LModclmod 19086 LSubSpclss 19155 LSpanclspn 19194 LVecclvec 19325 Atomscatm 35072 HLchlt 35159 LHypclh 35792 LTrncltrn 35909 trLctrl 35967 DVecAcdveca 36811 DIsoAcdia 36838

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1871 ax-4 1886 ax-5 1989 ax-6 2055 ax-7 2091 ax-8 2142 ax-9 2149 ax-10 2169 ax-11 2184 ax-12 2197 ax-13 2392 ax-ext 2741 ax-rep 4924 ax-sep 4934 ax-nul 4942 ax-pow 4993 ax-pr 5056 ax-un 7116 ax-cnex 10205 ax-resscn 10206 ax-1cn 10207 ax-icn 10208 ax-addcl 10209 ax-addrcl 10210 ax-mulcl 10211 ax-mulrcl 10212 ax-mulcom 10213 ax-addass 10214 ax-mulass 10215 ax-distr 10216 ax-i2m1 10217 ax-1ne0 10218 ax-1rid 10219 ax-rnegex 10220 ax-rrecex 10221 ax-cnre 10222 ax-pre-lttri 10223 ax-pre-lttrn 10224 ax-pre-ltadd 10225 ax-pre-mulgt0 10226 ax-riotaBAD 34761

This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-3or 1073 df-3an 1074 df-tru 1635 df-fal 1638 df-ex 1854 df-nf 1859 df-sb 2048 df-eu 2612 df-mo 2613 df-clab 2748 df-cleq 2754 df-clel 2757 df-nfc 2892 df-ne 2934 df-nel 3037 df-ral 3056 df-rex 3057 df-reu 3058 df-rmo 3059 df-rab 3060 df-v 3343 df-sbc 3578 df-csb 3676 df-dif 3719 df-un 3721 df-in 3723 df-ss 3730 df-pss 3732 df-nul 4060 df-if 4232 df-pw 4305 df-sn 4323 df-pr 4325 df-tp 4327 df-op 4329 df-uni 4590 df-int 4629 df-iun 4675 df-iin 4676 df-br 4806 df-opab 4866 df-mpt 4883 df-tr 4906 df-id 5175 df-eprel 5180 df-po 5188 df-so 5189 df-fr 5226 df-we 5228 df-xp 5273 df-rel 5274 df-cnv 5275 df-co 5276 df-dm 5277 df-rn 5278 df-res 5279 df-ima 5280 df-pred 5842 df-ord 5888 df-on 5889 df-lim 5890 df-suc 5891 df-iota 6013 df-fun 6052 df-fn 6053 df-f 6054 df-f1 6055 df-fo 6056 df-f1o 6057 df-fv 6058 df-riota 6776 df-ov 6818 df-oprab 6819 df-mpt2 6820 df-om 7233 df-1st 7335 df-2nd 7336 df-tpos 7523 df-undef 7570 df-wrecs 7578 df-recs 7639 df-rdg 7677 df-1o 7731 df-oadd 7735 df-er 7914 df-map 8028 df-en 8125 df-dom 8126 df-sdom 8127 df-fin 8128 df-pnf 10289 df-mnf 10290 df-xr 10291 df-ltxr 10292 df-le 10293 df-sub 10481 df-neg 10482 df-nn 11234 df-2 11292 df-3 11293 df-4 11294 df-5 11295 df-6 11296 df-n0 11506 df-z 11591 df-uz 11901 df-fz 12541 df-struct 16082 df-ndx 16083 df-slot 16084 df-base 16086 df-sets 16087 df-ress 16088 df-plusg 16177 df-mulr 16178 df-sca 16180 df-vsca 16181 df-0g 16325 df-preset 17150 df-poset 17168 df-plt 17180 df-lub 17196 df-glb 17197 df-join 17198 df-meet 17199 df-p0 17261 df-p1 17262 df-lat 17268 df-clat 17330 df-mgm 17464 df-sgrp 17506 df-mnd 17517 df-submnd 17558 df-grp 17647 df-minusg 17648 df-sbg 17649 df-subg 17813 df-cntz 17971 df-lsm 18272 df-cmn 18416 df-abl 18417 df-mgp 18711 df-ur 18723 df-ring 18770 df-oppr 18844 df-dvdsr 18862 df-unit 18863 df-invr 18893 df-dvr 18904 df-drng 18972 df-lmod 19088 df-lss 19156 df-lsp 19195 df-lvec 19326 df-oposet 34985 df-ol 34987 df-oml 34988 df-covers 35075 df-ats 35076 df-atl 35107 df-cvlat 35131 df-hlat 35160 df-llines 35306 df-lplanes 35307 df-lvols 35308 df-lines 35309 df-psubsp 35311 df-pmap 35312 df-padd 35604 df-lhyp 35796 df-laut 35797 df-ldil 35912 df-ltrn 35913 df-trl 35968 df-tgrp 36552 df-tendo 36564 df-edring 36566 df-dveca 36812 df-disoa 36839

This theorem is referenced by: dia2dimlem8 36881

W3C validator