Proof of Theorem dihjat
| Step | Hyp | Ref
| Expression |
| 1 | | eqid 2737 |
. . 3
⊢
(le‘𝐾) =
(le‘𝐾) |
| 2 | | dihjat.h |
. . 3
⊢ 𝐻 = (LHyp‘𝐾) |
| 3 | | dihjat.j |
. . 3
⊢ ∨ =
(join‘𝐾) |
| 4 | | dihjat.a |
. . 3
⊢ 𝐴 = (Atoms‘𝐾) |
| 5 | | dihjat.u |
. . 3
⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) |
| 6 | | dihjat.s |
. . 3
⊢ ⊕ =
(LSSum‘𝑈) |
| 7 | | dihjat.i |
. . 3
⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊) |
| 8 | | dihjat.k |
. . . 4
⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
| 9 | 8 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ (𝑃(le‘𝐾)𝑊 ∧ 𝑄(le‘𝐾)𝑊)) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
| 10 | | dihjat.p |
. . . . 5
⊢ (𝜑 → 𝑃 ∈ 𝐴) |
| 11 | 10 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ (𝑃(le‘𝐾)𝑊 ∧ 𝑄(le‘𝐾)𝑊)) → 𝑃 ∈ 𝐴) |
| 12 | | simprl 771 |
. . . 4
⊢ ((𝜑 ∧ (𝑃(le‘𝐾)𝑊 ∧ 𝑄(le‘𝐾)𝑊)) → 𝑃(le‘𝐾)𝑊) |
| 13 | 11, 12 | jca 511 |
. . 3
⊢ ((𝜑 ∧ (𝑃(le‘𝐾)𝑊 ∧ 𝑄(le‘𝐾)𝑊)) → (𝑃 ∈ 𝐴 ∧ 𝑃(le‘𝐾)𝑊)) |
| 14 | | dihjat.q |
. . . . 5
⊢ (𝜑 → 𝑄 ∈ 𝐴) |
| 15 | 14 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ (𝑃(le‘𝐾)𝑊 ∧ 𝑄(le‘𝐾)𝑊)) → 𝑄 ∈ 𝐴) |
| 16 | | simprr 773 |
. . . 4
⊢ ((𝜑 ∧ (𝑃(le‘𝐾)𝑊 ∧ 𝑄(le‘𝐾)𝑊)) → 𝑄(le‘𝐾)𝑊) |
| 17 | 15, 16 | jca 511 |
. . 3
⊢ ((𝜑 ∧ (𝑃(le‘𝐾)𝑊 ∧ 𝑄(le‘𝐾)𝑊)) → (𝑄 ∈ 𝐴 ∧ 𝑄(le‘𝐾)𝑊)) |
| 18 | 1, 2, 3, 4, 5, 6, 7, 9, 13, 17 | dihjatb 41418 |
. 2
⊢ ((𝜑 ∧ (𝑃(le‘𝐾)𝑊 ∧ 𝑄(le‘𝐾)𝑊)) → (𝐼‘(𝑃 ∨ 𝑄)) = ((𝐼‘𝑃) ⊕ (𝐼‘𝑄))) |
| 19 | | eqid 2737 |
. . 3
⊢
(Base‘𝐾) =
(Base‘𝐾) |
| 20 | 8 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ (𝑃(le‘𝐾)𝑊 ∧ ¬ 𝑄(le‘𝐾)𝑊)) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
| 21 | 19, 4 | atbase 39290 |
. . . . . 6
⊢ (𝑃 ∈ 𝐴 → 𝑃 ∈ (Base‘𝐾)) |
| 22 | 10, 21 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝑃 ∈ (Base‘𝐾)) |
| 23 | 22 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ (𝑃(le‘𝐾)𝑊 ∧ ¬ 𝑄(le‘𝐾)𝑊)) → 𝑃 ∈ (Base‘𝐾)) |
| 24 | | simprl 771 |
. . . 4
⊢ ((𝜑 ∧ (𝑃(le‘𝐾)𝑊 ∧ ¬ 𝑄(le‘𝐾)𝑊)) → 𝑃(le‘𝐾)𝑊) |
| 25 | 23, 24 | jca 511 |
. . 3
⊢ ((𝜑 ∧ (𝑃(le‘𝐾)𝑊 ∧ ¬ 𝑄(le‘𝐾)𝑊)) → (𝑃 ∈ (Base‘𝐾) ∧ 𝑃(le‘𝐾)𝑊)) |
| 26 | 14 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ (𝑃(le‘𝐾)𝑊 ∧ ¬ 𝑄(le‘𝐾)𝑊)) → 𝑄 ∈ 𝐴) |
| 27 | | simprr 773 |
. . . 4
⊢ ((𝜑 ∧ (𝑃(le‘𝐾)𝑊 ∧ ¬ 𝑄(le‘𝐾)𝑊)) → ¬ 𝑄(le‘𝐾)𝑊) |
| 28 | 26, 27 | jca 511 |
. . 3
⊢ ((𝜑 ∧ (𝑃(le‘𝐾)𝑊 ∧ ¬ 𝑄(le‘𝐾)𝑊)) → (𝑄 ∈ 𝐴 ∧ ¬ 𝑄(le‘𝐾)𝑊)) |
| 29 | 19, 1, 2, 3, 4, 5, 6, 7, 20, 25, 28 | dihjatc 41419 |
. 2
⊢ ((𝜑 ∧ (𝑃(le‘𝐾)𝑊 ∧ ¬ 𝑄(le‘𝐾)𝑊)) → (𝐼‘(𝑃 ∨ 𝑄)) = ((𝐼‘𝑃) ⊕ (𝐼‘𝑄))) |
| 30 | 8 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ (¬ 𝑃(le‘𝐾)𝑊 ∧ 𝑄(le‘𝐾)𝑊)) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
| 31 | 19, 4 | atbase 39290 |
. . . . . . 7
⊢ (𝑄 ∈ 𝐴 → 𝑄 ∈ (Base‘𝐾)) |
| 32 | 14, 31 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝑄 ∈ (Base‘𝐾)) |
| 33 | 32 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ (¬ 𝑃(le‘𝐾)𝑊 ∧ 𝑄(le‘𝐾)𝑊)) → 𝑄 ∈ (Base‘𝐾)) |
| 34 | | simprr 773 |
. . . . 5
⊢ ((𝜑 ∧ (¬ 𝑃(le‘𝐾)𝑊 ∧ 𝑄(le‘𝐾)𝑊)) → 𝑄(le‘𝐾)𝑊) |
| 35 | 33, 34 | jca 511 |
. . . 4
⊢ ((𝜑 ∧ (¬ 𝑃(le‘𝐾)𝑊 ∧ 𝑄(le‘𝐾)𝑊)) → (𝑄 ∈ (Base‘𝐾) ∧ 𝑄(le‘𝐾)𝑊)) |
| 36 | 10 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ (¬ 𝑃(le‘𝐾)𝑊 ∧ 𝑄(le‘𝐾)𝑊)) → 𝑃 ∈ 𝐴) |
| 37 | | simprl 771 |
. . . . 5
⊢ ((𝜑 ∧ (¬ 𝑃(le‘𝐾)𝑊 ∧ 𝑄(le‘𝐾)𝑊)) → ¬ 𝑃(le‘𝐾)𝑊) |
| 38 | 36, 37 | jca 511 |
. . . 4
⊢ ((𝜑 ∧ (¬ 𝑃(le‘𝐾)𝑊 ∧ 𝑄(le‘𝐾)𝑊)) → (𝑃 ∈ 𝐴 ∧ ¬ 𝑃(le‘𝐾)𝑊)) |
| 39 | 19, 1, 2, 3, 4, 5, 6, 7, 30, 35, 38 | dihjatc 41419 |
. . 3
⊢ ((𝜑 ∧ (¬ 𝑃(le‘𝐾)𝑊 ∧ 𝑄(le‘𝐾)𝑊)) → (𝐼‘(𝑄 ∨ 𝑃)) = ((𝐼‘𝑄) ⊕ (𝐼‘𝑃))) |
| 40 | 8 | simpld 494 |
. . . . . 6
⊢ (𝜑 → 𝐾 ∈ HL) |
| 41 | 3, 4 | hlatjcom 39369 |
. . . . . 6
⊢ ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) → (𝑃 ∨ 𝑄) = (𝑄 ∨ 𝑃)) |
| 42 | 40, 10, 14, 41 | syl3anc 1373 |
. . . . 5
⊢ (𝜑 → (𝑃 ∨ 𝑄) = (𝑄 ∨ 𝑃)) |
| 43 | 42 | fveq2d 6910 |
. . . 4
⊢ (𝜑 → (𝐼‘(𝑃 ∨ 𝑄)) = (𝐼‘(𝑄 ∨ 𝑃))) |
| 44 | 43 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ (¬ 𝑃(le‘𝐾)𝑊 ∧ 𝑄(le‘𝐾)𝑊)) → (𝐼‘(𝑃 ∨ 𝑄)) = (𝐼‘(𝑄 ∨ 𝑃))) |
| 45 | 2, 5, 8 | dvhlmod 41112 |
. . . . . 6
⊢ (𝜑 → 𝑈 ∈ LMod) |
| 46 | | lmodabl 20907 |
. . . . . 6
⊢ (𝑈 ∈ LMod → 𝑈 ∈ Abel) |
| 47 | 45, 46 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝑈 ∈ Abel) |
| 48 | | eqid 2737 |
. . . . . . . 8
⊢
(LSubSp‘𝑈) =
(LSubSp‘𝑈) |
| 49 | 48 | lsssssubg 20956 |
. . . . . . 7
⊢ (𝑈 ∈ LMod →
(LSubSp‘𝑈) ⊆
(SubGrp‘𝑈)) |
| 50 | 45, 49 | syl 17 |
. . . . . 6
⊢ (𝜑 → (LSubSp‘𝑈) ⊆ (SubGrp‘𝑈)) |
| 51 | 19, 2, 7, 5, 48 | dihlss 41252 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ∈ (Base‘𝐾)) → (𝐼‘𝑃) ∈ (LSubSp‘𝑈)) |
| 52 | 8, 22, 51 | syl2anc 584 |
. . . . . 6
⊢ (𝜑 → (𝐼‘𝑃) ∈ (LSubSp‘𝑈)) |
| 53 | 50, 52 | sseldd 3984 |
. . . . 5
⊢ (𝜑 → (𝐼‘𝑃) ∈ (SubGrp‘𝑈)) |
| 54 | 19, 2, 7, 5, 48 | dihlss 41252 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑄 ∈ (Base‘𝐾)) → (𝐼‘𝑄) ∈ (LSubSp‘𝑈)) |
| 55 | 8, 32, 54 | syl2anc 584 |
. . . . . 6
⊢ (𝜑 → (𝐼‘𝑄) ∈ (LSubSp‘𝑈)) |
| 56 | 50, 55 | sseldd 3984 |
. . . . 5
⊢ (𝜑 → (𝐼‘𝑄) ∈ (SubGrp‘𝑈)) |
| 57 | 6 | lsmcom 19876 |
. . . . 5
⊢ ((𝑈 ∈ Abel ∧ (𝐼‘𝑃) ∈ (SubGrp‘𝑈) ∧ (𝐼‘𝑄) ∈ (SubGrp‘𝑈)) → ((𝐼‘𝑃) ⊕ (𝐼‘𝑄)) = ((𝐼‘𝑄) ⊕ (𝐼‘𝑃))) |
| 58 | 47, 53, 56, 57 | syl3anc 1373 |
. . . 4
⊢ (𝜑 → ((𝐼‘𝑃) ⊕ (𝐼‘𝑄)) = ((𝐼‘𝑄) ⊕ (𝐼‘𝑃))) |
| 59 | 58 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ (¬ 𝑃(le‘𝐾)𝑊 ∧ 𝑄(le‘𝐾)𝑊)) → ((𝐼‘𝑃) ⊕ (𝐼‘𝑄)) = ((𝐼‘𝑄) ⊕ (𝐼‘𝑃))) |
| 60 | 39, 44, 59 | 3eqtr4d 2787 |
. 2
⊢ ((𝜑 ∧ (¬ 𝑃(le‘𝐾)𝑊 ∧ 𝑄(le‘𝐾)𝑊)) → (𝐼‘(𝑃 ∨ 𝑄)) = ((𝐼‘𝑃) ⊕ (𝐼‘𝑄))) |
| 61 | 8 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ (¬ 𝑃(le‘𝐾)𝑊 ∧ ¬ 𝑄(le‘𝐾)𝑊)) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
| 62 | 10 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ (¬ 𝑃(le‘𝐾)𝑊 ∧ ¬ 𝑄(le‘𝐾)𝑊)) → 𝑃 ∈ 𝐴) |
| 63 | | simprl 771 |
. . . 4
⊢ ((𝜑 ∧ (¬ 𝑃(le‘𝐾)𝑊 ∧ ¬ 𝑄(le‘𝐾)𝑊)) → ¬ 𝑃(le‘𝐾)𝑊) |
| 64 | 62, 63 | jca 511 |
. . 3
⊢ ((𝜑 ∧ (¬ 𝑃(le‘𝐾)𝑊 ∧ ¬ 𝑄(le‘𝐾)𝑊)) → (𝑃 ∈ 𝐴 ∧ ¬ 𝑃(le‘𝐾)𝑊)) |
| 65 | 14 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ (¬ 𝑃(le‘𝐾)𝑊 ∧ ¬ 𝑄(le‘𝐾)𝑊)) → 𝑄 ∈ 𝐴) |
| 66 | | simprr 773 |
. . . 4
⊢ ((𝜑 ∧ (¬ 𝑃(le‘𝐾)𝑊 ∧ ¬ 𝑄(le‘𝐾)𝑊)) → ¬ 𝑄(le‘𝐾)𝑊) |
| 67 | 65, 66 | jca 511 |
. . 3
⊢ ((𝜑 ∧ (¬ 𝑃(le‘𝐾)𝑊 ∧ ¬ 𝑄(le‘𝐾)𝑊)) → (𝑄 ∈ 𝐴 ∧ ¬ 𝑄(le‘𝐾)𝑊)) |
| 68 | 1, 2, 3, 4, 5, 6, 7, 61, 64, 67 | dihjatcc 41424 |
. 2
⊢ ((𝜑 ∧ (¬ 𝑃(le‘𝐾)𝑊 ∧ ¬ 𝑄(le‘𝐾)𝑊)) → (𝐼‘(𝑃 ∨ 𝑄)) = ((𝐼‘𝑃) ⊕ (𝐼‘𝑄))) |
| 69 | 18, 29, 60, 68 | 4casesdan 1042 |
1
⊢ (𝜑 → (𝐼‘(𝑃 ∨ 𝑄)) = ((𝐼‘𝑃) ⊕ (𝐼‘𝑄))) |