dia2dimlem6 - Mathbox for Norm Megill

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

Theorem dia2dimlem6 41013

Description: Lemma for dia2dim 41021. Eliminate auxiliary translations 𝐺 and 𝐷. (Contributed by NM, 8-Sep-2014.)

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

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

Proof of Theorem dia2dimlem6 Dummy variables 𝑔 𝑑 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		dia2dimlem6.k	. . 3 ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
2		dia2dimlem6.l	. . . 4 ⊢ ≤ = (le‘𝐾)
3		dia2dimlem6.j	. . . 4 ⊢ ∨ = (join‘𝐾)
4		dia2dimlem6.m	. . . 4 ⊢ ∧ = (meet‘𝐾)
5		dia2dimlem6.a	. . . 4 ⊢ 𝐴 = (Atoms‘𝐾)
6		dia2dimlem6.h	. . . 4 ⊢ 𝐻 = (LHyp‘𝐾)
7		dia2dimlem6.t	. . . 4 ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)
8		dia2dimlem6.r	. . . 4 ⊢ 𝑅 = ((trL‘𝐾)‘𝑊)
9		dia2dimlem6.q	. . . 4 ⊢ 𝑄 = ((𝑃 ∨ 𝑈) ∧ ((𝐹‘𝑃) ∨ 𝑉))
10		dia2dimlem6.u	. . . 4 ⊢ (𝜑 → (𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊))
11		dia2dimlem6.v	. . . 4 ⊢ (𝜑 → (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊))
12		dia2dimlem6.p	. . . 4 ⊢ (𝜑 → (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊))
13		dia2dimlem6.f	. . . 4 ⊢ (𝜑 → (𝐹 ∈ 𝑇 ∧ (𝐹‘𝑃) ≠ 𝑃))
14		dia2dimlem6.rf	. . . 4 ⊢ (𝜑 → (𝑅‘𝐹) ≤ (𝑈 ∨ 𝑉))
15		dia2dimlem6.uv	. . . 4 ⊢ (𝜑 → 𝑈 ≠ 𝑉)
16		dia2dimlem6.ru	. . . 4 ⊢ (𝜑 → (𝑅‘𝐹) ≠ 𝑈)
17	2, 3, 4, 5, 6, 7, 8, 9, 1, 10, 11, 12, 13, 14, 15, 16	dia2dimlem1 41008	. . 3 ⊢ (𝜑 → (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊))
18	13	simpld 494	. . . 4 ⊢ (𝜑 → 𝐹 ∈ 𝑇)
19	2, 5, 6, 7	ltrnel 40083	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → ((𝐹‘𝑃) ∈ 𝐴 ∧ ¬ (𝐹‘𝑃) ≤ 𝑊))
20	1, 18, 12, 19	syl3anc 1369	. . 3 ⊢ (𝜑 → ((𝐹‘𝑃) ∈ 𝐴 ∧ ¬ (𝐹‘𝑃) ≤ 𝑊))
21	2, 5, 6, 7	cdleme50ex 40503	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ ((𝐹‘𝑃) ∈ 𝐴 ∧ ¬ (𝐹‘𝑃) ≤ 𝑊)) → ∃𝑑 ∈ 𝑇 (𝑑‘𝑄) = (𝐹‘𝑃))
22	1, 17, 20, 21	syl3anc 1369	. 2 ⊢ (𝜑 → ∃𝑑 ∈ 𝑇 (𝑑‘𝑄) = (𝐹‘𝑃))
23	2, 5, 6, 7	cdleme50ex 40503	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → ∃𝑔 ∈ 𝑇 (𝑔‘𝑃) = 𝑄)
24	1, 12, 17, 23	syl3anc 1369	. . . 4 ⊢ (𝜑 → ∃𝑔 ∈ 𝑇 (𝑔‘𝑃) = 𝑄)
25		dia2dimlem6.y	. . . . . . . 8 ⊢ 𝑌 = ((DVecA‘𝐾)‘𝑊)
26		dia2dimlem6.s	. . . . . . . 8 ⊢ 𝑆 = (LSubSp‘𝑌)
27		dia2dimlem6.pl	. . . . . . . 8 ⊢ ⊕ = (LSSum‘𝑌)
28		dia2dimlem6.n	. . . . . . . 8 ⊢ 𝑁 = (LSpan‘𝑌)
29		dia2dimlem6.i	. . . . . . . 8 ⊢ 𝐼 = ((DIsoA‘𝐾)‘𝑊)
30	1	3ad2ant1 1131	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑔 ∈ 𝑇 ∧ (𝑔‘𝑃) = 𝑄 ∧ 𝑑 ∈ 𝑇) ∧ (𝑑‘𝑄) = (𝐹‘𝑃)) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
31	10	3ad2ant1 1131	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑔 ∈ 𝑇 ∧ (𝑔‘𝑃) = 𝑄 ∧ 𝑑 ∈ 𝑇) ∧ (𝑑‘𝑄) = (𝐹‘𝑃)) → (𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊))
32	11	3ad2ant1 1131	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑔 ∈ 𝑇 ∧ (𝑔‘𝑃) = 𝑄 ∧ 𝑑 ∈ 𝑇) ∧ (𝑑‘𝑄) = (𝐹‘𝑃)) → (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊))
33	12	3ad2ant1 1131	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑔 ∈ 𝑇 ∧ (𝑔‘𝑃) = 𝑄 ∧ 𝑑 ∈ 𝑇) ∧ (𝑑‘𝑄) = (𝐹‘𝑃)) → (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊))
34	13	3ad2ant1 1131	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑔 ∈ 𝑇 ∧ (𝑔‘𝑃) = 𝑄 ∧ 𝑑 ∈ 𝑇) ∧ (𝑑‘𝑄) = (𝐹‘𝑃)) → (𝐹 ∈ 𝑇 ∧ (𝐹‘𝑃) ≠ 𝑃))
35	14	3ad2ant1 1131	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑔 ∈ 𝑇 ∧ (𝑔‘𝑃) = 𝑄 ∧ 𝑑 ∈ 𝑇) ∧ (𝑑‘𝑄) = (𝐹‘𝑃)) → (𝑅‘𝐹) ≤ (𝑈 ∨ 𝑉))
36	15	3ad2ant1 1131	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑔 ∈ 𝑇 ∧ (𝑔‘𝑃) = 𝑄 ∧ 𝑑 ∈ 𝑇) ∧ (𝑑‘𝑄) = (𝐹‘𝑃)) → 𝑈 ≠ 𝑉)
37	16	3ad2ant1 1131	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑔 ∈ 𝑇 ∧ (𝑔‘𝑃) = 𝑄 ∧ 𝑑 ∈ 𝑇) ∧ (𝑑‘𝑄) = (𝐹‘𝑃)) → (𝑅‘𝐹) ≠ 𝑈)
38		dia2dimlem6.rv	. . . . . . . . 9 ⊢ (𝜑 → (𝑅‘𝐹) ≠ 𝑉)
39	38	3ad2ant1 1131	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑔 ∈ 𝑇 ∧ (𝑔‘𝑃) = 𝑄 ∧ 𝑑 ∈ 𝑇) ∧ (𝑑‘𝑄) = (𝐹‘𝑃)) → (𝑅‘𝐹) ≠ 𝑉)
40		simp21 1204	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑔 ∈ 𝑇 ∧ (𝑔‘𝑃) = 𝑄 ∧ 𝑑 ∈ 𝑇) ∧ (𝑑‘𝑄) = (𝐹‘𝑃)) → 𝑔 ∈ 𝑇)
41		simp22 1205	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑔 ∈ 𝑇 ∧ (𝑔‘𝑃) = 𝑄 ∧ 𝑑 ∈ 𝑇) ∧ (𝑑‘𝑄) = (𝐹‘𝑃)) → (𝑔‘𝑃) = 𝑄)
42		simp23 1206	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑔 ∈ 𝑇 ∧ (𝑔‘𝑃) = 𝑄 ∧ 𝑑 ∈ 𝑇) ∧ (𝑑‘𝑄) = (𝐹‘𝑃)) → 𝑑 ∈ 𝑇)
43		simp3 1136	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑔 ∈ 𝑇 ∧ (𝑔‘𝑃) = 𝑄 ∧ 𝑑 ∈ 𝑇) ∧ (𝑑‘𝑄) = (𝐹‘𝑃)) → (𝑑‘𝑄) = (𝐹‘𝑃))
44	2, 3, 4, 5, 6, 7, 8, 25, 26, 27, 28, 29, 9, 30, 31, 32, 33, 34, 35, 36, 37, 39, 40, 41, 42, 43	dia2dimlem5 41012	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑔 ∈ 𝑇 ∧ (𝑔‘𝑃) = 𝑄 ∧ 𝑑 ∈ 𝑇) ∧ (𝑑‘𝑄) = (𝐹‘𝑃)) → 𝐹 ∈ ((𝐼‘𝑈) ⊕ (𝐼‘𝑉)))
45	44	3exp 1117	. . . . . 6 ⊢ (𝜑 → ((𝑔 ∈ 𝑇 ∧ (𝑔‘𝑃) = 𝑄 ∧ 𝑑 ∈ 𝑇) → ((𝑑‘𝑄) = (𝐹‘𝑃) → 𝐹 ∈ ((𝐼‘𝑈) ⊕ (𝐼‘𝑉)))))
46	45	3expd 1351	. . . . 5 ⊢ (𝜑 → (𝑔 ∈ 𝑇 → ((𝑔‘𝑃) = 𝑄 → (𝑑 ∈ 𝑇 → ((𝑑‘𝑄) = (𝐹‘𝑃) → 𝐹 ∈ ((𝐼‘𝑈) ⊕ (𝐼‘𝑉)))))))
47	46	rexlimdv 3149	. . . 4 ⊢ (𝜑 → (∃𝑔 ∈ 𝑇 (𝑔‘𝑃) = 𝑄 → (𝑑 ∈ 𝑇 → ((𝑑‘𝑄) = (𝐹‘𝑃) → 𝐹 ∈ ((𝐼‘𝑈) ⊕ (𝐼‘𝑉))))))
48	24, 47	mpd 15	. . 3 ⊢ (𝜑 → (𝑑 ∈ 𝑇 → ((𝑑‘𝑄) = (𝐹‘𝑃) → 𝐹 ∈ ((𝐼‘𝑈) ⊕ (𝐼‘𝑉)))))
49	48	rexlimdv 3149	. 2 ⊢ (𝜑 → (∃𝑑 ∈ 𝑇 (𝑑‘𝑄) = (𝐹‘𝑃) → 𝐹 ∈ ((𝐼‘𝑈) ⊕ (𝐼‘𝑉))))
50	22, 49	mpd 15	1 ⊢ (𝜑 → 𝐹 ∈ ((𝐼‘𝑈) ⊕ (𝐼‘𝑉)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 395 ∧ w3a 1085 = wceq 1535 ∈ wcel 2104 ≠ wne 2936 ∃wrex 3066 class class class wbr 5149 ‘cfv 6558 (class class class)co 7425 lecple 17294 joincjn 18357 meetcmee 18358 LSSumclsm 19652 LSubSpclss 20928 LSpanclspn 20968 Atomscatm 39206 HLchlt 39293 LHypclh 39928 LTrncltrn 40045 trLctrl 40102 DVecAcdveca 40946 DIsoAcdia 40972

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1963 ax-7 2003 ax-8 2106 ax-9 2114 ax-10 2137 ax-11 2153 ax-12 2173 ax-ext 2704 ax-rep 5286 ax-sep 5300 ax-nul 5307 ax-pow 5366 ax-pr 5430 ax-un 7747 ax-cnex 11202 ax-resscn 11203 ax-1cn 11204 ax-icn 11205 ax-addcl 11206 ax-addrcl 11207 ax-mulcl 11208 ax-mulrcl 11209 ax-mulcom 11210 ax-addass 11211 ax-mulass 11212 ax-distr 11213 ax-i2m1 11214 ax-1ne0 11215 ax-1rid 11216 ax-rnegex 11217 ax-rrecex 11218 ax-cnre 11219 ax-pre-lttri 11220 ax-pre-lttrn 11221 ax-pre-ltadd 11222 ax-pre-mulgt0 11223 ax-riotaBAD 38896

This theorem depends on definitions: df-bi 207 df-an 396 df-or 847 df-3or 1086 df-3an 1087 df-tru 1538 df-fal 1548 df-ex 1775 df-nf 1779 df-sb 2061 df-mo 2536 df-eu 2565 df-clab 2711 df-cleq 2725 df-clel 2812 df-nfc 2888 df-ne 2937 df-nel 3043 df-ral 3058 df-rex 3067 df-rmo 3376 df-reu 3377 df-rab 3433 df-v 3479 df-sbc 3792 df-csb 3909 df-dif 3966 df-un 3968 df-in 3970 df-ss 3980 df-pss 3983 df-nul 4340 df-if 4531 df-pw 4606 df-sn 4631 df-pr 4633 df-tp 4635 df-op 4637 df-uni 4915 df-int 4954 df-iun 5000 df-iin 5001 df-br 5150 df-opab 5212 df-mpt 5233 df-tr 5267 df-id 5576 df-eprel 5582 df-po 5590 df-so 5591 df-fr 5635 df-we 5637 df-xp 5689 df-rel 5690 df-cnv 5691 df-co 5692 df-dm 5693 df-rn 5694 df-res 5695 df-ima 5696 df-pred 6317 df-ord 6383 df-on 6384 df-lim 6385 df-suc 6386 df-iota 6510 df-fun 6560 df-fn 6561 df-f 6562 df-f1 6563 df-fo 6564 df-f1o 6565 df-fv 6566 df-riota 7381 df-ov 7428 df-oprab 7429 df-mpo 7430 df-om 7881 df-1st 8007 df-2nd 8008 df-tpos 8244 df-undef 8291 df-frecs 8299 df-wrecs 8330 df-recs 8404 df-rdg 8443 df-1o 8499 df-er 8738 df-map 8861 df-en 8979 df-dom 8980 df-sdom 8981 df-fin 8982 df-pnf 11288 df-mnf 11289 df-xr 11290 df-ltxr 11291 df-le 11292 df-sub 11485 df-neg 11486 df-nn 12258 df-2 12320 df-3 12321 df-4 12322 df-5 12323 df-6 12324 df-n0 12518 df-z 12605 df-uz 12870 df-fz 13538 df-struct 17170 df-sets 17187 df-slot 17205 df-ndx 17217 df-base 17235 df-ress 17264 df-plusg 17300 df-mulr 17301 df-sca 17303 df-vsca 17304 df-0g 17477 df-proset 18341 df-poset 18359 df-plt 18376 df-lub 18392 df-glb 18393 df-join 18394 df-meet 18395 df-p0 18471 df-p1 18472 df-lat 18478 df-clat 18545 df-mgm 18654 df-sgrp 18733 df-mnd 18749 df-grp 18952 df-minusg 18953 df-sbg 18954 df-subg 19139 df-lsm 19654 df-cmn 19800 df-abl 19801 df-mgp 20138 df-rng 20156 df-ur 20185 df-ring 20238 df-oppr 20336 df-dvdsr 20359 df-unit 20360 df-invr 20390 df-dvr 20403 df-drng 20729 df-lmod 20858 df-lss 20929 df-lsp 20969 df-lvec 21101 df-oposet 39119 df-ol 39121 df-oml 39122 df-covers 39209 df-ats 39210 df-atl 39241 df-cvlat 39265 df-hlat 39294 df-llines 39442 df-lplanes 39443 df-lvols 39444 df-lines 39445 df-psubsp 39447 df-pmap 39448 df-padd 39740 df-lhyp 39932 df-laut 39933 df-ldil 40048 df-ltrn 40049 df-trl 40103 df-tgrp 40687 df-tendo 40699 df-edring 40701 df-dveca 40947 df-disoa 40973

This theorem is referenced by: dia2dimlem7 41014

W3C validator