![]() |
Mathbox for Norm Megill |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > trl0 | Structured version Visualization version GIF version |
Description: If an atom not under the fiducial co-atom 𝑊 equals its lattice translation, the trace of the translation is zero. (Contributed by NM, 24-May-2012.) |
Ref | Expression |
---|---|
trl0.l | ⊢ ≤ = (le‘𝐾) |
trl0.z | ⊢ 0 = (0.‘𝐾) |
trl0.a | ⊢ 𝐴 = (Atoms‘𝐾) |
trl0.h | ⊢ 𝐻 = (LHyp‘𝐾) |
trl0.t | ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) |
trl0.r | ⊢ 𝑅 = ((trL‘𝐾)‘𝑊) |
Ref | Expression |
---|---|
trl0 | ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝐹 ∈ 𝑇 ∧ (𝐹‘𝑃) = 𝑃)) → (𝑅‘𝐹) = 0 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simp1 1172 | . . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝐹 ∈ 𝑇 ∧ (𝐹‘𝑃) = 𝑃)) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) | |
2 | simp3l 1264 | . . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝐹 ∈ 𝑇 ∧ (𝐹‘𝑃) = 𝑃)) → 𝐹 ∈ 𝑇) | |
3 | simp2 1173 | . . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝐹 ∈ 𝑇 ∧ (𝐹‘𝑃) = 𝑃)) → (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) | |
4 | trl0.l | . . . 4 ⊢ ≤ = (le‘𝐾) | |
5 | eqid 2824 | . . . 4 ⊢ (join‘𝐾) = (join‘𝐾) | |
6 | eqid 2824 | . . . 4 ⊢ (meet‘𝐾) = (meet‘𝐾) | |
7 | trl0.a | . . . 4 ⊢ 𝐴 = (Atoms‘𝐾) | |
8 | trl0.h | . . . 4 ⊢ 𝐻 = (LHyp‘𝐾) | |
9 | trl0.t | . . . 4 ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) | |
10 | trl0.r | . . . 4 ⊢ 𝑅 = ((trL‘𝐾)‘𝑊) | |
11 | 4, 5, 6, 7, 8, 9, 10 | trlval2 36237 | . . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝑅‘𝐹) = ((𝑃(join‘𝐾)(𝐹‘𝑃))(meet‘𝐾)𝑊)) |
12 | 1, 2, 3, 11 | syl3anc 1496 | . 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝐹 ∈ 𝑇 ∧ (𝐹‘𝑃) = 𝑃)) → (𝑅‘𝐹) = ((𝑃(join‘𝐾)(𝐹‘𝑃))(meet‘𝐾)𝑊)) |
13 | simp3r 1265 | . . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝐹 ∈ 𝑇 ∧ (𝐹‘𝑃) = 𝑃)) → (𝐹‘𝑃) = 𝑃) | |
14 | 13 | oveq2d 6920 | . . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝐹 ∈ 𝑇 ∧ (𝐹‘𝑃) = 𝑃)) → (𝑃(join‘𝐾)(𝐹‘𝑃)) = (𝑃(join‘𝐾)𝑃)) |
15 | simp1l 1260 | . . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝐹 ∈ 𝑇 ∧ (𝐹‘𝑃) = 𝑃)) → 𝐾 ∈ HL) | |
16 | simp2l 1262 | . . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝐹 ∈ 𝑇 ∧ (𝐹‘𝑃) = 𝑃)) → 𝑃 ∈ 𝐴) | |
17 | 5, 7 | hlatjidm 35443 | . . . . 5 ⊢ ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴) → (𝑃(join‘𝐾)𝑃) = 𝑃) |
18 | 15, 16, 17 | syl2anc 581 | . . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝐹 ∈ 𝑇 ∧ (𝐹‘𝑃) = 𝑃)) → (𝑃(join‘𝐾)𝑃) = 𝑃) |
19 | 14, 18 | eqtrd 2860 | . . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝐹 ∈ 𝑇 ∧ (𝐹‘𝑃) = 𝑃)) → (𝑃(join‘𝐾)(𝐹‘𝑃)) = 𝑃) |
20 | 19 | oveq1d 6919 | . 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝐹 ∈ 𝑇 ∧ (𝐹‘𝑃) = 𝑃)) → ((𝑃(join‘𝐾)(𝐹‘𝑃))(meet‘𝐾)𝑊) = (𝑃(meet‘𝐾)𝑊)) |
21 | trl0.z | . . . 4 ⊢ 0 = (0.‘𝐾) | |
22 | 4, 6, 21, 7, 8 | lhpmat 36104 | . . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝑃(meet‘𝐾)𝑊) = 0 ) |
23 | 1, 3, 22 | syl2anc 581 | . 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝐹 ∈ 𝑇 ∧ (𝐹‘𝑃) = 𝑃)) → (𝑃(meet‘𝐾)𝑊) = 0 ) |
24 | 12, 20, 23 | 3eqtrd 2864 | 1 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝐹 ∈ 𝑇 ∧ (𝐹‘𝑃) = 𝑃)) → (𝑅‘𝐹) = 0 ) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∧ wa 386 ∧ w3a 1113 = wceq 1658 ∈ wcel 2166 class class class wbr 4872 ‘cfv 6122 (class class class)co 6904 lecple 16311 joincjn 17296 meetcmee 17297 0.cp0 17389 Atomscatm 35337 HLchlt 35424 LHypclh 36058 LTrncltrn 36175 trLctrl 36232 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1896 ax-4 1910 ax-5 2011 ax-6 2077 ax-7 2114 ax-8 2168 ax-9 2175 ax-10 2194 ax-11 2209 ax-12 2222 ax-13 2390 ax-ext 2802 ax-rep 4993 ax-sep 5004 ax-nul 5012 ax-pow 5064 ax-pr 5126 ax-un 7208 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 881 df-3an 1115 df-tru 1662 df-ex 1881 df-nf 1885 df-sb 2070 df-mo 2604 df-eu 2639 df-clab 2811 df-cleq 2817 df-clel 2820 df-nfc 2957 df-ne 2999 df-ral 3121 df-rex 3122 df-reu 3123 df-rab 3125 df-v 3415 df-sbc 3662 df-csb 3757 df-dif 3800 df-un 3802 df-in 3804 df-ss 3811 df-nul 4144 df-if 4306 df-pw 4379 df-sn 4397 df-pr 4399 df-op 4403 df-uni 4658 df-iun 4741 df-br 4873 df-opab 4935 df-mpt 4952 df-id 5249 df-xp 5347 df-rel 5348 df-cnv 5349 df-co 5350 df-dm 5351 df-rn 5352 df-res 5353 df-ima 5354 df-iota 6085 df-fun 6124 df-fn 6125 df-f 6126 df-f1 6127 df-fo 6128 df-f1o 6129 df-fv 6130 df-riota 6865 df-ov 6907 df-oprab 6908 df-mpt2 6909 df-map 8123 df-proset 17280 df-poset 17298 df-plt 17310 df-lub 17326 df-glb 17327 df-join 17328 df-meet 17329 df-p0 17391 df-lat 17398 df-covers 35340 df-ats 35341 df-atl 35372 df-cvlat 35396 df-hlat 35425 df-lhyp 36062 df-laut 36063 df-ldil 36178 df-ltrn 36179 df-trl 36233 |
This theorem is referenced by: trlator0 36245 ltrnnidn 36248 trlid0 36250 trlnidatb 36251 trlnle 36260 trlval3 36261 trlval4 36262 cdlemc6 36270 cdlemg31d 36774 |
Copyright terms: Public domain | W3C validator |