Theorem resvval2

Description: Value of nontrivial structure restriction. (Contributed by Thierry Arnoux, 6-Sep-2018)

	Ref	Expression
Hypotheses	resvsca.r	⊢ 𝑅 = ( 𝑊 ↾v 𝐴 )
	resvsca.f	⊢ 𝐹 = ( Scalar ‘ 𝑊 )
	resvsca.b	⊢ 𝐵 = ( Base ‘ 𝐹 )
Assertion	resvval2	⊢ ( ( ¬ 𝐵 ⊆ 𝐴 ∧ 𝑊 ∈ 𝑋 ∧ 𝐴 ∈ 𝑌 ) → 𝑅 = ( 𝑊 sSet ⟨ ( Scalar ‘ ndx ) , ( 𝐹 ↾s 𝐴 ) ⟩ ) )

Proof

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 𝐴 ) ⟩ ) )