![]() |
Mathbox for Norm Megill |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > dihjatcclem3 | Structured version Visualization version GIF version |
Description: Lemma for dihjatcc 39885. (Contributed by NM, 28-Sep-2014.) |
Ref | Expression |
---|---|
dihjatcclem.b | ⊢ 𝐵 = (Base‘𝐾) |
dihjatcclem.l | ⊢ ≤ = (le‘𝐾) |
dihjatcclem.h | ⊢ 𝐻 = (LHyp‘𝐾) |
dihjatcclem.j | ⊢ ∨ = (join‘𝐾) |
dihjatcclem.m | ⊢ ∧ = (meet‘𝐾) |
dihjatcclem.a | ⊢ 𝐴 = (Atoms‘𝐾) |
dihjatcclem.u | ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) |
dihjatcclem.s | ⊢ ⊕ = (LSSum‘𝑈) |
dihjatcclem.i | ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊) |
dihjatcclem.v | ⊢ 𝑉 = ((𝑃 ∨ 𝑄) ∧ 𝑊) |
dihjatcclem.k | ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
dihjatcclem.p | ⊢ (𝜑 → (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) |
dihjatcclem.q | ⊢ (𝜑 → (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) |
dihjatcc.w | ⊢ 𝐶 = ((oc‘𝐾)‘𝑊) |
dihjatcc.t | ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) |
dihjatcc.r | ⊢ 𝑅 = ((trL‘𝐾)‘𝑊) |
dihjatcc.e | ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊) |
dihjatcc.g | ⊢ 𝐺 = (℩𝑑 ∈ 𝑇 (𝑑‘𝐶) = 𝑃) |
dihjatcc.dd | ⊢ 𝐷 = (℩𝑑 ∈ 𝑇 (𝑑‘𝐶) = 𝑄) |
Ref | Expression |
---|---|
dihjatcclem3 | ⊢ (𝜑 → (𝑅‘(𝐺 ∘ ◡𝐷)) = 𝑉) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dihjatcclem.k | . . 3 ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) | |
2 | dihjatcclem.l | . . . . . . 7 ⊢ ≤ = (le‘𝐾) | |
3 | dihjatcclem.a | . . . . . . 7 ⊢ 𝐴 = (Atoms‘𝐾) | |
4 | dihjatcclem.h | . . . . . . 7 ⊢ 𝐻 = (LHyp‘𝐾) | |
5 | dihjatcc.w | . . . . . . 7 ⊢ 𝐶 = ((oc‘𝐾)‘𝑊) | |
6 | 2, 3, 4, 5 | lhpocnel2 38482 | . . . . . 6 ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → (𝐶 ∈ 𝐴 ∧ ¬ 𝐶 ≤ 𝑊)) |
7 | 1, 6 | syl 17 | . . . . 5 ⊢ (𝜑 → (𝐶 ∈ 𝐴 ∧ ¬ 𝐶 ≤ 𝑊)) |
8 | dihjatcclem.p | . . . . 5 ⊢ (𝜑 → (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) | |
9 | dihjatcc.t | . . . . . 6 ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) | |
10 | dihjatcc.g | . . . . . 6 ⊢ 𝐺 = (℩𝑑 ∈ 𝑇 (𝑑‘𝐶) = 𝑃) | |
11 | 2, 3, 4, 9, 10 | ltrniotacl 39042 | . . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐶 ∈ 𝐴 ∧ ¬ 𝐶 ≤ 𝑊) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → 𝐺 ∈ 𝑇) |
12 | 1, 7, 8, 11 | syl3anc 1371 | . . . 4 ⊢ (𝜑 → 𝐺 ∈ 𝑇) |
13 | dihjatcclem.q | . . . . . 6 ⊢ (𝜑 → (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) | |
14 | dihjatcc.dd | . . . . . . 7 ⊢ 𝐷 = (℩𝑑 ∈ 𝑇 (𝑑‘𝐶) = 𝑄) | |
15 | 2, 3, 4, 9, 14 | ltrniotacl 39042 | . . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐶 ∈ 𝐴 ∧ ¬ 𝐶 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → 𝐷 ∈ 𝑇) |
16 | 1, 7, 13, 15 | syl3anc 1371 | . . . . 5 ⊢ (𝜑 → 𝐷 ∈ 𝑇) |
17 | 4, 9 | ltrncnv 38609 | . . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐷 ∈ 𝑇) → ◡𝐷 ∈ 𝑇) |
18 | 1, 16, 17 | syl2anc 584 | . . . 4 ⊢ (𝜑 → ◡𝐷 ∈ 𝑇) |
19 | 4, 9 | ltrnco 39182 | . . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐺 ∈ 𝑇 ∧ ◡𝐷 ∈ 𝑇) → (𝐺 ∘ ◡𝐷) ∈ 𝑇) |
20 | 1, 12, 18, 19 | syl3anc 1371 | . . 3 ⊢ (𝜑 → (𝐺 ∘ ◡𝐷) ∈ 𝑇) |
21 | dihjatcclem.j | . . . 4 ⊢ ∨ = (join‘𝐾) | |
22 | dihjatcclem.m | . . . 4 ⊢ ∧ = (meet‘𝐾) | |
23 | dihjatcc.r | . . . 4 ⊢ 𝑅 = ((trL‘𝐾)‘𝑊) | |
24 | 2, 21, 22, 3, 4, 9, 23 | trlval2 38626 | . . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐺 ∘ ◡𝐷) ∈ 𝑇 ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → (𝑅‘(𝐺 ∘ ◡𝐷)) = ((𝑄 ∨ ((𝐺 ∘ ◡𝐷)‘𝑄)) ∧ 𝑊)) |
25 | 1, 20, 13, 24 | syl3anc 1371 | . 2 ⊢ (𝜑 → (𝑅‘(𝐺 ∘ ◡𝐷)) = ((𝑄 ∨ ((𝐺 ∘ ◡𝐷)‘𝑄)) ∧ 𝑊)) |
26 | 13 | simpld 495 | . . . . . . . 8 ⊢ (𝜑 → 𝑄 ∈ 𝐴) |
27 | 2, 3, 4, 9 | ltrncoval 38608 | . . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐺 ∈ 𝑇 ∧ ◡𝐷 ∈ 𝑇) ∧ 𝑄 ∈ 𝐴) → ((𝐺 ∘ ◡𝐷)‘𝑄) = (𝐺‘(◡𝐷‘𝑄))) |
28 | 1, 12, 18, 26, 27 | syl121anc 1375 | . . . . . . 7 ⊢ (𝜑 → ((𝐺 ∘ ◡𝐷)‘𝑄) = (𝐺‘(◡𝐷‘𝑄))) |
29 | 2, 3, 4, 9, 14 | ltrniotacnvval 39045 | . . . . . . . . . 10 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐶 ∈ 𝐴 ∧ ¬ 𝐶 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → (◡𝐷‘𝑄) = 𝐶) |
30 | 1, 7, 13, 29 | syl3anc 1371 | . . . . . . . . 9 ⊢ (𝜑 → (◡𝐷‘𝑄) = 𝐶) |
31 | 30 | fveq2d 6846 | . . . . . . . 8 ⊢ (𝜑 → (𝐺‘(◡𝐷‘𝑄)) = (𝐺‘𝐶)) |
32 | 2, 3, 4, 9, 10 | ltrniotaval 39044 | . . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐶 ∈ 𝐴 ∧ ¬ 𝐶 ≤ 𝑊) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝐺‘𝐶) = 𝑃) |
33 | 1, 7, 8, 32 | syl3anc 1371 | . . . . . . . 8 ⊢ (𝜑 → (𝐺‘𝐶) = 𝑃) |
34 | 31, 33 | eqtrd 2776 | . . . . . . 7 ⊢ (𝜑 → (𝐺‘(◡𝐷‘𝑄)) = 𝑃) |
35 | 28, 34 | eqtrd 2776 | . . . . . 6 ⊢ (𝜑 → ((𝐺 ∘ ◡𝐷)‘𝑄) = 𝑃) |
36 | 35 | oveq2d 7373 | . . . . 5 ⊢ (𝜑 → (𝑄 ∨ ((𝐺 ∘ ◡𝐷)‘𝑄)) = (𝑄 ∨ 𝑃)) |
37 | 1 | simpld 495 | . . . . . 6 ⊢ (𝜑 → 𝐾 ∈ HL) |
38 | 8 | simpld 495 | . . . . . 6 ⊢ (𝜑 → 𝑃 ∈ 𝐴) |
39 | 21, 3 | hlatjcom 37830 | . . . . . 6 ⊢ ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) → (𝑃 ∨ 𝑄) = (𝑄 ∨ 𝑃)) |
40 | 37, 38, 26, 39 | syl3anc 1371 | . . . . 5 ⊢ (𝜑 → (𝑃 ∨ 𝑄) = (𝑄 ∨ 𝑃)) |
41 | 36, 40 | eqtr4d 2779 | . . . 4 ⊢ (𝜑 → (𝑄 ∨ ((𝐺 ∘ ◡𝐷)‘𝑄)) = (𝑃 ∨ 𝑄)) |
42 | 41 | oveq1d 7372 | . . 3 ⊢ (𝜑 → ((𝑄 ∨ ((𝐺 ∘ ◡𝐷)‘𝑄)) ∧ 𝑊) = ((𝑃 ∨ 𝑄) ∧ 𝑊)) |
43 | dihjatcclem.v | . . 3 ⊢ 𝑉 = ((𝑃 ∨ 𝑄) ∧ 𝑊) | |
44 | 42, 43 | eqtr4di 2794 | . 2 ⊢ (𝜑 → ((𝑄 ∨ ((𝐺 ∘ ◡𝐷)‘𝑄)) ∧ 𝑊) = 𝑉) |
45 | 25, 44 | eqtrd 2776 | 1 ⊢ (𝜑 → (𝑅‘(𝐺 ∘ ◡𝐷)) = 𝑉) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∧ wa 396 = wceq 1541 ∈ wcel 2106 class class class wbr 5105 ◡ccnv 5632 ∘ ccom 5637 ‘cfv 6496 ℩crio 7312 (class class class)co 7357 Basecbs 17083 lecple 17140 occoc 17141 joincjn 18200 meetcmee 18201 LSSumclsm 19416 Atomscatm 37725 HLchlt 37812 LHypclh 38447 LTrncltrn 38564 trLctrl 38621 TEndoctendo 39215 DVecHcdvh 39541 DIsoHcdih 39691 |
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 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2707 ax-rep 5242 ax-sep 5256 ax-nul 5263 ax-pow 5320 ax-pr 5384 ax-un 7672 ax-riotaBAD 37415 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3or 1088 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2538 df-eu 2567 df-clab 2714 df-cleq 2728 df-clel 2814 df-nfc 2889 df-ne 2944 df-ral 3065 df-rex 3074 df-rmo 3353 df-reu 3354 df-rab 3408 df-v 3447 df-sbc 3740 df-csb 3856 df-dif 3913 df-un 3915 df-in 3917 df-ss 3927 df-nul 4283 df-if 4487 df-pw 4562 df-sn 4587 df-pr 4589 df-op 4593 df-uni 4866 df-iun 4956 df-iin 4957 df-br 5106 df-opab 5168 df-mpt 5189 df-id 5531 df-xp 5639 df-rel 5640 df-cnv 5641 df-co 5642 df-dm 5643 df-rn 5644 df-res 5645 df-ima 5646 df-iota 6448 df-fun 6498 df-fn 6499 df-f 6500 df-f1 6501 df-fo 6502 df-f1o 6503 df-fv 6504 df-riota 7313 df-ov 7360 df-oprab 7361 df-mpo 7362 df-1st 7921 df-2nd 7922 df-undef 8204 df-map 8767 df-proset 18184 df-poset 18202 df-plt 18219 df-lub 18235 df-glb 18236 df-join 18237 df-meet 18238 df-p0 18314 df-p1 18315 df-lat 18321 df-clat 18388 df-oposet 37638 df-ol 37640 df-oml 37641 df-covers 37728 df-ats 37729 df-atl 37760 df-cvlat 37784 df-hlat 37813 df-llines 37961 df-lplanes 37962 df-lvols 37963 df-lines 37964 df-psubsp 37966 df-pmap 37967 df-padd 38259 df-lhyp 38451 df-laut 38452 df-ldil 38567 df-ltrn 38568 df-trl 38622 |
This theorem is referenced by: dihjatcclem4 39884 |
Copyright terms: Public domain | W3C validator |