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 39331

Description: Lemma for dia2dim 39338. 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 2736	. . . . . 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 38436	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝐹 = ( I ↾ (Base‘𝐾)) ↔ (𝐹‘𝑃) = 𝑃))
10	1, 2, 3, 9	syl3anc 1370	. . . 4 ⊢ (𝜑 → (𝐹 = ( I ↾ (Base‘𝐾)) ↔ (𝐹‘𝑃) = 𝑃))
11		dia2dimlem7.y	. . . . . . . 8 ⊢ 𝑌 = ((DVecA‘𝐾)‘𝑊)
12		eqid 2736	. . . . . . . 8 ⊢ (0_g‘𝑌) = (0_g‘𝑌)
13	4, 7, 8, 11, 12	dva0g 39288	. . . . . . 7 ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → (0_g‘𝑌) = ( I ↾ (Base‘𝐾)))
14	1, 13	syl 17	. . . . . 6 ⊢ (𝜑 → (0_g‘𝑌) = ( I ↾ (Base‘𝐾)))
15	7, 11	dvalvec 39287	. . . . . . . 8 ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → 𝑌 ∈ LVec)
16		lveclmod 20466	. . . . . . . 8 ⊢ (𝑌 ∈ LVec → 𝑌 ∈ LMod)
17	1, 15, 16	3syl 18	. . . . . . 7 ⊢ (𝜑 → 𝑌 ∈ LMod)
18		dia2dimlem7.u	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊))
19	18	simpld 495	. . . . . . . . . 10 ⊢ (𝜑 → 𝑈 ∈ 𝐴)
20	4, 6	atbase 37549	. . . . . . . . . 10 ⊢ (𝑈 ∈ 𝐴 → 𝑈 ∈ (Base‘𝐾))
21	19, 20	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝑈 ∈ (Base‘𝐾))
22	18	simprd 496	. . . . . . . . 9 ⊢ (𝜑 → 𝑈 ≤ 𝑊)
23		dia2dimlem7.i	. . . . . . . . . 10 ⊢ 𝐼 = ((DIsoA‘𝐾)‘𝑊)
24		dia2dimlem7.s	. . . . . . . . . 10 ⊢ 𝑆 = (LSubSp‘𝑌)
25	4, 5, 7, 11, 23, 24	dialss 39307	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑈 ∈ (Base‘𝐾) ∧ 𝑈 ≤ 𝑊)) → (𝐼‘𝑈) ∈ 𝑆)
26	1, 21, 22, 25	syl12anc 834	. . . . . . . 8 ⊢ (𝜑 → (𝐼‘𝑈) ∈ 𝑆)
27		dia2dimlem7.v	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊))
28	27	simpld 495	. . . . . . . . . 10 ⊢ (𝜑 → 𝑉 ∈ 𝐴)
29	4, 6	atbase 37549	. . . . . . . . . 10 ⊢ (𝑉 ∈ 𝐴 → 𝑉 ∈ (Base‘𝐾))
30	28, 29	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝑉 ∈ (Base‘𝐾))
31	27	simprd 496	. . . . . . . . 9 ⊢ (𝜑 → 𝑉 ≤ 𝑊)
32	4, 5, 7, 11, 23, 24	dialss 39307	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑉 ∈ (Base‘𝐾) ∧ 𝑉 ≤ 𝑊)) → (𝐼‘𝑉) ∈ 𝑆)
33	1, 30, 31, 32	syl12anc 834	. . . . . . . 8 ⊢ (𝜑 → (𝐼‘𝑉) ∈ 𝑆)
34		dia2dimlem7.pl	. . . . . . . . 9 ⊢ ⊕ = (LSSum‘𝑌)
35	24, 34	lsmcl 20443	. . . . . . . 8 ⊢ ((𝑌 ∈ LMod ∧ (𝐼‘𝑈) ∈ 𝑆 ∧ (𝐼‘𝑉) ∈ 𝑆) → ((𝐼‘𝑈) ⊕ (𝐼‘𝑉)) ∈ 𝑆)
36	17, 26, 33, 35	syl3anc 1370	. . . . . . 7 ⊢ (𝜑 → ((𝐼‘𝑈) ⊕ (𝐼‘𝑉)) ∈ 𝑆)
37	12, 24	lss0cl 20306	. . . . . . 7 ⊢ ((𝑌 ∈ LMod ∧ ((𝐼‘𝑈) ⊕ (𝐼‘𝑉)) ∈ 𝑆) → (0_g‘𝑌) ∈ ((𝐼‘𝑈) ⊕ (𝐼‘𝑉)))
38	17, 36, 37	syl2anc 584	. . . . . 6 ⊢ (𝜑 → (0_g‘𝑌) ∈ ((𝐼‘𝑈) ⊕ (𝐼‘𝑉)))
39	14, 38	eqeltrrd 2838	. . . . 5 ⊢ (𝜑 → ( I ↾ (Base‘𝐾)) ∈ ((𝐼‘𝑈) ⊕ (𝐼‘𝑉)))
40		eleq1a 2832	. . . . 5 ⊢ (( I ↾ (Base‘𝐾)) ∈ ((𝐼‘𝑈) ⊕ (𝐼‘𝑉)) → (𝐹 = ( I ↾ (Base‘𝐾)) → 𝐹 ∈ ((𝐼‘𝑈) ⊕ (𝐼‘𝑉))))
41	39, 40	syl 17	. . . 4 ⊢ (𝜑 → (𝐹 = ( I ↾ (Base‘𝐾)) → 𝐹 ∈ ((𝐼‘𝑈) ⊕ (𝐼‘𝑉))))
42	10, 41	sylbird 259	. . 3 ⊢ (𝜑 → ((𝐹‘𝑃) = 𝑃 → 𝐹 ∈ ((𝐼‘𝑈) ⊕ (𝐼‘𝑉))))
43	42	imp 407	. 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 481	. . 3 ⊢ ((𝜑 ∧ (𝐹‘𝑃) ≠ 𝑃) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
50	18	adantr 481	. . 3 ⊢ ((𝜑 ∧ (𝐹‘𝑃) ≠ 𝑃) → (𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊))
51	27	adantr 481	. . 3 ⊢ ((𝜑 ∧ (𝐹‘𝑃) ≠ 𝑃) → (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊))
52	3	adantr 481	. . 3 ⊢ ((𝜑 ∧ (𝐹‘𝑃) ≠ 𝑃) → (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊))
53	2	anim1i 615	. . 3 ⊢ ((𝜑 ∧ (𝐹‘𝑃) ≠ 𝑃) → (𝐹 ∈ 𝑇 ∧ (𝐹‘𝑃) ≠ 𝑃))
54		dia2dimlem7.rf	. . . 4 ⊢ (𝜑 → (𝑅‘𝐹) ≤ (𝑈 ∨ 𝑉))
55	54	adantr 481	. . 3 ⊢ ((𝜑 ∧ (𝐹‘𝑃) ≠ 𝑃) → (𝑅‘𝐹) ≤ (𝑈 ∨ 𝑉))
56		dia2dimlem7.uv	. . . 4 ⊢ (𝜑 → 𝑈 ≠ 𝑉)
57	56	adantr 481	. . 3 ⊢ ((𝜑 ∧ (𝐹‘𝑃) ≠ 𝑃) → 𝑈 ≠ 𝑉)
58		dia2dimlem7.ru	. . . 4 ⊢ (𝜑 → (𝑅‘𝐹) ≠ 𝑈)
59	58	adantr 481	. . 3 ⊢ ((𝜑 ∧ (𝐹‘𝑃) ≠ 𝑃) → (𝑅‘𝐹) ≠ 𝑈)
60		dia2dimlem7.rv	. . . 4 ⊢ (𝜑 → (𝑅‘𝐹) ≠ 𝑉)
61	60	adantr 481	. . 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 39330	. 2 ⊢ ((𝜑 ∧ (𝐹‘𝑃) ≠ 𝑃) → 𝐹 ∈ ((𝐼‘𝑈) ⊕ (𝐼‘𝑉)))
63	43, 62	pm2.61dane 3029	1 ⊢ (𝜑 → 𝐹 ∈ ((𝐼‘𝑈) ⊕ (𝐼‘𝑉)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 396 = wceq 1540 ∈ wcel 2105 ≠ wne 2940 class class class wbr 5089 I cid 5511 ↾ cres 5616 ‘cfv 6473 (class class class)co 7329 Basecbs 17001 lecple 17058 0_gc0g 17239 joincjn 18118 meetcmee 18119 LSSumclsm 19327 LModclmod 20221 LSubSpclss 20291 LSpanclspn 20331 LVecclvec 20462 Atomscatm 37523 HLchlt 37610 LHypclh 38245 LTrncltrn 38362 trLctrl 38419 DVecAcdveca 39263 DIsoAcdia 39289

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 2707 ax-rep 5226 ax-sep 5240 ax-nul 5247 ax-pow 5305 ax-pr 5369 ax-un 7642 ax-cnex 11020 ax-resscn 11021 ax-1cn 11022 ax-icn 11023 ax-addcl 11024 ax-addrcl 11025 ax-mulcl 11026 ax-mulrcl 11027 ax-mulcom 11028 ax-addass 11029 ax-mulass 11030 ax-distr 11031 ax-i2m1 11032 ax-1ne0 11033 ax-1rid 11034 ax-rnegex 11035 ax-rrecex 11036 ax-cnre 11037 ax-pre-lttri 11038 ax-pre-lttrn 11039 ax-pre-ltadd 11040 ax-pre-mulgt0 11041 ax-riotaBAD 37213

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 2538 df-eu 2567 df-clab 2714 df-cleq 2728 df-clel 2814 df-nfc 2886 df-ne 2941 df-nel 3047 df-ral 3062 df-rex 3071 df-rmo 3349 df-reu 3350 df-rab 3404 df-v 3443 df-sbc 3727 df-csb 3843 df-dif 3900 df-un 3902 df-in 3904 df-ss 3914 df-pss 3916 df-nul 4269 df-if 4473 df-pw 4548 df-sn 4573 df-pr 4575 df-tp 4577 df-op 4579 df-uni 4852 df-int 4894 df-iun 4940 df-iin 4941 df-br 5090 df-opab 5152 df-mpt 5173 df-tr 5207 df-id 5512 df-eprel 5518 df-po 5526 df-so 5527 df-fr 5569 df-we 5571 df-xp 5620 df-rel 5621 df-cnv 5622 df-co 5623 df-dm 5624 df-rn 5625 df-res 5626 df-ima 5627 df-pred 6232 df-ord 6299 df-on 6300 df-lim 6301 df-suc 6302 df-iota 6425 df-fun 6475 df-fn 6476 df-f 6477 df-f1 6478 df-fo 6479 df-f1o 6480 df-fv 6481 df-riota 7286 df-ov 7332 df-oprab 7333 df-mpo 7334 df-om 7773 df-1st 7891 df-2nd 7892 df-tpos 8104 df-undef 8151 df-frecs 8159 df-wrecs 8190 df-recs 8264 df-rdg 8303 df-1o 8359 df-er 8561 df-map 8680 df-en 8797 df-dom 8798 df-sdom 8799 df-fin 8800 df-pnf 11104 df-mnf 11105 df-xr 11106 df-ltxr 11107 df-le 11108 df-sub 11300 df-neg 11301 df-nn 12067 df-2 12129 df-3 12130 df-4 12131 df-5 12132 df-6 12133 df-n0 12327 df-z 12413 df-uz 12676 df-fz 13333 df-struct 16937 df-sets 16954 df-slot 16972 df-ndx 16984 df-base 17002 df-ress 17031 df-plusg 17064 df-mulr 17065 df-sca 17067 df-vsca 17068 df-0g 17241 df-proset 18102 df-poset 18120 df-plt 18137 df-lub 18153 df-glb 18154 df-join 18155 df-meet 18156 df-p0 18232 df-p1 18233 df-lat 18239 df-clat 18306 df-mgm 18415 df-sgrp 18464 df-mnd 18475 df-submnd 18520 df-grp 18668 df-minusg 18669 df-sbg 18670 df-subg 18840 df-cntz 19011 df-lsm 19329 df-cmn 19475 df-abl 19476 df-mgp 19808 df-ur 19825 df-ring 19872 df-oppr 19949 df-dvdsr 19970 df-unit 19971 df-invr 20001 df-dvr 20012 df-drng 20087 df-lmod 20223 df-lss 20292 df-lsp 20332 df-lvec 20463 df-oposet 37436 df-ol 37438 df-oml 37439 df-covers 37526 df-ats 37527 df-atl 37558 df-cvlat 37582 df-hlat 37611 df-llines 37759 df-lplanes 37760 df-lvols 37761 df-lines 37762 df-psubsp 37764 df-pmap 37765 df-padd 38057 df-lhyp 38249 df-laut 38250 df-ldil 38365 df-ltrn 38366 df-trl 38420 df-tgrp 39004 df-tendo 39016 df-edring 39018 df-dveca 39264 df-disoa 39290

This theorem is referenced by: dia2dimlem8 39332

W3C validator