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 41058

Description: Lemma for dia2dim 41066. 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 41053	. . 3 ⊢ (𝜑 → (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊))
18	13	simpld 494	. . . 4 ⊢ (𝜑 → 𝐹 ∈ 𝑇)
19	2, 5, 6, 7	ltrnel 40128	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → ((𝐹‘𝑃) ∈ 𝐴 ∧ ¬ (𝐹‘𝑃) ≤ 𝑊))
20	1, 18, 12, 19	syl3anc 1373	. . 3 ⊢ (𝜑 → ((𝐹‘𝑃) ∈ 𝐴 ∧ ¬ (𝐹‘𝑃) ≤ 𝑊))
21	2, 5, 6, 7	cdleme50ex 40548	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ ((𝐹‘𝑃) ∈ 𝐴 ∧ ¬ (𝐹‘𝑃) ≤ 𝑊)) → ∃𝑑 ∈ 𝑇 (𝑑‘𝑄) = (𝐹‘𝑃))
22	1, 17, 20, 21	syl3anc 1373	. 2 ⊢ (𝜑 → ∃𝑑 ∈ 𝑇 (𝑑‘𝑄) = (𝐹‘𝑃))
23	2, 5, 6, 7	cdleme50ex 40548	. . . . 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 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 1207	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑔 ∈ 𝑇 ∧ (𝑔‘𝑃) = 𝑄 ∧ 𝑑 ∈ 𝑇) ∧ (𝑑‘𝑄) = (𝐹‘𝑃)) → 𝑔 ∈ 𝑇)
41		simp22 1208	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑔 ∈ 𝑇 ∧ (𝑔‘𝑃) = 𝑄 ∧ 𝑑 ∈ 𝑇) ∧ (𝑑‘𝑄) = (𝐹‘𝑃)) → (𝑔‘𝑃) = 𝑄)
42		simp23 1209	. . . . . . . 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 41057	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑔 ∈ 𝑇 ∧ (𝑔‘𝑃) = 𝑄 ∧ 𝑑 ∈ 𝑇) ∧ (𝑑‘𝑄) = (𝐹‘𝑃)) → 𝐹 ∈ ((𝐼‘𝑈) ⊕ (𝐼‘𝑉)))
45	44	3exp 1119	. . . . . 6 ⊢ (𝜑 → ((𝑔 ∈ 𝑇 ∧ (𝑔‘𝑃) = 𝑄 ∧ 𝑑 ∈ 𝑇) → ((𝑑‘𝑄) = (𝐹‘𝑃) → 𝐹 ∈ ((𝐼‘𝑈) ⊕ (𝐼‘𝑉)))))
46	45	3expd 1354	. . . . 5 ⊢ (𝜑 → (𝑔 ∈ 𝑇 → ((𝑔‘𝑃) = 𝑄 → (𝑑 ∈ 𝑇 → ((𝑑‘𝑄) = (𝐹‘𝑃) → 𝐹 ∈ ((𝐼‘𝑈) ⊕ (𝐼‘𝑉)))))))
47	46	rexlimdv 3133	. . . 4 ⊢ (𝜑 → (∃𝑔 ∈ 𝑇 (𝑔‘𝑃) = 𝑄 → (𝑑 ∈ 𝑇 → ((𝑑‘𝑄) = (𝐹‘𝑃) → 𝐹 ∈ ((𝐼‘𝑈) ⊕ (𝐼‘𝑉))))))
48	24, 47	mpd 15	. . 3 ⊢ (𝜑 → (𝑑 ∈ 𝑇 → ((𝑑‘𝑄) = (𝐹‘𝑃) → 𝐹 ∈ ((𝐼‘𝑈) ⊕ (𝐼‘𝑉)))))
49	48	rexlimdv 3133	. 2 ⊢ (𝜑 → (∃𝑑 ∈ 𝑇 (𝑑‘𝑄) = (𝐹‘𝑃) → 𝐹 ∈ ((𝐼‘𝑈) ⊕ (𝐼‘𝑉))))
50	22, 49	mpd 15	1 ⊢ (𝜑 → 𝐹 ∈ ((𝐼‘𝑈) ⊕ (𝐼‘𝑉)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 395 ∧ w3a 1086 = wceq 1540 ∈ wcel 2109 ≠ wne 2926 ∃wrex 3054 class class class wbr 5109 ‘cfv 6513 (class class class)co 7389 lecple 17233 joincjn 18278 meetcmee 18279 LSSumclsm 19570 LSubSpclss 20843 LSpanclspn 20883 Atomscatm 39251 HLchlt 39338 LHypclh 39973 LTrncltrn 40090 trLctrl 40147 DVecAcdveca 40991 DIsoAcdia 41017

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 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2702 ax-rep 5236 ax-sep 5253 ax-nul 5263 ax-pow 5322 ax-pr 5389 ax-un 7713 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 38941

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2534 df-eu 2563 df-clab 2709 df-cleq 2722 df-clel 2804 df-nfc 2879 df-ne 2927 df-nel 3031 df-ral 3046 df-rex 3055 df-rmo 3356 df-reu 3357 df-rab 3409 df-v 3452 df-sbc 3756 df-csb 3865 df-dif 3919 df-un 3921 df-in 3923 df-ss 3933 df-pss 3936 df-nul 4299 df-if 4491 df-pw 4567 df-sn 4592 df-pr 4594 df-tp 4596 df-op 4598 df-uni 4874 df-int 4913 df-iun 4959 df-iin 4960 df-br 5110 df-opab 5172 df-mpt 5191 df-tr 5217 df-id 5535 df-eprel 5540 df-po 5548 df-so 5549 df-fr 5593 df-we 5595 df-xp 5646 df-rel 5647 df-cnv 5648 df-co 5649 df-dm 5650 df-rn 5651 df-res 5652 df-ima 5653 df-pred 6276 df-ord 6337 df-on 6338 df-lim 6339 df-suc 6340 df-iota 6466 df-fun 6515 df-fn 6516 df-f 6517 df-f1 6518 df-fo 6519 df-f1o 6520 df-fv 6521 df-riota 7346 df-ov 7392 df-oprab 7393 df-mpo 7394 df-om 7845 df-1st 7970 df-2nd 7971 df-tpos 8207 df-undef 8254 df-frecs 8262 df-wrecs 8293 df-recs 8342 df-rdg 8380 df-1o 8436 df-er 8673 df-map 8803 df-en 8921 df-dom 8922 df-sdom 8923 df-fin 8924 df-pnf 11216 df-mnf 11217 df-xr 11218 df-ltxr 11219 df-le 11220 df-sub 11413 df-neg 11414 df-nn 12188 df-2 12250 df-3 12251 df-4 12252 df-5 12253 df-6 12254 df-n0 12449 df-z 12536 df-uz 12800 df-fz 13475 df-struct 17123 df-sets 17140 df-slot 17158 df-ndx 17170 df-base 17186 df-ress 17207 df-plusg 17239 df-mulr 17240 df-sca 17242 df-vsca 17243 df-0g 17410 df-proset 18261 df-poset 18280 df-plt 18295 df-lub 18311 df-glb 18312 df-join 18313 df-meet 18314 df-p0 18390 df-p1 18391 df-lat 18397 df-clat 18464 df-mgm 18573 df-sgrp 18652 df-mnd 18668 df-grp 18874 df-minusg 18875 df-sbg 18876 df-subg 19061 df-lsm 19572 df-cmn 19718 df-abl 19719 df-mgp 20056 df-rng 20068 df-ur 20097 df-ring 20150 df-oppr 20252 df-dvdsr 20272 df-unit 20273 df-invr 20303 df-dvr 20316 df-drng 20646 df-lmod 20774 df-lss 20844 df-lsp 20884 df-lvec 21016 df-oposet 39164 df-ol 39166 df-oml 39167 df-covers 39254 df-ats 39255 df-atl 39286 df-cvlat 39310 df-hlat 39339 df-llines 39487 df-lplanes 39488 df-lvols 39489 df-lines 39490 df-psubsp 39492 df-pmap 39493 df-padd 39785 df-lhyp 39977 df-laut 39978 df-ldil 40093 df-ltrn 40094 df-trl 40148 df-tgrp 40732 df-tendo 40744 df-edring 40746 df-dveca 40992 df-disoa 41018

This theorem is referenced by: dia2dimlem7 41059

W3C validator