Step | Hyp | Ref
| Expression |
1 | | elex 3461 |
. 2
β’ (πΎ β π β πΎ β V) |
2 | | fveq2 6839 |
. . . . 5
β’ (π = πΎ β (LHypβπ) = (LHypβπΎ)) |
3 | | erngset.h-r |
. . . . 5
β’ π» = (LHypβπΎ) |
4 | 2, 3 | eqtr4di 2795 |
. . . 4
β’ (π = πΎ β (LHypβπ) = π») |
5 | | fveq2 6839 |
. . . . . . 7
β’ (π = πΎ β (TEndoβπ) = (TEndoβπΎ)) |
6 | 5 | fveq1d 6841 |
. . . . . 6
β’ (π = πΎ β ((TEndoβπ)βπ€) = ((TEndoβπΎ)βπ€)) |
7 | 6 | opeq2d 4835 |
. . . . 5
β’ (π = πΎ β β¨(Baseβndx),
((TEndoβπ)βπ€)β© = β¨(Baseβndx),
((TEndoβπΎ)βπ€)β©) |
8 | | fveq2 6839 |
. . . . . . . . 9
β’ (π = πΎ β (LTrnβπ) = (LTrnβπΎ)) |
9 | 8 | fveq1d 6841 |
. . . . . . . 8
β’ (π = πΎ β ((LTrnβπ)βπ€) = ((LTrnβπΎ)βπ€)) |
10 | 9 | mpteq1d 5198 |
. . . . . . 7
β’ (π = πΎ β (π β ((LTrnβπ)βπ€) β¦ ((π βπ) β (π‘βπ))) = (π β ((LTrnβπΎ)βπ€) β¦ ((π βπ) β (π‘βπ)))) |
11 | 6, 6, 10 | mpoeq123dv 7426 |
. . . . . 6
β’ (π = πΎ β (π β ((TEndoβπ)βπ€), π‘ β ((TEndoβπ)βπ€) β¦ (π β ((LTrnβπ)βπ€) β¦ ((π βπ) β (π‘βπ)))) = (π β ((TEndoβπΎ)βπ€), π‘ β ((TEndoβπΎ)βπ€) β¦ (π β ((LTrnβπΎ)βπ€) β¦ ((π βπ) β (π‘βπ))))) |
12 | 11 | opeq2d 4835 |
. . . . 5
β’ (π = πΎ β β¨(+gβndx),
(π β
((TEndoβπ)βπ€), π‘ β ((TEndoβπ)βπ€) β¦ (π β ((LTrnβπ)βπ€) β¦ ((π βπ) β (π‘βπ))))β© = β¨(+gβndx),
(π β
((TEndoβπΎ)βπ€), π‘ β ((TEndoβπΎ)βπ€) β¦ (π β ((LTrnβπΎ)βπ€) β¦ ((π βπ) β (π‘βπ))))β©) |
13 | | eqidd 2738 |
. . . . . . 7
β’ (π = πΎ β (π‘ β π ) = (π‘ β π )) |
14 | 6, 6, 13 | mpoeq123dv 7426 |
. . . . . 6
β’ (π = πΎ β (π β ((TEndoβπ)βπ€), π‘ β ((TEndoβπ)βπ€) β¦ (π‘ β π )) = (π β ((TEndoβπΎ)βπ€), π‘ β ((TEndoβπΎ)βπ€) β¦ (π‘ β π ))) |
15 | 14 | opeq2d 4835 |
. . . . 5
β’ (π = πΎ β β¨(.rβndx),
(π β
((TEndoβπ)βπ€), π‘ β ((TEndoβπ)βπ€) β¦ (π‘ β π ))β© = β¨(.rβndx),
(π β
((TEndoβπΎ)βπ€), π‘ β ((TEndoβπΎ)βπ€) β¦ (π‘ β π ))β©) |
16 | 7, 12, 15 | tpeq123d 4707 |
. . . 4
β’ (π = πΎ β {β¨(Baseβndx),
((TEndoβπ)βπ€)β©, β¨(+gβndx),
(π β
((TEndoβπ)βπ€), π‘ β ((TEndoβπ)βπ€) β¦ (π β ((LTrnβπ)βπ€) β¦ ((π βπ) β (π‘βπ))))β©, β¨(.rβndx),
(π β
((TEndoβπ)βπ€), π‘ β ((TEndoβπ)βπ€) β¦ (π‘ β π ))β©} = {β¨(Baseβndx),
((TEndoβπΎ)βπ€)β©, β¨(+gβndx),
(π β
((TEndoβπΎ)βπ€), π‘ β ((TEndoβπΎ)βπ€) β¦ (π β ((LTrnβπΎ)βπ€) β¦ ((π βπ) β (π‘βπ))))β©, β¨(.rβndx),
(π β
((TEndoβπΎ)βπ€), π‘ β ((TEndoβπΎ)βπ€) β¦ (π‘ β π ))β©}) |
17 | 4, 16 | mpteq12dv 5194 |
. . 3
β’ (π = πΎ β (π€ β (LHypβπ) β¦ {β¨(Baseβndx),
((TEndoβπ)βπ€)β©, β¨(+gβndx),
(π β
((TEndoβπ)βπ€), π‘ β ((TEndoβπ)βπ€) β¦ (π β ((LTrnβπ)βπ€) β¦ ((π βπ) β (π‘βπ))))β©, β¨(.rβndx),
(π β
((TEndoβπ)βπ€), π‘ β ((TEndoβπ)βπ€) β¦ (π‘ β π ))β©}) = (π€ β π» β¦ {β¨(Baseβndx),
((TEndoβπΎ)βπ€)β©, β¨(+gβndx),
(π β
((TEndoβπΎ)βπ€), π‘ β ((TEndoβπΎ)βπ€) β¦ (π β ((LTrnβπΎ)βπ€) β¦ ((π βπ) β (π‘βπ))))β©, β¨(.rβndx),
(π β
((TEndoβπΎ)βπ€), π‘ β ((TEndoβπΎ)βπ€) β¦ (π‘ β π ))β©})) |
18 | | df-edring-rN 39157 |
. . 3
β’
EDRingR = (π β V β¦ (π€ β (LHypβπ) β¦ {β¨(Baseβndx),
((TEndoβπ)βπ€)β©, β¨(+gβndx),
(π β
((TEndoβπ)βπ€), π‘ β ((TEndoβπ)βπ€) β¦ (π β ((LTrnβπ)βπ€) β¦ ((π βπ) β (π‘βπ))))β©, β¨(.rβndx),
(π β
((TEndoβπ)βπ€), π‘ β ((TEndoβπ)βπ€) β¦ (π‘ β π ))β©})) |
19 | 17, 18, 3 | mptfvmpt 7174 |
. 2
β’ (πΎ β V β
(EDRingRβπΎ) = (π€ β π» β¦ {β¨(Baseβndx),
((TEndoβπΎ)βπ€)β©, β¨(+gβndx),
(π β
((TEndoβπΎ)βπ€), π‘ β ((TEndoβπΎ)βπ€) β¦ (π β ((LTrnβπΎ)βπ€) β¦ ((π βπ) β (π‘βπ))))β©, β¨(.rβndx),
(π β
((TEndoβπΎ)βπ€), π‘ β ((TEndoβπΎ)βπ€) β¦ (π‘ β π ))β©})) |
20 | 1, 19 | syl 17 |
1
β’ (πΎ β π β (EDRingRβπΎ) = (π€ β π» β¦ {β¨(Baseβndx),
((TEndoβπΎ)βπ€)β©, β¨(+gβndx),
(π β
((TEndoβπΎ)βπ€), π‘ β ((TEndoβπΎ)βπ€) β¦ (π β ((LTrnβπΎ)βπ€) β¦ ((π βπ) β (π‘βπ))))β©, β¨(.rβndx),
(π β
((TEndoβπΎ)βπ€), π‘ β ((TEndoβπΎ)βπ€) β¦ (π‘ β π ))β©})) |