Step | Hyp | Ref
| Expression |
1 | | scaid 17203 |
. . . . 5
β’ Scalar =
Slot (Scalarβndx) |
2 | | vscandxnscandx 17212 |
. . . . . 6
β’ (
Β·π βndx) β
(Scalarβndx) |
3 | 2 | necomi 2999 |
. . . . 5
β’
(Scalarβndx) β ( Β·π
βndx) |
4 | 1, 3 | setsnid 17088 |
. . . 4
β’
(Scalarβ(π
sSet β¨(Scalarβndx), (π βΎs π)β©)) = (Scalarβ((π sSet β¨(Scalarβndx),
(π βΎs
π)β©) sSet β¨(
Β·π βndx), (.rβπ)β©)) |
5 | | slotsdifipndx 17223 |
. . . . . 6
β’ ((
Β·π βndx) β
(Β·πβndx) β§ (Scalarβndx) β
(Β·πβndx)) |
6 | 5 | simpri 487 |
. . . . 5
β’
(Scalarβndx) β
(Β·πβndx) |
7 | 1, 6 | setsnid 17088 |
. . . 4
β’
(Scalarβ((π
sSet β¨(Scalarβndx), (π βΎs π)β©) sSet β¨(
Β·π βndx), (.rβπ)β©)) =
(Scalarβ(((π sSet
β¨(Scalarβndx), (π βΎs π)β©) sSet β¨(
Β·π βndx), (.rβπ)β©) sSet
β¨(Β·πβndx),
(.rβπ)β©)) |
8 | 4, 7 | eqtri 2765 |
. . 3
β’
(Scalarβ(π
sSet β¨(Scalarβndx), (π βΎs π)β©)) = (Scalarβ(((π sSet β¨(Scalarβndx),
(π βΎs
π)β©) sSet β¨(
Β·π βndx), (.rβπ)β©) sSet
β¨(Β·πβndx),
(.rβπ)β©)) |
9 | | ovexd 7397 |
. . . 4
β’ (π β (π βΎs π) β V) |
10 | 1 | setsid 17087 |
. . . 4
β’ ((π β V β§ (π βΎs π) β V) β (π βΎs π) = (Scalarβ(π sSet β¨(Scalarβndx),
(π βΎs
π)β©))) |
11 | 9, 10 | sylan2 594 |
. . 3
β’ ((π β V β§ π) β (π βΎs π) = (Scalarβ(π sSet β¨(Scalarβndx), (π βΎs π)β©))) |
12 | | srapart.a |
. . . . . 6
β’ (π β π΄ = ((subringAlg βπ)βπ)) |
13 | 12 | adantl 483 |
. . . . 5
β’ ((π β V β§ π) β π΄ = ((subringAlg βπ)βπ)) |
14 | | srapart.s |
. . . . . 6
β’ (π β π β (Baseβπ)) |
15 | | sraval 20653 |
. . . . . 6
β’ ((π β V β§ π β (Baseβπ)) β ((subringAlg
βπ)βπ) = (((π sSet β¨(Scalarβndx), (π βΎs π)β©) sSet β¨(
Β·π βndx), (.rβπ)β©) sSet
β¨(Β·πβndx),
(.rβπ)β©)) |
16 | 14, 15 | sylan2 594 |
. . . . 5
β’ ((π β V β§ π) β ((subringAlg βπ)βπ) = (((π sSet β¨(Scalarβndx), (π βΎs π)β©) sSet β¨(
Β·π βndx), (.rβπ)β©) sSet
β¨(Β·πβndx),
(.rβπ)β©)) |
17 | 13, 16 | eqtrd 2777 |
. . . 4
β’ ((π β V β§ π) β π΄ = (((π sSet β¨(Scalarβndx), (π βΎs π)β©) sSet β¨(
Β·π βndx), (.rβπ)β©) sSet
β¨(Β·πβndx),
(.rβπ)β©)) |
18 | 17 | fveq2d 6851 |
. . 3
β’ ((π β V β§ π) β (Scalarβπ΄) = (Scalarβ(((π sSet β¨(Scalarβndx), (π βΎs π)β©) sSet β¨(
Β·π βndx), (.rβπ)β©) sSet
β¨(Β·πβndx),
(.rβπ)β©))) |
19 | 8, 11, 18 | 3eqtr4a 2803 |
. 2
β’ ((π β V β§ π) β (π βΎs π) = (Scalarβπ΄)) |
20 | 1 | str0 17068 |
. . 3
β’ β
=
(Scalarββ
) |
21 | | reldmress 17121 |
. . . . 5
β’ Rel dom
βΎs |
22 | 21 | ovprc1 7401 |
. . . 4
β’ (Β¬
π β V β (π βΎs π) = β
) |
23 | 22 | adantr 482 |
. . 3
β’ ((Β¬
π β V β§ π) β (π βΎs π) = β
) |
24 | | fv2prc 6892 |
. . . . 5
β’ (Β¬
π β V β
((subringAlg βπ)βπ) = β
) |
25 | 12, 24 | sylan9eqr 2799 |
. . . 4
β’ ((Β¬
π β V β§ π) β π΄ = β
) |
26 | 25 | fveq2d 6851 |
. . 3
β’ ((Β¬
π β V β§ π) β (Scalarβπ΄) =
(Scalarββ
)) |
27 | 20, 23, 26 | 3eqtr4a 2803 |
. 2
β’ ((Β¬
π β V β§ π) β (π βΎs π) = (Scalarβπ΄)) |
28 | 19, 27 | pm2.61ian 811 |
1
β’ (π β (π βΎs π) = (Scalarβπ΄)) |