This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem resvsca

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

Ref Expression
Hypotheses resvsca.r ⊢ 𝑅 = ( 𝑊 ↾v 𝐴 )
resvsca.f ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
resvsca.b ⊢ 𝐵 = ( Base ‘ 𝐹 )
Assertion resvsca ( 𝐴 ∈ 𝑉 → ( 𝐹 ↾s 𝐴 ) = ( Scalar ‘ 𝑅 ) )

Proof

Step Hyp Ref Expression
1 resvsca.r ⊢ 𝑅 = ( 𝑊 ↾v 𝐴 )
2 resvsca.f ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
3 resvsca.b ⊢ 𝐵 = ( Base ‘ 𝐹 )
4 2 fvexi ⊢ 𝐹 ∈ V
5 eqid ⊢ ( 𝐹 ↾s 𝐴 ) = ( 𝐹 ↾s 𝐴 )
6 5 3 ressid2 ⊢ ( ( 𝐵 ⊆ 𝐴 ∧ 𝐹 ∈ V ∧ 𝐴 ∈ 𝑉 ) → ( 𝐹 ↾s 𝐴 ) = 𝐹 )
7 4 6 mp3an2 ⊢ ( ( 𝐵 ⊆ 𝐴 ∧ 𝐴 ∈ 𝑉 ) → ( 𝐹 ↾s 𝐴 ) = 𝐹 )
8 7 3adant2 ⊢ ( ( 𝐵 ⊆ 𝐴 ∧ 𝑊 ∈ V ∧ 𝐴 ∈ 𝑉 ) → ( 𝐹 ↾s 𝐴 ) = 𝐹 )
9 1 2 3 resvid2 ⊢ ( ( 𝐵 ⊆ 𝐴 ∧ 𝑊 ∈ V ∧ 𝐴 ∈ 𝑉 ) → 𝑅 = 𝑊 )
10 9 fveq2d ⊢ ( ( 𝐵 ⊆ 𝐴 ∧ 𝑊 ∈ V ∧ 𝐴 ∈ 𝑉 ) → ( Scalar ‘ 𝑅 ) = ( Scalar ‘ 𝑊 ) )
11 2 8 10 3eqtr4a ⊢ ( ( 𝐵 ⊆ 𝐴 ∧ 𝑊 ∈ V ∧ 𝐴 ∈ 𝑉 ) → ( 𝐹 ↾s 𝐴 ) = ( Scalar ‘ 𝑅 ) )
12 11 3expib ⊢ ( 𝐵 ⊆ 𝐴 → ( ( 𝑊 ∈ V ∧ 𝐴 ∈ 𝑉 ) → ( 𝐹 ↾s 𝐴 ) = ( Scalar ‘ 𝑅 ) ) )
13 simp2 ⊢ ( ( ¬ 𝐵 ⊆ 𝐴 ∧ 𝑊 ∈ V ∧ 𝐴 ∈ 𝑉 ) → 𝑊 ∈ V )
14 ovex ⊢ ( 𝐹 ↾s 𝐴 ) ∈ V
15 scaid ⊢ Scalar = Slot ( Scalar ‘ ndx )
16 15 setsid ⊢ ( ( 𝑊 ∈ V ∧ ( 𝐹 ↾s 𝐴 ) ∈ V ) → ( 𝐹 ↾s 𝐴 ) = ( Scalar ‘ ( 𝑊 sSet ⟨ ( Scalar ‘ ndx ) , ( 𝐹 ↾s 𝐴 ) ⟩ ) ) )
17 13 14 16 sylancl ⊢ ( ( ¬ 𝐵 ⊆ 𝐴 ∧ 𝑊 ∈ V ∧ 𝐴 ∈ 𝑉 ) → ( 𝐹 ↾s 𝐴 ) = ( Scalar ‘ ( 𝑊 sSet ⟨ ( Scalar ‘ ndx ) , ( 𝐹 ↾s 𝐴 ) ⟩ ) ) )
18 1 2 3 resvval2 ⊢ ( ( ¬ 𝐵 ⊆ 𝐴 ∧ 𝑊 ∈ V ∧ 𝐴 ∈ 𝑉 ) → 𝑅 = ( 𝑊 sSet ⟨ ( Scalar ‘ ndx ) , ( 𝐹 ↾s 𝐴 ) ⟩ ) )
19 18 fveq2d ⊢ ( ( ¬ 𝐵 ⊆ 𝐴 ∧ 𝑊 ∈ V ∧ 𝐴 ∈ 𝑉 ) → ( Scalar ‘ 𝑅 ) = ( Scalar ‘ ( 𝑊 sSet ⟨ ( Scalar ‘ ndx ) , ( 𝐹 ↾s 𝐴 ) ⟩ ) ) )
20 17 19 eqtr4d ⊢ ( ( ¬ 𝐵 ⊆ 𝐴 ∧ 𝑊 ∈ V ∧ 𝐴 ∈ 𝑉 ) → ( 𝐹 ↾s 𝐴 ) = ( Scalar ‘ 𝑅 ) )
21 20 3expib ⊢ ( ¬ 𝐵 ⊆ 𝐴 → ( ( 𝑊 ∈ V ∧ 𝐴 ∈ 𝑉 ) → ( 𝐹 ↾s 𝐴 ) = ( Scalar ‘ 𝑅 ) ) )
22 12 21 pm2.61i ⊢ ( ( 𝑊 ∈ V ∧ 𝐴 ∈ 𝑉 ) → ( 𝐹 ↾s 𝐴 ) = ( Scalar ‘ 𝑅 ) )
23 0fv ⊢ ( ∅ ‘ ( Scalar ‘ ndx ) ) = ∅
24 0ex ⊢ ∅ ∈ V
25 24 15 strfvn ⊢ ( Scalar ‘ ∅ ) = ( ∅ ‘ ( Scalar ‘ ndx ) )
26 ress0 ⊢ ( ∅ ↾s 𝐴 ) = ∅
27 23 25 26 3eqtr4ri ⊢ ( ∅ ↾s 𝐴 ) = ( Scalar ‘ ∅ )
28 fvprc ⊢ ( ¬ 𝑊 ∈ V → ( Scalar ‘ 𝑊 ) = ∅ )
29 2 28 eqtrid ⊢ ( ¬ 𝑊 ∈ V → 𝐹 = ∅ )
30 29 oveq1d ⊢ ( ¬ 𝑊 ∈ V → ( 𝐹 ↾s 𝐴 ) = ( ∅ ↾s 𝐴 ) )
31 reldmresv ⊢ Rel dom ↾v
32 31 ovprc1 ⊢ ( ¬ 𝑊 ∈ V → ( 𝑊 ↾v 𝐴 ) = ∅ )
33 1 32 eqtrid ⊢ ( ¬ 𝑊 ∈ V → 𝑅 = ∅ )
34 33 fveq2d ⊢ ( ¬ 𝑊 ∈ V → ( Scalar ‘ 𝑅 ) = ( Scalar ‘ ∅ ) )
35 27 30 34 3eqtr4a ⊢ ( ¬ 𝑊 ∈ V → ( 𝐹 ↾s 𝐴 ) = ( Scalar ‘ 𝑅 ) )
36 35 adantr ⊢ ( ( ¬ 𝑊 ∈ V ∧ 𝐴 ∈ 𝑉 ) → ( 𝐹 ↾s 𝐴 ) = ( Scalar ‘ 𝑅 ) )
37 22 36 pm2.61ian ⊢ ( 𝐴 ∈ 𝑉 → ( 𝐹 ↾s 𝐴 ) = ( Scalar ‘ 𝑅 ) )