Mathbox for Norm Megill |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > Mathboxes > dia2dimlem12 | Structured version Visualization version GIF version |
Description: Lemma for dia2dim 38711. Obtain subset relation. (Contributed by NM, 8-Sep-2014.) |
Ref | Expression |
---|---|
dia2dimlem12.l | ⊢ ≤ = (le‘𝐾) |
dia2dimlem12.j | ⊢ ∨ = (join‘𝐾) |
dia2dimlem12.m | ⊢ ∧ = (meet‘𝐾) |
dia2dimlem12.a | ⊢ 𝐴 = (Atoms‘𝐾) |
dia2dimlem12.h | ⊢ 𝐻 = (LHyp‘𝐾) |
dia2dimlem12.t | ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) |
dia2dimlem12.r | ⊢ 𝑅 = ((trL‘𝐾)‘𝑊) |
dia2dimlem12.y | ⊢ 𝑌 = ((DVecA‘𝐾)‘𝑊) |
dia2dimlem12.s | ⊢ 𝑆 = (LSubSp‘𝑌) |
dia2dimlem12.pl | ⊢ ⊕ = (LSSum‘𝑌) |
dia2dimlem12.n | ⊢ 𝑁 = (LSpan‘𝑌) |
dia2dimlem12.i | ⊢ 𝐼 = ((DIsoA‘𝐾)‘𝑊) |
dia2dimlem12.k | ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
dia2dimlem12.u | ⊢ (𝜑 → (𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊)) |
dia2dimlem12.v | ⊢ (𝜑 → (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)) |
dia2dimlem12.uv | ⊢ (𝜑 → 𝑈 ≠ 𝑉) |
Ref | Expression |
---|---|
dia2dimlem12 | ⊢ (𝜑 → (𝐼‘(𝑈 ∨ 𝑉)) ⊆ ((𝐼‘𝑈) ⊕ (𝐼‘𝑉))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dia2dimlem12.k | . . . . 5 ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) | |
2 | 1 | simpld 498 | . . . . . 6 ⊢ (𝜑 → 𝐾 ∈ HL) |
3 | dia2dimlem12.u | . . . . . . 7 ⊢ (𝜑 → (𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊)) | |
4 | 3 | simpld 498 | . . . . . 6 ⊢ (𝜑 → 𝑈 ∈ 𝐴) |
5 | dia2dimlem12.v | . . . . . . 7 ⊢ (𝜑 → (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)) | |
6 | 5 | simpld 498 | . . . . . 6 ⊢ (𝜑 → 𝑉 ∈ 𝐴) |
7 | eqid 2738 | . . . . . . 7 ⊢ (Base‘𝐾) = (Base‘𝐾) | |
8 | dia2dimlem12.j | . . . . . . 7 ⊢ ∨ = (join‘𝐾) | |
9 | dia2dimlem12.a | . . . . . . 7 ⊢ 𝐴 = (Atoms‘𝐾) | |
10 | 7, 8, 9 | hlatjcl 37001 | . . . . . 6 ⊢ ((𝐾 ∈ HL ∧ 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴) → (𝑈 ∨ 𝑉) ∈ (Base‘𝐾)) |
11 | 2, 4, 6, 10 | syl3anc 1372 | . . . . 5 ⊢ (𝜑 → (𝑈 ∨ 𝑉) ∈ (Base‘𝐾)) |
12 | 3 | simprd 499 | . . . . . 6 ⊢ (𝜑 → 𝑈 ≤ 𝑊) |
13 | 5 | simprd 499 | . . . . . 6 ⊢ (𝜑 → 𝑉 ≤ 𝑊) |
14 | 2 | hllatd 36998 | . . . . . . 7 ⊢ (𝜑 → 𝐾 ∈ Lat) |
15 | 7, 9 | atbase 36923 | . . . . . . . 8 ⊢ (𝑈 ∈ 𝐴 → 𝑈 ∈ (Base‘𝐾)) |
16 | 4, 15 | syl 17 | . . . . . . 7 ⊢ (𝜑 → 𝑈 ∈ (Base‘𝐾)) |
17 | 7, 9 | atbase 36923 | . . . . . . . 8 ⊢ (𝑉 ∈ 𝐴 → 𝑉 ∈ (Base‘𝐾)) |
18 | 6, 17 | syl 17 | . . . . . . 7 ⊢ (𝜑 → 𝑉 ∈ (Base‘𝐾)) |
19 | 1 | simprd 499 | . . . . . . . 8 ⊢ (𝜑 → 𝑊 ∈ 𝐻) |
20 | dia2dimlem12.h | . . . . . . . . 9 ⊢ 𝐻 = (LHyp‘𝐾) | |
21 | 7, 20 | lhpbase 37632 | . . . . . . . 8 ⊢ (𝑊 ∈ 𝐻 → 𝑊 ∈ (Base‘𝐾)) |
22 | 19, 21 | syl 17 | . . . . . . 7 ⊢ (𝜑 → 𝑊 ∈ (Base‘𝐾)) |
23 | dia2dimlem12.l | . . . . . . . 8 ⊢ ≤ = (le‘𝐾) | |
24 | 7, 23, 8 | latjle12 17789 | . . . . . . 7 ⊢ ((𝐾 ∈ Lat ∧ (𝑈 ∈ (Base‘𝐾) ∧ 𝑉 ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾))) → ((𝑈 ≤ 𝑊 ∧ 𝑉 ≤ 𝑊) ↔ (𝑈 ∨ 𝑉) ≤ 𝑊)) |
25 | 14, 16, 18, 22, 24 | syl13anc 1373 | . . . . . 6 ⊢ (𝜑 → ((𝑈 ≤ 𝑊 ∧ 𝑉 ≤ 𝑊) ↔ (𝑈 ∨ 𝑉) ≤ 𝑊)) |
26 | 12, 13, 25 | mpbi2and 712 | . . . . 5 ⊢ (𝜑 → (𝑈 ∨ 𝑉) ≤ 𝑊) |
27 | dia2dimlem12.t | . . . . . 6 ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) | |
28 | dia2dimlem12.i | . . . . . 6 ⊢ 𝐼 = ((DIsoA‘𝐾)‘𝑊) | |
29 | 7, 23, 20, 27, 28 | diass 38676 | . . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑈 ∨ 𝑉) ∈ (Base‘𝐾) ∧ (𝑈 ∨ 𝑉) ≤ 𝑊)) → (𝐼‘(𝑈 ∨ 𝑉)) ⊆ 𝑇) |
30 | 1, 11, 26, 29 | syl12anc 836 | . . . 4 ⊢ (𝜑 → (𝐼‘(𝑈 ∨ 𝑉)) ⊆ 𝑇) |
31 | 30 | sseld 3877 | . . 3 ⊢ (𝜑 → (𝑓 ∈ (𝐼‘(𝑈 ∨ 𝑉)) → 𝑓 ∈ 𝑇)) |
32 | dia2dimlem12.m | . . . . 5 ⊢ ∧ = (meet‘𝐾) | |
33 | dia2dimlem12.r | . . . . 5 ⊢ 𝑅 = ((trL‘𝐾)‘𝑊) | |
34 | dia2dimlem12.y | . . . . 5 ⊢ 𝑌 = ((DVecA‘𝐾)‘𝑊) | |
35 | dia2dimlem12.s | . . . . 5 ⊢ 𝑆 = (LSubSp‘𝑌) | |
36 | dia2dimlem12.pl | . . . . 5 ⊢ ⊕ = (LSSum‘𝑌) | |
37 | dia2dimlem12.n | . . . . 5 ⊢ 𝑁 = (LSpan‘𝑌) | |
38 | 1 | 3ad2ant1 1134 | . . . . 5 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝐼‘(𝑈 ∨ 𝑉)) ∧ 𝑓 ∈ 𝑇) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
39 | 3 | 3ad2ant1 1134 | . . . . 5 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝐼‘(𝑈 ∨ 𝑉)) ∧ 𝑓 ∈ 𝑇) → (𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊)) |
40 | 5 | 3ad2ant1 1134 | . . . . 5 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝐼‘(𝑈 ∨ 𝑉)) ∧ 𝑓 ∈ 𝑇) → (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)) |
41 | simp3 1139 | . . . . 5 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝐼‘(𝑈 ∨ 𝑉)) ∧ 𝑓 ∈ 𝑇) → 𝑓 ∈ 𝑇) | |
42 | dia2dimlem12.uv | . . . . . 6 ⊢ (𝜑 → 𝑈 ≠ 𝑉) | |
43 | 42 | 3ad2ant1 1134 | . . . . 5 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝐼‘(𝑈 ∨ 𝑉)) ∧ 𝑓 ∈ 𝑇) → 𝑈 ≠ 𝑉) |
44 | simp2 1138 | . . . . 5 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝐼‘(𝑈 ∨ 𝑉)) ∧ 𝑓 ∈ 𝑇) → 𝑓 ∈ (𝐼‘(𝑈 ∨ 𝑉))) | |
45 | 23, 8, 32, 9, 20, 27, 33, 34, 35, 36, 37, 28, 38, 39, 40, 41, 43, 44 | dia2dimlem11 38708 | . . . 4 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝐼‘(𝑈 ∨ 𝑉)) ∧ 𝑓 ∈ 𝑇) → 𝑓 ∈ ((𝐼‘𝑈) ⊕ (𝐼‘𝑉))) |
46 | 45 | 3exp 1120 | . . 3 ⊢ (𝜑 → (𝑓 ∈ (𝐼‘(𝑈 ∨ 𝑉)) → (𝑓 ∈ 𝑇 → 𝑓 ∈ ((𝐼‘𝑈) ⊕ (𝐼‘𝑉))))) |
47 | 31, 46 | mpdd 43 | . 2 ⊢ (𝜑 → (𝑓 ∈ (𝐼‘(𝑈 ∨ 𝑉)) → 𝑓 ∈ ((𝐼‘𝑈) ⊕ (𝐼‘𝑉)))) |
48 | 47 | ssrdv 3884 | 1 ⊢ (𝜑 → (𝐼‘(𝑈 ∨ 𝑉)) ⊆ ((𝐼‘𝑈) ⊕ (𝐼‘𝑉))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 209 ∧ wa 399 ∧ w3a 1088 = wceq 1542 ∈ wcel 2113 ≠ wne 2934 ⊆ wss 3844 class class class wbr 5031 ‘cfv 6340 (class class class)co 7171 Basecbs 16587 lecple 16676 joincjn 17671 meetcmee 17672 Latclat 17772 LSSumclsm 18878 LSubSpclss 19823 LSpanclspn 19863 Atomscatm 36897 HLchlt 36984 LHypclh 37618 LTrncltrn 37735 trLctrl 37792 DVecAcdveca 38636 DIsoAcdia 38662 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1916 ax-6 1974 ax-7 2019 ax-8 2115 ax-9 2123 ax-10 2144 ax-11 2161 ax-12 2178 ax-ext 2710 ax-rep 5155 ax-sep 5168 ax-nul 5175 ax-pow 5233 ax-pr 5297 ax-un 7480 ax-cnex 10672 ax-resscn 10673 ax-1cn 10674 ax-icn 10675 ax-addcl 10676 ax-addrcl 10677 ax-mulcl 10678 ax-mulrcl 10679 ax-mulcom 10680 ax-addass 10681 ax-mulass 10682 ax-distr 10683 ax-i2m1 10684 ax-1ne0 10685 ax-1rid 10686 ax-rnegex 10687 ax-rrecex 10688 ax-cnre 10689 ax-pre-lttri 10690 ax-pre-lttrn 10691 ax-pre-ltadd 10692 ax-pre-mulgt0 10693 ax-riotaBAD 36587 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 847 df-3or 1089 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1787 df-nf 1791 df-sb 2074 df-mo 2540 df-eu 2570 df-clab 2717 df-cleq 2730 df-clel 2811 df-nfc 2881 df-ne 2935 df-nel 3039 df-ral 3058 df-rex 3059 df-reu 3060 df-rmo 3061 df-rab 3062 df-v 3400 df-sbc 3683 df-csb 3792 df-dif 3847 df-un 3849 df-in 3851 df-ss 3861 df-pss 3863 df-nul 4213 df-if 4416 df-pw 4491 df-sn 4518 df-pr 4520 df-tp 4522 df-op 4524 df-uni 4798 df-int 4838 df-iun 4884 df-iin 4885 df-br 5032 df-opab 5094 df-mpt 5112 df-tr 5138 df-id 5430 df-eprel 5435 df-po 5443 df-so 5444 df-fr 5484 df-we 5486 df-xp 5532 df-rel 5533 df-cnv 5534 df-co 5535 df-dm 5536 df-rn 5537 df-res 5538 df-ima 5539 df-pred 6130 df-ord 6176 df-on 6177 df-lim 6178 df-suc 6179 df-iota 6298 df-fun 6342 df-fn 6343 df-f 6344 df-f1 6345 df-fo 6346 df-f1o 6347 df-fv 6348 df-riota 7128 df-ov 7174 df-oprab 7175 df-mpo 7176 df-om 7601 df-1st 7715 df-2nd 7716 df-tpos 7922 df-undef 7969 df-wrecs 7977 df-recs 8038 df-rdg 8076 df-1o 8132 df-er 8321 df-map 8440 df-en 8557 df-dom 8558 df-sdom 8559 df-fin 8560 df-pnf 10756 df-mnf 10757 df-xr 10758 df-ltxr 10759 df-le 10760 df-sub 10951 df-neg 10952 df-nn 11718 df-2 11780 df-3 11781 df-4 11782 df-5 11783 df-6 11784 df-n0 11978 df-z 12064 df-uz 12326 df-fz 12983 df-struct 16589 df-ndx 16590 df-slot 16591 df-base 16593 df-sets 16594 df-ress 16595 df-plusg 16682 df-mulr 16683 df-sca 16685 df-vsca 16686 df-0g 16819 df-proset 17655 df-poset 17673 df-plt 17685 df-lub 17701 df-glb 17702 df-join 17703 df-meet 17704 df-p0 17766 df-p1 17767 df-lat 17773 df-clat 17835 df-mgm 17969 df-sgrp 18018 df-mnd 18029 df-submnd 18074 df-grp 18223 df-minusg 18224 df-sbg 18225 df-subg 18395 df-cntz 18566 df-lsm 18880 df-cmn 19027 df-abl 19028 df-mgp 19360 df-ur 19372 df-ring 19419 df-oppr 19496 df-dvdsr 19514 df-unit 19515 df-invr 19545 df-dvr 19556 df-drng 19624 df-lmod 19756 df-lss 19824 df-lsp 19864 df-lvec 19995 df-oposet 36810 df-ol 36812 df-oml 36813 df-covers 36900 df-ats 36901 df-atl 36932 df-cvlat 36956 df-hlat 36985 df-llines 37132 df-lplanes 37133 df-lvols 37134 df-lines 37135 df-psubsp 37137 df-pmap 37138 df-padd 37430 df-lhyp 37622 df-laut 37623 df-ldil 37738 df-ltrn 37739 df-trl 37793 df-tgrp 38377 df-tendo 38389 df-edring 38391 df-dveca 38637 df-disoa 38663 |
This theorem is referenced by: dia2dimlem13 38710 |
Copyright terms: Public domain | W3C validator |