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 41049

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

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 395 ∧ w3a 1087 = wceq 1540 ∈ wcel 2108 ≠ wne 2939 ∃wrex 3069 class class class wbr 5141 ‘cfv 6559 (class class class)co 7429 lecple 17300 joincjn 18353 meetcmee 18354 LSSumclsm 19648 LSubSpclss 20921 LSpanclspn 20961 Atomscatm 39242 HLchlt 39329 LHypclh 39964 LTrncltrn 40081 trLctrl 40138 DVecAcdveca 40982 DIsoAcdia 41008

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2157 ax-12 2177 ax-ext 2707 ax-rep 5277 ax-sep 5294 ax-nul 5304 ax-pow 5363 ax-pr 5430 ax-un 7751 ax-cnex 11207 ax-resscn 11208 ax-1cn 11209 ax-icn 11210 ax-addcl 11211 ax-addrcl 11212 ax-mulcl 11213 ax-mulrcl 11214 ax-mulcom 11215 ax-addass 11216 ax-mulass 11217 ax-distr 11218 ax-i2m1 11219 ax-1ne0 11220 ax-1rid 11221 ax-rnegex 11222 ax-rrecex 11223 ax-cnre 11224 ax-pre-lttri 11225 ax-pre-lttrn 11226 ax-pre-ltadd 11227 ax-pre-mulgt0 11228 ax-riotaBAD 38932

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2065 df-mo 2539 df-eu 2568 df-clab 2714 df-cleq 2728 df-clel 2815 df-nfc 2891 df-ne 2940 df-nel 3046 df-ral 3061 df-rex 3070 df-rmo 3379 df-reu 3380 df-rab 3436 df-v 3481 df-sbc 3788 df-csb 3899 df-dif 3953 df-un 3955 df-in 3957 df-ss 3967 df-pss 3970 df-nul 4333 df-if 4525 df-pw 4600 df-sn 4625 df-pr 4627 df-tp 4629 df-op 4631 df-uni 4906 df-int 4945 df-iun 4991 df-iin 4992 df-br 5142 df-opab 5204 df-mpt 5224 df-tr 5258 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 6319 df-ord 6385 df-on 6386 df-lim 6387 df-suc 6388 df-iota 6512 df-fun 6561 df-fn 6562 df-f 6563 df-f1 6564 df-fo 6565 df-f1o 6566 df-fv 6567 df-riota 7386 df-ov 7432 df-oprab 7433 df-mpo 7434 df-om 7884 df-1st 8010 df-2nd 8011 df-tpos 8247 df-undef 8294 df-frecs 8302 df-wrecs 8333 df-recs 8407 df-rdg 8446 df-1o 8502 df-er 8741 df-map 8864 df-en 8982 df-dom 8983 df-sdom 8984 df-fin 8985 df-pnf 11293 df-mnf 11294 df-xr 11295 df-ltxr 11296 df-le 11297 df-sub 11490 df-neg 11491 df-nn 12263 df-2 12325 df-3 12326 df-4 12327 df-5 12328 df-6 12329 df-n0 12523 df-z 12610 df-uz 12875 df-fz 13544 df-struct 17180 df-sets 17197 df-slot 17215 df-ndx 17227 df-base 17244 df-ress 17271 df-plusg 17306 df-mulr 17307 df-sca 17309 df-vsca 17310 df-0g 17482 df-proset 18336 df-poset 18355 df-plt 18371 df-lub 18387 df-glb 18388 df-join 18389 df-meet 18390 df-p0 18466 df-p1 18467 df-lat 18473 df-clat 18540 df-mgm 18649 df-sgrp 18728 df-mnd 18744 df-grp 18950 df-minusg 18951 df-sbg 18952 df-subg 19137 df-lsm 19650 df-cmn 19796 df-abl 19797 df-mgp 20134 df-rng 20146 df-ur 20175 df-ring 20228 df-oppr 20326 df-dvdsr 20349 df-unit 20350 df-invr 20380 df-dvr 20393 df-drng 20723 df-lmod 20852 df-lss 20922 df-lsp 20962 df-lvec 21094 df-oposet 39155 df-ol 39157 df-oml 39158 df-covers 39245 df-ats 39246 df-atl 39277 df-cvlat 39301 df-hlat 39330 df-llines 39478 df-lplanes 39479 df-lvols 39480 df-lines 39481 df-psubsp 39483 df-pmap 39484 df-padd 39776 df-lhyp 39968 df-laut 39969 df-ldil 40084 df-ltrn 40085 df-trl 40139 df-tgrp 40723 df-tendo 40735 df-edring 40737 df-dveca 40983 df-disoa 41009

This theorem is referenced by: dia2dimlem7 41050

W3C validator