Step | Hyp | Ref
| Expression |
1 | | sralem.1 |
. . . . 5
β’ πΈ = Slot (πΈβndx) |
2 | | sralem.2 |
. . . . . 6
β’
(Scalarβndx) β (πΈβndx) |
3 | 2 | necomi 2999 |
. . . . 5
β’ (πΈβndx) β
(Scalarβndx) |
4 | 1, 3 | setsnid 17088 |
. . . 4
β’ (πΈβπ) = (πΈβ(π sSet β¨(Scalarβndx), (π βΎs π)β©)) |
5 | | sralem.3 |
. . . . . 6
β’ (
Β·π βndx) β (πΈβndx) |
6 | 5 | necomi 2999 |
. . . . 5
β’ (πΈβndx) β (
Β·π βndx) |
7 | 1, 6 | setsnid 17088 |
. . . 4
β’ (πΈβ(π sSet β¨(Scalarβndx), (π βΎs π)β©)) = (πΈβ((π sSet β¨(Scalarβndx), (π βΎs π)β©) sSet β¨(
Β·π βndx), (.rβπ)β©)) |
8 | | sralem.4 |
. . . . . 6
β’
(Β·πβndx) β (πΈβndx) |
9 | 8 | necomi 2999 |
. . . . 5
β’ (πΈβndx) β
(Β·πβndx) |
10 | 1, 9 | setsnid 17088 |
. . . 4
β’ (πΈβ((π sSet β¨(Scalarβndx), (π βΎs π)β©) sSet β¨(
Β·π βndx), (.rβπ)β©)) = (πΈβ(((π sSet β¨(Scalarβndx), (π βΎs π)β©) sSet β¨(
Β·π βndx), (.rβπ)β©) sSet
β¨(Β·πβndx),
(.rβπ)β©)) |
11 | 4, 7, 10 | 3eqtri 2769 |
. . 3
β’ (πΈβπ) = (πΈβ(((π sSet β¨(Scalarβndx), (π βΎs π)β©) sSet β¨(
Β·π βndx), (.rβπ)β©) sSet
β¨(Β·πβndx),
(.rβπ)β©)) |
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 β§ π) β (πΈβπ΄) = (πΈβ(((π sSet β¨(Scalarβndx), (π βΎs π)β©) sSet β¨(
Β·π βndx), (.rβπ)β©) sSet
β¨(Β·πβndx),
(.rβπ)β©))) |
19 | 11, 18 | eqtr4id 2796 |
. 2
β’ ((π β V β§ π) β (πΈβπ) = (πΈβπ΄)) |
20 | 1 | str0 17068 |
. . 3
β’ β
=
(πΈββ
) |
21 | | fvprc 6839 |
. . . 4
β’ (Β¬
π β V β (πΈβπ) = β
) |
22 | 21 | adantr 482 |
. . 3
β’ ((Β¬
π β V β§ π) β (πΈβπ) = β
) |
23 | | fv2prc 6892 |
. . . . 5
β’ (Β¬
π β V β
((subringAlg βπ)βπ) = β
) |
24 | 12, 23 | sylan9eqr 2799 |
. . . 4
β’ ((Β¬
π β V β§ π) β π΄ = β
) |
25 | 24 | fveq2d 6851 |
. . 3
β’ ((Β¬
π β V β§ π) β (πΈβπ΄) = (πΈββ
)) |
26 | 20, 22, 25 | 3eqtr4a 2803 |
. 2
β’ ((Β¬
π β V β§ π) β (πΈβπ) = (πΈβπ΄)) |
27 | 19, 26 | pm2.61ian 811 |
1
β’ (π β (πΈβπ) = (πΈβπ΄)) |