Step | Hyp | Ref
| Expression |
1 | | resvsca.f |
. . . . 5
β’ πΉ = (Scalarβπ) |
2 | 1 | fvexi 6857 |
. . . . . . 7
β’ πΉ β V |
3 | | eqid 2733 |
. . . . . . . 8
β’ (πΉ βΎs π΄) = (πΉ βΎs π΄) |
4 | | resvsca.b |
. . . . . . . 8
β’ π΅ = (BaseβπΉ) |
5 | 3, 4 | ressid2 17121 |
. . . . . . 7
β’ ((π΅ β π΄ β§ πΉ β V β§ π΄ β π) β (πΉ βΎs π΄) = πΉ) |
6 | 2, 5 | mp3an2 1450 |
. . . . . 6
β’ ((π΅ β π΄ β§ π΄ β π) β (πΉ βΎs π΄) = πΉ) |
7 | 6 | 3adant2 1132 |
. . . . 5
β’ ((π΅ β π΄ β§ π β V β§ π΄ β π) β (πΉ βΎs π΄) = πΉ) |
8 | | resvsca.r |
. . . . . . 7
β’ π
= (π βΎv π΄) |
9 | 8, 1, 4 | resvid2 32166 |
. . . . . 6
β’ ((π΅ β π΄ β§ π β V β§ π΄ β π) β π
= π) |
10 | 9 | fveq2d 6847 |
. . . . 5
β’ ((π΅ β π΄ β§ π β V β§ π΄ β π) β (Scalarβπ
) = (Scalarβπ)) |
11 | 1, 7, 10 | 3eqtr4a 2799 |
. . . 4
β’ ((π΅ β π΄ β§ π β V β§ π΄ β π) β (πΉ βΎs π΄) = (Scalarβπ
)) |
12 | 11 | 3expib 1123 |
. . 3
β’ (π΅ β π΄ β ((π β V β§ π΄ β π) β (πΉ βΎs π΄) = (Scalarβπ
))) |
13 | | simp2 1138 |
. . . . . 6
β’ ((Β¬
π΅ β π΄ β§ π β V β§ π΄ β π) β π β V) |
14 | | ovex 7391 |
. . . . . 6
β’ (πΉ βΎs π΄) β V |
15 | | scaid 17201 |
. . . . . . 7
β’ Scalar =
Slot (Scalarβndx) |
16 | 15 | setsid 17085 |
. . . . . 6
β’ ((π β V β§ (πΉ βΎs π΄) β V) β (πΉ βΎs π΄) = (Scalarβ(π sSet β¨(Scalarβndx),
(πΉ βΎs
π΄)β©))) |
17 | 13, 14, 16 | sylancl 587 |
. . . . 5
β’ ((Β¬
π΅ β π΄ β§ π β V β§ π΄ β π) β (πΉ βΎs π΄) = (Scalarβ(π sSet β¨(Scalarβndx), (πΉ βΎs π΄)β©))) |
18 | 8, 1, 4 | resvval2 32167 |
. . . . . 6
β’ ((Β¬
π΅ β π΄ β§ π β V β§ π΄ β π) β π
= (π sSet β¨(Scalarβndx), (πΉ βΎs π΄)β©)) |
19 | 18 | fveq2d 6847 |
. . . . 5
β’ ((Β¬
π΅ β π΄ β§ π β V β§ π΄ β π) β (Scalarβπ
) = (Scalarβ(π sSet β¨(Scalarβndx), (πΉ βΎs π΄)β©))) |
20 | 17, 19 | eqtr4d 2776 |
. . . 4
β’ ((Β¬
π΅ β π΄ β§ π β V β§ π΄ β π) β (πΉ βΎs π΄) = (Scalarβπ
)) |
21 | 20 | 3expib 1123 |
. . 3
β’ (Β¬
π΅ β π΄ β ((π β V β§ π΄ β π) β (πΉ βΎs π΄) = (Scalarβπ
))) |
22 | 12, 21 | pm2.61i 182 |
. 2
β’ ((π β V β§ π΄ β π) β (πΉ βΎs π΄) = (Scalarβπ
)) |
23 | | 0fv 6887 |
. . . . 5
β’
(β
β(Scalarβndx)) = β
|
24 | | 0ex 5265 |
. . . . . 6
β’ β
β V |
25 | 24, 15 | strfvn 17063 |
. . . . 5
β’
(Scalarββ
) =
(β
β(Scalarβndx)) |
26 | | ress0 17129 |
. . . . 5
β’ (β
βΎs π΄) =
β
|
27 | 23, 25, 26 | 3eqtr4ri 2772 |
. . . 4
β’ (β
βΎs π΄) =
(Scalarββ
) |
28 | | fvprc 6835 |
. . . . . 6
β’ (Β¬
π β V β
(Scalarβπ) =
β
) |
29 | 1, 28 | eqtrid 2785 |
. . . . 5
β’ (Β¬
π β V β πΉ = β
) |
30 | 29 | oveq1d 7373 |
. . . 4
β’ (Β¬
π β V β (πΉ βΎs π΄) = (β
βΎs
π΄)) |
31 | | reldmresv 32164 |
. . . . . . 7
β’ Rel dom
βΎv |
32 | 31 | ovprc1 7397 |
. . . . . 6
β’ (Β¬
π β V β (π βΎv π΄) = β
) |
33 | 8, 32 | eqtrid 2785 |
. . . . 5
β’ (Β¬
π β V β π
= β
) |
34 | 33 | fveq2d 6847 |
. . . 4
β’ (Β¬
π β V β
(Scalarβπ
) =
(Scalarββ
)) |
35 | 27, 30, 34 | 3eqtr4a 2799 |
. . 3
β’ (Β¬
π β V β (πΉ βΎs π΄) = (Scalarβπ
)) |
36 | 35 | adantr 482 |
. 2
β’ ((Β¬
π β V β§ π΄ β π) β (πΉ βΎs π΄) = (Scalarβπ
)) |
37 | 22, 36 | pm2.61ian 811 |
1
β’ (π΄ β π β (πΉ βΎs π΄) = (Scalarβπ
)) |