Mathbox for Thierry Arnoux < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  resvlem Structured version   Visualization version   GIF version

Theorem resvlem 30940
 Description: Other elements of a structure restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.)
Hypotheses
Ref Expression
resvlem.r 𝑅 = (𝑊v 𝐴)
resvlem.e 𝐶 = (𝐸𝑊)
resvlem.f 𝐸 = Slot 𝑁
resvlem.n 𝑁 ∈ ℕ
resvlem.b 𝑁 ≠ 5
Assertion
Ref Expression
resvlem (𝐴𝑉𝐶 = (𝐸𝑅))

Proof of Theorem resvlem
StepHypRef Expression
1 resvlem.r . . . . . . 7 𝑅 = (𝑊v 𝐴)
2 eqid 2824 . . . . . . 7 (Scalar‘𝑊) = (Scalar‘𝑊)
3 eqid 2824 . . . . . . 7 (Base‘(Scalar‘𝑊)) = (Base‘(Scalar‘𝑊))
41, 2, 3resvid2 30937 . . . . . 6 (((Base‘(Scalar‘𝑊)) ⊆ 𝐴𝑊 ∈ V ∧ 𝐴𝑉) → 𝑅 = 𝑊)
54fveq2d 6665 . . . . 5 (((Base‘(Scalar‘𝑊)) ⊆ 𝐴𝑊 ∈ V ∧ 𝐴𝑉) → (𝐸𝑅) = (𝐸𝑊))
653expib 1119 . . . 4 ((Base‘(Scalar‘𝑊)) ⊆ 𝐴 → ((𝑊 ∈ V ∧ 𝐴𝑉) → (𝐸𝑅) = (𝐸𝑊)))
71, 2, 3resvval2 30938 . . . . . . 7 ((¬ (Base‘(Scalar‘𝑊)) ⊆ 𝐴𝑊 ∈ V ∧ 𝐴𝑉) → 𝑅 = (𝑊 sSet ⟨(Scalar‘ndx), ((Scalar‘𝑊) ↾s 𝐴)⟩))
87fveq2d 6665 . . . . . 6 ((¬ (Base‘(Scalar‘𝑊)) ⊆ 𝐴𝑊 ∈ V ∧ 𝐴𝑉) → (𝐸𝑅) = (𝐸‘(𝑊 sSet ⟨(Scalar‘ndx), ((Scalar‘𝑊) ↾s 𝐴)⟩)))
9 resvlem.f . . . . . . . 8 𝐸 = Slot 𝑁
10 resvlem.n . . . . . . . 8 𝑁 ∈ ℕ
119, 10ndxid 16509 . . . . . . 7 𝐸 = Slot (𝐸‘ndx)
129, 10ndxarg 16508 . . . . . . . . 9 (𝐸‘ndx) = 𝑁
13 resvlem.b . . . . . . . . 9 𝑁 ≠ 5
1412, 13eqnetri 3084 . . . . . . . 8 (𝐸‘ndx) ≠ 5
15 scandx 16632 . . . . . . . 8 (Scalar‘ndx) = 5
1614, 15neeqtrri 3087 . . . . . . 7 (𝐸‘ndx) ≠ (Scalar‘ndx)
1711, 16setsnid 16539 . . . . . 6 (𝐸𝑊) = (𝐸‘(𝑊 sSet ⟨(Scalar‘ndx), ((Scalar‘𝑊) ↾s 𝐴)⟩))
188, 17syl6eqr 2877 . . . . 5 ((¬ (Base‘(Scalar‘𝑊)) ⊆ 𝐴𝑊 ∈ V ∧ 𝐴𝑉) → (𝐸𝑅) = (𝐸𝑊))
19183expib 1119 . . . 4 (¬ (Base‘(Scalar‘𝑊)) ⊆ 𝐴 → ((𝑊 ∈ V ∧ 𝐴𝑉) → (𝐸𝑅) = (𝐸𝑊)))
206, 19pm2.61i 185 . . 3 ((𝑊 ∈ V ∧ 𝐴𝑉) → (𝐸𝑅) = (𝐸𝑊))
21 reldmresv 30935 . . . . . . . . 9 Rel dom ↾v
2221ovprc1 7188 . . . . . . . 8 𝑊 ∈ V → (𝑊v 𝐴) = ∅)
231, 22syl5eq 2871 . . . . . . 7 𝑊 ∈ V → 𝑅 = ∅)
2423fveq2d 6665 . . . . . 6 𝑊 ∈ V → (𝐸𝑅) = (𝐸‘∅))
259str0 16535 . . . . . 6 ∅ = (𝐸‘∅)
2624, 25syl6eqr 2877 . . . . 5 𝑊 ∈ V → (𝐸𝑅) = ∅)
27 fvprc 6654 . . . . 5 𝑊 ∈ V → (𝐸𝑊) = ∅)
2826, 27eqtr4d 2862 . . . 4 𝑊 ∈ V → (𝐸𝑅) = (𝐸𝑊))
2928adantr 484 . . 3 ((¬ 𝑊 ∈ V ∧ 𝐴𝑉) → (𝐸𝑅) = (𝐸𝑊))
3020, 29pm2.61ian 811 . 2 (𝐴𝑉 → (𝐸𝑅) = (𝐸𝑊))
31 resvlem.e . 2 𝐶 = (𝐸𝑊)
3230, 31syl6reqr 2878 1 (𝐴𝑉𝐶 = (𝐸𝑅))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 399   ∧ w3a 1084   = wceq 1538   ∈ wcel 2115   ≠ wne 3014  Vcvv 3480   ⊆ wss 3919  ∅c0 4276  ⟨cop 4556  ‘cfv 6343  (class class class)co 7149  ℕcn 11634  5c5 11692  ndxcnx 16480   sSet csts 16481  Slot cslot 16482  Basecbs 16483   ↾s cress 16484  Scalarcsca 16568   ↾v cresv 30933 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796  ax-sep 5189  ax-nul 5196  ax-pow 5253  ax-pr 5317  ax-un 7455  ax-cnex 10591  ax-1cn 10593  ax-addcl 10595 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-mo 2624  df-eu 2655  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2964  df-ne 3015  df-ral 3138  df-rex 3139  df-reu 3140  df-rab 3142  df-v 3482  df-sbc 3759  df-csb 3867  df-dif 3922  df-un 3924  df-in 3926  df-ss 3936  df-pss 3938  df-nul 4277  df-if 4451  df-pw 4524  df-sn 4551  df-pr 4553  df-tp 4555  df-op 4557  df-uni 4825  df-iun 4907  df-br 5053  df-opab 5115  df-mpt 5133  df-tr 5159  df-id 5447  df-eprel 5452  df-po 5461  df-so 5462  df-fr 5501  df-we 5503  df-xp 5548  df-rel 5549  df-cnv 5550  df-co 5551  df-dm 5552  df-rn 5553  df-res 5554  df-ima 5555  df-pred 6135  df-ord 6181  df-on 6182  df-lim 6183  df-suc 6184  df-iota 6302  df-fun 6345  df-fn 6346  df-f 6347  df-f1 6348  df-fo 6349  df-f1o 6350  df-fv 6351  df-ov 7152  df-oprab 7153  df-mpo 7154  df-om 7575  df-wrecs 7943  df-recs 8004  df-rdg 8042  df-nn 11635  df-2 11697  df-3 11698  df-4 11699  df-5 11700  df-ndx 16486  df-slot 16487  df-sets 16490  df-sca 16581  df-resv 30934 This theorem is referenced by:  resvbas  30941  resvplusg  30942  resvvsca  30943  resvmulr  30944
 Copyright terms: Public domain W3C validator