Step |
Hyp |
Ref |
Expression |
0 |
|
cprjsp |
⊢ ℙ𝕣𝕠𝕛 |
1 |
|
vv |
⊢ 𝑣 |
2 |
|
clvec |
⊢ LVec |
3 |
|
cbs |
⊢ Base |
4 |
1
|
cv |
⊢ 𝑣 |
5 |
4 3
|
cfv |
⊢ ( Base ‘ 𝑣 ) |
6 |
|
c0g |
⊢ 0g |
7 |
4 6
|
cfv |
⊢ ( 0g ‘ 𝑣 ) |
8 |
7
|
csn |
⊢ { ( 0g ‘ 𝑣 ) } |
9 |
5 8
|
cdif |
⊢ ( ( Base ‘ 𝑣 ) ∖ { ( 0g ‘ 𝑣 ) } ) |
10 |
|
vb |
⊢ 𝑏 |
11 |
10
|
cv |
⊢ 𝑏 |
12 |
|
vx |
⊢ 𝑥 |
13 |
|
vy |
⊢ 𝑦 |
14 |
12
|
cv |
⊢ 𝑥 |
15 |
14 11
|
wcel |
⊢ 𝑥 ∈ 𝑏 |
16 |
13
|
cv |
⊢ 𝑦 |
17 |
16 11
|
wcel |
⊢ 𝑦 ∈ 𝑏 |
18 |
15 17
|
wa |
⊢ ( 𝑥 ∈ 𝑏 ∧ 𝑦 ∈ 𝑏 ) |
19 |
|
vl |
⊢ 𝑙 |
20 |
|
csca |
⊢ Scalar |
21 |
4 20
|
cfv |
⊢ ( Scalar ‘ 𝑣 ) |
22 |
21 3
|
cfv |
⊢ ( Base ‘ ( Scalar ‘ 𝑣 ) ) |
23 |
19
|
cv |
⊢ 𝑙 |
24 |
|
cvsca |
⊢ ·𝑠 |
25 |
4 24
|
cfv |
⊢ ( ·𝑠 ‘ 𝑣 ) |
26 |
23 16 25
|
co |
⊢ ( 𝑙 ( ·𝑠 ‘ 𝑣 ) 𝑦 ) |
27 |
14 26
|
wceq |
⊢ 𝑥 = ( 𝑙 ( ·𝑠 ‘ 𝑣 ) 𝑦 ) |
28 |
27 19 22
|
wrex |
⊢ ∃ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑣 ) ) 𝑥 = ( 𝑙 ( ·𝑠 ‘ 𝑣 ) 𝑦 ) |
29 |
18 28
|
wa |
⊢ ( ( 𝑥 ∈ 𝑏 ∧ 𝑦 ∈ 𝑏 ) ∧ ∃ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑣 ) ) 𝑥 = ( 𝑙 ( ·𝑠 ‘ 𝑣 ) 𝑦 ) ) |
30 |
29 12 13
|
copab |
⊢ { 〈 𝑥 , 𝑦 〉 ∣ ( ( 𝑥 ∈ 𝑏 ∧ 𝑦 ∈ 𝑏 ) ∧ ∃ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑣 ) ) 𝑥 = ( 𝑙 ( ·𝑠 ‘ 𝑣 ) 𝑦 ) ) } |
31 |
11 30
|
cqs |
⊢ ( 𝑏 / { 〈 𝑥 , 𝑦 〉 ∣ ( ( 𝑥 ∈ 𝑏 ∧ 𝑦 ∈ 𝑏 ) ∧ ∃ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑣 ) ) 𝑥 = ( 𝑙 ( ·𝑠 ‘ 𝑣 ) 𝑦 ) ) } ) |
32 |
10 9 31
|
csb |
⊢ ⦋ ( ( Base ‘ 𝑣 ) ∖ { ( 0g ‘ 𝑣 ) } ) / 𝑏 ⦌ ( 𝑏 / { 〈 𝑥 , 𝑦 〉 ∣ ( ( 𝑥 ∈ 𝑏 ∧ 𝑦 ∈ 𝑏 ) ∧ ∃ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑣 ) ) 𝑥 = ( 𝑙 ( ·𝑠 ‘ 𝑣 ) 𝑦 ) ) } ) |
33 |
1 2 32
|
cmpt |
⊢ ( 𝑣 ∈ LVec ↦ ⦋ ( ( Base ‘ 𝑣 ) ∖ { ( 0g ‘ 𝑣 ) } ) / 𝑏 ⦌ ( 𝑏 / { 〈 𝑥 , 𝑦 〉 ∣ ( ( 𝑥 ∈ 𝑏 ∧ 𝑦 ∈ 𝑏 ) ∧ ∃ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑣 ) ) 𝑥 = ( 𝑙 ( ·𝑠 ‘ 𝑣 ) 𝑦 ) ) } ) ) |
34 |
0 33
|
wceq |
⊢ ℙ𝕣𝕠𝕛 = ( 𝑣 ∈ LVec ↦ ⦋ ( ( Base ‘ 𝑣 ) ∖ { ( 0g ‘ 𝑣 ) } ) / 𝑏 ⦌ ( 𝑏 / { 〈 𝑥 , 𝑦 〉 ∣ ( ( 𝑥 ∈ 𝑏 ∧ 𝑦 ∈ 𝑏 ) ∧ ∃ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑣 ) ) 𝑥 = ( 𝑙 ( ·𝑠 ‘ 𝑣 ) 𝑦 ) ) } ) ) |