| Step | Hyp | Ref
| Expression |
| 1 | | lsmsat.q |
. . 3
⊢ (𝜑 → 𝑄 ∈ 𝐴) |
| 2 | | lsmsat.w |
. . . 4
⊢ (𝜑 → 𝑊 ∈ LMod) |
| 3 | | eqid 2737 |
. . . . 5
⊢
(Base‘𝑊) =
(Base‘𝑊) |
| 4 | | eqid 2737 |
. . . . 5
⊢
(LSpan‘𝑊) =
(LSpan‘𝑊) |
| 5 | | lsmsat.o |
. . . . 5
⊢ 0 =
(0g‘𝑊) |
| 6 | | lsmsat.a |
. . . . 5
⊢ 𝐴 = (LSAtoms‘𝑊) |
| 7 | 3, 4, 5, 6 | islsat 38992 |
. . . 4
⊢ (𝑊 ∈ LMod → (𝑄 ∈ 𝐴 ↔ ∃𝑟 ∈ ((Base‘𝑊) ∖ { 0 })𝑄 = ((LSpan‘𝑊)‘{𝑟}))) |
| 8 | 2, 7 | syl 17 |
. . 3
⊢ (𝜑 → (𝑄 ∈ 𝐴 ↔ ∃𝑟 ∈ ((Base‘𝑊) ∖ { 0 })𝑄 = ((LSpan‘𝑊)‘{𝑟}))) |
| 9 | 1, 8 | mpbid 232 |
. 2
⊢ (𝜑 → ∃𝑟 ∈ ((Base‘𝑊) ∖ { 0 })𝑄 = ((LSpan‘𝑊)‘{𝑟})) |
| 10 | | simp3 1139 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑟 ∈ ((Base‘𝑊) ∖ { 0 }) ∧ 𝑄 = ((LSpan‘𝑊)‘{𝑟})) → 𝑄 = ((LSpan‘𝑊)‘{𝑟})) |
| 11 | | lsmsat.l |
. . . . . . . . . 10
⊢ (𝜑 → 𝑄 ⊆ (𝑇 ⊕ 𝑈)) |
| 12 | 11 | 3ad2ant1 1134 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑟 ∈ ((Base‘𝑊) ∖ { 0 }) ∧ 𝑄 = ((LSpan‘𝑊)‘{𝑟})) → 𝑄 ⊆ (𝑇 ⊕ 𝑈)) |
| 13 | 10, 12 | eqsstrrd 4019 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑟 ∈ ((Base‘𝑊) ∖ { 0 }) ∧ 𝑄 = ((LSpan‘𝑊)‘{𝑟})) → ((LSpan‘𝑊)‘{𝑟}) ⊆ (𝑇 ⊕ 𝑈)) |
| 14 | | lsmsat.s |
. . . . . . . . 9
⊢ 𝑆 = (LSubSp‘𝑊) |
| 15 | 2 | 3ad2ant1 1134 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑟 ∈ ((Base‘𝑊) ∖ { 0 }) ∧ 𝑄 = ((LSpan‘𝑊)‘{𝑟})) → 𝑊 ∈ LMod) |
| 16 | | lsmsat.t |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑇 ∈ 𝑆) |
| 17 | | lsmsat.u |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑈 ∈ 𝑆) |
| 18 | | lsmsat.p |
. . . . . . . . . . . 12
⊢ ⊕ =
(LSSum‘𝑊) |
| 19 | 14, 18 | lsmcl 21082 |
. . . . . . . . . . 11
⊢ ((𝑊 ∈ LMod ∧ 𝑇 ∈ 𝑆 ∧ 𝑈 ∈ 𝑆) → (𝑇 ⊕ 𝑈) ∈ 𝑆) |
| 20 | 2, 16, 17, 19 | syl3anc 1373 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑇 ⊕ 𝑈) ∈ 𝑆) |
| 21 | 20 | 3ad2ant1 1134 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑟 ∈ ((Base‘𝑊) ∖ { 0 }) ∧ 𝑄 = ((LSpan‘𝑊)‘{𝑟})) → (𝑇 ⊕ 𝑈) ∈ 𝑆) |
| 22 | | eldifi 4131 |
. . . . . . . . . 10
⊢ (𝑟 ∈ ((Base‘𝑊) ∖ { 0 }) → 𝑟 ∈ (Base‘𝑊)) |
| 23 | 22 | 3ad2ant2 1135 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑟 ∈ ((Base‘𝑊) ∖ { 0 }) ∧ 𝑄 = ((LSpan‘𝑊)‘{𝑟})) → 𝑟 ∈ (Base‘𝑊)) |
| 24 | 3, 14, 4, 15, 21, 23 | ellspsn5b 20993 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑟 ∈ ((Base‘𝑊) ∖ { 0 }) ∧ 𝑄 = ((LSpan‘𝑊)‘{𝑟})) → (𝑟 ∈ (𝑇 ⊕ 𝑈) ↔ ((LSpan‘𝑊)‘{𝑟}) ⊆ (𝑇 ⊕ 𝑈))) |
| 25 | 13, 24 | mpbird 257 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑟 ∈ ((Base‘𝑊) ∖ { 0 }) ∧ 𝑄 = ((LSpan‘𝑊)‘{𝑟})) → 𝑟 ∈ (𝑇 ⊕ 𝑈)) |
| 26 | 14 | lsssssubg 20956 |
. . . . . . . . . 10
⊢ (𝑊 ∈ LMod → 𝑆 ⊆ (SubGrp‘𝑊)) |
| 27 | 15, 26 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑟 ∈ ((Base‘𝑊) ∖ { 0 }) ∧ 𝑄 = ((LSpan‘𝑊)‘{𝑟})) → 𝑆 ⊆ (SubGrp‘𝑊)) |
| 28 | 16 | 3ad2ant1 1134 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑟 ∈ ((Base‘𝑊) ∖ { 0 }) ∧ 𝑄 = ((LSpan‘𝑊)‘{𝑟})) → 𝑇 ∈ 𝑆) |
| 29 | 27, 28 | sseldd 3984 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑟 ∈ ((Base‘𝑊) ∖ { 0 }) ∧ 𝑄 = ((LSpan‘𝑊)‘{𝑟})) → 𝑇 ∈ (SubGrp‘𝑊)) |
| 30 | 17 | 3ad2ant1 1134 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑟 ∈ ((Base‘𝑊) ∖ { 0 }) ∧ 𝑄 = ((LSpan‘𝑊)‘{𝑟})) → 𝑈 ∈ 𝑆) |
| 31 | 27, 30 | sseldd 3984 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑟 ∈ ((Base‘𝑊) ∖ { 0 }) ∧ 𝑄 = ((LSpan‘𝑊)‘{𝑟})) → 𝑈 ∈ (SubGrp‘𝑊)) |
| 32 | | eqid 2737 |
. . . . . . . . 9
⊢
(+g‘𝑊) = (+g‘𝑊) |
| 33 | 32, 18 | lsmelval 19667 |
. . . . . . . 8
⊢ ((𝑇 ∈ (SubGrp‘𝑊) ∧ 𝑈 ∈ (SubGrp‘𝑊)) → (𝑟 ∈ (𝑇 ⊕ 𝑈) ↔ ∃𝑦 ∈ 𝑇 ∃𝑧 ∈ 𝑈 𝑟 = (𝑦(+g‘𝑊)𝑧))) |
| 34 | 29, 31, 33 | syl2anc 584 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑟 ∈ ((Base‘𝑊) ∖ { 0 }) ∧ 𝑄 = ((LSpan‘𝑊)‘{𝑟})) → (𝑟 ∈ (𝑇 ⊕ 𝑈) ↔ ∃𝑦 ∈ 𝑇 ∃𝑧 ∈ 𝑈 𝑟 = (𝑦(+g‘𝑊)𝑧))) |
| 35 | 25, 34 | mpbid 232 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑟 ∈ ((Base‘𝑊) ∖ { 0 }) ∧ 𝑄 = ((LSpan‘𝑊)‘{𝑟})) → ∃𝑦 ∈ 𝑇 ∃𝑧 ∈ 𝑈 𝑟 = (𝑦(+g‘𝑊)𝑧)) |
| 36 | | lsmsat.n |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑇 ≠ { 0 }) |
| 37 | 5, 14 | lssne0 20949 |
. . . . . . . . . . . . . . . 16
⊢ (𝑇 ∈ 𝑆 → (𝑇 ≠ { 0 } ↔ ∃𝑞 ∈ 𝑇 𝑞 ≠ 0 )) |
| 38 | 16, 37 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑇 ≠ { 0 } ↔ ∃𝑞 ∈ 𝑇 𝑞 ≠ 0 )) |
| 39 | 36, 38 | mpbid 232 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ∃𝑞 ∈ 𝑇 𝑞 ≠ 0 ) |
| 40 | 39 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑟 ∈ ((Base‘𝑊) ∖ { 0 })) → ∃𝑞 ∈ 𝑇 𝑞 ≠ 0 ) |
| 41 | 40 | 3ad2ant1 1134 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑟 ∈ ((Base‘𝑊) ∖ { 0 })) ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈) ∧ 𝑟 = (𝑦(+g‘𝑊)𝑧)) → ∃𝑞 ∈ 𝑇 𝑞 ≠ 0 ) |
| 42 | 41 | adantr 480 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑟 ∈ ((Base‘𝑊) ∖ { 0 })) ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈) ∧ 𝑟 = (𝑦(+g‘𝑊)𝑧)) ∧ 𝑦 = 0 ) → ∃𝑞 ∈ 𝑇 𝑞 ≠ 0 ) |
| 43 | 2 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑟 ∈ ((Base‘𝑊) ∖ { 0 })) → 𝑊 ∈ LMod) |
| 44 | 43 | 3ad2ant1 1134 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑟 ∈ ((Base‘𝑊) ∖ { 0 })) ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈) ∧ 𝑟 = (𝑦(+g‘𝑊)𝑧)) → 𝑊 ∈ LMod) |
| 45 | 44 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑟 ∈ ((Base‘𝑊) ∖ { 0 })) ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈) ∧ 𝑟 = (𝑦(+g‘𝑊)𝑧)) ∧ (𝑦 = 0 ∧ 𝑞 ∈ 𝑇 ∧ 𝑞 ≠ 0 )) → 𝑊 ∈ LMod) |
| 46 | 16 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑟 ∈ ((Base‘𝑊) ∖ { 0 })) → 𝑇 ∈ 𝑆) |
| 47 | 46 | 3ad2ant1 1134 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑟 ∈ ((Base‘𝑊) ∖ { 0 })) ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈) ∧ 𝑟 = (𝑦(+g‘𝑊)𝑧)) → 𝑇 ∈ 𝑆) |
| 48 | 47 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑟 ∈ ((Base‘𝑊) ∖ { 0 })) ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈) ∧ 𝑟 = (𝑦(+g‘𝑊)𝑧)) ∧ (𝑦 = 0 ∧ 𝑞 ∈ 𝑇 ∧ 𝑞 ≠ 0 )) → 𝑇 ∈ 𝑆) |
| 49 | | simpr2 1196 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑟 ∈ ((Base‘𝑊) ∖ { 0 })) ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈) ∧ 𝑟 = (𝑦(+g‘𝑊)𝑧)) ∧ (𝑦 = 0 ∧ 𝑞 ∈ 𝑇 ∧ 𝑞 ≠ 0 )) → 𝑞 ∈ 𝑇) |
| 50 | 3, 14 | lssel 20935 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑇 ∈ 𝑆 ∧ 𝑞 ∈ 𝑇) → 𝑞 ∈ (Base‘𝑊)) |
| 51 | 48, 49, 50 | syl2anc 584 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑟 ∈ ((Base‘𝑊) ∖ { 0 })) ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈) ∧ 𝑟 = (𝑦(+g‘𝑊)𝑧)) ∧ (𝑦 = 0 ∧ 𝑞 ∈ 𝑇 ∧ 𝑞 ≠ 0 )) → 𝑞 ∈ (Base‘𝑊)) |
| 52 | | simpr3 1197 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑟 ∈ ((Base‘𝑊) ∖ { 0 })) ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈) ∧ 𝑟 = (𝑦(+g‘𝑊)𝑧)) ∧ (𝑦 = 0 ∧ 𝑞 ∈ 𝑇 ∧ 𝑞 ≠ 0 )) → 𝑞 ≠ 0 ) |
| 53 | 3, 4, 5, 6 | lsatlspsn2 38993 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑊 ∈ LMod ∧ 𝑞 ∈ (Base‘𝑊) ∧ 𝑞 ≠ 0 ) →
((LSpan‘𝑊)‘{𝑞}) ∈ 𝐴) |
| 54 | 45, 51, 52, 53 | syl3anc 1373 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑟 ∈ ((Base‘𝑊) ∖ { 0 })) ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈) ∧ 𝑟 = (𝑦(+g‘𝑊)𝑧)) ∧ (𝑦 = 0 ∧ 𝑞 ∈ 𝑇 ∧ 𝑞 ≠ 0 )) →
((LSpan‘𝑊)‘{𝑞}) ∈ 𝐴) |
| 55 | 14, 4, 45, 48, 49 | ellspsn5 20994 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑟 ∈ ((Base‘𝑊) ∖ { 0 })) ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈) ∧ 𝑟 = (𝑦(+g‘𝑊)𝑧)) ∧ (𝑦 = 0 ∧ 𝑞 ∈ 𝑇 ∧ 𝑞 ≠ 0 )) →
((LSpan‘𝑊)‘{𝑞}) ⊆ 𝑇) |
| 56 | | simpl3 1194 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑟 ∈ ((Base‘𝑊) ∖ { 0 })) ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈) ∧ 𝑟 = (𝑦(+g‘𝑊)𝑧)) ∧ (𝑦 = 0 ∧ 𝑞 ∈ 𝑇 ∧ 𝑞 ≠ 0 )) → 𝑟 = (𝑦(+g‘𝑊)𝑧)) |
| 57 | | simpr1 1195 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑟 ∈ ((Base‘𝑊) ∖ { 0 })) ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈) ∧ 𝑟 = (𝑦(+g‘𝑊)𝑧)) ∧ (𝑦 = 0 ∧ 𝑞 ∈ 𝑇 ∧ 𝑞 ≠ 0 )) → 𝑦 = 0 ) |
| 58 | 57 | oveq1d 7446 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑟 ∈ ((Base‘𝑊) ∖ { 0 })) ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈) ∧ 𝑟 = (𝑦(+g‘𝑊)𝑧)) ∧ (𝑦 = 0 ∧ 𝑞 ∈ 𝑇 ∧ 𝑞 ≠ 0 )) → (𝑦(+g‘𝑊)𝑧) = ( 0 (+g‘𝑊)𝑧)) |
| 59 | 17 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑟 ∈ ((Base‘𝑊) ∖ { 0 })) → 𝑈 ∈ 𝑆) |
| 60 | 59 | 3ad2ant1 1134 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑟 ∈ ((Base‘𝑊) ∖ { 0 })) ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈) ∧ 𝑟 = (𝑦(+g‘𝑊)𝑧)) → 𝑈 ∈ 𝑆) |
| 61 | | simp2r 1201 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑟 ∈ ((Base‘𝑊) ∖ { 0 })) ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈) ∧ 𝑟 = (𝑦(+g‘𝑊)𝑧)) → 𝑧 ∈ 𝑈) |
| 62 | 3, 14 | lssel 20935 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑈 ∈ 𝑆 ∧ 𝑧 ∈ 𝑈) → 𝑧 ∈ (Base‘𝑊)) |
| 63 | 60, 61, 62 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑟 ∈ ((Base‘𝑊) ∖ { 0 })) ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈) ∧ 𝑟 = (𝑦(+g‘𝑊)𝑧)) → 𝑧 ∈ (Base‘𝑊)) |
| 64 | 63 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑟 ∈ ((Base‘𝑊) ∖ { 0 })) ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈) ∧ 𝑟 = (𝑦(+g‘𝑊)𝑧)) ∧ (𝑦 = 0 ∧ 𝑞 ∈ 𝑇 ∧ 𝑞 ≠ 0 )) → 𝑧 ∈ (Base‘𝑊)) |
| 65 | 3, 32, 5 | lmod0vlid 20890 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑊 ∈ LMod ∧ 𝑧 ∈ (Base‘𝑊)) → ( 0 (+g‘𝑊)𝑧) = 𝑧) |
| 66 | 45, 64, 65 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑟 ∈ ((Base‘𝑊) ∖ { 0 })) ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈) ∧ 𝑟 = (𝑦(+g‘𝑊)𝑧)) ∧ (𝑦 = 0 ∧ 𝑞 ∈ 𝑇 ∧ 𝑞 ≠ 0 )) → ( 0
(+g‘𝑊)𝑧) = 𝑧) |
| 67 | 56, 58, 66 | 3eqtrd 2781 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑟 ∈ ((Base‘𝑊) ∖ { 0 })) ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈) ∧ 𝑟 = (𝑦(+g‘𝑊)𝑧)) ∧ (𝑦 = 0 ∧ 𝑞 ∈ 𝑇 ∧ 𝑞 ≠ 0 )) → 𝑟 = 𝑧) |
| 68 | 67 | sneqd 4638 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑟 ∈ ((Base‘𝑊) ∖ { 0 })) ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈) ∧ 𝑟 = (𝑦(+g‘𝑊)𝑧)) ∧ (𝑦 = 0 ∧ 𝑞 ∈ 𝑇 ∧ 𝑞 ≠ 0 )) → {𝑟} = {𝑧}) |
| 69 | 68 | fveq2d 6910 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑟 ∈ ((Base‘𝑊) ∖ { 0 })) ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈) ∧ 𝑟 = (𝑦(+g‘𝑊)𝑧)) ∧ (𝑦 = 0 ∧ 𝑞 ∈ 𝑇 ∧ 𝑞 ≠ 0 )) →
((LSpan‘𝑊)‘{𝑟}) = ((LSpan‘𝑊)‘{𝑧})) |
| 70 | 14, 4, 44, 60, 61 | ellspsn5 20994 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑟 ∈ ((Base‘𝑊) ∖ { 0 })) ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈) ∧ 𝑟 = (𝑦(+g‘𝑊)𝑧)) → ((LSpan‘𝑊)‘{𝑧}) ⊆ 𝑈) |
| 71 | 70 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑟 ∈ ((Base‘𝑊) ∖ { 0 })) ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈) ∧ 𝑟 = (𝑦(+g‘𝑊)𝑧)) ∧ (𝑦 = 0 ∧ 𝑞 ∈ 𝑇 ∧ 𝑞 ≠ 0 )) →
((LSpan‘𝑊)‘{𝑧}) ⊆ 𝑈) |
| 72 | 69, 71 | eqsstrd 4018 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑟 ∈ ((Base‘𝑊) ∖ { 0 })) ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈) ∧ 𝑟 = (𝑦(+g‘𝑊)𝑧)) ∧ (𝑦 = 0 ∧ 𝑞 ∈ 𝑇 ∧ 𝑞 ≠ 0 )) →
((LSpan‘𝑊)‘{𝑟}) ⊆ 𝑈) |
| 73 | 3, 4 | lspsnsubg 20978 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑊 ∈ LMod ∧ 𝑞 ∈ (Base‘𝑊)) → ((LSpan‘𝑊)‘{𝑞}) ∈ (SubGrp‘𝑊)) |
| 74 | 45, 51, 73 | syl2anc 584 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑟 ∈ ((Base‘𝑊) ∖ { 0 })) ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈) ∧ 𝑟 = (𝑦(+g‘𝑊)𝑧)) ∧ (𝑦 = 0 ∧ 𝑞 ∈ 𝑇 ∧ 𝑞 ≠ 0 )) →
((LSpan‘𝑊)‘{𝑞}) ∈ (SubGrp‘𝑊)) |
| 75 | 45, 26 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑟 ∈ ((Base‘𝑊) ∖ { 0 })) ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈) ∧ 𝑟 = (𝑦(+g‘𝑊)𝑧)) ∧ (𝑦 = 0 ∧ 𝑞 ∈ 𝑇 ∧ 𝑞 ≠ 0 )) → 𝑆 ⊆ (SubGrp‘𝑊)) |
| 76 | 60 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑟 ∈ ((Base‘𝑊) ∖ { 0 })) ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈) ∧ 𝑟 = (𝑦(+g‘𝑊)𝑧)) ∧ (𝑦 = 0 ∧ 𝑞 ∈ 𝑇 ∧ 𝑞 ≠ 0 )) → 𝑈 ∈ 𝑆) |
| 77 | 75, 76 | sseldd 3984 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑟 ∈ ((Base‘𝑊) ∖ { 0 })) ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈) ∧ 𝑟 = (𝑦(+g‘𝑊)𝑧)) ∧ (𝑦 = 0 ∧ 𝑞 ∈ 𝑇 ∧ 𝑞 ≠ 0 )) → 𝑈 ∈ (SubGrp‘𝑊)) |
| 78 | 18 | lsmub2 19676 |
. . . . . . . . . . . . . . . . 17
⊢
((((LSpan‘𝑊)‘{𝑞}) ∈ (SubGrp‘𝑊) ∧ 𝑈 ∈ (SubGrp‘𝑊)) → 𝑈 ⊆ (((LSpan‘𝑊)‘{𝑞}) ⊕ 𝑈)) |
| 79 | 74, 77, 78 | syl2anc 584 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑟 ∈ ((Base‘𝑊) ∖ { 0 })) ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈) ∧ 𝑟 = (𝑦(+g‘𝑊)𝑧)) ∧ (𝑦 = 0 ∧ 𝑞 ∈ 𝑇 ∧ 𝑞 ≠ 0 )) → 𝑈 ⊆ (((LSpan‘𝑊)‘{𝑞}) ⊕ 𝑈)) |
| 80 | 72, 79 | sstrd 3994 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑟 ∈ ((Base‘𝑊) ∖ { 0 })) ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈) ∧ 𝑟 = (𝑦(+g‘𝑊)𝑧)) ∧ (𝑦 = 0 ∧ 𝑞 ∈ 𝑇 ∧ 𝑞 ≠ 0 )) →
((LSpan‘𝑊)‘{𝑟}) ⊆ (((LSpan‘𝑊)‘{𝑞}) ⊕ 𝑈)) |
| 81 | | sseq1 4009 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑝 = ((LSpan‘𝑊)‘{𝑞}) → (𝑝 ⊆ 𝑇 ↔ ((LSpan‘𝑊)‘{𝑞}) ⊆ 𝑇)) |
| 82 | | oveq1 7438 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑝 = ((LSpan‘𝑊)‘{𝑞}) → (𝑝 ⊕ 𝑈) = (((LSpan‘𝑊)‘{𝑞}) ⊕ 𝑈)) |
| 83 | 82 | sseq2d 4016 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑝 = ((LSpan‘𝑊)‘{𝑞}) → (((LSpan‘𝑊)‘{𝑟}) ⊆ (𝑝 ⊕ 𝑈) ↔ ((LSpan‘𝑊)‘{𝑟}) ⊆ (((LSpan‘𝑊)‘{𝑞}) ⊕ 𝑈))) |
| 84 | 81, 83 | anbi12d 632 |
. . . . . . . . . . . . . . . 16
⊢ (𝑝 = ((LSpan‘𝑊)‘{𝑞}) → ((𝑝 ⊆ 𝑇 ∧ ((LSpan‘𝑊)‘{𝑟}) ⊆ (𝑝 ⊕ 𝑈)) ↔ (((LSpan‘𝑊)‘{𝑞}) ⊆ 𝑇 ∧ ((LSpan‘𝑊)‘{𝑟}) ⊆ (((LSpan‘𝑊)‘{𝑞}) ⊕ 𝑈)))) |
| 85 | 84 | rspcev 3622 |
. . . . . . . . . . . . . . 15
⊢
((((LSpan‘𝑊)‘{𝑞}) ∈ 𝐴 ∧ (((LSpan‘𝑊)‘{𝑞}) ⊆ 𝑇 ∧ ((LSpan‘𝑊)‘{𝑟}) ⊆ (((LSpan‘𝑊)‘{𝑞}) ⊕ 𝑈))) → ∃𝑝 ∈ 𝐴 (𝑝 ⊆ 𝑇 ∧ ((LSpan‘𝑊)‘{𝑟}) ⊆ (𝑝 ⊕ 𝑈))) |
| 86 | 54, 55, 80, 85 | syl12anc 837 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑟 ∈ ((Base‘𝑊) ∖ { 0 })) ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈) ∧ 𝑟 = (𝑦(+g‘𝑊)𝑧)) ∧ (𝑦 = 0 ∧ 𝑞 ∈ 𝑇 ∧ 𝑞 ≠ 0 )) → ∃𝑝 ∈ 𝐴 (𝑝 ⊆ 𝑇 ∧ ((LSpan‘𝑊)‘{𝑟}) ⊆ (𝑝 ⊕ 𝑈))) |
| 87 | 86 | 3exp2 1355 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑟 ∈ ((Base‘𝑊) ∖ { 0 })) ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈) ∧ 𝑟 = (𝑦(+g‘𝑊)𝑧)) → (𝑦 = 0 → (𝑞 ∈ 𝑇 → (𝑞 ≠ 0 → ∃𝑝 ∈ 𝐴 (𝑝 ⊆ 𝑇 ∧ ((LSpan‘𝑊)‘{𝑟}) ⊆ (𝑝 ⊕ 𝑈)))))) |
| 88 | 87 | imp 406 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑟 ∈ ((Base‘𝑊) ∖ { 0 })) ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈) ∧ 𝑟 = (𝑦(+g‘𝑊)𝑧)) ∧ 𝑦 = 0 ) → (𝑞 ∈ 𝑇 → (𝑞 ≠ 0 → ∃𝑝 ∈ 𝐴 (𝑝 ⊆ 𝑇 ∧ ((LSpan‘𝑊)‘{𝑟}) ⊆ (𝑝 ⊕ 𝑈))))) |
| 89 | 88 | rexlimdv 3153 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑟 ∈ ((Base‘𝑊) ∖ { 0 })) ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈) ∧ 𝑟 = (𝑦(+g‘𝑊)𝑧)) ∧ 𝑦 = 0 ) → (∃𝑞 ∈ 𝑇 𝑞 ≠ 0 → ∃𝑝 ∈ 𝐴 (𝑝 ⊆ 𝑇 ∧ ((LSpan‘𝑊)‘{𝑟}) ⊆ (𝑝 ⊕ 𝑈)))) |
| 90 | 42, 89 | mpd 15 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑟 ∈ ((Base‘𝑊) ∖ { 0 })) ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈) ∧ 𝑟 = (𝑦(+g‘𝑊)𝑧)) ∧ 𝑦 = 0 ) → ∃𝑝 ∈ 𝐴 (𝑝 ⊆ 𝑇 ∧ ((LSpan‘𝑊)‘{𝑟}) ⊆ (𝑝 ⊕ 𝑈))) |
| 91 | 44 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑟 ∈ ((Base‘𝑊) ∖ { 0 })) ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈) ∧ 𝑟 = (𝑦(+g‘𝑊)𝑧)) ∧ 𝑦 ≠ 0 ) → 𝑊 ∈ LMod) |
| 92 | | simp2l 1200 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑟 ∈ ((Base‘𝑊) ∖ { 0 })) ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈) ∧ 𝑟 = (𝑦(+g‘𝑊)𝑧)) → 𝑦 ∈ 𝑇) |
| 93 | 3, 14 | lssel 20935 |
. . . . . . . . . . . . . 14
⊢ ((𝑇 ∈ 𝑆 ∧ 𝑦 ∈ 𝑇) → 𝑦 ∈ (Base‘𝑊)) |
| 94 | 47, 92, 93 | syl2anc 584 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑟 ∈ ((Base‘𝑊) ∖ { 0 })) ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈) ∧ 𝑟 = (𝑦(+g‘𝑊)𝑧)) → 𝑦 ∈ (Base‘𝑊)) |
| 95 | 94 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑟 ∈ ((Base‘𝑊) ∖ { 0 })) ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈) ∧ 𝑟 = (𝑦(+g‘𝑊)𝑧)) ∧ 𝑦 ≠ 0 ) → 𝑦 ∈ (Base‘𝑊)) |
| 96 | | simpr 484 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑟 ∈ ((Base‘𝑊) ∖ { 0 })) ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈) ∧ 𝑟 = (𝑦(+g‘𝑊)𝑧)) ∧ 𝑦 ≠ 0 ) → 𝑦 ≠ 0 ) |
| 97 | 3, 4, 5, 6 | lsatlspsn2 38993 |
. . . . . . . . . . . 12
⊢ ((𝑊 ∈ LMod ∧ 𝑦 ∈ (Base‘𝑊) ∧ 𝑦 ≠ 0 ) →
((LSpan‘𝑊)‘{𝑦}) ∈ 𝐴) |
| 98 | 91, 95, 96, 97 | syl3anc 1373 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑟 ∈ ((Base‘𝑊) ∖ { 0 })) ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈) ∧ 𝑟 = (𝑦(+g‘𝑊)𝑧)) ∧ 𝑦 ≠ 0 ) →
((LSpan‘𝑊)‘{𝑦}) ∈ 𝐴) |
| 99 | 14, 4, 44, 47, 92 | ellspsn5 20994 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑟 ∈ ((Base‘𝑊) ∖ { 0 })) ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈) ∧ 𝑟 = (𝑦(+g‘𝑊)𝑧)) → ((LSpan‘𝑊)‘{𝑦}) ⊆ 𝑇) |
| 100 | 99 | adantr 480 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑟 ∈ ((Base‘𝑊) ∖ { 0 })) ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈) ∧ 𝑟 = (𝑦(+g‘𝑊)𝑧)) ∧ 𝑦 ≠ 0 ) →
((LSpan‘𝑊)‘{𝑦}) ⊆ 𝑇) |
| 101 | | simp3 1139 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑟 ∈ ((Base‘𝑊) ∖ { 0 })) ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈) ∧ 𝑟 = (𝑦(+g‘𝑊)𝑧)) → 𝑟 = (𝑦(+g‘𝑊)𝑧)) |
| 102 | 101 | sneqd 4638 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑟 ∈ ((Base‘𝑊) ∖ { 0 })) ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈) ∧ 𝑟 = (𝑦(+g‘𝑊)𝑧)) → {𝑟} = {(𝑦(+g‘𝑊)𝑧)}) |
| 103 | 102 | fveq2d 6910 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑟 ∈ ((Base‘𝑊) ∖ { 0 })) ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈) ∧ 𝑟 = (𝑦(+g‘𝑊)𝑧)) → ((LSpan‘𝑊)‘{𝑟}) = ((LSpan‘𝑊)‘{(𝑦(+g‘𝑊)𝑧)})) |
| 104 | 3, 32, 4 | lspvadd 21095 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑊 ∈ LMod ∧ 𝑦 ∈ (Base‘𝑊) ∧ 𝑧 ∈ (Base‘𝑊)) → ((LSpan‘𝑊)‘{(𝑦(+g‘𝑊)𝑧)}) ⊆ ((LSpan‘𝑊)‘{𝑦, 𝑧})) |
| 105 | 44, 94, 63, 104 | syl3anc 1373 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑟 ∈ ((Base‘𝑊) ∖ { 0 })) ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈) ∧ 𝑟 = (𝑦(+g‘𝑊)𝑧)) → ((LSpan‘𝑊)‘{(𝑦(+g‘𝑊)𝑧)}) ⊆ ((LSpan‘𝑊)‘{𝑦, 𝑧})) |
| 106 | 103, 105 | eqsstrd 4018 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑟 ∈ ((Base‘𝑊) ∖ { 0 })) ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈) ∧ 𝑟 = (𝑦(+g‘𝑊)𝑧)) → ((LSpan‘𝑊)‘{𝑟}) ⊆ ((LSpan‘𝑊)‘{𝑦, 𝑧})) |
| 107 | 3, 4, 18, 44, 94, 63 | lsmpr 21088 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑟 ∈ ((Base‘𝑊) ∖ { 0 })) ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈) ∧ 𝑟 = (𝑦(+g‘𝑊)𝑧)) → ((LSpan‘𝑊)‘{𝑦, 𝑧}) = (((LSpan‘𝑊)‘{𝑦}) ⊕ ((LSpan‘𝑊)‘{𝑧}))) |
| 108 | 106, 107 | sseqtrd 4020 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑟 ∈ ((Base‘𝑊) ∖ { 0 })) ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈) ∧ 𝑟 = (𝑦(+g‘𝑊)𝑧)) → ((LSpan‘𝑊)‘{𝑟}) ⊆ (((LSpan‘𝑊)‘{𝑦}) ⊕ ((LSpan‘𝑊)‘{𝑧}))) |
| 109 | 44, 26 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑟 ∈ ((Base‘𝑊) ∖ { 0 })) ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈) ∧ 𝑟 = (𝑦(+g‘𝑊)𝑧)) → 𝑆 ⊆ (SubGrp‘𝑊)) |
| 110 | 3, 14, 4 | lspsncl 20975 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑊 ∈ LMod ∧ 𝑦 ∈ (Base‘𝑊)) → ((LSpan‘𝑊)‘{𝑦}) ∈ 𝑆) |
| 111 | 44, 94, 110 | syl2anc 584 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑟 ∈ ((Base‘𝑊) ∖ { 0 })) ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈) ∧ 𝑟 = (𝑦(+g‘𝑊)𝑧)) → ((LSpan‘𝑊)‘{𝑦}) ∈ 𝑆) |
| 112 | 109, 111 | sseldd 3984 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑟 ∈ ((Base‘𝑊) ∖ { 0 })) ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈) ∧ 𝑟 = (𝑦(+g‘𝑊)𝑧)) → ((LSpan‘𝑊)‘{𝑦}) ∈ (SubGrp‘𝑊)) |
| 113 | 109, 60 | sseldd 3984 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑟 ∈ ((Base‘𝑊) ∖ { 0 })) ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈) ∧ 𝑟 = (𝑦(+g‘𝑊)𝑧)) → 𝑈 ∈ (SubGrp‘𝑊)) |
| 114 | 18 | lsmless2 19679 |
. . . . . . . . . . . . . 14
⊢
((((LSpan‘𝑊)‘{𝑦}) ∈ (SubGrp‘𝑊) ∧ 𝑈 ∈ (SubGrp‘𝑊) ∧ ((LSpan‘𝑊)‘{𝑧}) ⊆ 𝑈) → (((LSpan‘𝑊)‘{𝑦}) ⊕ ((LSpan‘𝑊)‘{𝑧})) ⊆ (((LSpan‘𝑊)‘{𝑦}) ⊕ 𝑈)) |
| 115 | 112, 113,
70, 114 | syl3anc 1373 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑟 ∈ ((Base‘𝑊) ∖ { 0 })) ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈) ∧ 𝑟 = (𝑦(+g‘𝑊)𝑧)) → (((LSpan‘𝑊)‘{𝑦}) ⊕ ((LSpan‘𝑊)‘{𝑧})) ⊆ (((LSpan‘𝑊)‘{𝑦}) ⊕ 𝑈)) |
| 116 | 108, 115 | sstrd 3994 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑟 ∈ ((Base‘𝑊) ∖ { 0 })) ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈) ∧ 𝑟 = (𝑦(+g‘𝑊)𝑧)) → ((LSpan‘𝑊)‘{𝑟}) ⊆ (((LSpan‘𝑊)‘{𝑦}) ⊕ 𝑈)) |
| 117 | 116 | adantr 480 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑟 ∈ ((Base‘𝑊) ∖ { 0 })) ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈) ∧ 𝑟 = (𝑦(+g‘𝑊)𝑧)) ∧ 𝑦 ≠ 0 ) →
((LSpan‘𝑊)‘{𝑟}) ⊆ (((LSpan‘𝑊)‘{𝑦}) ⊕ 𝑈)) |
| 118 | | sseq1 4009 |
. . . . . . . . . . . . 13
⊢ (𝑝 = ((LSpan‘𝑊)‘{𝑦}) → (𝑝 ⊆ 𝑇 ↔ ((LSpan‘𝑊)‘{𝑦}) ⊆ 𝑇)) |
| 119 | | oveq1 7438 |
. . . . . . . . . . . . . 14
⊢ (𝑝 = ((LSpan‘𝑊)‘{𝑦}) → (𝑝 ⊕ 𝑈) = (((LSpan‘𝑊)‘{𝑦}) ⊕ 𝑈)) |
| 120 | 119 | sseq2d 4016 |
. . . . . . . . . . . . 13
⊢ (𝑝 = ((LSpan‘𝑊)‘{𝑦}) → (((LSpan‘𝑊)‘{𝑟}) ⊆ (𝑝 ⊕ 𝑈) ↔ ((LSpan‘𝑊)‘{𝑟}) ⊆ (((LSpan‘𝑊)‘{𝑦}) ⊕ 𝑈))) |
| 121 | 118, 120 | anbi12d 632 |
. . . . . . . . . . . 12
⊢ (𝑝 = ((LSpan‘𝑊)‘{𝑦}) → ((𝑝 ⊆ 𝑇 ∧ ((LSpan‘𝑊)‘{𝑟}) ⊆ (𝑝 ⊕ 𝑈)) ↔ (((LSpan‘𝑊)‘{𝑦}) ⊆ 𝑇 ∧ ((LSpan‘𝑊)‘{𝑟}) ⊆ (((LSpan‘𝑊)‘{𝑦}) ⊕ 𝑈)))) |
| 122 | 121 | rspcev 3622 |
. . . . . . . . . . 11
⊢
((((LSpan‘𝑊)‘{𝑦}) ∈ 𝐴 ∧ (((LSpan‘𝑊)‘{𝑦}) ⊆ 𝑇 ∧ ((LSpan‘𝑊)‘{𝑟}) ⊆ (((LSpan‘𝑊)‘{𝑦}) ⊕ 𝑈))) → ∃𝑝 ∈ 𝐴 (𝑝 ⊆ 𝑇 ∧ ((LSpan‘𝑊)‘{𝑟}) ⊆ (𝑝 ⊕ 𝑈))) |
| 123 | 98, 100, 117, 122 | syl12anc 837 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑟 ∈ ((Base‘𝑊) ∖ { 0 })) ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈) ∧ 𝑟 = (𝑦(+g‘𝑊)𝑧)) ∧ 𝑦 ≠ 0 ) → ∃𝑝 ∈ 𝐴 (𝑝 ⊆ 𝑇 ∧ ((LSpan‘𝑊)‘{𝑟}) ⊆ (𝑝 ⊕ 𝑈))) |
| 124 | 90, 123 | pm2.61dane 3029 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑟 ∈ ((Base‘𝑊) ∖ { 0 })) ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈) ∧ 𝑟 = (𝑦(+g‘𝑊)𝑧)) → ∃𝑝 ∈ 𝐴 (𝑝 ⊆ 𝑇 ∧ ((LSpan‘𝑊)‘{𝑟}) ⊆ (𝑝 ⊕ 𝑈))) |
| 125 | 124 | 3exp 1120 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑟 ∈ ((Base‘𝑊) ∖ { 0 })) → ((𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈) → (𝑟 = (𝑦(+g‘𝑊)𝑧) → ∃𝑝 ∈ 𝐴 (𝑝 ⊆ 𝑇 ∧ ((LSpan‘𝑊)‘{𝑟}) ⊆ (𝑝 ⊕ 𝑈))))) |
| 126 | 125 | rexlimdvv 3212 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑟 ∈ ((Base‘𝑊) ∖ { 0 })) → (∃𝑦 ∈ 𝑇 ∃𝑧 ∈ 𝑈 𝑟 = (𝑦(+g‘𝑊)𝑧) → ∃𝑝 ∈ 𝐴 (𝑝 ⊆ 𝑇 ∧ ((LSpan‘𝑊)‘{𝑟}) ⊆ (𝑝 ⊕ 𝑈)))) |
| 127 | 126 | 3adant3 1133 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑟 ∈ ((Base‘𝑊) ∖ { 0 }) ∧ 𝑄 = ((LSpan‘𝑊)‘{𝑟})) → (∃𝑦 ∈ 𝑇 ∃𝑧 ∈ 𝑈 𝑟 = (𝑦(+g‘𝑊)𝑧) → ∃𝑝 ∈ 𝐴 (𝑝 ⊆ 𝑇 ∧ ((LSpan‘𝑊)‘{𝑟}) ⊆ (𝑝 ⊕ 𝑈)))) |
| 128 | 35, 127 | mpd 15 |
. . . . 5
⊢ ((𝜑 ∧ 𝑟 ∈ ((Base‘𝑊) ∖ { 0 }) ∧ 𝑄 = ((LSpan‘𝑊)‘{𝑟})) → ∃𝑝 ∈ 𝐴 (𝑝 ⊆ 𝑇 ∧ ((LSpan‘𝑊)‘{𝑟}) ⊆ (𝑝 ⊕ 𝑈))) |
| 129 | | sseq1 4009 |
. . . . . . . 8
⊢ (𝑄 = ((LSpan‘𝑊)‘{𝑟}) → (𝑄 ⊆ (𝑝 ⊕ 𝑈) ↔ ((LSpan‘𝑊)‘{𝑟}) ⊆ (𝑝 ⊕ 𝑈))) |
| 130 | 129 | anbi2d 630 |
. . . . . . 7
⊢ (𝑄 = ((LSpan‘𝑊)‘{𝑟}) → ((𝑝 ⊆ 𝑇 ∧ 𝑄 ⊆ (𝑝 ⊕ 𝑈)) ↔ (𝑝 ⊆ 𝑇 ∧ ((LSpan‘𝑊)‘{𝑟}) ⊆ (𝑝 ⊕ 𝑈)))) |
| 131 | 130 | rexbidv 3179 |
. . . . . 6
⊢ (𝑄 = ((LSpan‘𝑊)‘{𝑟}) → (∃𝑝 ∈ 𝐴 (𝑝 ⊆ 𝑇 ∧ 𝑄 ⊆ (𝑝 ⊕ 𝑈)) ↔ ∃𝑝 ∈ 𝐴 (𝑝 ⊆ 𝑇 ∧ ((LSpan‘𝑊)‘{𝑟}) ⊆ (𝑝 ⊕ 𝑈)))) |
| 132 | 131 | 3ad2ant3 1136 |
. . . . 5
⊢ ((𝜑 ∧ 𝑟 ∈ ((Base‘𝑊) ∖ { 0 }) ∧ 𝑄 = ((LSpan‘𝑊)‘{𝑟})) → (∃𝑝 ∈ 𝐴 (𝑝 ⊆ 𝑇 ∧ 𝑄 ⊆ (𝑝 ⊕ 𝑈)) ↔ ∃𝑝 ∈ 𝐴 (𝑝 ⊆ 𝑇 ∧ ((LSpan‘𝑊)‘{𝑟}) ⊆ (𝑝 ⊕ 𝑈)))) |
| 133 | 128, 132 | mpbird 257 |
. . . 4
⊢ ((𝜑 ∧ 𝑟 ∈ ((Base‘𝑊) ∖ { 0 }) ∧ 𝑄 = ((LSpan‘𝑊)‘{𝑟})) → ∃𝑝 ∈ 𝐴 (𝑝 ⊆ 𝑇 ∧ 𝑄 ⊆ (𝑝 ⊕ 𝑈))) |
| 134 | 133 | 3exp 1120 |
. . 3
⊢ (𝜑 → (𝑟 ∈ ((Base‘𝑊) ∖ { 0 }) → (𝑄 = ((LSpan‘𝑊)‘{𝑟}) → ∃𝑝 ∈ 𝐴 (𝑝 ⊆ 𝑇 ∧ 𝑄 ⊆ (𝑝 ⊕ 𝑈))))) |
| 135 | 134 | rexlimdv 3153 |
. 2
⊢ (𝜑 → (∃𝑟 ∈ ((Base‘𝑊) ∖ { 0 })𝑄 = ((LSpan‘𝑊)‘{𝑟}) → ∃𝑝 ∈ 𝐴 (𝑝 ⊆ 𝑇 ∧ 𝑄 ⊆ (𝑝 ⊕ 𝑈)))) |
| 136 | 9, 135 | mpd 15 |
1
⊢ (𝜑 → ∃𝑝 ∈ 𝐴 (𝑝 ⊆ 𝑇 ∧ 𝑄 ⊆ (𝑝 ⊕ 𝑈))) |