Metamath Proof Explorer

Theorem resvlem

Description: Other elements of a scalar restriction. (Contributed by Thierry Arnoux, 6-Sep-2018) (Revised by AV, 31-Oct-2024)

Ref Expression
Hypotheses resvlem.r ⊢ 𝑅 = ( 𝑊 ↾v 𝐴 )
resvlem.e ⊢ 𝐶 = ( 𝐸 ‘ 𝑊 )
resvlem.f ⊢ 𝐸 = Slot ( 𝐸 ‘ ndx )
resvlem.n ⊢ ( 𝐸 ‘ ndx ) ≠ ( Scalar ‘ ndx )
Assertion resvlem ( 𝐴 ∈ 𝑉 → 𝐶 = ( 𝐸 ‘ 𝑅 ) )

Proof

Step Hyp Ref Expression
1 resvlem.r ⊢ 𝑅 = ( 𝑊 ↾v 𝐴 )
2 resvlem.e ⊢ 𝐶 = ( 𝐸 ‘ 𝑊 )
3 resvlem.f ⊢ 𝐸 = Slot ( 𝐸 ‘ ndx )
4 resvlem.n ⊢ ( 𝐸 ‘ ndx ) ≠ ( Scalar ‘ ndx )
5 eqid ⊢ ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑊 )
6 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝑊 ) ) = ( Base ‘ ( Scalar ‘ 𝑊 ) )
7 1 5 6 resvid2 ⊢ ( ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ⊆ 𝐴 ∧ 𝑊 ∈ V ∧ 𝐴 ∈ 𝑉 ) → 𝑅 = 𝑊 )
8 7 fveq2d ⊢ ( ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ⊆ 𝐴 ∧ 𝑊 ∈ V ∧ 𝐴 ∈ 𝑉 ) → ( 𝐸 ‘ 𝑅 ) = ( 𝐸 ‘ 𝑊 ) )
9 8 3expib ⊢ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ⊆ 𝐴 → ( ( 𝑊 ∈ V ∧ 𝐴 ∈ 𝑉 ) → ( 𝐸 ‘ 𝑅 ) = ( 𝐸 ‘ 𝑊 ) ) )
10 1 5 6 resvval2 ⊢ ( ( ¬ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ⊆ 𝐴 ∧ 𝑊 ∈ V ∧ 𝐴 ∈ 𝑉 ) → 𝑅 = ( 𝑊 sSet ⟨ ( Scalar ‘ ndx ) , ( ( Scalar ‘ 𝑊 ) ↾s 𝐴 ) ⟩ ) )
11 10 fveq2d ⊢ ( ( ¬ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ⊆ 𝐴 ∧ 𝑊 ∈ V ∧ 𝐴 ∈ 𝑉 ) → ( 𝐸 ‘ 𝑅 ) = ( 𝐸 ‘ ( 𝑊 sSet ⟨ ( Scalar ‘ ndx ) , ( ( Scalar ‘ 𝑊 ) ↾s 𝐴 ) ⟩ ) ) )
12 3 4 setsnid ⊢ ( 𝐸 ‘ 𝑊 ) = ( 𝐸 ‘ ( 𝑊 sSet ⟨ ( Scalar ‘ ndx ) , ( ( Scalar ‘ 𝑊 ) ↾s 𝐴 ) ⟩ ) )
13 11 12 eqtr4di ⊢ ( ( ¬ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ⊆ 𝐴 ∧ 𝑊 ∈ V ∧ 𝐴 ∈ 𝑉 ) → ( 𝐸 ‘ 𝑅 ) = ( 𝐸 ‘ 𝑊 ) )
14 13 3expib ⊢ ( ¬ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ⊆ 𝐴 → ( ( 𝑊 ∈ V ∧ 𝐴 ∈ 𝑉 ) → ( 𝐸 ‘ 𝑅 ) = ( 𝐸 ‘ 𝑊 ) ) )
15 9 14 pm2.61i ⊢ ( ( 𝑊 ∈ V ∧ 𝐴 ∈ 𝑉 ) → ( 𝐸 ‘ 𝑅 ) = ( 𝐸 ‘ 𝑊 ) )
16 3 str0 ⊢ ∅ = ( 𝐸 ‘ ∅ )
17 16 eqcomi ⊢ ( 𝐸 ‘ ∅ ) = ∅
18 reldmresv ⊢ Rel dom ↾v
19 17 1 18 oveqprc ⊢ ( ¬ 𝑊 ∈ V → ( 𝐸 ‘ 𝑊 ) = ( 𝐸 ‘ 𝑅 ) )
20 19 eqcomd ⊢ ( ¬ 𝑊 ∈ V → ( 𝐸 ‘ 𝑅 ) = ( 𝐸 ‘ 𝑊 ) )
21 20 adantr ⊢ ( ( ¬ 𝑊 ∈ V ∧ 𝐴 ∈ 𝑉 ) → ( 𝐸 ‘ 𝑅 ) = ( 𝐸 ‘ 𝑊 ) )
22 15 21 pm2.61ian ⊢ ( 𝐴 ∈ 𝑉 → ( 𝐸 ‘ 𝑅 ) = ( 𝐸 ‘ 𝑊 ) )
23 2 22 eqtr4id ⊢ ( 𝐴 ∈ 𝑉 → 𝐶 = ( 𝐸 ‘ 𝑅 ) )