Step | Hyp | Ref
| Expression |
1 | | ovex 7444 |
. . . 4
β’ ((π sSet β¨(Scalarβndx),
(π βΎs
π)β©) sSet β¨(
Β·π βndx), (.rβπ)β©) β
V |
2 | | fvex 6903 |
. . . 4
β’
(.rβπ) β V |
3 | | ipid 17280 |
. . . . 5
β’
Β·π = Slot
(Β·πβndx) |
4 | 3 | setsid 17145 |
. . . 4
β’ ((((π sSet β¨(Scalarβndx),
(π βΎs
π)β©) sSet β¨(
Β·π βndx), (.rβπ)β©) β V β§
(.rβπ)
β V) β (.rβπ) =
(Β·πβ(((π sSet β¨(Scalarβndx), (π βΎs π)β©) sSet β¨(
Β·π βndx), (.rβπ)β©) sSet
β¨(Β·πβndx),
(.rβπ)β©))) |
5 | 1, 2, 4 | mp2an 688 |
. . 3
β’
(.rβπ) =
(Β·πβ(((π sSet β¨(Scalarβndx), (π βΎs π)β©) sSet β¨(
Β·π βndx), (.rβπ)β©) sSet
β¨(Β·πβndx),
(.rβπ)β©)) |
6 | | srapart.a |
. . . . . 6
β’ (π β π΄ = ((subringAlg βπ)βπ)) |
7 | 6 | adantl 480 |
. . . . 5
β’ ((π β V β§ π) β π΄ = ((subringAlg βπ)βπ)) |
8 | | srapart.s |
. . . . . 6
β’ (π β π β (Baseβπ)) |
9 | | sraval 20934 |
. . . . . 6
β’ ((π β V β§ π β (Baseβπ)) β ((subringAlg
βπ)βπ) = (((π sSet β¨(Scalarβndx), (π βΎs π)β©) sSet β¨(
Β·π βndx), (.rβπ)β©) sSet
β¨(Β·πβndx),
(.rβπ)β©)) |
10 | 8, 9 | sylan2 591 |
. . . . 5
β’ ((π β V β§ π) β ((subringAlg βπ)βπ) = (((π sSet β¨(Scalarβndx), (π βΎs π)β©) sSet β¨(
Β·π βndx), (.rβπ)β©) sSet
β¨(Β·πβndx),
(.rβπ)β©)) |
11 | 7, 10 | eqtrd 2770 |
. . . 4
β’ ((π β V β§ π) β π΄ = (((π sSet β¨(Scalarβndx), (π βΎs π)β©) sSet β¨(
Β·π βndx), (.rβπ)β©) sSet
β¨(Β·πβndx),
(.rβπ)β©)) |
12 | 11 | fveq2d 6894 |
. . 3
β’ ((π β V β§ π) β
(Β·πβπ΄) =
(Β·πβ(((π sSet β¨(Scalarβndx), (π βΎs π)β©) sSet β¨(
Β·π βndx), (.rβπ)β©) sSet
β¨(Β·πβndx),
(.rβπ)β©))) |
13 | 5, 12 | eqtr4id 2789 |
. 2
β’ ((π β V β§ π) β (.rβπ) =
(Β·πβπ΄)) |
14 | 3 | str0 17126 |
. . 3
β’ β
=
(Β·πββ
) |
15 | | fvprc 6882 |
. . . 4
β’ (Β¬
π β V β
(.rβπ) =
β
) |
16 | 15 | adantr 479 |
. . 3
β’ ((Β¬
π β V β§ π) β
(.rβπ) =
β
) |
17 | | fv2prc 6935 |
. . . . 5
β’ (Β¬
π β V β
((subringAlg βπ)βπ) = β
) |
18 | 6, 17 | sylan9eqr 2792 |
. . . 4
β’ ((Β¬
π β V β§ π) β π΄ = β
) |
19 | 18 | fveq2d 6894 |
. . 3
β’ ((Β¬
π β V β§ π) β
(Β·πβπ΄) =
(Β·πββ
)) |
20 | 14, 16, 19 | 3eqtr4a 2796 |
. 2
β’ ((Β¬
π β V β§ π) β
(.rβπ) =
(Β·πβπ΄)) |
21 | 13, 20 | pm2.61ian 808 |
1
β’ (π β (.rβπ) =
(Β·πβπ΄)) |