Mathbox for Norm Megill |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > Mathboxes > trlconid | Structured version Visualization version GIF version |
Description: The composition of two different translations is not the identity translation. (Contributed by NM, 22-Jul-2013.) |
Ref | Expression |
---|---|
trlconid.b | ⊢ 𝐵 = (Base‘𝐾) |
trlconid.h | ⊢ 𝐻 = (LHyp‘𝐾) |
trlconid.t | ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) |
trlconid.r | ⊢ 𝑅 = ((trL‘𝐾)‘𝑊) |
Ref | Expression |
---|---|
trlconid | ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺)) → (𝐹 ∘ 𝐺) ≠ ( I ↾ 𝐵)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqid 2738 | . . 3 ⊢ (Atoms‘𝐾) = (Atoms‘𝐾) | |
2 | trlconid.h | . . 3 ⊢ 𝐻 = (LHyp‘𝐾) | |
3 | trlconid.t | . . 3 ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) | |
4 | trlconid.r | . . 3 ⊢ 𝑅 = ((trL‘𝐾)‘𝑊) | |
5 | 1, 2, 3, 4 | trlcoat 38487 | . 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺)) → (𝑅‘(𝐹 ∘ 𝐺)) ∈ (Atoms‘𝐾)) |
6 | simp1 1138 | . . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺)) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) | |
7 | simp2l 1201 | . . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺)) → 𝐹 ∈ 𝑇) | |
8 | simp2r 1202 | . . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺)) → 𝐺 ∈ 𝑇) | |
9 | 2, 3 | ltrnco 38483 | . . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) → (𝐹 ∘ 𝐺) ∈ 𝑇) |
10 | 6, 7, 8, 9 | syl3anc 1373 | . . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺)) → (𝐹 ∘ 𝐺) ∈ 𝑇) |
11 | trlconid.b | . . . 4 ⊢ 𝐵 = (Base‘𝐾) | |
12 | 11, 1, 2, 3, 4 | trlnidatb 37941 | . . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∘ 𝐺) ∈ 𝑇) → ((𝐹 ∘ 𝐺) ≠ ( I ↾ 𝐵) ↔ (𝑅‘(𝐹 ∘ 𝐺)) ∈ (Atoms‘𝐾))) |
13 | 6, 10, 12 | syl2anc 587 | . 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺)) → ((𝐹 ∘ 𝐺) ≠ ( I ↾ 𝐵) ↔ (𝑅‘(𝐹 ∘ 𝐺)) ∈ (Atoms‘𝐾))) |
14 | 5, 13 | mpbird 260 | 1 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺)) → (𝐹 ∘ 𝐺) ≠ ( I ↾ 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 209 ∧ wa 399 ∧ w3a 1089 = wceq 1543 ∈ wcel 2111 ≠ wne 2941 I cid 5463 ↾ cres 5562 ∘ ccom 5564 ‘cfv 6389 Basecbs 16773 Atomscatm 37027 HLchlt 37114 LHypclh 37748 LTrncltrn 37865 trLctrl 37922 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2016 ax-8 2113 ax-9 2121 ax-10 2142 ax-11 2159 ax-12 2176 ax-ext 2709 ax-rep 5188 ax-sep 5201 ax-nul 5208 ax-pow 5267 ax-pr 5331 ax-un 7532 ax-riotaBAD 36717 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 848 df-3or 1090 df-3an 1091 df-tru 1546 df-fal 1556 df-ex 1788 df-nf 1792 df-sb 2072 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2817 df-nfc 2887 df-ne 2942 df-ral 3067 df-rex 3068 df-reu 3069 df-rmo 3070 df-rab 3071 df-v 3417 df-sbc 3704 df-csb 3821 df-dif 3878 df-un 3880 df-in 3882 df-ss 3892 df-nul 4247 df-if 4449 df-pw 4524 df-sn 4551 df-pr 4553 df-op 4557 df-uni 4829 df-iun 4915 df-iin 4916 df-br 5063 df-opab 5125 df-mpt 5145 df-id 5464 df-xp 5566 df-rel 5567 df-cnv 5568 df-co 5569 df-dm 5570 df-rn 5571 df-res 5572 df-ima 5573 df-iota 6347 df-fun 6391 df-fn 6392 df-f 6393 df-f1 6394 df-fo 6395 df-f1o 6396 df-fv 6397 df-riota 7179 df-ov 7225 df-oprab 7226 df-mpo 7227 df-1st 7770 df-2nd 7771 df-undef 8024 df-map 8519 df-proset 17815 df-poset 17833 df-plt 17849 df-lub 17865 df-glb 17866 df-join 17867 df-meet 17868 df-p0 17944 df-p1 17945 df-lat 17951 df-clat 18018 df-oposet 36940 df-ol 36942 df-oml 36943 df-covers 37030 df-ats 37031 df-atl 37062 df-cvlat 37086 df-hlat 37115 df-llines 37262 df-lplanes 37263 df-lvols 37264 df-lines 37265 df-psubsp 37267 df-pmap 37268 df-padd 37560 df-lhyp 37752 df-laut 37753 df-ldil 37868 df-ltrn 37869 df-trl 37923 |
This theorem is referenced by: cdlemk47 38713 cdlemk52 38718 cdlemk53a 38719 |
Copyright terms: Public domain | W3C validator |