Step |
Hyp |
Ref |
Expression |
1 |
|
phssip.x |
⊢ 𝑋 = ( 𝑊 ↾s 𝑈 ) |
2 |
|
phssip.s |
⊢ 𝑆 = ( LSubSp ‘ 𝑊 ) |
3 |
|
phssip.i |
⊢ · = ( ·if ‘ 𝑊 ) |
4 |
|
phssip.p |
⊢ 𝑃 = ( ·if ‘ 𝑋 ) |
5 |
|
eqid |
⊢ ( Base ‘ 𝑋 ) = ( Base ‘ 𝑋 ) |
6 |
|
eqid |
⊢ ( ·𝑖 ‘ 𝑋 ) = ( ·𝑖 ‘ 𝑋 ) |
7 |
5 6 4
|
ipffval |
⊢ 𝑃 = ( 𝑥 ∈ ( Base ‘ 𝑋 ) , 𝑦 ∈ ( Base ‘ 𝑋 ) ↦ ( 𝑥 ( ·𝑖 ‘ 𝑋 ) 𝑦 ) ) |
8 |
|
phllmod |
⊢ ( 𝑊 ∈ PreHil → 𝑊 ∈ LMod ) |
9 |
2
|
lsssubg |
⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) → 𝑈 ∈ ( SubGrp ‘ 𝑊 ) ) |
10 |
8 9
|
sylan |
⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑈 ∈ 𝑆 ) → 𝑈 ∈ ( SubGrp ‘ 𝑊 ) ) |
11 |
1
|
subgbas |
⊢ ( 𝑈 ∈ ( SubGrp ‘ 𝑊 ) → 𝑈 = ( Base ‘ 𝑋 ) ) |
12 |
10 11
|
syl |
⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑈 ∈ 𝑆 ) → 𝑈 = ( Base ‘ 𝑋 ) ) |
13 |
|
eqidd |
⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑈 ∈ 𝑆 ) → ( 𝑥 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) = ( 𝑥 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) ) |
14 |
12 12 13
|
mpoeq123dv |
⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑈 ∈ 𝑆 ) → ( 𝑥 ∈ 𝑈 , 𝑦 ∈ 𝑈 ↦ ( 𝑥 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) ) = ( 𝑥 ∈ ( Base ‘ 𝑋 ) , 𝑦 ∈ ( Base ‘ 𝑋 ) ↦ ( 𝑥 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) ) ) |
15 |
|
eqid |
⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 ) |
16 |
15
|
subgss |
⊢ ( 𝑈 ∈ ( SubGrp ‘ 𝑊 ) → 𝑈 ⊆ ( Base ‘ 𝑊 ) ) |
17 |
10 16
|
syl |
⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑈 ∈ 𝑆 ) → 𝑈 ⊆ ( Base ‘ 𝑊 ) ) |
18 |
|
resmpo |
⊢ ( ( 𝑈 ⊆ ( Base ‘ 𝑊 ) ∧ 𝑈 ⊆ ( Base ‘ 𝑊 ) ) → ( ( 𝑥 ∈ ( Base ‘ 𝑊 ) , 𝑦 ∈ ( Base ‘ 𝑊 ) ↦ ( 𝑥 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) ) ↾ ( 𝑈 × 𝑈 ) ) = ( 𝑥 ∈ 𝑈 , 𝑦 ∈ 𝑈 ↦ ( 𝑥 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) ) ) |
19 |
17 17 18
|
syl2anc |
⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑈 ∈ 𝑆 ) → ( ( 𝑥 ∈ ( Base ‘ 𝑊 ) , 𝑦 ∈ ( Base ‘ 𝑊 ) ↦ ( 𝑥 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) ) ↾ ( 𝑈 × 𝑈 ) ) = ( 𝑥 ∈ 𝑈 , 𝑦 ∈ 𝑈 ↦ ( 𝑥 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) ) ) |
20 |
|
eqid |
⊢ ( ·𝑖 ‘ 𝑊 ) = ( ·𝑖 ‘ 𝑊 ) |
21 |
1 20 6
|
ssipeq |
⊢ ( 𝑈 ∈ 𝑆 → ( ·𝑖 ‘ 𝑋 ) = ( ·𝑖 ‘ 𝑊 ) ) |
22 |
21
|
adantl |
⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑈 ∈ 𝑆 ) → ( ·𝑖 ‘ 𝑋 ) = ( ·𝑖 ‘ 𝑊 ) ) |
23 |
22
|
oveqd |
⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑈 ∈ 𝑆 ) → ( 𝑥 ( ·𝑖 ‘ 𝑋 ) 𝑦 ) = ( 𝑥 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) ) |
24 |
23
|
mpoeq3dv |
⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑈 ∈ 𝑆 ) → ( 𝑥 ∈ ( Base ‘ 𝑋 ) , 𝑦 ∈ ( Base ‘ 𝑋 ) ↦ ( 𝑥 ( ·𝑖 ‘ 𝑋 ) 𝑦 ) ) = ( 𝑥 ∈ ( Base ‘ 𝑋 ) , 𝑦 ∈ ( Base ‘ 𝑋 ) ↦ ( 𝑥 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) ) ) |
25 |
14 19 24
|
3eqtr4rd |
⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑈 ∈ 𝑆 ) → ( 𝑥 ∈ ( Base ‘ 𝑋 ) , 𝑦 ∈ ( Base ‘ 𝑋 ) ↦ ( 𝑥 ( ·𝑖 ‘ 𝑋 ) 𝑦 ) ) = ( ( 𝑥 ∈ ( Base ‘ 𝑊 ) , 𝑦 ∈ ( Base ‘ 𝑊 ) ↦ ( 𝑥 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) ) ↾ ( 𝑈 × 𝑈 ) ) ) |
26 |
7 25
|
syl5eq |
⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑈 ∈ 𝑆 ) → 𝑃 = ( ( 𝑥 ∈ ( Base ‘ 𝑊 ) , 𝑦 ∈ ( Base ‘ 𝑊 ) ↦ ( 𝑥 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) ) ↾ ( 𝑈 × 𝑈 ) ) ) |
27 |
15 20 3
|
ipffval |
⊢ · = ( 𝑥 ∈ ( Base ‘ 𝑊 ) , 𝑦 ∈ ( Base ‘ 𝑊 ) ↦ ( 𝑥 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) ) |
28 |
27
|
a1i |
⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑈 ∈ 𝑆 ) → · = ( 𝑥 ∈ ( Base ‘ 𝑊 ) , 𝑦 ∈ ( Base ‘ 𝑊 ) ↦ ( 𝑥 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) ) ) |
29 |
28
|
reseq1d |
⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑈 ∈ 𝑆 ) → ( · ↾ ( 𝑈 × 𝑈 ) ) = ( ( 𝑥 ∈ ( Base ‘ 𝑊 ) , 𝑦 ∈ ( Base ‘ 𝑊 ) ↦ ( 𝑥 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) ) ↾ ( 𝑈 × 𝑈 ) ) ) |
30 |
26 29
|
eqtr4d |
⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑈 ∈ 𝑆 ) → 𝑃 = ( · ↾ ( 𝑈 × 𝑈 ) ) ) |