Metamath Proof Explorer

Theorem resvlem

Description: Other elements of a structure restriction. (Contributed by Thierry Arnoux, 6-Sep-2018)

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

Proof

Step Hyp Ref Expression
1 resvlem.r ⊢ 𝑅 = ( 𝑊 ↾v 𝐴 )
2 resvlem.e ⊢ 𝐶 = ( 𝐸 ‘ 𝑊 )
3 resvlem.f ⊢ 𝐸 = Slot 𝑁
4 resvlem.n ⊢ 𝑁 ∈ ℕ
5 resvlem.b ⊢ 𝑁 ≠ 5
6 eqid ⊢ ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑊 )
7 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝑊 ) ) = ( Base ‘ ( Scalar ‘ 𝑊 ) )
8 1 6 7 resvid2 ⊢ ( ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ⊆ 𝐴 ∧ 𝑊 ∈ V ∧ 𝐴 ∈ 𝑉 ) → 𝑅 = 𝑊 )
9 8 fveq2d ⊢ ( ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ⊆ 𝐴 ∧ 𝑊 ∈ V ∧ 𝐴 ∈ 𝑉 ) → ( 𝐸 ‘ 𝑅 ) = ( 𝐸 ‘ 𝑊 ) )
10 9 3expib ⊢ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ⊆ 𝐴 → ( ( 𝑊 ∈ V ∧ 𝐴 ∈ 𝑉 ) → ( 𝐸 ‘ 𝑅 ) = ( 𝐸 ‘ 𝑊 ) ) )
11 1 6 7 resvval2 ⊢ ( ( ¬ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ⊆ 𝐴 ∧ 𝑊 ∈ V ∧ 𝐴 ∈ 𝑉 ) → 𝑅 = ( 𝑊 sSet ⟨ ( Scalar ‘ ndx ) , ( ( Scalar ‘ 𝑊 ) ↾s 𝐴 ) ⟩ ) )
12 11 fveq2d ⊢ ( ( ¬ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ⊆ 𝐴 ∧ 𝑊 ∈ V ∧ 𝐴 ∈ 𝑉 ) → ( 𝐸 ‘ 𝑅 ) = ( 𝐸 ‘ ( 𝑊 sSet ⟨ ( Scalar ‘ ndx ) , ( ( Scalar ‘ 𝑊 ) ↾s 𝐴 ) ⟩ ) ) )
13 3 4 ndxid ⊢ 𝐸 = Slot ( 𝐸 ‘ ndx )
14 3 4 ndxarg ⊢ ( 𝐸 ‘ ndx ) = 𝑁
15 14 5 eqnetri ⊢ ( 𝐸 ‘ ndx ) ≠ 5
16 scandx ⊢ ( Scalar ‘ ndx ) = 5
17 15 16 neeqtrri ⊢ ( 𝐸 ‘ ndx ) ≠ ( Scalar ‘ ndx )
18 13 17 setsnid ⊢ ( 𝐸 ‘ 𝑊 ) = ( 𝐸 ‘ ( 𝑊 sSet ⟨ ( Scalar ‘ ndx ) , ( ( Scalar ‘ 𝑊 ) ↾s 𝐴 ) ⟩ ) )
19 12 18 eqtr4di ⊢ ( ( ¬ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ⊆ 𝐴 ∧ 𝑊 ∈ V ∧ 𝐴 ∈ 𝑉 ) → ( 𝐸 ‘ 𝑅 ) = ( 𝐸 ‘ 𝑊 ) )
20 19 3expib ⊢ ( ¬ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ⊆ 𝐴 → ( ( 𝑊 ∈ V ∧ 𝐴 ∈ 𝑉 ) → ( 𝐸 ‘ 𝑅 ) = ( 𝐸 ‘ 𝑊 ) ) )
21 10 20 pm2.61i ⊢ ( ( 𝑊 ∈ V ∧ 𝐴 ∈ 𝑉 ) → ( 𝐸 ‘ 𝑅 ) = ( 𝐸 ‘ 𝑊 ) )
22 reldmresv ⊢ Rel dom ↾v
23 22 ovprc1 ⊢ ( ¬ 𝑊 ∈ V → ( 𝑊 ↾v 𝐴 ) = ∅ )
24 1 23 syl5eq ⊢ ( ¬ 𝑊 ∈ V → 𝑅 = ∅ )
25 24 fveq2d ⊢ ( ¬ 𝑊 ∈ V → ( 𝐸 ‘ 𝑅 ) = ( 𝐸 ‘ ∅ ) )
26 3 str0 ⊢ ∅ = ( 𝐸 ‘ ∅ )
27 25 26 eqtr4di ⊢ ( ¬ 𝑊 ∈ V → ( 𝐸 ‘ 𝑅 ) = ∅ )
28 fvprc ⊢ ( ¬ 𝑊 ∈ V → ( 𝐸 ‘ 𝑊 ) = ∅ )
29 27 28 eqtr4d ⊢ ( ¬ 𝑊 ∈ V → ( 𝐸 ‘ 𝑅 ) = ( 𝐸 ‘ 𝑊 ) )
30 29 adantr ⊢ ( ( ¬ 𝑊 ∈ V ∧ 𝐴 ∈ 𝑉 ) → ( 𝐸 ‘ 𝑅 ) = ( 𝐸 ‘ 𝑊 ) )
31 21 30 pm2.61ian ⊢ ( 𝐴 ∈ 𝑉 → ( 𝐸 ‘ 𝑅 ) = ( 𝐸 ‘ 𝑊 ) )
32 2 31 eqtr4id ⊢ ( 𝐴 ∈ 𝑉 → 𝐶 = ( 𝐸 ‘ 𝑅 ) )