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 41571

Description: Lemma for dia2dim 41578. 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 2739	. . . . . 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 40676	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝐹 = ( I ↾ (Base‘𝐾)) ↔ (𝐹‘𝑃) = 𝑃))
10	1, 2, 3, 9	syl3anc 1379	. . . 4 ⊢ (𝜑 → (𝐹 = ( I ↾ (Base‘𝐾)) ↔ (𝐹‘𝑃) = 𝑃))
11		dia2dimlem7.y	. . . . . . . 8 ⊢ 𝑌 = ((DVecA‘𝐾)‘𝑊)
12		eqid 2739	. . . . . . . 8 ⊢ (0_g‘𝑌) = (0_g‘𝑌)
13	4, 7, 8, 11, 12	dva0g 41528	. . . . . . 7 ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → (0_g‘𝑌) = ( I ↾ (Base‘𝐾)))
14	1, 13	syl 17	. . . . . 6 ⊢ (𝜑 → (0_g‘𝑌) = ( I ↾ (Base‘𝐾)))
15	7, 11	dvalvec 41527	. . . . . . . 8 ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → 𝑌 ∈ LVec)
16		lveclmod 21097	. . . . . . . 8 ⊢ (𝑌 ∈ LVec → 𝑌 ∈ LMod)
17	1, 15, 16	3syl 18	. . . . . . 7 ⊢ (𝜑 → 𝑌 ∈ LMod)
18		dia2dimlem7.u	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊))
19	18	simpld 495	. . . . . . . . . 10 ⊢ (𝜑 → 𝑈 ∈ 𝐴)
20	4, 6	atbase 39790	. . . . . . . . . 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 41547	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑈 ∈ (Base‘𝐾) ∧ 𝑈 ≤ 𝑊)) → (𝐼‘𝑈) ∈ 𝑆)
26	1, 21, 22, 25	syl12anc 842	. . . . . . . 8 ⊢ (𝜑 → (𝐼‘𝑈) ∈ 𝑆)
27		dia2dimlem7.v	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊))
28	27	simpld 495	. . . . . . . . . 10 ⊢ (𝜑 → 𝑉 ∈ 𝐴)
29	4, 6	atbase 39790	. . . . . . . . . 10 ⊢ (𝑉 ∈ 𝐴 → 𝑉 ∈ (Base‘𝐾))
30	28, 29	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝑉 ∈ (Base‘𝐾))
31	27	simprd 496	. . . . . . . . 9 ⊢ (𝜑 → 𝑉 ≤ 𝑊)
32	4, 5, 7, 11, 23, 24	dialss 41547	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑉 ∈ (Base‘𝐾) ∧ 𝑉 ≤ 𝑊)) → (𝐼‘𝑉) ∈ 𝑆)
33	1, 30, 31, 32	syl12anc 842	. . . . . . . 8 ⊢ (𝜑 → (𝐼‘𝑉) ∈ 𝑆)
34		dia2dimlem7.pl	. . . . . . . . 9 ⊢ ⊕ = (LSSum‘𝑌)
35	24, 34	lsmcl 21074	. . . . . . . 8 ⊢ ((𝑌 ∈ LMod ∧ (𝐼‘𝑈) ∈ 𝑆 ∧ (𝐼‘𝑉) ∈ 𝑆) → ((𝐼‘𝑈) ⊕ (𝐼‘𝑉)) ∈ 𝑆)
36	17, 26, 33, 35	syl3anc 1379	. . . . . . 7 ⊢ (𝜑 → ((𝐼‘𝑈) ⊕ (𝐼‘𝑉)) ∈ 𝑆)
37	12, 24	lss0cl 20938	. . . . . . 7 ⊢ ((𝑌 ∈ LMod ∧ ((𝐼‘𝑈) ⊕ (𝐼‘𝑉)) ∈ 𝑆) → (0_g‘𝑌) ∈ ((𝐼‘𝑈) ⊕ (𝐼‘𝑉)))
38	17, 36, 37	syl2anc 590	. . . . . 6 ⊢ (𝜑 → (0_g‘𝑌) ∈ ((𝐼‘𝑈) ⊕ (𝐼‘𝑉)))
39	14, 38	eqeltrrd 2840	. . . . 5 ⊢ (𝜑 → ( I ↾ (Base‘𝐾)) ∈ ((𝐼‘𝑈) ⊕ (𝐼‘𝑉)))
40		eleq1a 2834	. . . . 5 ⊢ (( I ↾ (Base‘𝐾)) ∈ ((𝐼‘𝑈) ⊕ (𝐼‘𝑉)) → (𝐹 = ( I ↾ (Base‘𝐾)) → 𝐹 ∈ ((𝐼‘𝑈) ⊕ (𝐼‘𝑉))))
41	39, 40	syl 17	. . . 4 ⊢ (𝜑 → (𝐹 = ( I ↾ (Base‘𝐾)) → 𝐹 ∈ ((𝐼‘𝑈) ⊕ (𝐼‘𝑉))))
42	10, 41	sylbird 261	. . 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 621	. . 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 41570	. 2 ⊢ ((𝜑 ∧ (𝐹‘𝑃) ≠ 𝑃) → 𝐹 ∈ ((𝐼‘𝑈) ⊕ (𝐼‘𝑉)))
63	43, 62	pm2.61dane 3021	1 ⊢ (𝜑 → 𝐹 ∈ ((𝐼‘𝑈) ⊕ (𝐼‘𝑉)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 207 ∧ wa 396 = wceq 1547 ∈ wcel 2119 ≠ wne 2934 class class class wbr 5073 I cid 5513 ↾ cres 5621 ‘cfv 6486 (class class class)co 7357 Basecbs 17171 lecple 17219 0_gc0g 17394 joincjn 18269 meetcmee 18270 LSSumclsm 19601 LModclmod 20851 LSubSpclss 20922 LSpanclspn 20962 LVecclvec 21093 Atomscatm 39764 HLchlt 39851 LHypclh 40485 LTrncltrn 40602 trLctrl 40659 DVecAcdveca 41503 DIsoAcdia 41529

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1974 ax-7 2015 ax-8 2121 ax-9 2129 ax-10 2152 ax-11 2168 ax-12 2189 ax-ext 2711 ax-rep 5200 ax-sep 5219 ax-nul 5229 ax-pow 5295 ax-pr 5363 ax-un 7679 ax-cnex 11086 ax-resscn 11087 ax-1cn 11088 ax-icn 11089 ax-addcl 11090 ax-addrcl 11091 ax-mulcl 11092 ax-mulrcl 11093 ax-mulcom 11094 ax-addass 11095 ax-mulass 11096 ax-distr 11097 ax-i2m1 11098 ax-1ne0 11099 ax-1rid 11100 ax-rnegex 11101 ax-rrecex 11102 ax-cnre 11103 ax-pre-lttri 11104 ax-pre-lttrn 11105 ax-pre-ltadd 11106 ax-pre-mulgt0 11107 ax-riotaBAD 39454

This theorem depends on definitions: df-bi 208 df-an 397 df-or 854 df-3or 1093 df-3an 1094 df-tru 1550 df-fal 1560 df-ex 1787 df-nf 1791 df-sb 2074 df-mo 2543 df-eu 2573 df-clab 2718 df-cleq 2731 df-clel 2814 df-nfc 2888 df-ne 2935 df-nel 3039 df-ral 3054 df-rex 3064 df-rmo 3344 df-reu 3345 df-rab 3392 df-v 3433 df-sbc 3724 df-csb 3832 df-dif 3886 df-un 3888 df-in 3890 df-ss 3900 df-pss 3903 df-nul 4263 df-if 4456 df-pw 4532 df-sn 4557 df-pr 4559 df-tp 4561 df-op 4563 df-uni 4840 df-int 4879 df-iun 4924 df-iin 4925 df-br 5074 df-opab 5136 df-mpt 5155 df-tr 5181 df-id 5514 df-eprel 5519 df-po 5527 df-so 5528 df-fr 5572 df-we 5574 df-xp 5625 df-rel 5626 df-cnv 5627 df-co 5628 df-dm 5629 df-rn 5630 df-res 5631 df-ima 5632 df-pred 6253 df-ord 6314 df-on 6315 df-lim 6316 df-suc 6317 df-iota 6442 df-fun 6488 df-fn 6489 df-f 6490 df-f1 6491 df-fo 6492 df-f1o 6493 df-fv 6494 df-riota 7314 df-ov 7360 df-oprab 7361 df-mpo 7362 df-om 7808 df-1st 7932 df-2nd 7933 df-tpos 8167 df-undef 8214 df-frecs 8222 df-wrecs 8253 df-recs 8302 df-rdg 8340 df-1o 8396 df-er 8634 df-map 8766 df-en 8885 df-dom 8886 df-sdom 8887 df-fin 8888 df-pnf 11173 df-mnf 11174 df-xr 11175 df-ltxr 11176 df-le 11177 df-sub 11371 df-neg 11372 df-nn 12167 df-2 12236 df-3 12237 df-4 12238 df-5 12239 df-6 12240 df-n0 12430 df-z 12517 df-uz 12781 df-fz 13454 df-struct 17109 df-sets 17126 df-slot 17144 df-ndx 17156 df-base 17172 df-ress 17193 df-plusg 17225 df-mulr 17226 df-sca 17228 df-vsca 17229 df-0g 17396 df-proset 18252 df-poset 18271 df-plt 18286 df-lub 18302 df-glb 18303 df-join 18304 df-meet 18305 df-p0 18381 df-p1 18382 df-lat 18390 df-clat 18457 df-mgm 18600 df-sgrp 18679 df-mnd 18695 df-submnd 18744 df-grp 18904 df-minusg 18905 df-sbg 18906 df-subg 19091 df-cntz 19284 df-lsm 19603 df-cmn 19749 df-abl 19750 df-mgp 20114 df-rng 20126 df-ur 20155 df-ring 20208 df-oppr 20309 df-dvdsr 20329 df-unit 20330 df-invr 20360 df-dvr 20373 df-drng 20704 df-lmod 20853 df-lss 20923 df-lsp 20963 df-lvec 21094 df-oposet 39677 df-ol 39679 df-oml 39680 df-covers 39767 df-ats 39768 df-atl 39799 df-cvlat 39823 df-hlat 39852 df-llines 39999 df-lplanes 40000 df-lvols 40001 df-lines 40002 df-psubsp 40004 df-pmap 40005 df-padd 40297 df-lhyp 40489 df-laut 40490 df-ldil 40605 df-ltrn 40606 df-trl 40660 df-tgrp 41244 df-tendo 41256 df-edring 41258 df-dveca 41504 df-disoa 41530

This theorem is referenced by: dia2dimlem8 41572

W3C validator