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 41046

Description: Lemma for dia2dim 41054. 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 41041	. . 3 ⊢ (𝜑 → (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊))
18	13	simpld 494	. . . 4 ⊢ (𝜑 → 𝐹 ∈ 𝑇)
19	2, 5, 6, 7	ltrnel 40116	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → ((𝐹‘𝑃) ∈ 𝐴 ∧ ¬ (𝐹‘𝑃) ≤ 𝑊))
20	1, 18, 12, 19	syl3anc 1372	. . 3 ⊢ (𝜑 → ((𝐹‘𝑃) ∈ 𝐴 ∧ ¬ (𝐹‘𝑃) ≤ 𝑊))
21	2, 5, 6, 7	cdleme50ex 40536	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ ((𝐹‘𝑃) ∈ 𝐴 ∧ ¬ (𝐹‘𝑃) ≤ 𝑊)) → ∃𝑑 ∈ 𝑇 (𝑑‘𝑄) = (𝐹‘𝑃))
22	1, 17, 20, 21	syl3anc 1372	. 2 ⊢ (𝜑 → ∃𝑑 ∈ 𝑇 (𝑑‘𝑄) = (𝐹‘𝑃))
23	2, 5, 6, 7	cdleme50ex 40536	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → ∃𝑔 ∈ 𝑇 (𝑔‘𝑃) = 𝑄)
24	1, 12, 17, 23	syl3anc 1372	. . . 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 1133	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑔 ∈ 𝑇 ∧ (𝑔‘𝑃) = 𝑄 ∧ 𝑑 ∈ 𝑇) ∧ (𝑑‘𝑄) = (𝐹‘𝑃)) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
31	10	3ad2ant1 1133	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑔 ∈ 𝑇 ∧ (𝑔‘𝑃) = 𝑄 ∧ 𝑑 ∈ 𝑇) ∧ (𝑑‘𝑄) = (𝐹‘𝑃)) → (𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊))
32	11	3ad2ant1 1133	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑔 ∈ 𝑇 ∧ (𝑔‘𝑃) = 𝑄 ∧ 𝑑 ∈ 𝑇) ∧ (𝑑‘𝑄) = (𝐹‘𝑃)) → (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊))
33	12	3ad2ant1 1133	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑔 ∈ 𝑇 ∧ (𝑔‘𝑃) = 𝑄 ∧ 𝑑 ∈ 𝑇) ∧ (𝑑‘𝑄) = (𝐹‘𝑃)) → (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊))
34	13	3ad2ant1 1133	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑔 ∈ 𝑇 ∧ (𝑔‘𝑃) = 𝑄 ∧ 𝑑 ∈ 𝑇) ∧ (𝑑‘𝑄) = (𝐹‘𝑃)) → (𝐹 ∈ 𝑇 ∧ (𝐹‘𝑃) ≠ 𝑃))
35	14	3ad2ant1 1133	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑔 ∈ 𝑇 ∧ (𝑔‘𝑃) = 𝑄 ∧ 𝑑 ∈ 𝑇) ∧ (𝑑‘𝑄) = (𝐹‘𝑃)) → (𝑅‘𝐹) ≤ (𝑈 ∨ 𝑉))
36	15	3ad2ant1 1133	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑔 ∈ 𝑇 ∧ (𝑔‘𝑃) = 𝑄 ∧ 𝑑 ∈ 𝑇) ∧ (𝑑‘𝑄) = (𝐹‘𝑃)) → 𝑈 ≠ 𝑉)
37	16	3ad2ant1 1133	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑔 ∈ 𝑇 ∧ (𝑔‘𝑃) = 𝑄 ∧ 𝑑 ∈ 𝑇) ∧ (𝑑‘𝑄) = (𝐹‘𝑃)) → (𝑅‘𝐹) ≠ 𝑈)
38		dia2dimlem6.rv	. . . . . . . . 9 ⊢ (𝜑 → (𝑅‘𝐹) ≠ 𝑉)
39	38	3ad2ant1 1133	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑔 ∈ 𝑇 ∧ (𝑔‘𝑃) = 𝑄 ∧ 𝑑 ∈ 𝑇) ∧ (𝑑‘𝑄) = (𝐹‘𝑃)) → (𝑅‘𝐹) ≠ 𝑉)
40		simp21 1206	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑔 ∈ 𝑇 ∧ (𝑔‘𝑃) = 𝑄 ∧ 𝑑 ∈ 𝑇) ∧ (𝑑‘𝑄) = (𝐹‘𝑃)) → 𝑔 ∈ 𝑇)
41		simp22 1207	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑔 ∈ 𝑇 ∧ (𝑔‘𝑃) = 𝑄 ∧ 𝑑 ∈ 𝑇) ∧ (𝑑‘𝑄) = (𝐹‘𝑃)) → (𝑔‘𝑃) = 𝑄)
42		simp23 1208	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑔 ∈ 𝑇 ∧ (𝑔‘𝑃) = 𝑄 ∧ 𝑑 ∈ 𝑇) ∧ (𝑑‘𝑄) = (𝐹‘𝑃)) → 𝑑 ∈ 𝑇)
43		simp3 1138	. . . . . . . 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 41045	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑔 ∈ 𝑇 ∧ (𝑔‘𝑃) = 𝑄 ∧ 𝑑 ∈ 𝑇) ∧ (𝑑‘𝑄) = (𝐹‘𝑃)) → 𝐹 ∈ ((𝐼‘𝑈) ⊕ (𝐼‘𝑉)))
45	44	3exp 1119	. . . . . 6 ⊢ (𝜑 → ((𝑔 ∈ 𝑇 ∧ (𝑔‘𝑃) = 𝑄 ∧ 𝑑 ∈ 𝑇) → ((𝑑‘𝑄) = (𝐹‘𝑃) → 𝐹 ∈ ((𝐼‘𝑈) ⊕ (𝐼‘𝑉)))))
46	45	3expd 1353	. . . . 5 ⊢ (𝜑 → (𝑔 ∈ 𝑇 → ((𝑔‘𝑃) = 𝑄 → (𝑑 ∈ 𝑇 → ((𝑑‘𝑄) = (𝐹‘𝑃) → 𝐹 ∈ ((𝐼‘𝑈) ⊕ (𝐼‘𝑉)))))))
47	46	rexlimdv 3140	. . . 4 ⊢ (𝜑 → (∃𝑔 ∈ 𝑇 (𝑔‘𝑃) = 𝑄 → (𝑑 ∈ 𝑇 → ((𝑑‘𝑄) = (𝐹‘𝑃) → 𝐹 ∈ ((𝐼‘𝑈) ⊕ (𝐼‘𝑉))))))
48	24, 47	mpd 15	. . 3 ⊢ (𝜑 → (𝑑 ∈ 𝑇 → ((𝑑‘𝑄) = (𝐹‘𝑃) → 𝐹 ∈ ((𝐼‘𝑈) ⊕ (𝐼‘𝑉)))))
49	48	rexlimdv 3140	. 2 ⊢ (𝜑 → (∃𝑑 ∈ 𝑇 (𝑑‘𝑄) = (𝐹‘𝑃) → 𝐹 ∈ ((𝐼‘𝑈) ⊕ (𝐼‘𝑉))))
50	22, 49	mpd 15	1 ⊢ (𝜑 → 𝐹 ∈ ((𝐼‘𝑈) ⊕ (𝐼‘𝑉)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 395 ∧ w3a 1086 = wceq 1539 ∈ wcel 2107 ≠ wne 2931 ∃wrex 3059 class class class wbr 5123 ‘cfv 6541 (class class class)co 7413 lecple 17281 joincjn 18328 meetcmee 18329 LSSumclsm 19621 LSubSpclss 20898 LSpanclspn 20938 Atomscatm 39239 HLchlt 39326 LHypclh 39961 LTrncltrn 40078 trLctrl 40135 DVecAcdveca 40979 DIsoAcdia 41005

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1909 ax-6 1966 ax-7 2006 ax-8 2109 ax-9 2117 ax-10 2140 ax-11 2156 ax-12 2176 ax-ext 2706 ax-rep 5259 ax-sep 5276 ax-nul 5286 ax-pow 5345 ax-pr 5412 ax-un 7737 ax-cnex 11193 ax-resscn 11194 ax-1cn 11195 ax-icn 11196 ax-addcl 11197 ax-addrcl 11198 ax-mulcl 11199 ax-mulrcl 11200 ax-mulcom 11201 ax-addass 11202 ax-mulass 11203 ax-distr 11204 ax-i2m1 11205 ax-1ne0 11206 ax-1rid 11207 ax-rnegex 11208 ax-rrecex 11209 ax-cnre 11210 ax-pre-lttri 11211 ax-pre-lttrn 11212 ax-pre-ltadd 11213 ax-pre-mulgt0 11214 ax-riotaBAD 38929

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1779 df-nf 1783 df-sb 2064 df-mo 2538 df-eu 2567 df-clab 2713 df-cleq 2726 df-clel 2808 df-nfc 2884 df-ne 2932 df-nel 3036 df-ral 3051 df-rex 3060 df-rmo 3363 df-reu 3364 df-rab 3420 df-v 3465 df-sbc 3771 df-csb 3880 df-dif 3934 df-un 3936 df-in 3938 df-ss 3948 df-pss 3951 df-nul 4314 df-if 4506 df-pw 4582 df-sn 4607 df-pr 4609 df-tp 4611 df-op 4613 df-uni 4888 df-int 4927 df-iun 4973 df-iin 4974 df-br 5124 df-opab 5186 df-mpt 5206 df-tr 5240 df-id 5558 df-eprel 5564 df-po 5572 df-so 5573 df-fr 5617 df-we 5619 df-xp 5671 df-rel 5672 df-cnv 5673 df-co 5674 df-dm 5675 df-rn 5676 df-res 5677 df-ima 5678 df-pred 6301 df-ord 6366 df-on 6367 df-lim 6368 df-suc 6369 df-iota 6494 df-fun 6543 df-fn 6544 df-f 6545 df-f1 6546 df-fo 6547 df-f1o 6548 df-fv 6549 df-riota 7370 df-ov 7416 df-oprab 7417 df-mpo 7418 df-om 7870 df-1st 7996 df-2nd 7997 df-tpos 8233 df-undef 8280 df-frecs 8288 df-wrecs 8319 df-recs 8393 df-rdg 8432 df-1o 8488 df-er 8727 df-map 8850 df-en 8968 df-dom 8969 df-sdom 8970 df-fin 8971 df-pnf 11279 df-mnf 11280 df-xr 11281 df-ltxr 11282 df-le 11283 df-sub 11476 df-neg 11477 df-nn 12249 df-2 12311 df-3 12312 df-4 12313 df-5 12314 df-6 12315 df-n0 12510 df-z 12597 df-uz 12861 df-fz 13530 df-struct 17167 df-sets 17184 df-slot 17202 df-ndx 17214 df-base 17231 df-ress 17254 df-plusg 17287 df-mulr 17288 df-sca 17290 df-vsca 17291 df-0g 17458 df-proset 18311 df-poset 18330 df-plt 18345 df-lub 18361 df-glb 18362 df-join 18363 df-meet 18364 df-p0 18440 df-p1 18441 df-lat 18447 df-clat 18514 df-mgm 18623 df-sgrp 18702 df-mnd 18718 df-grp 18924 df-minusg 18925 df-sbg 18926 df-subg 19111 df-lsm 19623 df-cmn 19769 df-abl 19770 df-mgp 20107 df-rng 20119 df-ur 20148 df-ring 20201 df-oppr 20303 df-dvdsr 20326 df-unit 20327 df-invr 20357 df-dvr 20370 df-drng 20700 df-lmod 20829 df-lss 20899 df-lsp 20939 df-lvec 21071 df-oposet 39152 df-ol 39154 df-oml 39155 df-covers 39242 df-ats 39243 df-atl 39274 df-cvlat 39298 df-hlat 39327 df-llines 39475 df-lplanes 39476 df-lvols 39477 df-lines 39478 df-psubsp 39480 df-pmap 39481 df-padd 39773 df-lhyp 39965 df-laut 39966 df-ldil 40081 df-ltrn 40082 df-trl 40136 df-tgrp 40720 df-tendo 40732 df-edring 40734 df-dveca 40980 df-disoa 41006

This theorem is referenced by: dia2dimlem7 41047

W3C validator