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 41695

Description: Lemma for dia2dim 41702. 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 2763	. . . . . 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 40800	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝐹 = ( I ↾ (Base‘𝐾)) ↔ (𝐹‘𝑃) = 𝑃))
10	1, 2, 3, 9	syl3anc 1391	. . . 4 ⊢ (𝜑 → (𝐹 = ( I ↾ (Base‘𝐾)) ↔ (𝐹‘𝑃) = 𝑃))
11		dia2dimlem7.y	. . . . . . . 8 ⊢ 𝑌 = ((DVecA‘𝐾)‘𝑊)
12		eqid 2763	. . . . . . . 8 ⊢ (0_g‘𝑌) = (0_g‘𝑌)
13	4, 7, 8, 11, 12	dva0g 41652	. . . . . . 7 ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → (0_g‘𝑌) = ( I ↾ (Base‘𝐾)))
14	1, 13	syl 17	. . . . . 6 ⊢ (𝜑 → (0_g‘𝑌) = ( I ↾ (Base‘𝐾)))
15	7, 11	dvalvec 41651	. . . . . . . 8 ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → 𝑌 ∈ LVec)
16		lveclmod 21174	. . . . . . . 8 ⊢ (𝑌 ∈ LVec → 𝑌 ∈ LMod)
17	1, 15, 16	3syl 18	. . . . . . 7 ⊢ (𝜑 → 𝑌 ∈ LMod)
18		dia2dimlem7.u	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊))
19	18	simpld 498	. . . . . . . . . 10 ⊢ (𝜑 → 𝑈 ∈ 𝐴)
20	4, 6	atbase 39914	. . . . . . . . . 10 ⊢ (𝑈 ∈ 𝐴 → 𝑈 ∈ (Base‘𝐾))
21	19, 20	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝑈 ∈ (Base‘𝐾))
22	18	simprd 499	. . . . . . . . 9 ⊢ (𝜑 → 𝑈 ≤ 𝑊)
23		dia2dimlem7.i	. . . . . . . . . 10 ⊢ 𝐼 = ((DIsoA‘𝐾)‘𝑊)
24		dia2dimlem7.s	. . . . . . . . . 10 ⊢ 𝑆 = (LSubSp‘𝑌)
25	4, 5, 7, 11, 23, 24	dialss 41671	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑈 ∈ (Base‘𝐾) ∧ 𝑈 ≤ 𝑊)) → (𝐼‘𝑈) ∈ 𝑆)
26	1, 21, 22, 25	syl12anc 847	. . . . . . . 8 ⊢ (𝜑 → (𝐼‘𝑈) ∈ 𝑆)
27		dia2dimlem7.v	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊))
28	27	simpld 498	. . . . . . . . . 10 ⊢ (𝜑 → 𝑉 ∈ 𝐴)
29	4, 6	atbase 39914	. . . . . . . . . 10 ⊢ (𝑉 ∈ 𝐴 → 𝑉 ∈ (Base‘𝐾))
30	28, 29	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝑉 ∈ (Base‘𝐾))
31	27	simprd 499	. . . . . . . . 9 ⊢ (𝜑 → 𝑉 ≤ 𝑊)
32	4, 5, 7, 11, 23, 24	dialss 41671	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑉 ∈ (Base‘𝐾) ∧ 𝑉 ≤ 𝑊)) → (𝐼‘𝑉) ∈ 𝑆)
33	1, 30, 31, 32	syl12anc 847	. . . . . . . 8 ⊢ (𝜑 → (𝐼‘𝑉) ∈ 𝑆)
34		dia2dimlem7.pl	. . . . . . . . 9 ⊢ ⊕ = (LSSum‘𝑌)
35	24, 34	lsmcl 21151	. . . . . . . 8 ⊢ ((𝑌 ∈ LMod ∧ (𝐼‘𝑈) ∈ 𝑆 ∧ (𝐼‘𝑉) ∈ 𝑆) → ((𝐼‘𝑈) ⊕ (𝐼‘𝑉)) ∈ 𝑆)
36	17, 26, 33, 35	syl3anc 1391	. . . . . . 7 ⊢ (𝜑 → ((𝐼‘𝑈) ⊕ (𝐼‘𝑉)) ∈ 𝑆)
37	12, 24	lss0cl 21015	. . . . . . 7 ⊢ ((𝑌 ∈ LMod ∧ ((𝐼‘𝑈) ⊕ (𝐼‘𝑉)) ∈ 𝑆) → (0_g‘𝑌) ∈ ((𝐼‘𝑈) ⊕ (𝐼‘𝑉)))
38	17, 36, 37	syl2anc 593	. . . . . 6 ⊢ (𝜑 → (0_g‘𝑌) ∈ ((𝐼‘𝑈) ⊕ (𝐼‘𝑉)))
39	14, 38	eqeltrrd 2864	. . . . 5 ⊢ (𝜑 → ( I ↾ (Base‘𝐾)) ∈ ((𝐼‘𝑈) ⊕ (𝐼‘𝑉)))
40		eleq1a 2858	. . . . 5 ⊢ (( I ↾ (Base‘𝐾)) ∈ ((𝐼‘𝑈) ⊕ (𝐼‘𝑉)) → (𝐹 = ( I ↾ (Base‘𝐾)) → 𝐹 ∈ ((𝐼‘𝑈) ⊕ (𝐼‘𝑉))))
41	39, 40	syl 17	. . . 4 ⊢ (𝜑 → (𝐹 = ( I ↾ (Base‘𝐾)) → 𝐹 ∈ ((𝐼‘𝑈) ⊕ (𝐼‘𝑉))))
42	10, 41	sylbird 262	. . 3 ⊢ (𝜑 → ((𝐹‘𝑃) = 𝑃 → 𝐹 ∈ ((𝐼‘𝑈) ⊕ (𝐼‘𝑉))))
43	42	imp 410	. 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 484	. . 3 ⊢ ((𝜑 ∧ (𝐹‘𝑃) ≠ 𝑃) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
50	18	adantr 484	. . 3 ⊢ ((𝜑 ∧ (𝐹‘𝑃) ≠ 𝑃) → (𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊))
51	27	adantr 484	. . 3 ⊢ ((𝜑 ∧ (𝐹‘𝑃) ≠ 𝑃) → (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊))
52	3	adantr 484	. . 3 ⊢ ((𝜑 ∧ (𝐹‘𝑃) ≠ 𝑃) → (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊))
53	2	anim1i 624	. . 3 ⊢ ((𝜑 ∧ (𝐹‘𝑃) ≠ 𝑃) → (𝐹 ∈ 𝑇 ∧ (𝐹‘𝑃) ≠ 𝑃))
54		dia2dimlem7.rf	. . . 4 ⊢ (𝜑 → (𝑅‘𝐹) ≤ (𝑈 ∨ 𝑉))
55	54	adantr 484	. . 3 ⊢ ((𝜑 ∧ (𝐹‘𝑃) ≠ 𝑃) → (𝑅‘𝐹) ≤ (𝑈 ∨ 𝑉))
56		dia2dimlem7.uv	. . . 4 ⊢ (𝜑 → 𝑈 ≠ 𝑉)
57	56	adantr 484	. . 3 ⊢ ((𝜑 ∧ (𝐹‘𝑃) ≠ 𝑃) → 𝑈 ≠ 𝑉)
58		dia2dimlem7.ru	. . . 4 ⊢ (𝜑 → (𝑅‘𝐹) ≠ 𝑈)
59	58	adantr 484	. . 3 ⊢ ((𝜑 ∧ (𝐹‘𝑃) ≠ 𝑃) → (𝑅‘𝐹) ≠ 𝑈)
60		dia2dimlem7.rv	. . . 4 ⊢ (𝜑 → (𝑅‘𝐹) ≠ 𝑉)
61	60	adantr 484	. . 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 41694	. 2 ⊢ ((𝜑 ∧ (𝐹‘𝑃) ≠ 𝑃) → 𝐹 ∈ ((𝐼‘𝑈) ⊕ (𝐼‘𝑉)))
63	43, 62	pm2.61dane 3045	1 ⊢ (𝜑 → 𝐹 ∈ ((𝐼‘𝑈) ⊕ (𝐼‘𝑉)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 208 ∧ wa 399 = wceq 1561 ∈ wcel 2143 ≠ wne 2958 class class class wbr 5101 I cid 5542 ↾ cres 5650 ‘cfv 6522 (class class class)co 7397 Basecbs 17246 lecple 17294 0_gc0g 17469 joincjn 18344 meetcmee 18345 LSSumclsm 19675 LModclmod 20928 LSubSpclss 20999 LSpanclspn 21039 LVecclvec 21170 Atomscatm 39888 HLchlt 39975 LHypclh 40609 LTrncltrn 40726 trLctrl 40783 DVecAcdveca 41627 DIsoAcdia 41653

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1816 ax-4 1830 ax-5 1931 ax-6 1988 ax-7 2029 ax-8 2145 ax-9 2153 ax-10 2176 ax-11 2192 ax-12 2213 ax-ext 2735 ax-rep 5228 ax-sep 5247 ax-nul 5257 ax-pow 5323 ax-pr 5391 ax-un 7719 ax-cnex 11130 ax-resscn 11131 ax-1cn 11132 ax-icn 11133 ax-addcl 11134 ax-addrcl 11135 ax-mulcl 11136 ax-mulrcl 11137 ax-mulcom 11138 ax-addass 11139 ax-mulass 11140 ax-distr 11141 ax-i2m1 11142 ax-1ne0 11143 ax-1rid 11144 ax-rnegex 11145 ax-rrecex 11146 ax-cnre 11147 ax-pre-lttri 11148 ax-pre-lttrn 11149 ax-pre-ltadd 11150 ax-pre-mulgt0 11151 ax-riotaBAD 39578

This theorem depends on definitions: df-bi 209 df-an 400 df-or 859 df-3or 1100 df-3an 1101 df-tru 1564 df-fal 1574 df-ex 1801 df-nf 1805 df-sb 2092 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2838 df-nfc 2912 df-ne 2959 df-nel 3063 df-ral 3078 df-rex 3088 df-rmo 3368 df-reu 3369 df-rab 3416 df-v 3457 df-sbc 3746 df-csb 3854 df-dif 3908 df-un 3910 df-in 3912 df-ss 3922 df-pss 3925 df-nul 4287 df-if 4482 df-pw 4558 df-sn 4584 df-pr 4586 df-tp 4588 df-op 4590 df-uni 4867 df-int 4907 df-iun 4952 df-iin 4953 df-br 5102 df-opab 5164 df-mpt 5183 df-tr 5209 df-id 5543 df-eprel 5548 df-po 5556 df-so 5557 df-fr 5601 df-we 5603 df-xp 5654 df-rel 5655 df-cnv 5656 df-co 5657 df-dm 5658 df-rn 5659 df-res 5660 df-ima 5661 df-pred 6289 df-ord 6350 df-on 6351 df-lim 6352 df-suc 6353 df-iota 6478 df-fun 6524 df-fn 6525 df-f 6526 df-f1 6527 df-fo 6528 df-f1o 6529 df-fv 6530 df-riota 7354 df-ov 7400 df-oprab 7401 df-mpo 7402 df-om 7848 df-1st 7971 df-2nd 7972 df-tpos 8207 df-undef 8254 df-frecs 8263 df-wrecs 8294 df-recs 8343 df-rdg 8382 df-1o 8438 df-er 8679 df-map 8811 df-en 8929 df-dom 8930 df-sdom 8931 df-fin 8932 df-pnf 11219 df-mnf 11220 df-xr 11221 df-ltxr 11222 df-le 11223 df-sub 11417 df-neg 11418 df-nn 12212 df-2 12281 df-3 12282 df-4 12283 df-5 12284 df-6 12285 df-n0 12483 df-z 12570 df-uz 12841 df-fz 13514 df-struct 17184 df-sets 17201 df-slot 17219 df-ndx 17231 df-base 17247 df-ress 17268 df-plusg 17300 df-mulr 17301 df-sca 17303 df-vsca 17304 df-0g 17471 df-proset 18327 df-poset 18346 df-plt 18361 df-lub 18377 df-glb 18378 df-join 18379 df-meet 18380 df-p0 18456 df-p1 18457 df-lat 18465 df-clat 18532 df-mgm 18675 df-sgrp 18754 df-mnd 18770 df-submnd 18819 df-grp 18979 df-minusg 18980 df-sbg 18981 df-subg 19166 df-cntz 19358 df-lsm 19677 df-cmn 19823 df-abl 19824 df-mgp 20188 df-rng 20200 df-ur 20233 df-ring 20286 df-oppr 20387 df-dvdsr 20407 df-unit 20408 df-invr 20438 df-dvr 20451 df-drng 20782 df-lmod 20930 df-lss 21000 df-lsp 21040 df-lvec 21171 df-oposet 39801 df-ol 39803 df-oml 39804 df-covers 39891 df-ats 39892 df-atl 39923 df-cvlat 39947 df-hlat 39976 df-llines 40123 df-lplanes 40124 df-lvols 40125 df-lines 40126 df-psubsp 40128 df-pmap 40129 df-padd 40421 df-lhyp 40613 df-laut 40614 df-ldil 40729 df-ltrn 40730 df-trl 40784 df-tgrp 41368 df-tendo 41380 df-edring 41382 df-dveca 41628 df-disoa 41654

This theorem is referenced by: dia2dimlem8 41696

W3C validator