Step | Hyp | Ref
| Expression |
1 | | sralemOLD.1 |
. . . . . 6
β’ πΈ = Slot π |
2 | | sralemOLD.2 |
. . . . . 6
β’ π β β |
3 | 1, 2 | ndxid 17130 |
. . . . 5
β’ πΈ = Slot (πΈβndx) |
4 | | sralemOLD.3 |
. . . . . . 7
β’ (π < 5 β¨ 8 < π) |
5 | 2 | nnrei 12221 |
. . . . . . . . . 10
β’ π β β |
6 | | 5re 12299 |
. . . . . . . . . 10
β’ 5 β
β |
7 | 5, 6 | ltnei 11338 |
. . . . . . . . 9
β’ (π < 5 β 5 β π) |
8 | 7 | necomd 2997 |
. . . . . . . 8
β’ (π < 5 β π β 5) |
9 | | 5lt8 12406 |
. . . . . . . . . 10
β’ 5 <
8 |
10 | | 8re 12308 |
. . . . . . . . . . 11
β’ 8 β
β |
11 | 6, 10, 5 | lttri 11340 |
. . . . . . . . . 10
β’ ((5 <
8 β§ 8 < π) β 5
< π) |
12 | 9, 11 | mpan 689 |
. . . . . . . . 9
β’ (8 <
π β 5 < π) |
13 | 6, 5 | ltnei 11338 |
. . . . . . . . 9
β’ (5 <
π β π β 5) |
14 | 12, 13 | syl 17 |
. . . . . . . 8
β’ (8 <
π β π β 5) |
15 | 8, 14 | jaoi 856 |
. . . . . . 7
β’ ((π < 5 β¨ 8 < π) β π β 5) |
16 | 4, 15 | ax-mp 5 |
. . . . . 6
β’ π β 5 |
17 | 1, 2 | ndxarg 17129 |
. . . . . . 7
β’ (πΈβndx) = π |
18 | | scandx 17259 |
. . . . . . 7
β’
(Scalarβndx) = 5 |
19 | 17, 18 | neeq12i 3008 |
. . . . . 6
β’ ((πΈβndx) β
(Scalarβndx) β π
β 5) |
20 | 16, 19 | mpbir 230 |
. . . . 5
β’ (πΈβndx) β
(Scalarβndx) |
21 | 3, 20 | setsnid 17142 |
. . . 4
β’ (πΈβπ) = (πΈβ(π sSet β¨(Scalarβndx), (π βΎs π)β©)) |
22 | | 5lt6 12393 |
. . . . . . . . . . 11
β’ 5 <
6 |
23 | | 6re 12302 |
. . . . . . . . . . . 12
β’ 6 β
β |
24 | 5, 6, 23 | lttri 11340 |
. . . . . . . . . . 11
β’ ((π < 5 β§ 5 < 6) β
π < 6) |
25 | 22, 24 | mpan2 690 |
. . . . . . . . . 10
β’ (π < 5 β π < 6) |
26 | 5, 23 | ltnei 11338 |
. . . . . . . . . 10
β’ (π < 6 β 6 β π) |
27 | 25, 26 | syl 17 |
. . . . . . . . 9
β’ (π < 5 β 6 β π) |
28 | 27 | necomd 2997 |
. . . . . . . 8
β’ (π < 5 β π β 6) |
29 | | 6lt8 12405 |
. . . . . . . . . 10
β’ 6 <
8 |
30 | 23, 10, 5 | lttri 11340 |
. . . . . . . . . 10
β’ ((6 <
8 β§ 8 < π) β 6
< π) |
31 | 29, 30 | mpan 689 |
. . . . . . . . 9
β’ (8 <
π β 6 < π) |
32 | 23, 5 | ltnei 11338 |
. . . . . . . . 9
β’ (6 <
π β π β 6) |
33 | 31, 32 | syl 17 |
. . . . . . . 8
β’ (8 <
π β π β 6) |
34 | 28, 33 | jaoi 856 |
. . . . . . 7
β’ ((π < 5 β¨ 8 < π) β π β 6) |
35 | 4, 34 | ax-mp 5 |
. . . . . 6
β’ π β 6 |
36 | | vscandx 17264 |
. . . . . . 7
β’ (
Β·π βndx) = 6 |
37 | 17, 36 | neeq12i 3008 |
. . . . . 6
β’ ((πΈβndx) β (
Β·π βndx) β π β 6) |
38 | 35, 37 | mpbir 230 |
. . . . 5
β’ (πΈβndx) β (
Β·π βndx) |
39 | 3, 38 | setsnid 17142 |
. . . 4
β’ (πΈβ(π sSet β¨(Scalarβndx), (π βΎs π)β©)) = (πΈβ((π sSet β¨(Scalarβndx), (π βΎs π)β©) sSet β¨(
Β·π βndx), (.rβπ)β©)) |
40 | 5, 6, 10 | lttri 11340 |
. . . . . . . . . . 11
β’ ((π < 5 β§ 5 < 8) β
π < 8) |
41 | 9, 40 | mpan2 690 |
. . . . . . . . . 10
β’ (π < 5 β π < 8) |
42 | 5, 10 | ltnei 11338 |
. . . . . . . . . 10
β’ (π < 8 β 8 β π) |
43 | 41, 42 | syl 17 |
. . . . . . . . 9
β’ (π < 5 β 8 β π) |
44 | 43 | necomd 2997 |
. . . . . . . 8
β’ (π < 5 β π β 8) |
45 | 10, 5 | ltnei 11338 |
. . . . . . . 8
β’ (8 <
π β π β 8) |
46 | 44, 45 | jaoi 856 |
. . . . . . 7
β’ ((π < 5 β¨ 8 < π) β π β 8) |
47 | 4, 46 | ax-mp 5 |
. . . . . 6
β’ π β 8 |
48 | | ipndx 17275 |
. . . . . . 7
β’
(Β·πβndx) = 8 |
49 | 17, 48 | neeq12i 3008 |
. . . . . 6
β’ ((πΈβndx) β
(Β·πβndx) β π β 8) |
50 | 47, 49 | mpbir 230 |
. . . . 5
β’ (πΈβndx) β
(Β·πβndx) |
51 | 3, 50 | setsnid 17142 |
. . . 4
β’ (πΈβ((π sSet β¨(Scalarβndx), (π βΎs π)β©) sSet β¨(
Β·π βndx), (.rβπ)β©)) = (πΈβ(((π sSet β¨(Scalarβndx), (π βΎs π)β©) sSet β¨(
Β·π βndx), (.rβπ)β©) sSet
β¨(Β·πβndx),
(.rβπ)β©)) |
52 | 21, 39, 51 | 3eqtri 2765 |
. . 3
β’ (πΈβπ) = (πΈβ(((π sSet β¨(Scalarβndx), (π βΎs π)β©) sSet β¨(
Β·π βndx), (.rβπ)β©) sSet
β¨(Β·πβndx),
(.rβπ)β©)) |
53 | | srapart.a |
. . . . . 6
β’ (π β π΄ = ((subringAlg βπ)βπ)) |
54 | 53 | adantl 483 |
. . . . 5
β’ ((π β V β§ π) β π΄ = ((subringAlg βπ)βπ)) |
55 | | srapart.s |
. . . . . 6
β’ (π β π β (Baseβπ)) |
56 | | sraval 20789 |
. . . . . 6
β’ ((π β V β§ π β (Baseβπ)) β ((subringAlg
βπ)βπ) = (((π sSet β¨(Scalarβndx), (π βΎs π)β©) sSet β¨(
Β·π βndx), (.rβπ)β©) sSet
β¨(Β·πβndx),
(.rβπ)β©)) |
57 | 55, 56 | sylan2 594 |
. . . . 5
β’ ((π β V β§ π) β ((subringAlg βπ)βπ) = (((π sSet β¨(Scalarβndx), (π βΎs π)β©) sSet β¨(
Β·π βndx), (.rβπ)β©) sSet
β¨(Β·πβndx),
(.rβπ)β©)) |
58 | 54, 57 | eqtrd 2773 |
. . . 4
β’ ((π β V β§ π) β π΄ = (((π sSet β¨(Scalarβndx), (π βΎs π)β©) sSet β¨(
Β·π βndx), (.rβπ)β©) sSet
β¨(Β·πβndx),
(.rβπ)β©)) |
59 | 58 | fveq2d 6896 |
. . 3
β’ ((π β V β§ π) β (πΈβπ΄) = (πΈβ(((π sSet β¨(Scalarβndx), (π βΎs π)β©) sSet β¨(
Β·π βndx), (.rβπ)β©) sSet
β¨(Β·πβndx),
(.rβπ)β©))) |
60 | 52, 59 | eqtr4id 2792 |
. 2
β’ ((π β V β§ π) β (πΈβπ) = (πΈβπ΄)) |
61 | 1 | str0 17122 |
. . 3
β’ β
=
(πΈββ
) |
62 | | fvprc 6884 |
. . . 4
β’ (Β¬
π β V β (πΈβπ) = β
) |
63 | 62 | adantr 482 |
. . 3
β’ ((Β¬
π β V β§ π) β (πΈβπ) = β
) |
64 | | fv2prc 6937 |
. . . . 5
β’ (Β¬
π β V β
((subringAlg βπ)βπ) = β
) |
65 | 53, 64 | sylan9eqr 2795 |
. . . 4
β’ ((Β¬
π β V β§ π) β π΄ = β
) |
66 | 65 | fveq2d 6896 |
. . 3
β’ ((Β¬
π β V β§ π) β (πΈβπ΄) = (πΈββ
)) |
67 | 61, 63, 66 | 3eqtr4a 2799 |
. 2
β’ ((Β¬
π β V β§ π) β (πΈβπ) = (πΈβπ΄)) |
68 | 60, 67 | pm2.61ian 811 |
1
β’ (π β (πΈβπ) = (πΈβπ΄)) |