Step | Hyp | Ref
| Expression |
1 | | resvlemOLD.e |
. 2
β’ πΆ = (πΈβπ) |
2 | | resvlemOLD.r |
. . . . . . 7
β’ π
= (π βΎv π΄) |
3 | | eqid 2733 |
. . . . . . 7
β’
(Scalarβπ) =
(Scalarβπ) |
4 | | eqid 2733 |
. . . . . . 7
β’
(Baseβ(Scalarβπ)) = (Baseβ(Scalarβπ)) |
5 | 2, 3, 4 | resvid2 32166 |
. . . . . 6
β’
(((Baseβ(Scalarβπ)) β π΄ β§ π β V β§ π΄ β π) β π
= π) |
6 | 5 | fveq2d 6847 |
. . . . 5
β’
(((Baseβ(Scalarβπ)) β π΄ β§ π β V β§ π΄ β π) β (πΈβπ
) = (πΈβπ)) |
7 | 6 | 3expib 1123 |
. . . 4
β’
((Baseβ(Scalarβπ)) β π΄ β ((π β V β§ π΄ β π) β (πΈβπ
) = (πΈβπ))) |
8 | 2, 3, 4 | resvval2 32167 |
. . . . . . 7
β’ ((Β¬
(Baseβ(Scalarβπ)) β π΄ β§ π β V β§ π΄ β π) β π
= (π sSet β¨(Scalarβndx),
((Scalarβπ)
βΎs π΄)β©)) |
9 | 8 | fveq2d 6847 |
. . . . . 6
β’ ((Β¬
(Baseβ(Scalarβπ)) β π΄ β§ π β V β§ π΄ β π) β (πΈβπ
) = (πΈβ(π sSet β¨(Scalarβndx),
((Scalarβπ)
βΎs π΄)β©))) |
10 | | resvlemOLD.f |
. . . . . . . 8
β’ πΈ = Slot π |
11 | | resvlemOLD.n |
. . . . . . . 8
β’ π β β |
12 | 10, 11 | ndxid 17074 |
. . . . . . 7
β’ πΈ = Slot (πΈβndx) |
13 | 10, 11 | ndxarg 17073 |
. . . . . . . . 9
β’ (πΈβndx) = π |
14 | | resvlemOLD.b |
. . . . . . . . 9
β’ π β 5 |
15 | 13, 14 | eqnetri 3011 |
. . . . . . . 8
β’ (πΈβndx) β
5 |
16 | | scandx 17200 |
. . . . . . . 8
β’
(Scalarβndx) = 5 |
17 | 15, 16 | neeqtrri 3014 |
. . . . . . 7
β’ (πΈβndx) β
(Scalarβndx) |
18 | 12, 17 | setsnid 17086 |
. . . . . 6
β’ (πΈβπ) = (πΈβ(π sSet β¨(Scalarβndx),
((Scalarβπ)
βΎs π΄)β©)) |
19 | 9, 18 | eqtr4di 2791 |
. . . . 5
β’ ((Β¬
(Baseβ(Scalarβπ)) β π΄ β§ π β V β§ π΄ β π) β (πΈβπ
) = (πΈβπ)) |
20 | 19 | 3expib 1123 |
. . . 4
β’ (Β¬
(Baseβ(Scalarβπ)) β π΄ β ((π β V β§ π΄ β π) β (πΈβπ
) = (πΈβπ))) |
21 | 7, 20 | pm2.61i 182 |
. . 3
β’ ((π β V β§ π΄ β π) β (πΈβπ
) = (πΈβπ)) |
22 | | reldmresv 32164 |
. . . . . . . . 9
β’ Rel dom
βΎv |
23 | 22 | ovprc1 7397 |
. . . . . . . 8
β’ (Β¬
π β V β (π βΎv π΄) = β
) |
24 | 2, 23 | eqtrid 2785 |
. . . . . . 7
β’ (Β¬
π β V β π
= β
) |
25 | 24 | fveq2d 6847 |
. . . . . 6
β’ (Β¬
π β V β (πΈβπ
) = (πΈββ
)) |
26 | 10 | str0 17066 |
. . . . . 6
β’ β
=
(πΈββ
) |
27 | 25, 26 | eqtr4di 2791 |
. . . . 5
β’ (Β¬
π β V β (πΈβπ
) = β
) |
28 | | fvprc 6835 |
. . . . 5
β’ (Β¬
π β V β (πΈβπ) = β
) |
29 | 27, 28 | eqtr4d 2776 |
. . . 4
β’ (Β¬
π β V β (πΈβπ
) = (πΈβπ)) |
30 | 29 | adantr 482 |
. . 3
β’ ((Β¬
π β V β§ π΄ β π) β (πΈβπ
) = (πΈβπ)) |
31 | 21, 30 | pm2.61ian 811 |
. 2
β’ (π΄ β π β (πΈβπ
) = (πΈβπ)) |
32 | 1, 31 | eqtr4id 2792 |
1
β’ (π΄ β π β πΆ = (πΈβπ
)) |