Description: General behavior of trivial restriction. (Contributed by Thierry Arnoux, 6-Sep-2018)
Ref | Expression | ||
---|---|---|---|
Hypotheses | resvsca.r | ⊢ 𝑅 = ( 𝑊 ↾v 𝐴 ) | |
resvsca.f | ⊢ 𝐹 = ( Scalar ‘ 𝑊 ) | ||
resvsca.b | ⊢ 𝐵 = ( Base ‘ 𝐹 ) | ||
Assertion | resvid2 | ⊢ ( ( 𝐵 ⊆ 𝐴 ∧ 𝑊 ∈ 𝑋 ∧ 𝐴 ∈ 𝑌 ) → 𝑅 = 𝑊 ) |
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 | iftrue | ⊢ ( 𝐵 ⊆ 𝐴 → if ( 𝐵 ⊆ 𝐴 , 𝑊 , ( 𝑊 sSet 〈 ( Scalar ‘ ndx ) , ( 𝐹 ↾s 𝐴 ) 〉 ) ) = 𝑊 ) | |
6 | 4 5 | sylan9eqr | ⊢ ( ( 𝐵 ⊆ 𝐴 ∧ ( 𝑊 ∈ 𝑋 ∧ 𝐴 ∈ 𝑌 ) ) → 𝑅 = 𝑊 ) |
7 | 6 | 3impb | ⊢ ( ( 𝐵 ⊆ 𝐴 ∧ 𝑊 ∈ 𝑋 ∧ 𝐴 ∈ 𝑌 ) → 𝑅 = 𝑊 ) |