Proof of Theorem cdlemn5pre
| Step | Hyp | Ref
| Expression |
|---|
| 1 | | simp1 1136 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ 𝑅 ≤ (𝑄 ∨ 𝑋)) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
| 2 | | simp22 1207 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ 𝑅 ≤ (𝑄 ∨ 𝑋)) → (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) |
| 3 | | cdlemn5.l |
. . . 4
⊢ ≤ =
(le‘𝐾) |
| 4 | | cdlemn5.a |
. . . 4
⊢ 𝐴 = (Atoms‘𝐾) |
| 5 | | cdlemn5.h |
. . . 4
⊢ 𝐻 = (LHyp‘𝐾) |
| 6 | | cdlemn5.p |
. . . 4
⊢ 𝑃 = ((oc‘𝐾)‘𝑊) |
| 7 | | cdlemn5.t |
. . . 4
⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) |
| 8 | | cdlemn5.J |
. . . 4
⊢ 𝐽 = ((DIsoC‘𝐾)‘𝑊) |
| 9 | | cdlemn5.u |
. . . 4
⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) |
| 10 | | cdlemn5.n |
. . . 4
⊢ 𝑁 = (LSpan‘𝑈) |
| 11 | | cdlemn5.g |
. . . 4
⊢ 𝐺 = (℩ℎ ∈ 𝑇 (ℎ‘𝑃) = 𝑅) |
| 12 | 3, 4, 5, 6, 7, 8, 9, 10, 11 | diclspsn 41197 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) → (𝐽‘𝑅) = (𝑁‘{⟨𝐺, ( I ↾ 𝑇)⟩})) |
| 13 | 1, 2, 12 | syl2anc 584 |
. 2
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ 𝑅 ≤ (𝑄 ∨ 𝑋)) → (𝐽‘𝑅) = (𝑁‘{⟨𝐺, ( I ↾ 𝑇)⟩})) |
| 14 | | simp21 1206 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ 𝑅 ≤ (𝑄 ∨ 𝑋)) → (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) |
| 15 | | cdlemn5.b |
. . . . . 6
⊢ 𝐵 = (Base‘𝐾) |
| 16 | | cdlemn5.o |
. . . . . 6
⊢ 𝑂 = (ℎ ∈ 𝑇 ↦ ( I ↾ 𝐵)) |
| 17 | | cdlemn5.f |
. . . . . 6
⊢ 𝐹 = (℩ℎ ∈ 𝑇 (ℎ‘𝑃) = 𝑄) |
| 18 | | cdlemn5.m |
. . . . . 6
⊢ 𝑀 = (℩ℎ ∈ 𝑇 (ℎ‘𝑄) = 𝑅) |
| 19 | | cdlemn5.s |
. . . . . 6
⊢ ⊕ =
(LSSum‘𝑈) |
| 20 | 15, 3, 4, 6, 5, 7, 16, 9, 17, 11, 18, 10, 19 | cdlemn4a 41202 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) → (𝑁‘{⟨𝐺, ( I ↾ 𝑇)⟩}) ⊆ ((𝑁‘{⟨𝐹, ( I ↾ 𝑇)⟩}) ⊕ (𝑁‘{⟨𝑀, 𝑂⟩}))) |
| 21 | 1, 14, 2, 20 | syl3anc 1372 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ 𝑅 ≤ (𝑄 ∨ 𝑋)) → (𝑁‘{⟨𝐺, ( I ↾ 𝑇)⟩}) ⊆ ((𝑁‘{⟨𝐹, ( I ↾ 𝑇)⟩}) ⊕ (𝑁‘{⟨𝑀, 𝑂⟩}))) |
| 22 | 3, 4, 5, 6, 7, 8, 9, 10, 17 | diclspsn 41197 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → (𝐽‘𝑄) = (𝑁‘{⟨𝐹, ( I ↾ 𝑇)⟩})) |
| 23 | 1, 14, 22 | syl2anc 584 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ 𝑅 ≤ (𝑄 ∨ 𝑋)) → (𝐽‘𝑄) = (𝑁‘{⟨𝐹, ( I ↾ 𝑇)⟩})) |
| 24 | 23 | oveq1d 7447 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ 𝑅 ≤ (𝑄 ∨ 𝑋)) → ((𝐽‘𝑄) ⊕ (𝑁‘{⟨𝑀, 𝑂⟩})) = ((𝑁‘{⟨𝐹, ( I ↾ 𝑇)⟩}) ⊕ (𝑁‘{⟨𝑀, 𝑂⟩}))) |
| 25 | 21, 24 | sseqtrrd 4020 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ 𝑅 ≤ (𝑄 ∨ 𝑋)) → (𝑁‘{⟨𝐺, ( I ↾ 𝑇)⟩}) ⊆ ((𝐽‘𝑄) ⊕ (𝑁‘{⟨𝑀, 𝑂⟩}))) |
| 26 | 5, 9, 1 | dvhlmod 41113 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ 𝑅 ≤ (𝑄 ∨ 𝑋)) → 𝑈 ∈ LMod) |
| 27 | | eqid 2736 |
. . . . . . 7
⊢
(LSubSp‘𝑈) =
(LSubSp‘𝑈) |
| 28 | 27 | lsssssubg 20957 |
. . . . . 6
⊢ (𝑈 ∈ LMod →
(LSubSp‘𝑈) ⊆
(SubGrp‘𝑈)) |
| 29 | 26, 28 | syl 17 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ 𝑅 ≤ (𝑄 ∨ 𝑋)) → (LSubSp‘𝑈) ⊆ (SubGrp‘𝑈)) |
| 30 | 3, 4, 5, 9, 8, 27 | diclss 41196 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → (𝐽‘𝑄) ∈ (LSubSp‘𝑈)) |
| 31 | 1, 14, 30 | syl2anc 584 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ 𝑅 ≤ (𝑄 ∨ 𝑋)) → (𝐽‘𝑄) ∈ (LSubSp‘𝑈)) |
| 32 | 29, 31 | sseldd 3983 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ 𝑅 ≤ (𝑄 ∨ 𝑋)) → (𝐽‘𝑄) ∈ (SubGrp‘𝑈)) |
| 33 | | simp23 1208 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ 𝑅 ≤ (𝑄 ∨ 𝑋)) → (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) |
| 34 | | cdlemn5.i |
. . . . . . 7
⊢ 𝐼 = ((DIsoB‘𝐾)‘𝑊) |
| 35 | 15, 3, 5, 9, 34, 27 | diblss 41173 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) → (𝐼‘𝑋) ∈ (LSubSp‘𝑈)) |
| 36 | 1, 33, 35 | syl2anc 584 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ 𝑅 ≤ (𝑄 ∨ 𝑋)) → (𝐼‘𝑋) ∈ (LSubSp‘𝑈)) |
| 37 | 29, 36 | sseldd 3983 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ 𝑅 ≤ (𝑄 ∨ 𝑋)) → (𝐼‘𝑋) ∈ (SubGrp‘𝑈)) |
| 38 | | cdlemn5.j |
. . . . 5
⊢ ∨ =
(join‘𝐾) |
| 39 | | eqid 2736 |
. . . . 5
⊢
((trL‘𝐾)‘𝑊) = ((trL‘𝐾)‘𝑊) |
| 40 | 15, 3, 38, 4, 5, 7,
39, 16, 34, 9, 10, 18 | cdlemn2a 41199 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ 𝑅 ≤ (𝑄 ∨ 𝑋)) → (𝑁‘{⟨𝑀, 𝑂⟩}) ⊆ (𝐼‘𝑋)) |
| 41 | 19 | lsmless2 19680 |
. . . 4
⊢ (((𝐽‘𝑄) ∈ (SubGrp‘𝑈) ∧ (𝐼‘𝑋) ∈ (SubGrp‘𝑈) ∧ (𝑁‘{⟨𝑀, 𝑂⟩}) ⊆ (𝐼‘𝑋)) → ((𝐽‘𝑄) ⊕ (𝑁‘{⟨𝑀, 𝑂⟩})) ⊆ ((𝐽‘𝑄) ⊕ (𝐼‘𝑋))) |
| 42 | 32, 37, 40, 41 | syl3anc 1372 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ 𝑅 ≤ (𝑄 ∨ 𝑋)) → ((𝐽‘𝑄) ⊕ (𝑁‘{⟨𝑀, 𝑂⟩})) ⊆ ((𝐽‘𝑄) ⊕ (𝐼‘𝑋))) |
| 43 | 25, 42 | sstrd 3993 |
. 2
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ 𝑅 ≤ (𝑄 ∨ 𝑋)) → (𝑁‘{⟨𝐺, ( I ↾ 𝑇)⟩}) ⊆ ((𝐽‘𝑄) ⊕ (𝐼‘𝑋))) |
| 44 | 13, 43 | eqsstrd 4017 |
1
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ 𝑅 ≤ (𝑄 ∨ 𝑋)) → (𝐽‘𝑅) ⊆ ((𝐽‘𝑄) ⊕ (𝐼‘𝑋))) |
