Step |
Hyp |
Ref |
Expression |
1 |
|
resvsca.r |
⊢ 𝑅 = ( 𝑊 ↾v 𝐴 ) |
2 |
|
resvsca.f |
⊢ 𝐹 = ( Scalar ‘ 𝑊 ) |
3 |
|
resvsca.b |
⊢ 𝐵 = ( Base ‘ 𝐹 ) |
4 |
1 2 3
|
resvval |
⊢ ( ( 𝑊 ∈ 𝑋 ∧ 𝐴 ∈ 𝑌 ) → 𝑅 = if ( 𝐵 ⊆ 𝐴 , 𝑊 , ( 𝑊 sSet 〈 ( Scalar ‘ ndx ) , ( 𝐹 ↾s 𝐴 ) 〉 ) ) ) |
5 |
|
iffalse |
⊢ ( ¬ 𝐵 ⊆ 𝐴 → if ( 𝐵 ⊆ 𝐴 , 𝑊 , ( 𝑊 sSet 〈 ( Scalar ‘ ndx ) , ( 𝐹 ↾s 𝐴 ) 〉 ) ) = ( 𝑊 sSet 〈 ( Scalar ‘ ndx ) , ( 𝐹 ↾s 𝐴 ) 〉 ) ) |
6 |
4 5
|
sylan9eqr |
⊢ ( ( ¬ 𝐵 ⊆ 𝐴 ∧ ( 𝑊 ∈ 𝑋 ∧ 𝐴 ∈ 𝑌 ) ) → 𝑅 = ( 𝑊 sSet 〈 ( Scalar ‘ ndx ) , ( 𝐹 ↾s 𝐴 ) 〉 ) ) |
7 |
6
|
3impb |
⊢ ( ( ¬ 𝐵 ⊆ 𝐴 ∧ 𝑊 ∈ 𝑋 ∧ 𝐴 ∈ 𝑌 ) → 𝑅 = ( 𝑊 sSet 〈 ( Scalar ‘ ndx ) , ( 𝐹 ↾s 𝐴 ) 〉 ) ) |