| Step | Hyp | Ref
| Expression |
| 1 | | lsmcss.3 |
. . . . . . 7
⊢ (𝜑 → ( ⊥ ‘( ⊥
‘𝑆)) ⊆ (𝑆 ⊕ ( ⊥
‘𝑆))) |
| 2 | 1 | sseld 3982 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ ( ⊥ ‘( ⊥
‘𝑆)) → 𝑥 ∈ (𝑆 ⊕ ( ⊥
‘𝑆)))) |
| 3 | | lsmcss.1 |
. . . . . . . 8
⊢ (𝜑 → 𝑊 ∈ PreHil) |
| 4 | | phllmod 21648 |
. . . . . . . 8
⊢ (𝑊 ∈ PreHil → 𝑊 ∈ LMod) |
| 5 | 3, 4 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝑊 ∈ LMod) |
| 6 | | lsmcss.2 |
. . . . . . 7
⊢ (𝜑 → 𝑆 ⊆ 𝑉) |
| 7 | | lsmcss.j |
. . . . . . . . 9
⊢ 𝑉 = (Base‘𝑊) |
| 8 | | lsmcss.o |
. . . . . . . . 9
⊢ ⊥ =
(ocv‘𝑊) |
| 9 | 7, 8 | ocvss 21688 |
. . . . . . . 8
⊢ ( ⊥
‘𝑆) ⊆ 𝑉 |
| 10 | 9 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → ( ⊥ ‘𝑆) ⊆ 𝑉) |
| 11 | | eqid 2737 |
. . . . . . . 8
⊢
(+g‘𝑊) = (+g‘𝑊) |
| 12 | | lsmcss.p |
. . . . . . . 8
⊢ ⊕ =
(LSSum‘𝑊) |
| 13 | 7, 11, 12 | lsmelvalx 19658 |
. . . . . . 7
⊢ ((𝑊 ∈ LMod ∧ 𝑆 ⊆ 𝑉 ∧ ( ⊥ ‘𝑆) ⊆ 𝑉) → (𝑥 ∈ (𝑆 ⊕ ( ⊥
‘𝑆)) ↔
∃𝑦 ∈ 𝑆 ∃𝑧 ∈ ( ⊥ ‘𝑆)𝑥 = (𝑦(+g‘𝑊)𝑧))) |
| 14 | 5, 6, 10, 13 | syl3anc 1373 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ (𝑆 ⊕ ( ⊥
‘𝑆)) ↔
∃𝑦 ∈ 𝑆 ∃𝑧 ∈ ( ⊥ ‘𝑆)𝑥 = (𝑦(+g‘𝑊)𝑧))) |
| 15 | 2, 14 | sylibd 239 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ ( ⊥ ‘( ⊥
‘𝑆)) →
∃𝑦 ∈ 𝑆 ∃𝑧 ∈ ( ⊥ ‘𝑆)𝑥 = (𝑦(+g‘𝑊)𝑧))) |
| 16 | 3 | ad2antrr 726 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑧 ∈ ( ⊥ ‘𝑆))) ∧ (𝑦(+g‘𝑊)𝑧) ∈ ( ⊥ ‘( ⊥
‘𝑆))) → 𝑊 ∈ PreHil) |
| 17 | 6 | ad2antrr 726 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑧 ∈ ( ⊥ ‘𝑆))) ∧ (𝑦(+g‘𝑊)𝑧) ∈ ( ⊥ ‘( ⊥
‘𝑆))) → 𝑆 ⊆ 𝑉) |
| 18 | | simplrl 777 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑧 ∈ ( ⊥ ‘𝑆))) ∧ (𝑦(+g‘𝑊)𝑧) ∈ ( ⊥ ‘( ⊥
‘𝑆))) → 𝑦 ∈ 𝑆) |
| 19 | 17, 18 | sseldd 3984 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑧 ∈ ( ⊥ ‘𝑆))) ∧ (𝑦(+g‘𝑊)𝑧) ∈ ( ⊥ ‘( ⊥
‘𝑆))) → 𝑦 ∈ 𝑉) |
| 20 | | simplrr 778 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑧 ∈ ( ⊥ ‘𝑆))) ∧ (𝑦(+g‘𝑊)𝑧) ∈ ( ⊥ ‘( ⊥
‘𝑆))) → 𝑧 ∈ ( ⊥ ‘𝑆)) |
| 21 | 9, 20 | sselid 3981 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑧 ∈ ( ⊥ ‘𝑆))) ∧ (𝑦(+g‘𝑊)𝑧) ∈ ( ⊥ ‘( ⊥
‘𝑆))) → 𝑧 ∈ 𝑉) |
| 22 | | eqid 2737 |
. . . . . . . . . . . . . . . 16
⊢
(Scalar‘𝑊) =
(Scalar‘𝑊) |
| 23 | | eqid 2737 |
. . . . . . . . . . . . . . . 16
⊢
(·𝑖‘𝑊) =
(·𝑖‘𝑊) |
| 24 | | eqid 2737 |
. . . . . . . . . . . . . . . 16
⊢
(+g‘(Scalar‘𝑊)) =
(+g‘(Scalar‘𝑊)) |
| 25 | 22, 23, 7, 11, 24 | ipdir 21657 |
. . . . . . . . . . . . . . 15
⊢ ((𝑊 ∈ PreHil ∧ (𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → ((𝑦(+g‘𝑊)𝑧)(·𝑖‘𝑊)𝑧) = ((𝑦(·𝑖‘𝑊)𝑧)(+g‘(Scalar‘𝑊))(𝑧(·𝑖‘𝑊)𝑧))) |
| 26 | 16, 19, 21, 21, 25 | syl13anc 1374 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑧 ∈ ( ⊥ ‘𝑆))) ∧ (𝑦(+g‘𝑊)𝑧) ∈ ( ⊥ ‘( ⊥
‘𝑆))) → ((𝑦(+g‘𝑊)𝑧)(·𝑖‘𝑊)𝑧) = ((𝑦(·𝑖‘𝑊)𝑧)(+g‘(Scalar‘𝑊))(𝑧(·𝑖‘𝑊)𝑧))) |
| 27 | | eqid 2737 |
. . . . . . . . . . . . . . . . . 18
⊢
(0g‘(Scalar‘𝑊)) =
(0g‘(Scalar‘𝑊)) |
| 28 | 7, 23, 22, 27, 8 | ocvi 21687 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑧 ∈ ( ⊥ ‘𝑆) ∧ 𝑦 ∈ 𝑆) → (𝑧(·𝑖‘𝑊)𝑦) = (0g‘(Scalar‘𝑊))) |
| 29 | 20, 18, 28 | syl2anc 584 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑧 ∈ ( ⊥ ‘𝑆))) ∧ (𝑦(+g‘𝑊)𝑧) ∈ ( ⊥ ‘( ⊥
‘𝑆))) → (𝑧(·𝑖‘𝑊)𝑦) = (0g‘(Scalar‘𝑊))) |
| 30 | 22, 23, 7, 27 | iporthcom 21653 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑊 ∈ PreHil ∧ 𝑧 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) → ((𝑧(·𝑖‘𝑊)𝑦) = (0g‘(Scalar‘𝑊)) ↔ (𝑦(·𝑖‘𝑊)𝑧) = (0g‘(Scalar‘𝑊)))) |
| 31 | 16, 21, 19, 30 | syl3anc 1373 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑧 ∈ ( ⊥ ‘𝑆))) ∧ (𝑦(+g‘𝑊)𝑧) ∈ ( ⊥ ‘( ⊥
‘𝑆))) → ((𝑧(·𝑖‘𝑊)𝑦) = (0g‘(Scalar‘𝑊)) ↔ (𝑦(·𝑖‘𝑊)𝑧) = (0g‘(Scalar‘𝑊)))) |
| 32 | 29, 31 | mpbid 232 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑧 ∈ ( ⊥ ‘𝑆))) ∧ (𝑦(+g‘𝑊)𝑧) ∈ ( ⊥ ‘( ⊥
‘𝑆))) → (𝑦(·𝑖‘𝑊)𝑧) = (0g‘(Scalar‘𝑊))) |
| 33 | 32 | oveq1d 7446 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑧 ∈ ( ⊥ ‘𝑆))) ∧ (𝑦(+g‘𝑊)𝑧) ∈ ( ⊥ ‘( ⊥
‘𝑆))) → ((𝑦(·𝑖‘𝑊)𝑧)(+g‘(Scalar‘𝑊))(𝑧(·𝑖‘𝑊)𝑧)) = ((0g‘(Scalar‘𝑊))(+g‘(Scalar‘𝑊))(𝑧(·𝑖‘𝑊)𝑧))) |
| 34 | 16, 4 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑧 ∈ ( ⊥ ‘𝑆))) ∧ (𝑦(+g‘𝑊)𝑧) ∈ ( ⊥ ‘( ⊥
‘𝑆))) → 𝑊 ∈ LMod) |
| 35 | 22 | lmodfgrp 20867 |
. . . . . . . . . . . . . . . 16
⊢ (𝑊 ∈ LMod →
(Scalar‘𝑊) ∈
Grp) |
| 36 | 34, 35 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑧 ∈ ( ⊥ ‘𝑆))) ∧ (𝑦(+g‘𝑊)𝑧) ∈ ( ⊥ ‘( ⊥
‘𝑆))) →
(Scalar‘𝑊) ∈
Grp) |
| 37 | | eqid 2737 |
. . . . . . . . . . . . . . . . 17
⊢
(Base‘(Scalar‘𝑊)) = (Base‘(Scalar‘𝑊)) |
| 38 | 22, 23, 7, 37 | ipcl 21651 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑊 ∈ PreHil ∧ 𝑧 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉) → (𝑧(·𝑖‘𝑊)𝑧) ∈ (Base‘(Scalar‘𝑊))) |
| 39 | 16, 21, 21, 38 | syl3anc 1373 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑧 ∈ ( ⊥ ‘𝑆))) ∧ (𝑦(+g‘𝑊)𝑧) ∈ ( ⊥ ‘( ⊥
‘𝑆))) → (𝑧(·𝑖‘𝑊)𝑧) ∈ (Base‘(Scalar‘𝑊))) |
| 40 | 37, 24, 27 | grplid 18985 |
. . . . . . . . . . . . . . 15
⊢
(((Scalar‘𝑊)
∈ Grp ∧ (𝑧(·𝑖‘𝑊)𝑧) ∈ (Base‘(Scalar‘𝑊))) →
((0g‘(Scalar‘𝑊))(+g‘(Scalar‘𝑊))(𝑧(·𝑖‘𝑊)𝑧)) = (𝑧(·𝑖‘𝑊)𝑧)) |
| 41 | 36, 39, 40 | syl2anc 584 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑧 ∈ ( ⊥ ‘𝑆))) ∧ (𝑦(+g‘𝑊)𝑧) ∈ ( ⊥ ‘( ⊥
‘𝑆))) →
((0g‘(Scalar‘𝑊))(+g‘(Scalar‘𝑊))(𝑧(·𝑖‘𝑊)𝑧)) = (𝑧(·𝑖‘𝑊)𝑧)) |
| 42 | 26, 33, 41 | 3eqtrd 2781 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑧 ∈ ( ⊥ ‘𝑆))) ∧ (𝑦(+g‘𝑊)𝑧) ∈ ( ⊥ ‘( ⊥
‘𝑆))) → ((𝑦(+g‘𝑊)𝑧)(·𝑖‘𝑊)𝑧) = (𝑧(·𝑖‘𝑊)𝑧)) |
| 43 | | simpr 484 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑧 ∈ ( ⊥ ‘𝑆))) ∧ (𝑦(+g‘𝑊)𝑧) ∈ ( ⊥ ‘( ⊥
‘𝑆))) → (𝑦(+g‘𝑊)𝑧) ∈ ( ⊥ ‘( ⊥
‘𝑆))) |
| 44 | 7, 23, 22, 27, 8 | ocvi 21687 |
. . . . . . . . . . . . . 14
⊢ (((𝑦(+g‘𝑊)𝑧) ∈ ( ⊥ ‘( ⊥
‘𝑆)) ∧ 𝑧 ∈ ( ⊥ ‘𝑆)) → ((𝑦(+g‘𝑊)𝑧)(·𝑖‘𝑊)𝑧) = (0g‘(Scalar‘𝑊))) |
| 45 | 43, 20, 44 | syl2anc 584 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑧 ∈ ( ⊥ ‘𝑆))) ∧ (𝑦(+g‘𝑊)𝑧) ∈ ( ⊥ ‘( ⊥
‘𝑆))) → ((𝑦(+g‘𝑊)𝑧)(·𝑖‘𝑊)𝑧) = (0g‘(Scalar‘𝑊))) |
| 46 | 42, 45 | eqtr3d 2779 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑧 ∈ ( ⊥ ‘𝑆))) ∧ (𝑦(+g‘𝑊)𝑧) ∈ ( ⊥ ‘( ⊥
‘𝑆))) → (𝑧(·𝑖‘𝑊)𝑧) = (0g‘(Scalar‘𝑊))) |
| 47 | | eqid 2737 |
. . . . . . . . . . . . . 14
⊢
(0g‘𝑊) = (0g‘𝑊) |
| 48 | 22, 23, 7, 27, 47 | ipeq0 21656 |
. . . . . . . . . . . . 13
⊢ ((𝑊 ∈ PreHil ∧ 𝑧 ∈ 𝑉) → ((𝑧(·𝑖‘𝑊)𝑧) = (0g‘(Scalar‘𝑊)) ↔ 𝑧 = (0g‘𝑊))) |
| 49 | 16, 21, 48 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑧 ∈ ( ⊥ ‘𝑆))) ∧ (𝑦(+g‘𝑊)𝑧) ∈ ( ⊥ ‘( ⊥
‘𝑆))) → ((𝑧(·𝑖‘𝑊)𝑧) = (0g‘(Scalar‘𝑊)) ↔ 𝑧 = (0g‘𝑊))) |
| 50 | 46, 49 | mpbid 232 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑧 ∈ ( ⊥ ‘𝑆))) ∧ (𝑦(+g‘𝑊)𝑧) ∈ ( ⊥ ‘( ⊥
‘𝑆))) → 𝑧 = (0g‘𝑊)) |
| 51 | 50 | oveq2d 7447 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑧 ∈ ( ⊥ ‘𝑆))) ∧ (𝑦(+g‘𝑊)𝑧) ∈ ( ⊥ ‘( ⊥
‘𝑆))) → (𝑦(+g‘𝑊)𝑧) = (𝑦(+g‘𝑊)(0g‘𝑊))) |
| 52 | | lmodgrp 20865 |
. . . . . . . . . . . . 13
⊢ (𝑊 ∈ LMod → 𝑊 ∈ Grp) |
| 53 | 5, 52 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑊 ∈ Grp) |
| 54 | 53 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑧 ∈ ( ⊥ ‘𝑆))) ∧ (𝑦(+g‘𝑊)𝑧) ∈ ( ⊥ ‘( ⊥
‘𝑆))) → 𝑊 ∈ Grp) |
| 55 | 7, 11, 47 | grprid 18986 |
. . . . . . . . . . 11
⊢ ((𝑊 ∈ Grp ∧ 𝑦 ∈ 𝑉) → (𝑦(+g‘𝑊)(0g‘𝑊)) = 𝑦) |
| 56 | 54, 19, 55 | syl2anc 584 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑧 ∈ ( ⊥ ‘𝑆))) ∧ (𝑦(+g‘𝑊)𝑧) ∈ ( ⊥ ‘( ⊥
‘𝑆))) → (𝑦(+g‘𝑊)(0g‘𝑊)) = 𝑦) |
| 57 | 51, 56 | eqtrd 2777 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑧 ∈ ( ⊥ ‘𝑆))) ∧ (𝑦(+g‘𝑊)𝑧) ∈ ( ⊥ ‘( ⊥
‘𝑆))) → (𝑦(+g‘𝑊)𝑧) = 𝑦) |
| 58 | 57, 18 | eqeltrd 2841 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑧 ∈ ( ⊥ ‘𝑆))) ∧ (𝑦(+g‘𝑊)𝑧) ∈ ( ⊥ ‘( ⊥
‘𝑆))) → (𝑦(+g‘𝑊)𝑧) ∈ 𝑆) |
| 59 | 58 | ex 412 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑧 ∈ ( ⊥ ‘𝑆))) → ((𝑦(+g‘𝑊)𝑧) ∈ ( ⊥ ‘( ⊥
‘𝑆)) → (𝑦(+g‘𝑊)𝑧) ∈ 𝑆)) |
| 60 | | eleq1 2829 |
. . . . . . . 8
⊢ (𝑥 = (𝑦(+g‘𝑊)𝑧) → (𝑥 ∈ ( ⊥ ‘( ⊥
‘𝑆)) ↔ (𝑦(+g‘𝑊)𝑧) ∈ ( ⊥ ‘( ⊥
‘𝑆)))) |
| 61 | | eleq1 2829 |
. . . . . . . 8
⊢ (𝑥 = (𝑦(+g‘𝑊)𝑧) → (𝑥 ∈ 𝑆 ↔ (𝑦(+g‘𝑊)𝑧) ∈ 𝑆)) |
| 62 | 60, 61 | imbi12d 344 |
. . . . . . 7
⊢ (𝑥 = (𝑦(+g‘𝑊)𝑧) → ((𝑥 ∈ ( ⊥ ‘( ⊥
‘𝑆)) → 𝑥 ∈ 𝑆) ↔ ((𝑦(+g‘𝑊)𝑧) ∈ ( ⊥ ‘( ⊥
‘𝑆)) → (𝑦(+g‘𝑊)𝑧) ∈ 𝑆))) |
| 63 | 59, 62 | syl5ibrcom 247 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑧 ∈ ( ⊥ ‘𝑆))) → (𝑥 = (𝑦(+g‘𝑊)𝑧) → (𝑥 ∈ ( ⊥ ‘( ⊥
‘𝑆)) → 𝑥 ∈ 𝑆))) |
| 64 | 63 | rexlimdvva 3213 |
. . . . 5
⊢ (𝜑 → (∃𝑦 ∈ 𝑆 ∃𝑧 ∈ ( ⊥ ‘𝑆)𝑥 = (𝑦(+g‘𝑊)𝑧) → (𝑥 ∈ ( ⊥ ‘( ⊥
‘𝑆)) → 𝑥 ∈ 𝑆))) |
| 65 | 15, 64 | syld 47 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ ( ⊥ ‘( ⊥
‘𝑆)) → (𝑥 ∈ ( ⊥ ‘( ⊥
‘𝑆)) → 𝑥 ∈ 𝑆))) |
| 66 | 65 | pm2.43d 53 |
. . 3
⊢ (𝜑 → (𝑥 ∈ ( ⊥ ‘( ⊥
‘𝑆)) → 𝑥 ∈ 𝑆)) |
| 67 | 66 | ssrdv 3989 |
. 2
⊢ (𝜑 → ( ⊥ ‘( ⊥
‘𝑆)) ⊆ 𝑆) |
| 68 | | lsmcss.c |
. . . 4
⊢ 𝐶 = (ClSubSp‘𝑊) |
| 69 | 7, 68, 8 | iscss2 21704 |
. . 3
⊢ ((𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉) → (𝑆 ∈ 𝐶 ↔ ( ⊥ ‘( ⊥
‘𝑆)) ⊆ 𝑆)) |
| 70 | 3, 6, 69 | syl2anc 584 |
. 2
⊢ (𝜑 → (𝑆 ∈ 𝐶 ↔ ( ⊥ ‘( ⊥
‘𝑆)) ⊆ 𝑆)) |
| 71 | 67, 70 | mpbird 257 |
1
⊢ (𝜑 → 𝑆 ∈ 𝐶) |