dia2dimlem9 - Mathbox for Norm Megill

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

Theorem dia2dimlem9 41536

Description: Lemma for dia2dim 41541. Eliminate (𝑅‘𝐹) ≠ 𝑈, 𝑉 conditions. (Contributed by NM, 8-Sep-2014.)

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

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

**Proof of Theorem dia2dimlem9**
Step	Hyp	Ref	Expression
1		dia2dimlem9.k	. . . . . . 7 ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
2		dia2dimlem9.h	. . . . . . . 8 ⊢ 𝐻 = (LHyp‘𝐾)
3		dia2dimlem9.y	. . . . . . . 8 ⊢ 𝑌 = ((DVecA‘𝐾)‘𝑊)
4	2, 3	dvalvec 41490	. . . . . . 7 ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → 𝑌 ∈ LVec)
5		lveclmod 21097	. . . . . . 7 ⊢ (𝑌 ∈ LVec → 𝑌 ∈ LMod)
6		dia2dimlem9.s	. . . . . . . 8 ⊢ 𝑆 = (LSubSp‘𝑌)
7	6	lsssssubg 20948	. . . . . . 7 ⊢ (𝑌 ∈ LMod → 𝑆 ⊆ (SubGrp‘𝑌))
8	1, 4, 5, 7	4syl 19	. . . . . 6 ⊢ (𝜑 → 𝑆 ⊆ (SubGrp‘𝑌))
9		dia2dimlem9.u	. . . . . . . . 9 ⊢ (𝜑 → (𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊))
10	9	simpld 494	. . . . . . . 8 ⊢ (𝜑 → 𝑈 ∈ 𝐴)
11		eqid 2737	. . . . . . . . 9 ⊢ (Base‘𝐾) = (Base‘𝐾)
12		dia2dimlem9.a	. . . . . . . . 9 ⊢ 𝐴 = (Atoms‘𝐾)
13	11, 12	atbase 39753	. . . . . . . 8 ⊢ (𝑈 ∈ 𝐴 → 𝑈 ∈ (Base‘𝐾))
14	10, 13	syl 17	. . . . . . 7 ⊢ (𝜑 → 𝑈 ∈ (Base‘𝐾))
15	9	simprd 495	. . . . . . 7 ⊢ (𝜑 → 𝑈 ≤ 𝑊)
16		dia2dimlem9.l	. . . . . . . 8 ⊢ ≤ = (le‘𝐾)
17		dia2dimlem9.i	. . . . . . . 8 ⊢ 𝐼 = ((DIsoA‘𝐾)‘𝑊)
18	11, 16, 2, 3, 17, 6	dialss 41510	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑈 ∈ (Base‘𝐾) ∧ 𝑈 ≤ 𝑊)) → (𝐼‘𝑈) ∈ 𝑆)
19	1, 14, 15, 18	syl12anc 837	. . . . . 6 ⊢ (𝜑 → (𝐼‘𝑈) ∈ 𝑆)
20	8, 19	sseldd 3923	. . . . 5 ⊢ (𝜑 → (𝐼‘𝑈) ∈ (SubGrp‘𝑌))
21		dia2dimlem9.v	. . . . . . . . 9 ⊢ (𝜑 → (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊))
22	21	simpld 494	. . . . . . . 8 ⊢ (𝜑 → 𝑉 ∈ 𝐴)
23	11, 12	atbase 39753	. . . . . . . 8 ⊢ (𝑉 ∈ 𝐴 → 𝑉 ∈ (Base‘𝐾))
24	22, 23	syl 17	. . . . . . 7 ⊢ (𝜑 → 𝑉 ∈ (Base‘𝐾))
25	21	simprd 495	. . . . . . 7 ⊢ (𝜑 → 𝑉 ≤ 𝑊)
26	11, 16, 2, 3, 17, 6	dialss 41510	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑉 ∈ (Base‘𝐾) ∧ 𝑉 ≤ 𝑊)) → (𝐼‘𝑉) ∈ 𝑆)
27	1, 24, 25, 26	syl12anc 837	. . . . . 6 ⊢ (𝜑 → (𝐼‘𝑉) ∈ 𝑆)
28	8, 27	sseldd 3923	. . . . 5 ⊢ (𝜑 → (𝐼‘𝑉) ∈ (SubGrp‘𝑌))
29		dia2dimlem9.pl	. . . . . 6 ⊢ ⊕ = (LSSum‘𝑌)
30	29	lsmub1 19627	. . . . 5 ⊢ (((𝐼‘𝑈) ∈ (SubGrp‘𝑌) ∧ (𝐼‘𝑉) ∈ (SubGrp‘𝑌)) → (𝐼‘𝑈) ⊆ ((𝐼‘𝑈) ⊕ (𝐼‘𝑉)))
31	20, 28, 30	syl2anc 585	. . . 4 ⊢ (𝜑 → (𝐼‘𝑈) ⊆ ((𝐼‘𝑈) ⊕ (𝐼‘𝑉)))
32	31	adantr 480	. . 3 ⊢ ((𝜑 ∧ (𝑅‘𝐹) = 𝑈) → (𝐼‘𝑈) ⊆ ((𝐼‘𝑈) ⊕ (𝐼‘𝑉)))
33		dia2dimlem9.f	. . . . . 6 ⊢ (𝜑 → 𝐹 ∈ 𝑇)
34		dia2dimlem9.t	. . . . . . 7 ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)
35		dia2dimlem9.r	. . . . . . 7 ⊢ 𝑅 = ((trL‘𝐾)‘𝑊)
36	2, 34, 35, 17	dia1dimid 41527	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) → 𝐹 ∈ (𝐼‘(𝑅‘𝐹)))
37	1, 33, 36	syl2anc 585	. . . . 5 ⊢ (𝜑 → 𝐹 ∈ (𝐼‘(𝑅‘𝐹)))
38	37	adantr 480	. . . 4 ⊢ ((𝜑 ∧ (𝑅‘𝐹) = 𝑈) → 𝐹 ∈ (𝐼‘(𝑅‘𝐹)))
39		fveq2 6836	. . . . 5 ⊢ ((𝑅‘𝐹) = 𝑈 → (𝐼‘(𝑅‘𝐹)) = (𝐼‘𝑈))
40	39	adantl 481	. . . 4 ⊢ ((𝜑 ∧ (𝑅‘𝐹) = 𝑈) → (𝐼‘(𝑅‘𝐹)) = (𝐼‘𝑈))
41	38, 40	eleqtrd 2839	. . 3 ⊢ ((𝜑 ∧ (𝑅‘𝐹) = 𝑈) → 𝐹 ∈ (𝐼‘𝑈))
42	32, 41	sseldd 3923	. 2 ⊢ ((𝜑 ∧ (𝑅‘𝐹) = 𝑈) → 𝐹 ∈ ((𝐼‘𝑈) ⊕ (𝐼‘𝑉)))
43	20	adantr 480	. . . 4 ⊢ ((𝜑 ∧ (𝑅‘𝐹) = 𝑉) → (𝐼‘𝑈) ∈ (SubGrp‘𝑌))
44	28	adantr 480	. . . 4 ⊢ ((𝜑 ∧ (𝑅‘𝐹) = 𝑉) → (𝐼‘𝑉) ∈ (SubGrp‘𝑌))
45	29	lsmub2 19628	. . . 4 ⊢ (((𝐼‘𝑈) ∈ (SubGrp‘𝑌) ∧ (𝐼‘𝑉) ∈ (SubGrp‘𝑌)) → (𝐼‘𝑉) ⊆ ((𝐼‘𝑈) ⊕ (𝐼‘𝑉)))
46	43, 44, 45	syl2anc 585	. . 3 ⊢ ((𝜑 ∧ (𝑅‘𝐹) = 𝑉) → (𝐼‘𝑉) ⊆ ((𝐼‘𝑈) ⊕ (𝐼‘𝑉)))
47	37	adantr 480	. . . 4 ⊢ ((𝜑 ∧ (𝑅‘𝐹) = 𝑉) → 𝐹 ∈ (𝐼‘(𝑅‘𝐹)))
48		fveq2 6836	. . . . 5 ⊢ ((𝑅‘𝐹) = 𝑉 → (𝐼‘(𝑅‘𝐹)) = (𝐼‘𝑉))
49	48	adantl 481	. . . 4 ⊢ ((𝜑 ∧ (𝑅‘𝐹) = 𝑉) → (𝐼‘(𝑅‘𝐹)) = (𝐼‘𝑉))
50	47, 49	eleqtrd 2839	. . 3 ⊢ ((𝜑 ∧ (𝑅‘𝐹) = 𝑉) → 𝐹 ∈ (𝐼‘𝑉))
51	46, 50	sseldd 3923	. 2 ⊢ ((𝜑 ∧ (𝑅‘𝐹) = 𝑉) → 𝐹 ∈ ((𝐼‘𝑈) ⊕ (𝐼‘𝑉)))
52		dia2dimlem9.j	. . 3 ⊢ ∨ = (join‘𝐾)
53		dia2dimlem9.m	. . 3 ⊢ ∧ = (meet‘𝐾)
54		dia2dimlem9.n	. . 3 ⊢ 𝑁 = (LSpan‘𝑌)
55	1	adantr 480	. . 3 ⊢ ((𝜑 ∧ ((𝑅‘𝐹) ≠ 𝑈 ∧ (𝑅‘𝐹) ≠ 𝑉)) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
56	9	adantr 480	. . 3 ⊢ ((𝜑 ∧ ((𝑅‘𝐹) ≠ 𝑈 ∧ (𝑅‘𝐹) ≠ 𝑉)) → (𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊))
57	21	adantr 480	. . 3 ⊢ ((𝜑 ∧ ((𝑅‘𝐹) ≠ 𝑈 ∧ (𝑅‘𝐹) ≠ 𝑉)) → (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊))
58	33	adantr 480	. . 3 ⊢ ((𝜑 ∧ ((𝑅‘𝐹) ≠ 𝑈 ∧ (𝑅‘𝐹) ≠ 𝑉)) → 𝐹 ∈ 𝑇)
59		dia2dimlem9.rf	. . . 4 ⊢ (𝜑 → (𝑅‘𝐹) ≤ (𝑈 ∨ 𝑉))
60	59	adantr 480	. . 3 ⊢ ((𝜑 ∧ ((𝑅‘𝐹) ≠ 𝑈 ∧ (𝑅‘𝐹) ≠ 𝑉)) → (𝑅‘𝐹) ≤ (𝑈 ∨ 𝑉))
61		dia2dimlem9.uv	. . . 4 ⊢ (𝜑 → 𝑈 ≠ 𝑉)
62	61	adantr 480	. . 3 ⊢ ((𝜑 ∧ ((𝑅‘𝐹) ≠ 𝑈 ∧ (𝑅‘𝐹) ≠ 𝑉)) → 𝑈 ≠ 𝑉)
63		simprl 771	. . 3 ⊢ ((𝜑 ∧ ((𝑅‘𝐹) ≠ 𝑈 ∧ (𝑅‘𝐹) ≠ 𝑉)) → (𝑅‘𝐹) ≠ 𝑈)
64		simprr 773	. . 3 ⊢ ((𝜑 ∧ ((𝑅‘𝐹) ≠ 𝑈 ∧ (𝑅‘𝐹) ≠ 𝑉)) → (𝑅‘𝐹) ≠ 𝑉)
65	16, 52, 53, 12, 2, 34, 35, 3, 6, 29, 54, 17, 55, 56, 57, 58, 60, 62, 63, 64	dia2dimlem8 41535	. 2 ⊢ ((𝜑 ∧ ((𝑅‘𝐹) ≠ 𝑈 ∧ (𝑅‘𝐹) ≠ 𝑉)) → 𝐹 ∈ ((𝐼‘𝑈) ⊕ (𝐼‘𝑉)))
66	42, 51, 65	pm2.61da2ne 3021	1 ⊢ (𝜑 → 𝐹 ∈ ((𝐼‘𝑈) ⊕ (𝐼‘𝑉)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 395 = wceq 1542 ∈ wcel 2114 ≠ wne 2933 ⊆ wss 3890 class class class wbr 5086 ‘cfv 6494 (class class class)co 7362 Basecbs 17174 lecple 17222 joincjn 18272 meetcmee 18273 SubGrpcsubg 19091 LSSumclsm 19604 LModclmod 20850 LSubSpclss 20921 LSpanclspn 20961 LVecclvec 21093 Atomscatm 39727 HLchlt 39814 LHypclh 40448 LTrncltrn 40565 trLctrl 40622 DVecAcdveca 41466 DIsoAcdia 41492

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2709 ax-rep 5213 ax-sep 5232 ax-nul 5242 ax-pow 5304 ax-pr 5372 ax-un 7684 ax-cnex 11089 ax-resscn 11090 ax-1cn 11091 ax-icn 11092 ax-addcl 11093 ax-addrcl 11094 ax-mulcl 11095 ax-mulrcl 11096 ax-mulcom 11097 ax-addass 11098 ax-mulass 11099 ax-distr 11100 ax-i2m1 11101 ax-1ne0 11102 ax-1rid 11103 ax-rnegex 11104 ax-rrecex 11105 ax-cnre 11106 ax-pre-lttri 11107 ax-pre-lttrn 11108 ax-pre-ltadd 11109 ax-pre-mulgt0 11110 ax-riotaBAD 39417

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2540 df-eu 2570 df-clab 2716 df-cleq 2729 df-clel 2812 df-nfc 2886 df-ne 2934 df-nel 3038 df-ral 3053 df-rex 3063 df-rmo 3343 df-reu 3344 df-rab 3391 df-v 3432 df-sbc 3730 df-csb 3839 df-dif 3893 df-un 3895 df-in 3897 df-ss 3907 df-pss 3910 df-nul 4275 df-if 4468 df-pw 4544 df-sn 4569 df-pr 4571 df-tp 4573 df-op 4575 df-uni 4852 df-int 4891 df-iun 4936 df-iin 4937 df-br 5087 df-opab 5149 df-mpt 5168 df-tr 5194 df-id 5521 df-eprel 5526 df-po 5534 df-so 5535 df-fr 5579 df-we 5581 df-xp 5632 df-rel 5633 df-cnv 5634 df-co 5635 df-dm 5636 df-rn 5637 df-res 5638 df-ima 5639 df-pred 6261 df-ord 6322 df-on 6323 df-lim 6324 df-suc 6325 df-iota 6450 df-fun 6496 df-fn 6497 df-f 6498 df-f1 6499 df-fo 6500 df-f1o 6501 df-fv 6502 df-riota 7319 df-ov 7365 df-oprab 7366 df-mpo 7367 df-om 7813 df-1st 7937 df-2nd 7938 df-tpos 8171 df-undef 8218 df-frecs 8226 df-wrecs 8257 df-recs 8306 df-rdg 8344 df-1o 8400 df-er 8638 df-map 8770 df-en 8889 df-dom 8890 df-sdom 8891 df-fin 8892 df-pnf 11176 df-mnf 11177 df-xr 11178 df-ltxr 11179 df-le 11180 df-sub 11374 df-neg 11375 df-nn 12170 df-2 12239 df-3 12240 df-4 12241 df-5 12242 df-6 12243 df-n0 12433 df-z 12520 df-uz 12784 df-fz 13457 df-struct 17112 df-sets 17129 df-slot 17147 df-ndx 17159 df-base 17175 df-ress 17196 df-plusg 17228 df-mulr 17229 df-sca 17231 df-vsca 17232 df-0g 17399 df-proset 18255 df-poset 18274 df-plt 18289 df-lub 18305 df-glb 18306 df-join 18307 df-meet 18308 df-p0 18384 df-p1 18385 df-lat 18393 df-clat 18460 df-mgm 18603 df-sgrp 18682 df-mnd 18698 df-submnd 18747 df-grp 18907 df-minusg 18908 df-sbg 18909 df-subg 19094 df-cntz 19287 df-lsm 19606 df-cmn 19752 df-abl 19753 df-mgp 20117 df-rng 20129 df-ur 20158 df-ring 20211 df-oppr 20312 df-dvdsr 20332 df-unit 20333 df-invr 20363 df-dvr 20376 df-drng 20703 df-lmod 20852 df-lss 20922 df-lsp 20962 df-lvec 21094 df-oposet 39640 df-ol 39642 df-oml 39643 df-covers 39730 df-ats 39731 df-atl 39762 df-cvlat 39786 df-hlat 39815 df-llines 39962 df-lplanes 39963 df-lvols 39964 df-lines 39965 df-psubsp 39967 df-pmap 39968 df-padd 40260 df-lhyp 40452 df-laut 40453 df-ldil 40568 df-ltrn 40569 df-trl 40623 df-tgrp 41207 df-tendo 41219 df-edring 41221 df-dveca 41467 df-disoa 41493

This theorem is referenced by: dia2dimlem11 41538

W3C validator