Proof of Theorem dihjatcclem1
Step | Hyp | Ref
| Expression |
1 | | dihjatcclem.h |
. . . . 5
⊢ 𝐻 = (LHyp‘𝐾) |
2 | | dihjatcclem.u |
. . . . 5
⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) |
3 | | dihjatcclem.k |
. . . . 5
⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
4 | 1, 2, 3 | dvhlmod 38736 |
. . . 4
⊢ (𝜑 → 𝑈 ∈ LMod) |
5 | | lmodabl 19793 |
. . . 4
⊢ (𝑈 ∈ LMod → 𝑈 ∈ Abel) |
6 | 4, 5 | syl 17 |
. . 3
⊢ (𝜑 → 𝑈 ∈ Abel) |
7 | | eqid 2738 |
. . . . . 6
⊢
(LSubSp‘𝑈) =
(LSubSp‘𝑈) |
8 | 7 | lsssssubg 19842 |
. . . . 5
⊢ (𝑈 ∈ LMod →
(LSubSp‘𝑈) ⊆
(SubGrp‘𝑈)) |
9 | 4, 8 | syl 17 |
. . . 4
⊢ (𝜑 → (LSubSp‘𝑈) ⊆ (SubGrp‘𝑈)) |
10 | | dihjatcclem.p |
. . . . . . 7
⊢ (𝜑 → (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) |
11 | 10 | simpld 498 |
. . . . . 6
⊢ (𝜑 → 𝑃 ∈ 𝐴) |
12 | | dihjatcclem.b |
. . . . . . 7
⊢ 𝐵 = (Base‘𝐾) |
13 | | dihjatcclem.a |
. . . . . . 7
⊢ 𝐴 = (Atoms‘𝐾) |
14 | 12, 13 | atbase 36915 |
. . . . . 6
⊢ (𝑃 ∈ 𝐴 → 𝑃 ∈ 𝐵) |
15 | 11, 14 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝑃 ∈ 𝐵) |
16 | | dihjatcclem.i |
. . . . . 6
⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊) |
17 | 12, 1, 16, 2, 7 | dihlss 38876 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ∈ 𝐵) → (𝐼‘𝑃) ∈ (LSubSp‘𝑈)) |
18 | 3, 15, 17 | syl2anc 587 |
. . . 4
⊢ (𝜑 → (𝐼‘𝑃) ∈ (LSubSp‘𝑈)) |
19 | 9, 18 | sseldd 3876 |
. . 3
⊢ (𝜑 → (𝐼‘𝑃) ∈ (SubGrp‘𝑈)) |
20 | | dihjatcclem.v |
. . . . . 6
⊢ 𝑉 = ((𝑃 ∨ 𝑄) ∧ 𝑊) |
21 | 3 | simpld 498 |
. . . . . . . 8
⊢ (𝜑 → 𝐾 ∈ HL) |
22 | 21 | hllatd 36990 |
. . . . . . 7
⊢ (𝜑 → 𝐾 ∈ Lat) |
23 | | dihjatcclem.q |
. . . . . . . . 9
⊢ (𝜑 → (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) |
24 | 23 | simpld 498 |
. . . . . . . 8
⊢ (𝜑 → 𝑄 ∈ 𝐴) |
25 | | dihjatcclem.j |
. . . . . . . . 9
⊢ ∨ =
(join‘𝐾) |
26 | 12, 25, 13 | hlatjcl 36993 |
. . . . . . . 8
⊢ ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) → (𝑃 ∨ 𝑄) ∈ 𝐵) |
27 | 21, 11, 24, 26 | syl3anc 1372 |
. . . . . . 7
⊢ (𝜑 → (𝑃 ∨ 𝑄) ∈ 𝐵) |
28 | 3 | simprd 499 |
. . . . . . . 8
⊢ (𝜑 → 𝑊 ∈ 𝐻) |
29 | 12, 1 | lhpbase 37624 |
. . . . . . . 8
⊢ (𝑊 ∈ 𝐻 → 𝑊 ∈ 𝐵) |
30 | 28, 29 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝑊 ∈ 𝐵) |
31 | | dihjatcclem.m |
. . . . . . . 8
⊢ ∧ =
(meet‘𝐾) |
32 | 12, 31 | latmcl 17771 |
. . . . . . 7
⊢ ((𝐾 ∈ Lat ∧ (𝑃 ∨ 𝑄) ∈ 𝐵 ∧ 𝑊 ∈ 𝐵) → ((𝑃 ∨ 𝑄) ∧ 𝑊) ∈ 𝐵) |
33 | 22, 27, 30, 32 | syl3anc 1372 |
. . . . . 6
⊢ (𝜑 → ((𝑃 ∨ 𝑄) ∧ 𝑊) ∈ 𝐵) |
34 | 20, 33 | eqeltrid 2837 |
. . . . 5
⊢ (𝜑 → 𝑉 ∈ 𝐵) |
35 | 12, 1, 16, 2, 7 | dihlss 38876 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑉 ∈ 𝐵) → (𝐼‘𝑉) ∈ (LSubSp‘𝑈)) |
36 | 3, 34, 35 | syl2anc 587 |
. . . 4
⊢ (𝜑 → (𝐼‘𝑉) ∈ (LSubSp‘𝑈)) |
37 | 9, 36 | sseldd 3876 |
. . 3
⊢ (𝜑 → (𝐼‘𝑉) ∈ (SubGrp‘𝑈)) |
38 | 12, 13 | atbase 36915 |
. . . . . 6
⊢ (𝑄 ∈ 𝐴 → 𝑄 ∈ 𝐵) |
39 | 24, 38 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝑄 ∈ 𝐵) |
40 | 12, 1, 16, 2, 7 | dihlss 38876 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑄 ∈ 𝐵) → (𝐼‘𝑄) ∈ (LSubSp‘𝑈)) |
41 | 3, 39, 40 | syl2anc 587 |
. . . 4
⊢ (𝜑 → (𝐼‘𝑄) ∈ (LSubSp‘𝑈)) |
42 | 9, 41 | sseldd 3876 |
. . 3
⊢ (𝜑 → (𝐼‘𝑄) ∈ (SubGrp‘𝑈)) |
43 | | dihjatcclem.s |
. . . 4
⊢ ⊕ =
(LSSum‘𝑈) |
44 | 43 | lsm4 19092 |
. . 3
⊢ ((𝑈 ∈ Abel ∧ ((𝐼‘𝑃) ∈ (SubGrp‘𝑈) ∧ (𝐼‘𝑉) ∈ (SubGrp‘𝑈)) ∧ ((𝐼‘𝑄) ∈ (SubGrp‘𝑈) ∧ (𝐼‘𝑉) ∈ (SubGrp‘𝑈))) → (((𝐼‘𝑃) ⊕ (𝐼‘𝑉)) ⊕ ((𝐼‘𝑄) ⊕ (𝐼‘𝑉))) = (((𝐼‘𝑃) ⊕ (𝐼‘𝑄)) ⊕ ((𝐼‘𝑉) ⊕ (𝐼‘𝑉)))) |
45 | 6, 19, 37, 42, 37, 44 | syl122anc 1380 |
. 2
⊢ (𝜑 → (((𝐼‘𝑃) ⊕ (𝐼‘𝑉)) ⊕ ((𝐼‘𝑄) ⊕ (𝐼‘𝑉))) = (((𝐼‘𝑃) ⊕ (𝐼‘𝑄)) ⊕ ((𝐼‘𝑉) ⊕ (𝐼‘𝑉)))) |
46 | 23 | simprd 499 |
. . . . . . . 8
⊢ (𝜑 → ¬ 𝑄 ≤ 𝑊) |
47 | 46 | intnand 492 |
. . . . . . 7
⊢ (𝜑 → ¬ (𝑃 ≤ 𝑊 ∧ 𝑄 ≤ 𝑊)) |
48 | | dihjatcclem.l |
. . . . . . . . 9
⊢ ≤ =
(le‘𝐾) |
49 | 12, 48, 25 | latjle12 17781 |
. . . . . . . 8
⊢ ((𝐾 ∈ Lat ∧ (𝑃 ∈ 𝐵 ∧ 𝑄 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵)) → ((𝑃 ≤ 𝑊 ∧ 𝑄 ≤ 𝑊) ↔ (𝑃 ∨ 𝑄) ≤ 𝑊)) |
50 | 22, 15, 39, 30, 49 | syl13anc 1373 |
. . . . . . 7
⊢ (𝜑 → ((𝑃 ≤ 𝑊 ∧ 𝑄 ≤ 𝑊) ↔ (𝑃 ∨ 𝑄) ≤ 𝑊)) |
51 | 47, 50 | mtbid 327 |
. . . . . 6
⊢ (𝜑 → ¬ (𝑃 ∨ 𝑄) ≤ 𝑊) |
52 | 48, 25, 13 | hlatlej1 37001 |
. . . . . . 7
⊢ ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) → 𝑃 ≤ (𝑃 ∨ 𝑄)) |
53 | 21, 11, 24, 52 | syl3anc 1372 |
. . . . . 6
⊢ (𝜑 → 𝑃 ≤ (𝑃 ∨ 𝑄)) |
54 | 12, 48, 25, 31, 13, 1, 16, 2, 43 | dihvalcq2 38873 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∨ 𝑄) ∈ 𝐵 ∧ ¬ (𝑃 ∨ 𝑄) ≤ 𝑊) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝑃 ≤ (𝑃 ∨ 𝑄))) → (𝐼‘(𝑃 ∨ 𝑄)) = ((𝐼‘𝑃) ⊕ (𝐼‘((𝑃 ∨ 𝑄) ∧ 𝑊)))) |
55 | 3, 27, 51, 10, 53, 54 | syl122anc 1380 |
. . . . 5
⊢ (𝜑 → (𝐼‘(𝑃 ∨ 𝑄)) = ((𝐼‘𝑃) ⊕ (𝐼‘((𝑃 ∨ 𝑄) ∧ 𝑊)))) |
56 | 20 | fveq2i 6671 |
. . . . . 6
⊢ (𝐼‘𝑉) = (𝐼‘((𝑃 ∨ 𝑄) ∧ 𝑊)) |
57 | 56 | oveq2i 7175 |
. . . . 5
⊢ ((𝐼‘𝑃) ⊕ (𝐼‘𝑉)) = ((𝐼‘𝑃) ⊕ (𝐼‘((𝑃 ∨ 𝑄) ∧ 𝑊))) |
58 | 55, 57 | eqtr4di 2791 |
. . . 4
⊢ (𝜑 → (𝐼‘(𝑃 ∨ 𝑄)) = ((𝐼‘𝑃) ⊕ (𝐼‘𝑉))) |
59 | 48, 25, 13 | hlatlej2 37002 |
. . . . . . 7
⊢ ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) → 𝑄 ≤ (𝑃 ∨ 𝑄)) |
60 | 21, 11, 24, 59 | syl3anc 1372 |
. . . . . 6
⊢ (𝜑 → 𝑄 ≤ (𝑃 ∨ 𝑄)) |
61 | 12, 48, 25, 31, 13, 1, 16, 2, 43 | dihvalcq2 38873 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∨ 𝑄) ∈ 𝐵 ∧ ¬ (𝑃 ∨ 𝑄) ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑄 ≤ (𝑃 ∨ 𝑄))) → (𝐼‘(𝑃 ∨ 𝑄)) = ((𝐼‘𝑄) ⊕ (𝐼‘((𝑃 ∨ 𝑄) ∧ 𝑊)))) |
62 | 3, 27, 51, 23, 60, 61 | syl122anc 1380 |
. . . . 5
⊢ (𝜑 → (𝐼‘(𝑃 ∨ 𝑄)) = ((𝐼‘𝑄) ⊕ (𝐼‘((𝑃 ∨ 𝑄) ∧ 𝑊)))) |
63 | 56 | oveq2i 7175 |
. . . . 5
⊢ ((𝐼‘𝑄) ⊕ (𝐼‘𝑉)) = ((𝐼‘𝑄) ⊕ (𝐼‘((𝑃 ∨ 𝑄) ∧ 𝑊))) |
64 | 62, 63 | eqtr4di 2791 |
. . . 4
⊢ (𝜑 → (𝐼‘(𝑃 ∨ 𝑄)) = ((𝐼‘𝑄) ⊕ (𝐼‘𝑉))) |
65 | 58, 64 | oveq12d 7182 |
. . 3
⊢ (𝜑 → ((𝐼‘(𝑃 ∨ 𝑄)) ⊕ (𝐼‘(𝑃 ∨ 𝑄))) = (((𝐼‘𝑃) ⊕ (𝐼‘𝑉)) ⊕ ((𝐼‘𝑄) ⊕ (𝐼‘𝑉)))) |
66 | 12, 1, 16, 2, 7 | dihlss 38876 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∨ 𝑄) ∈ 𝐵) → (𝐼‘(𝑃 ∨ 𝑄)) ∈ (LSubSp‘𝑈)) |
67 | 3, 27, 66 | syl2anc 587 |
. . . . 5
⊢ (𝜑 → (𝐼‘(𝑃 ∨ 𝑄)) ∈ (LSubSp‘𝑈)) |
68 | 9, 67 | sseldd 3876 |
. . . 4
⊢ (𝜑 → (𝐼‘(𝑃 ∨ 𝑄)) ∈ (SubGrp‘𝑈)) |
69 | 43 | lsmidm 18899 |
. . . 4
⊢ ((𝐼‘(𝑃 ∨ 𝑄)) ∈ (SubGrp‘𝑈) → ((𝐼‘(𝑃 ∨ 𝑄)) ⊕ (𝐼‘(𝑃 ∨ 𝑄))) = (𝐼‘(𝑃 ∨ 𝑄))) |
70 | 68, 69 | syl 17 |
. . 3
⊢ (𝜑 → ((𝐼‘(𝑃 ∨ 𝑄)) ⊕ (𝐼‘(𝑃 ∨ 𝑄))) = (𝐼‘(𝑃 ∨ 𝑄))) |
71 | 65, 70 | eqtr3d 2775 |
. 2
⊢ (𝜑 → (((𝐼‘𝑃) ⊕ (𝐼‘𝑉)) ⊕ ((𝐼‘𝑄) ⊕ (𝐼‘𝑉))) = (𝐼‘(𝑃 ∨ 𝑄))) |
72 | 43 | lsmidm 18899 |
. . . 4
⊢ ((𝐼‘𝑉) ∈ (SubGrp‘𝑈) → ((𝐼‘𝑉) ⊕ (𝐼‘𝑉)) = (𝐼‘𝑉)) |
73 | 37, 72 | syl 17 |
. . 3
⊢ (𝜑 → ((𝐼‘𝑉) ⊕ (𝐼‘𝑉)) = (𝐼‘𝑉)) |
74 | 73 | oveq2d 7180 |
. 2
⊢ (𝜑 → (((𝐼‘𝑃) ⊕ (𝐼‘𝑄)) ⊕ ((𝐼‘𝑉) ⊕ (𝐼‘𝑉))) = (((𝐼‘𝑃) ⊕ (𝐼‘𝑄)) ⊕ (𝐼‘𝑉))) |
75 | 45, 71, 74 | 3eqtr3d 2781 |
1
⊢ (𝜑 → (𝐼‘(𝑃 ∨ 𝑄)) = (((𝐼‘𝑃) ⊕ (𝐼‘𝑄)) ⊕ (𝐼‘𝑉))) |