Step | Hyp | Ref
| Expression |
1 | | simpll 767 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑠 ⊆ 𝐵) ∧ (𝑧 ∈ 𝑃 ∧ (𝑎 ∈ 𝑠 ∧ 𝑏 ∈ 𝑠))) → 𝜑) |
2 | | simprl 771 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑠 ⊆ 𝐵) ∧ (𝑧 ∈ 𝑃 ∧ (𝑎 ∈ 𝑠 ∧ 𝑏 ∈ 𝑠))) → 𝑧 ∈ 𝑃) |
3 | | simplr 769 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑠 ⊆ 𝐵) ∧ (𝑧 ∈ 𝑃 ∧ (𝑎 ∈ 𝑠 ∧ 𝑏 ∈ 𝑠))) → 𝑠 ⊆ 𝐵) |
4 | | simprrl 781 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑠 ⊆ 𝐵) ∧ (𝑧 ∈ 𝑃 ∧ (𝑎 ∈ 𝑠 ∧ 𝑏 ∈ 𝑠))) → 𝑎 ∈ 𝑠) |
5 | 3, 4 | sseldd 3902 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑠 ⊆ 𝐵) ∧ (𝑧 ∈ 𝑃 ∧ (𝑎 ∈ 𝑠 ∧ 𝑏 ∈ 𝑠))) → 𝑎 ∈ 𝐵) |
6 | | lsspropd.s1 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝐵)) → (𝑥( ·𝑠
‘𝐾)𝑦) ∈ 𝑊) |
7 | 6 | ralrimivva 3112 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝐵 (𝑥( ·𝑠
‘𝐾)𝑦) ∈ 𝑊) |
8 | 7 | ad2antrr 726 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑠 ⊆ 𝐵) ∧ (𝑧 ∈ 𝑃 ∧ (𝑎 ∈ 𝑠 ∧ 𝑏 ∈ 𝑠))) → ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝐵 (𝑥( ·𝑠
‘𝐾)𝑦) ∈ 𝑊) |
9 | | ovrspc2v 7239 |
. . . . . . . . . . . . . 14
⊢ (((𝑧 ∈ 𝑃 ∧ 𝑎 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝐵 (𝑥( ·𝑠
‘𝐾)𝑦) ∈ 𝑊) → (𝑧( ·𝑠
‘𝐾)𝑎) ∈ 𝑊) |
10 | 2, 5, 8, 9 | syl21anc 838 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑠 ⊆ 𝐵) ∧ (𝑧 ∈ 𝑃 ∧ (𝑎 ∈ 𝑠 ∧ 𝑏 ∈ 𝑠))) → (𝑧( ·𝑠
‘𝐾)𝑎) ∈ 𝑊) |
11 | | lsspropd.w |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐵 ⊆ 𝑊) |
12 | 11 | ad2antrr 726 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑠 ⊆ 𝐵) ∧ (𝑧 ∈ 𝑃 ∧ (𝑎 ∈ 𝑠 ∧ 𝑏 ∈ 𝑠))) → 𝐵 ⊆ 𝑊) |
13 | | simprrr 782 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑠 ⊆ 𝐵) ∧ (𝑧 ∈ 𝑃 ∧ (𝑎 ∈ 𝑠 ∧ 𝑏 ∈ 𝑠))) → 𝑏 ∈ 𝑠) |
14 | 3, 13 | sseldd 3902 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑠 ⊆ 𝐵) ∧ (𝑧 ∈ 𝑃 ∧ (𝑎 ∈ 𝑠 ∧ 𝑏 ∈ 𝑠))) → 𝑏 ∈ 𝐵) |
15 | 12, 14 | sseldd 3902 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑠 ⊆ 𝐵) ∧ (𝑧 ∈ 𝑃 ∧ (𝑎 ∈ 𝑠 ∧ 𝑏 ∈ 𝑠))) → 𝑏 ∈ 𝑊) |
16 | | lsspropd.p |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → (𝑥(+g‘𝐾)𝑦) = (𝑥(+g‘𝐿)𝑦)) |
17 | 16 | oveqrspc2v 7240 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ ((𝑧( ·𝑠
‘𝐾)𝑎) ∈ 𝑊 ∧ 𝑏 ∈ 𝑊)) → ((𝑧( ·𝑠
‘𝐾)𝑎)(+g‘𝐾)𝑏) = ((𝑧( ·𝑠
‘𝐾)𝑎)(+g‘𝐿)𝑏)) |
18 | 1, 10, 15, 17 | syl12anc 837 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑠 ⊆ 𝐵) ∧ (𝑧 ∈ 𝑃 ∧ (𝑎 ∈ 𝑠 ∧ 𝑏 ∈ 𝑠))) → ((𝑧( ·𝑠
‘𝐾)𝑎)(+g‘𝐾)𝑏) = ((𝑧( ·𝑠
‘𝐾)𝑎)(+g‘𝐿)𝑏)) |
19 | | lsspropd.s2 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝐵)) → (𝑥( ·𝑠
‘𝐾)𝑦) = (𝑥( ·𝑠
‘𝐿)𝑦)) |
20 | 19 | oveqrspc2v 7240 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑃 ∧ 𝑎 ∈ 𝐵)) → (𝑧( ·𝑠
‘𝐾)𝑎) = (𝑧( ·𝑠
‘𝐿)𝑎)) |
21 | 1, 2, 5, 20 | syl12anc 837 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑠 ⊆ 𝐵) ∧ (𝑧 ∈ 𝑃 ∧ (𝑎 ∈ 𝑠 ∧ 𝑏 ∈ 𝑠))) → (𝑧( ·𝑠
‘𝐾)𝑎) = (𝑧( ·𝑠
‘𝐿)𝑎)) |
22 | 21 | oveq1d 7228 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑠 ⊆ 𝐵) ∧ (𝑧 ∈ 𝑃 ∧ (𝑎 ∈ 𝑠 ∧ 𝑏 ∈ 𝑠))) → ((𝑧( ·𝑠
‘𝐾)𝑎)(+g‘𝐿)𝑏) = ((𝑧( ·𝑠
‘𝐿)𝑎)(+g‘𝐿)𝑏)) |
23 | 18, 22 | eqtrd 2777 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑠 ⊆ 𝐵) ∧ (𝑧 ∈ 𝑃 ∧ (𝑎 ∈ 𝑠 ∧ 𝑏 ∈ 𝑠))) → ((𝑧( ·𝑠
‘𝐾)𝑎)(+g‘𝐾)𝑏) = ((𝑧( ·𝑠
‘𝐿)𝑎)(+g‘𝐿)𝑏)) |
24 | 23 | eleq1d 2822 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑠 ⊆ 𝐵) ∧ (𝑧 ∈ 𝑃 ∧ (𝑎 ∈ 𝑠 ∧ 𝑏 ∈ 𝑠))) → (((𝑧( ·𝑠
‘𝐾)𝑎)(+g‘𝐾)𝑏) ∈ 𝑠 ↔ ((𝑧( ·𝑠
‘𝐿)𝑎)(+g‘𝐿)𝑏) ∈ 𝑠)) |
25 | 24 | anassrs 471 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑠 ⊆ 𝐵) ∧ 𝑧 ∈ 𝑃) ∧ (𝑎 ∈ 𝑠 ∧ 𝑏 ∈ 𝑠)) → (((𝑧( ·𝑠
‘𝐾)𝑎)(+g‘𝐾)𝑏) ∈ 𝑠 ↔ ((𝑧( ·𝑠
‘𝐿)𝑎)(+g‘𝐿)𝑏) ∈ 𝑠)) |
26 | 25 | 2ralbidva 3119 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑠 ⊆ 𝐵) ∧ 𝑧 ∈ 𝑃) → (∀𝑎 ∈ 𝑠 ∀𝑏 ∈ 𝑠 ((𝑧( ·𝑠
‘𝐾)𝑎)(+g‘𝐾)𝑏) ∈ 𝑠 ↔ ∀𝑎 ∈ 𝑠 ∀𝑏 ∈ 𝑠 ((𝑧( ·𝑠
‘𝐿)𝑎)(+g‘𝐿)𝑏) ∈ 𝑠)) |
27 | 26 | ralbidva 3117 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ⊆ 𝐵) → (∀𝑧 ∈ 𝑃 ∀𝑎 ∈ 𝑠 ∀𝑏 ∈ 𝑠 ((𝑧( ·𝑠
‘𝐾)𝑎)(+g‘𝐾)𝑏) ∈ 𝑠 ↔ ∀𝑧 ∈ 𝑃 ∀𝑎 ∈ 𝑠 ∀𝑏 ∈ 𝑠 ((𝑧( ·𝑠
‘𝐿)𝑎)(+g‘𝐿)𝑏) ∈ 𝑠)) |
28 | 27 | anbi2d 632 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑠 ⊆ 𝐵) → ((𝑠 ≠ ∅ ∧ ∀𝑧 ∈ 𝑃 ∀𝑎 ∈ 𝑠 ∀𝑏 ∈ 𝑠 ((𝑧( ·𝑠
‘𝐾)𝑎)(+g‘𝐾)𝑏) ∈ 𝑠) ↔ (𝑠 ≠ ∅ ∧ ∀𝑧 ∈ 𝑃 ∀𝑎 ∈ 𝑠 ∀𝑏 ∈ 𝑠 ((𝑧( ·𝑠
‘𝐿)𝑎)(+g‘𝐿)𝑏) ∈ 𝑠))) |
29 | 28 | pm5.32da 582 |
. . . . 5
⊢ (𝜑 → ((𝑠 ⊆ 𝐵 ∧ (𝑠 ≠ ∅ ∧ ∀𝑧 ∈ 𝑃 ∀𝑎 ∈ 𝑠 ∀𝑏 ∈ 𝑠 ((𝑧( ·𝑠
‘𝐾)𝑎)(+g‘𝐾)𝑏) ∈ 𝑠)) ↔ (𝑠 ⊆ 𝐵 ∧ (𝑠 ≠ ∅ ∧ ∀𝑧 ∈ 𝑃 ∀𝑎 ∈ 𝑠 ∀𝑏 ∈ 𝑠 ((𝑧( ·𝑠
‘𝐿)𝑎)(+g‘𝐿)𝑏) ∈ 𝑠)))) |
30 | | 3anass 1097 |
. . . . 5
⊢ ((𝑠 ⊆ 𝐵 ∧ 𝑠 ≠ ∅ ∧ ∀𝑧 ∈ 𝑃 ∀𝑎 ∈ 𝑠 ∀𝑏 ∈ 𝑠 ((𝑧( ·𝑠
‘𝐾)𝑎)(+g‘𝐾)𝑏) ∈ 𝑠) ↔ (𝑠 ⊆ 𝐵 ∧ (𝑠 ≠ ∅ ∧ ∀𝑧 ∈ 𝑃 ∀𝑎 ∈ 𝑠 ∀𝑏 ∈ 𝑠 ((𝑧( ·𝑠
‘𝐾)𝑎)(+g‘𝐾)𝑏) ∈ 𝑠))) |
31 | | 3anass 1097 |
. . . . 5
⊢ ((𝑠 ⊆ 𝐵 ∧ 𝑠 ≠ ∅ ∧ ∀𝑧 ∈ 𝑃 ∀𝑎 ∈ 𝑠 ∀𝑏 ∈ 𝑠 ((𝑧( ·𝑠
‘𝐿)𝑎)(+g‘𝐿)𝑏) ∈ 𝑠) ↔ (𝑠 ⊆ 𝐵 ∧ (𝑠 ≠ ∅ ∧ ∀𝑧 ∈ 𝑃 ∀𝑎 ∈ 𝑠 ∀𝑏 ∈ 𝑠 ((𝑧( ·𝑠
‘𝐿)𝑎)(+g‘𝐿)𝑏) ∈ 𝑠))) |
32 | 29, 30, 31 | 3bitr4g 317 |
. . . 4
⊢ (𝜑 → ((𝑠 ⊆ 𝐵 ∧ 𝑠 ≠ ∅ ∧ ∀𝑧 ∈ 𝑃 ∀𝑎 ∈ 𝑠 ∀𝑏 ∈ 𝑠 ((𝑧( ·𝑠
‘𝐾)𝑎)(+g‘𝐾)𝑏) ∈ 𝑠) ↔ (𝑠 ⊆ 𝐵 ∧ 𝑠 ≠ ∅ ∧ ∀𝑧 ∈ 𝑃 ∀𝑎 ∈ 𝑠 ∀𝑏 ∈ 𝑠 ((𝑧( ·𝑠
‘𝐿)𝑎)(+g‘𝐿)𝑏) ∈ 𝑠))) |
33 | | lsspropd.b1 |
. . . . . 6
⊢ (𝜑 → 𝐵 = (Base‘𝐾)) |
34 | 33 | sseq2d 3933 |
. . . . 5
⊢ (𝜑 → (𝑠 ⊆ 𝐵 ↔ 𝑠 ⊆ (Base‘𝐾))) |
35 | | lsspropd.p1 |
. . . . . 6
⊢ (𝜑 → 𝑃 = (Base‘(Scalar‘𝐾))) |
36 | 35 | raleqdv 3325 |
. . . . 5
⊢ (𝜑 → (∀𝑧 ∈ 𝑃 ∀𝑎 ∈ 𝑠 ∀𝑏 ∈ 𝑠 ((𝑧( ·𝑠
‘𝐾)𝑎)(+g‘𝐾)𝑏) ∈ 𝑠 ↔ ∀𝑧 ∈ (Base‘(Scalar‘𝐾))∀𝑎 ∈ 𝑠 ∀𝑏 ∈ 𝑠 ((𝑧( ·𝑠
‘𝐾)𝑎)(+g‘𝐾)𝑏) ∈ 𝑠)) |
37 | 34, 36 | 3anbi13d 1440 |
. . . 4
⊢ (𝜑 → ((𝑠 ⊆ 𝐵 ∧ 𝑠 ≠ ∅ ∧ ∀𝑧 ∈ 𝑃 ∀𝑎 ∈ 𝑠 ∀𝑏 ∈ 𝑠 ((𝑧( ·𝑠
‘𝐾)𝑎)(+g‘𝐾)𝑏) ∈ 𝑠) ↔ (𝑠 ⊆ (Base‘𝐾) ∧ 𝑠 ≠ ∅ ∧ ∀𝑧 ∈
(Base‘(Scalar‘𝐾))∀𝑎 ∈ 𝑠 ∀𝑏 ∈ 𝑠 ((𝑧( ·𝑠
‘𝐾)𝑎)(+g‘𝐾)𝑏) ∈ 𝑠))) |
38 | | lsspropd.b2 |
. . . . . 6
⊢ (𝜑 → 𝐵 = (Base‘𝐿)) |
39 | 38 | sseq2d 3933 |
. . . . 5
⊢ (𝜑 → (𝑠 ⊆ 𝐵 ↔ 𝑠 ⊆ (Base‘𝐿))) |
40 | | lsspropd.p2 |
. . . . . 6
⊢ (𝜑 → 𝑃 = (Base‘(Scalar‘𝐿))) |
41 | 40 | raleqdv 3325 |
. . . . 5
⊢ (𝜑 → (∀𝑧 ∈ 𝑃 ∀𝑎 ∈ 𝑠 ∀𝑏 ∈ 𝑠 ((𝑧( ·𝑠
‘𝐿)𝑎)(+g‘𝐿)𝑏) ∈ 𝑠 ↔ ∀𝑧 ∈ (Base‘(Scalar‘𝐿))∀𝑎 ∈ 𝑠 ∀𝑏 ∈ 𝑠 ((𝑧( ·𝑠
‘𝐿)𝑎)(+g‘𝐿)𝑏) ∈ 𝑠)) |
42 | 39, 41 | 3anbi13d 1440 |
. . . 4
⊢ (𝜑 → ((𝑠 ⊆ 𝐵 ∧ 𝑠 ≠ ∅ ∧ ∀𝑧 ∈ 𝑃 ∀𝑎 ∈ 𝑠 ∀𝑏 ∈ 𝑠 ((𝑧( ·𝑠
‘𝐿)𝑎)(+g‘𝐿)𝑏) ∈ 𝑠) ↔ (𝑠 ⊆ (Base‘𝐿) ∧ 𝑠 ≠ ∅ ∧ ∀𝑧 ∈
(Base‘(Scalar‘𝐿))∀𝑎 ∈ 𝑠 ∀𝑏 ∈ 𝑠 ((𝑧( ·𝑠
‘𝐿)𝑎)(+g‘𝐿)𝑏) ∈ 𝑠))) |
43 | 32, 37, 42 | 3bitr3d 312 |
. . 3
⊢ (𝜑 → ((𝑠 ⊆ (Base‘𝐾) ∧ 𝑠 ≠ ∅ ∧ ∀𝑧 ∈
(Base‘(Scalar‘𝐾))∀𝑎 ∈ 𝑠 ∀𝑏 ∈ 𝑠 ((𝑧( ·𝑠
‘𝐾)𝑎)(+g‘𝐾)𝑏) ∈ 𝑠) ↔ (𝑠 ⊆ (Base‘𝐿) ∧ 𝑠 ≠ ∅ ∧ ∀𝑧 ∈
(Base‘(Scalar‘𝐿))∀𝑎 ∈ 𝑠 ∀𝑏 ∈ 𝑠 ((𝑧( ·𝑠
‘𝐿)𝑎)(+g‘𝐿)𝑏) ∈ 𝑠))) |
44 | | eqid 2737 |
. . . 4
⊢
(Scalar‘𝐾) =
(Scalar‘𝐾) |
45 | | eqid 2737 |
. . . 4
⊢
(Base‘(Scalar‘𝐾)) = (Base‘(Scalar‘𝐾)) |
46 | | eqid 2737 |
. . . 4
⊢
(Base‘𝐾) =
(Base‘𝐾) |
47 | | eqid 2737 |
. . . 4
⊢
(+g‘𝐾) = (+g‘𝐾) |
48 | | eqid 2737 |
. . . 4
⊢ (
·𝑠 ‘𝐾) = ( ·𝑠
‘𝐾) |
49 | | eqid 2737 |
. . . 4
⊢
(LSubSp‘𝐾) =
(LSubSp‘𝐾) |
50 | 44, 45, 46, 47, 48, 49 | islss 19971 |
. . 3
⊢ (𝑠 ∈ (LSubSp‘𝐾) ↔ (𝑠 ⊆ (Base‘𝐾) ∧ 𝑠 ≠ ∅ ∧ ∀𝑧 ∈
(Base‘(Scalar‘𝐾))∀𝑎 ∈ 𝑠 ∀𝑏 ∈ 𝑠 ((𝑧( ·𝑠
‘𝐾)𝑎)(+g‘𝐾)𝑏) ∈ 𝑠)) |
51 | | eqid 2737 |
. . . 4
⊢
(Scalar‘𝐿) =
(Scalar‘𝐿) |
52 | | eqid 2737 |
. . . 4
⊢
(Base‘(Scalar‘𝐿)) = (Base‘(Scalar‘𝐿)) |
53 | | eqid 2737 |
. . . 4
⊢
(Base‘𝐿) =
(Base‘𝐿) |
54 | | eqid 2737 |
. . . 4
⊢
(+g‘𝐿) = (+g‘𝐿) |
55 | | eqid 2737 |
. . . 4
⊢ (
·𝑠 ‘𝐿) = ( ·𝑠
‘𝐿) |
56 | | eqid 2737 |
. . . 4
⊢
(LSubSp‘𝐿) =
(LSubSp‘𝐿) |
57 | 51, 52, 53, 54, 55, 56 | islss 19971 |
. . 3
⊢ (𝑠 ∈ (LSubSp‘𝐿) ↔ (𝑠 ⊆ (Base‘𝐿) ∧ 𝑠 ≠ ∅ ∧ ∀𝑧 ∈
(Base‘(Scalar‘𝐿))∀𝑎 ∈ 𝑠 ∀𝑏 ∈ 𝑠 ((𝑧( ·𝑠
‘𝐿)𝑎)(+g‘𝐿)𝑏) ∈ 𝑠)) |
58 | 43, 50, 57 | 3bitr4g 317 |
. 2
⊢ (𝜑 → (𝑠 ∈ (LSubSp‘𝐾) ↔ 𝑠 ∈ (LSubSp‘𝐿))) |
59 | 58 | eqrdv 2735 |
1
⊢ (𝜑 → (LSubSp‘𝐾) = (LSubSp‘𝐿)) |