Proof of Theorem lsmelval2
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | lsmelval2.w | . . . . . 6
⊢ (𝜑 → 𝑊 ∈ LMod) | 
| 2 |  | lsmelval2.t | . . . . . 6
⊢ (𝜑 → 𝑇 ∈ 𝑆) | 
| 3 |  | lsmelval2.s | . . . . . . 7
⊢ 𝑆 = (LSubSp‘𝑊) | 
| 4 | 3 | lsssubg 20956 | . . . . . 6
⊢ ((𝑊 ∈ LMod ∧ 𝑇 ∈ 𝑆) → 𝑇 ∈ (SubGrp‘𝑊)) | 
| 5 | 1, 2, 4 | syl2anc 584 | . . . . 5
⊢ (𝜑 → 𝑇 ∈ (SubGrp‘𝑊)) | 
| 6 |  | lsmelval2.u | . . . . . 6
⊢ (𝜑 → 𝑈 ∈ 𝑆) | 
| 7 | 3 | lsssubg 20956 | . . . . . 6
⊢ ((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆) → 𝑈 ∈ (SubGrp‘𝑊)) | 
| 8 | 1, 6, 7 | syl2anc 584 | . . . . 5
⊢ (𝜑 → 𝑈 ∈ (SubGrp‘𝑊)) | 
| 9 |  | eqid 2736 | . . . . . 6
⊢
(+g‘𝑊) = (+g‘𝑊) | 
| 10 |  | lsmelval2.p | . . . . . 6
⊢  ⊕ =
(LSSum‘𝑊) | 
| 11 | 9, 10 | lsmelval 19668 | . . . . 5
⊢ ((𝑇 ∈ (SubGrp‘𝑊) ∧ 𝑈 ∈ (SubGrp‘𝑊)) → (𝑋 ∈ (𝑇 ⊕ 𝑈) ↔ ∃𝑦 ∈ 𝑇 ∃𝑧 ∈ 𝑈 𝑋 = (𝑦(+g‘𝑊)𝑧))) | 
| 12 | 5, 8, 11 | syl2anc 584 | . . . 4
⊢ (𝜑 → (𝑋 ∈ (𝑇 ⊕ 𝑈) ↔ ∃𝑦 ∈ 𝑇 ∃𝑧 ∈ 𝑈 𝑋 = (𝑦(+g‘𝑊)𝑧))) | 
| 13 | 1 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈)) → 𝑊 ∈ LMod) | 
| 14 | 2 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈)) → 𝑇 ∈ 𝑆) | 
| 15 |  | simprl 770 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈)) → 𝑦 ∈ 𝑇) | 
| 16 |  | lsmelval2.v | . . . . . . . . . . . 12
⊢ 𝑉 = (Base‘𝑊) | 
| 17 | 16, 3 | lssel 20936 | . . . . . . . . . . 11
⊢ ((𝑇 ∈ 𝑆 ∧ 𝑦 ∈ 𝑇) → 𝑦 ∈ 𝑉) | 
| 18 | 14, 15, 17 | syl2anc 584 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈)) → 𝑦 ∈ 𝑉) | 
| 19 |  | lsmelval2.n | . . . . . . . . . . 11
⊢ 𝑁 = (LSpan‘𝑊) | 
| 20 | 16, 3, 19 | lspsncl 20976 | . . . . . . . . . 10
⊢ ((𝑊 ∈ LMod ∧ 𝑦 ∈ 𝑉) → (𝑁‘{𝑦}) ∈ 𝑆) | 
| 21 | 13, 18, 20 | syl2anc 584 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈)) → (𝑁‘{𝑦}) ∈ 𝑆) | 
| 22 | 3 | lsssubg 20956 | . . . . . . . . 9
⊢ ((𝑊 ∈ LMod ∧ (𝑁‘{𝑦}) ∈ 𝑆) → (𝑁‘{𝑦}) ∈ (SubGrp‘𝑊)) | 
| 23 | 13, 21, 22 | syl2anc 584 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈)) → (𝑁‘{𝑦}) ∈ (SubGrp‘𝑊)) | 
| 24 | 6 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈)) → 𝑈 ∈ 𝑆) | 
| 25 |  | simprr 772 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈)) → 𝑧 ∈ 𝑈) | 
| 26 | 16, 3 | lssel 20936 | . . . . . . . . . . 11
⊢ ((𝑈 ∈ 𝑆 ∧ 𝑧 ∈ 𝑈) → 𝑧 ∈ 𝑉) | 
| 27 | 24, 25, 26 | syl2anc 584 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈)) → 𝑧 ∈ 𝑉) | 
| 28 | 16, 3, 19 | lspsncl 20976 | . . . . . . . . . 10
⊢ ((𝑊 ∈ LMod ∧ 𝑧 ∈ 𝑉) → (𝑁‘{𝑧}) ∈ 𝑆) | 
| 29 | 13, 27, 28 | syl2anc 584 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈)) → (𝑁‘{𝑧}) ∈ 𝑆) | 
| 30 | 3 | lsssubg 20956 | . . . . . . . . 9
⊢ ((𝑊 ∈ LMod ∧ (𝑁‘{𝑧}) ∈ 𝑆) → (𝑁‘{𝑧}) ∈ (SubGrp‘𝑊)) | 
| 31 | 13, 29, 30 | syl2anc 584 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈)) → (𝑁‘{𝑧}) ∈ (SubGrp‘𝑊)) | 
| 32 | 16, 19 | lspsnid 20992 | . . . . . . . . 9
⊢ ((𝑊 ∈ LMod ∧ 𝑦 ∈ 𝑉) → 𝑦 ∈ (𝑁‘{𝑦})) | 
| 33 | 13, 18, 32 | syl2anc 584 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈)) → 𝑦 ∈ (𝑁‘{𝑦})) | 
| 34 | 16, 19 | lspsnid 20992 | . . . . . . . . 9
⊢ ((𝑊 ∈ LMod ∧ 𝑧 ∈ 𝑉) → 𝑧 ∈ (𝑁‘{𝑧})) | 
| 35 | 13, 27, 34 | syl2anc 584 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈)) → 𝑧 ∈ (𝑁‘{𝑧})) | 
| 36 | 9, 10 | lsmelvali 19669 | . . . . . . . 8
⊢ ((((𝑁‘{𝑦}) ∈ (SubGrp‘𝑊) ∧ (𝑁‘{𝑧}) ∈ (SubGrp‘𝑊)) ∧ (𝑦 ∈ (𝑁‘{𝑦}) ∧ 𝑧 ∈ (𝑁‘{𝑧}))) → (𝑦(+g‘𝑊)𝑧) ∈ ((𝑁‘{𝑦}) ⊕ (𝑁‘{𝑧}))) | 
| 37 | 23, 31, 33, 35, 36 | syl22anc 838 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈)) → (𝑦(+g‘𝑊)𝑧) ∈ ((𝑁‘{𝑦}) ⊕ (𝑁‘{𝑧}))) | 
| 38 |  | eleq1a 2835 | . . . . . . 7
⊢ ((𝑦(+g‘𝑊)𝑧) ∈ ((𝑁‘{𝑦}) ⊕ (𝑁‘{𝑧})) → (𝑋 = (𝑦(+g‘𝑊)𝑧) → 𝑋 ∈ ((𝑁‘{𝑦}) ⊕ (𝑁‘{𝑧})))) | 
| 39 | 37, 38 | syl 17 | . . . . . 6
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈)) → (𝑋 = (𝑦(+g‘𝑊)𝑧) → 𝑋 ∈ ((𝑁‘{𝑦}) ⊕ (𝑁‘{𝑧})))) | 
| 40 | 3, 10 | lsmcl 21083 | . . . . . . . 8
⊢ ((𝑊 ∈ LMod ∧ (𝑁‘{𝑦}) ∈ 𝑆 ∧ (𝑁‘{𝑧}) ∈ 𝑆) → ((𝑁‘{𝑦}) ⊕ (𝑁‘{𝑧})) ∈ 𝑆) | 
| 41 | 13, 21, 29, 40 | syl3anc 1372 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈)) → ((𝑁‘{𝑦}) ⊕ (𝑁‘{𝑧})) ∈ 𝑆) | 
| 42 | 16, 3, 19, 13, 41 | ellspsn6 20993 | . . . . . 6
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈)) → (𝑋 ∈ ((𝑁‘{𝑦}) ⊕ (𝑁‘{𝑧})) ↔ (𝑋 ∈ 𝑉 ∧ (𝑁‘{𝑋}) ⊆ ((𝑁‘{𝑦}) ⊕ (𝑁‘{𝑧}))))) | 
| 43 | 39, 42 | sylibd 239 | . . . . 5
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈)) → (𝑋 = (𝑦(+g‘𝑊)𝑧) → (𝑋 ∈ 𝑉 ∧ (𝑁‘{𝑋}) ⊆ ((𝑁‘{𝑦}) ⊕ (𝑁‘{𝑧}))))) | 
| 44 | 43 | reximdvva 3206 | . . . 4
⊢ (𝜑 → (∃𝑦 ∈ 𝑇 ∃𝑧 ∈ 𝑈 𝑋 = (𝑦(+g‘𝑊)𝑧) → ∃𝑦 ∈ 𝑇 ∃𝑧 ∈ 𝑈 (𝑋 ∈ 𝑉 ∧ (𝑁‘{𝑋}) ⊆ ((𝑁‘{𝑦}) ⊕ (𝑁‘{𝑧}))))) | 
| 45 | 12, 44 | sylbid 240 | . . 3
⊢ (𝜑 → (𝑋 ∈ (𝑇 ⊕ 𝑈) → ∃𝑦 ∈ 𝑇 ∃𝑧 ∈ 𝑈 (𝑋 ∈ 𝑉 ∧ (𝑁‘{𝑋}) ⊆ ((𝑁‘{𝑦}) ⊕ (𝑁‘{𝑧}))))) | 
| 46 | 5 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈)) → 𝑇 ∈ (SubGrp‘𝑊)) | 
| 47 | 3, 19, 13, 14, 15 | ellspsn5 20995 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈)) → (𝑁‘{𝑦}) ⊆ 𝑇) | 
| 48 | 10 | lsmless1 19679 | . . . . . . . 8
⊢ ((𝑇 ∈ (SubGrp‘𝑊) ∧ (𝑁‘{𝑧}) ∈ (SubGrp‘𝑊) ∧ (𝑁‘{𝑦}) ⊆ 𝑇) → ((𝑁‘{𝑦}) ⊕ (𝑁‘{𝑧})) ⊆ (𝑇 ⊕ (𝑁‘{𝑧}))) | 
| 49 | 46, 31, 47, 48 | syl3anc 1372 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈)) → ((𝑁‘{𝑦}) ⊕ (𝑁‘{𝑧})) ⊆ (𝑇 ⊕ (𝑁‘{𝑧}))) | 
| 50 | 8 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈)) → 𝑈 ∈ (SubGrp‘𝑊)) | 
| 51 | 3, 19, 13, 24, 25 | ellspsn5 20995 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈)) → (𝑁‘{𝑧}) ⊆ 𝑈) | 
| 52 | 10 | lsmless2 19680 | . . . . . . . 8
⊢ ((𝑇 ∈ (SubGrp‘𝑊) ∧ 𝑈 ∈ (SubGrp‘𝑊) ∧ (𝑁‘{𝑧}) ⊆ 𝑈) → (𝑇 ⊕ (𝑁‘{𝑧})) ⊆ (𝑇 ⊕ 𝑈)) | 
| 53 | 46, 50, 51, 52 | syl3anc 1372 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈)) → (𝑇 ⊕ (𝑁‘{𝑧})) ⊆ (𝑇 ⊕ 𝑈)) | 
| 54 | 49, 53 | sstrd 3993 | . . . . . 6
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈)) → ((𝑁‘{𝑦}) ⊕ (𝑁‘{𝑧})) ⊆ (𝑇 ⊕ 𝑈)) | 
| 55 | 54 | sseld 3981 | . . . . 5
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈)) → (𝑋 ∈ ((𝑁‘{𝑦}) ⊕ (𝑁‘{𝑧})) → 𝑋 ∈ (𝑇 ⊕ 𝑈))) | 
| 56 | 42, 55 | sylbird 260 | . . . 4
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈)) → ((𝑋 ∈ 𝑉 ∧ (𝑁‘{𝑋}) ⊆ ((𝑁‘{𝑦}) ⊕ (𝑁‘{𝑧}))) → 𝑋 ∈ (𝑇 ⊕ 𝑈))) | 
| 57 | 56 | rexlimdvva 3212 | . . 3
⊢ (𝜑 → (∃𝑦 ∈ 𝑇 ∃𝑧 ∈ 𝑈 (𝑋 ∈ 𝑉 ∧ (𝑁‘{𝑋}) ⊆ ((𝑁‘{𝑦}) ⊕ (𝑁‘{𝑧}))) → 𝑋 ∈ (𝑇 ⊕ 𝑈))) | 
| 58 | 45, 57 | impbid 212 | . 2
⊢ (𝜑 → (𝑋 ∈ (𝑇 ⊕ 𝑈) ↔ ∃𝑦 ∈ 𝑇 ∃𝑧 ∈ 𝑈 (𝑋 ∈ 𝑉 ∧ (𝑁‘{𝑋}) ⊆ ((𝑁‘{𝑦}) ⊕ (𝑁‘{𝑧}))))) | 
| 59 |  | r19.42v 3190 | . . . 4
⊢
(∃𝑧 ∈
𝑈 (𝑋 ∈ 𝑉 ∧ (𝑁‘{𝑋}) ⊆ ((𝑁‘{𝑦}) ⊕ (𝑁‘{𝑧}))) ↔ (𝑋 ∈ 𝑉 ∧ ∃𝑧 ∈ 𝑈 (𝑁‘{𝑋}) ⊆ ((𝑁‘{𝑦}) ⊕ (𝑁‘{𝑧})))) | 
| 60 | 59 | rexbii 3093 | . . 3
⊢
(∃𝑦 ∈
𝑇 ∃𝑧 ∈ 𝑈 (𝑋 ∈ 𝑉 ∧ (𝑁‘{𝑋}) ⊆ ((𝑁‘{𝑦}) ⊕ (𝑁‘{𝑧}))) ↔ ∃𝑦 ∈ 𝑇 (𝑋 ∈ 𝑉 ∧ ∃𝑧 ∈ 𝑈 (𝑁‘{𝑋}) ⊆ ((𝑁‘{𝑦}) ⊕ (𝑁‘{𝑧})))) | 
| 61 |  | r19.42v 3190 | . . 3
⊢
(∃𝑦 ∈
𝑇 (𝑋 ∈ 𝑉 ∧ ∃𝑧 ∈ 𝑈 (𝑁‘{𝑋}) ⊆ ((𝑁‘{𝑦}) ⊕ (𝑁‘{𝑧}))) ↔ (𝑋 ∈ 𝑉 ∧ ∃𝑦 ∈ 𝑇 ∃𝑧 ∈ 𝑈 (𝑁‘{𝑋}) ⊆ ((𝑁‘{𝑦}) ⊕ (𝑁‘{𝑧})))) | 
| 62 | 60, 61 | bitri 275 | . 2
⊢
(∃𝑦 ∈
𝑇 ∃𝑧 ∈ 𝑈 (𝑋 ∈ 𝑉 ∧ (𝑁‘{𝑋}) ⊆ ((𝑁‘{𝑦}) ⊕ (𝑁‘{𝑧}))) ↔ (𝑋 ∈ 𝑉 ∧ ∃𝑦 ∈ 𝑇 ∃𝑧 ∈ 𝑈 (𝑁‘{𝑋}) ⊆ ((𝑁‘{𝑦}) ⊕ (𝑁‘{𝑧})))) | 
| 63 | 58, 62 | bitrdi 287 | 1
⊢ (𝜑 → (𝑋 ∈ (𝑇 ⊕ 𝑈) ↔ (𝑋 ∈ 𝑉 ∧ ∃𝑦 ∈ 𝑇 ∃𝑧 ∈ 𝑈 (𝑁‘{𝑋}) ⊆ ((𝑁‘{𝑦}) ⊕ (𝑁‘{𝑧}))))) |