Step | Hyp | Ref
| Expression |
1 | | erngset.d |
. . 3
β’ π· = ((EDRingβπΎ)βπ) |
2 | | erngset.h |
. . . . 5
β’ π» = (LHypβπΎ) |
3 | 2 | erngfset 39200 |
. . . 4
β’ (πΎ β π β (EDRingβπΎ) = (π€ β π» β¦ {β¨(Baseβndx),
((TEndoβπΎ)βπ€)β©, β¨(+gβndx),
(π β
((TEndoβπΎ)βπ€), π‘ β ((TEndoβπΎ)βπ€) β¦ (π β ((LTrnβπΎ)βπ€) β¦ ((π βπ) β (π‘βπ))))β©, β¨(.rβndx),
(π β
((TEndoβπΎ)βπ€), π‘ β ((TEndoβπΎ)βπ€) β¦ (π β π‘))β©})) |
4 | 3 | fveq1d 6841 |
. . 3
β’ (πΎ β π β ((EDRingβπΎ)βπ) = ((π€ β π» β¦ {β¨(Baseβndx),
((TEndoβπΎ)βπ€)β©, β¨(+gβndx),
(π β
((TEndoβπΎ)βπ€), π‘ β ((TEndoβπΎ)βπ€) β¦ (π β ((LTrnβπΎ)βπ€) β¦ ((π βπ) β (π‘βπ))))β©, β¨(.rβndx),
(π β
((TEndoβπΎ)βπ€), π‘ β ((TEndoβπΎ)βπ€) β¦ (π β π‘))β©})βπ)) |
5 | 1, 4 | eqtrid 2789 |
. 2
β’ (πΎ β π β π· = ((π€ β π» β¦ {β¨(Baseβndx),
((TEndoβπΎ)βπ€)β©, β¨(+gβndx),
(π β
((TEndoβπΎ)βπ€), π‘ β ((TEndoβπΎ)βπ€) β¦ (π β ((LTrnβπΎ)βπ€) β¦ ((π βπ) β (π‘βπ))))β©, β¨(.rβndx),
(π β
((TEndoβπΎ)βπ€), π‘ β ((TEndoβπΎ)βπ€) β¦ (π β π‘))β©})βπ)) |
6 | | fveq2 6839 |
. . . . . 6
β’ (π€ = π β ((TEndoβπΎ)βπ€) = ((TEndoβπΎ)βπ)) |
7 | 6 | opeq2d 4835 |
. . . . 5
β’ (π€ = π β β¨(Baseβndx),
((TEndoβπΎ)βπ€)β© = β¨(Baseβndx),
((TEndoβπΎ)βπ)β©) |
8 | | tpeq1 4701 |
. . . . . 6
β’
(β¨(Baseβndx), ((TEndoβπΎ)βπ€)β© = β¨(Baseβndx),
((TEndoβπΎ)βπ)β© β {β¨(Baseβndx),
((TEndoβπΎ)βπ€)β©, β¨(+gβndx),
(π β
((TEndoβπΎ)βπ€), π‘ β ((TEndoβπΎ)βπ€) β¦ (π β ((LTrnβπΎ)βπ€) β¦ ((π βπ) β (π‘βπ))))β©, β¨(.rβndx),
(π β
((TEndoβπΎ)βπ€), π‘ β ((TEndoβπΎ)βπ€) β¦ (π β π‘))β©} = {β¨(Baseβndx),
((TEndoβπΎ)βπ)β©, β¨(+gβndx),
(π β
((TEndoβπΎ)βπ€), π‘ β ((TEndoβπΎ)βπ€) β¦ (π β ((LTrnβπΎ)βπ€) β¦ ((π βπ) β (π‘βπ))))β©, β¨(.rβndx),
(π β
((TEndoβπΎ)βπ€), π‘ β ((TEndoβπΎ)βπ€) β¦ (π β π‘))β©}) |
9 | | erngset.e |
. . . . . . . 8
β’ πΈ = ((TEndoβπΎ)βπ) |
10 | 9 | opeq2i 4832 |
. . . . . . 7
β’
β¨(Baseβndx), πΈβ© = β¨(Baseβndx),
((TEndoβπΎ)βπ)β© |
11 | | tpeq1 4701 |
. . . . . . 7
β’
(β¨(Baseβndx), πΈβ© = β¨(Baseβndx),
((TEndoβπΎ)βπ)β© β {β¨(Baseβndx),
πΈβ©,
β¨(+gβndx), (π β ((TEndoβπΎ)βπ€), π‘ β ((TEndoβπΎ)βπ€) β¦ (π β ((LTrnβπΎ)βπ€) β¦ ((π βπ) β (π‘βπ))))β©, β¨(.rβndx),
(π β
((TEndoβπΎ)βπ€), π‘ β ((TEndoβπΎ)βπ€) β¦ (π β π‘))β©} = {β¨(Baseβndx),
((TEndoβπΎ)βπ)β©, β¨(+gβndx),
(π β
((TEndoβπΎ)βπ€), π‘ β ((TEndoβπΎ)βπ€) β¦ (π β ((LTrnβπΎ)βπ€) β¦ ((π βπ) β (π‘βπ))))β©, β¨(.rβndx),
(π β
((TEndoβπΎ)βπ€), π‘ β ((TEndoβπΎ)βπ€) β¦ (π β π‘))β©}) |
12 | 10, 11 | ax-mp 5 |
. . . . . 6
β’
{β¨(Baseβndx), πΈβ©, β¨(+gβndx),
(π β
((TEndoβπΎ)βπ€), π‘ β ((TEndoβπΎ)βπ€) β¦ (π β ((LTrnβπΎ)βπ€) β¦ ((π βπ) β (π‘βπ))))β©, β¨(.rβndx),
(π β
((TEndoβπΎ)βπ€), π‘ β ((TEndoβπΎ)βπ€) β¦ (π β π‘))β©} = {β¨(Baseβndx),
((TEndoβπΎ)βπ)β©, β¨(+gβndx),
(π β
((TEndoβπΎ)βπ€), π‘ β ((TEndoβπΎ)βπ€) β¦ (π β ((LTrnβπΎ)βπ€) β¦ ((π βπ) β (π‘βπ))))β©, β¨(.rβndx),
(π β
((TEndoβπΎ)βπ€), π‘ β ((TEndoβπΎ)βπ€) β¦ (π β π‘))β©} |
13 | 8, 12 | eqtr4di 2795 |
. . . . 5
β’
(β¨(Baseβndx), ((TEndoβπΎ)βπ€)β© = β¨(Baseβndx),
((TEndoβπΎ)βπ)β© β {β¨(Baseβndx),
((TEndoβπΎ)βπ€)β©, β¨(+gβndx),
(π β
((TEndoβπΎ)βπ€), π‘ β ((TEndoβπΎ)βπ€) β¦ (π β ((LTrnβπΎ)βπ€) β¦ ((π βπ) β (π‘βπ))))β©, β¨(.rβndx),
(π β
((TEndoβπΎ)βπ€), π‘ β ((TEndoβπΎ)βπ€) β¦ (π β π‘))β©} = {β¨(Baseβndx), πΈβ©,
β¨(+gβndx), (π β ((TEndoβπΎ)βπ€), π‘ β ((TEndoβπΎ)βπ€) β¦ (π β ((LTrnβπΎ)βπ€) β¦ ((π βπ) β (π‘βπ))))β©, β¨(.rβndx),
(π β
((TEndoβπΎ)βπ€), π‘ β ((TEndoβπΎ)βπ€) β¦ (π β π‘))β©}) |
14 | 7, 13 | syl 17 |
. . . 4
β’ (π€ = π β {β¨(Baseβndx),
((TEndoβπΎ)βπ€)β©, β¨(+gβndx),
(π β
((TEndoβπΎ)βπ€), π‘ β ((TEndoβπΎ)βπ€) β¦ (π β ((LTrnβπΎ)βπ€) β¦ ((π βπ) β (π‘βπ))))β©, β¨(.rβndx),
(π β
((TEndoβπΎ)βπ€), π‘ β ((TEndoβπΎ)βπ€) β¦ (π β π‘))β©} = {β¨(Baseβndx), πΈβ©,
β¨(+gβndx), (π β ((TEndoβπΎ)βπ€), π‘ β ((TEndoβπΎ)βπ€) β¦ (π β ((LTrnβπΎ)βπ€) β¦ ((π βπ) β (π‘βπ))))β©, β¨(.rβndx),
(π β
((TEndoβπΎ)βπ€), π‘ β ((TEndoβπΎ)βπ€) β¦ (π β π‘))β©}) |
15 | 6, 9 | eqtr4di 2795 |
. . . . . . 7
β’ (π€ = π β ((TEndoβπΎ)βπ€) = πΈ) |
16 | | fveq2 6839 |
. . . . . . . . 9
β’ (π€ = π β ((LTrnβπΎ)βπ€) = ((LTrnβπΎ)βπ)) |
17 | | erngset.t |
. . . . . . . . 9
β’ π = ((LTrnβπΎ)βπ) |
18 | 16, 17 | eqtr4di 2795 |
. . . . . . . 8
β’ (π€ = π β ((LTrnβπΎ)βπ€) = π) |
19 | | eqidd 2738 |
. . . . . . . 8
β’ (π€ = π β ((π βπ) β (π‘βπ)) = ((π βπ) β (π‘βπ))) |
20 | 18, 19 | mpteq12dv 5194 |
. . . . . . 7
β’ (π€ = π β (π β ((LTrnβπΎ)βπ€) β¦ ((π βπ) β (π‘βπ))) = (π β π β¦ ((π βπ) β (π‘βπ)))) |
21 | 15, 15, 20 | mpoeq123dv 7426 |
. . . . . 6
β’ (π€ = π β (π β ((TEndoβπΎ)βπ€), π‘ β ((TEndoβπΎ)βπ€) β¦ (π β ((LTrnβπΎ)βπ€) β¦ ((π βπ) β (π‘βπ)))) = (π β πΈ, π‘ β πΈ β¦ (π β π β¦ ((π βπ) β (π‘βπ))))) |
22 | 21 | opeq2d 4835 |
. . . . 5
β’ (π€ = π β β¨(+gβndx),
(π β
((TEndoβπΎ)βπ€), π‘ β ((TEndoβπΎ)βπ€) β¦ (π β ((LTrnβπΎ)βπ€) β¦ ((π βπ) β (π‘βπ))))β© = β¨(+gβndx),
(π β πΈ, π‘ β πΈ β¦ (π β π β¦ ((π βπ) β (π‘βπ))))β©) |
23 | 22 | tpeq2d 4705 |
. . . 4
β’ (π€ = π β {β¨(Baseβndx), πΈβ©,
β¨(+gβndx), (π β ((TEndoβπΎ)βπ€), π‘ β ((TEndoβπΎ)βπ€) β¦ (π β ((LTrnβπΎ)βπ€) β¦ ((π βπ) β (π‘βπ))))β©, β¨(.rβndx),
(π β
((TEndoβπΎ)βπ€), π‘ β ((TEndoβπΎ)βπ€) β¦ (π β π‘))β©} = {β¨(Baseβndx), πΈβ©,
β¨(+gβndx), (π β πΈ, π‘ β πΈ β¦ (π β π β¦ ((π βπ) β (π‘βπ))))β©, β¨(.rβndx),
(π β
((TEndoβπΎ)βπ€), π‘ β ((TEndoβπΎ)βπ€) β¦ (π β π‘))β©}) |
24 | | eqidd 2738 |
. . . . . . 7
β’ (π€ = π β (π β π‘) = (π β π‘)) |
25 | 15, 15, 24 | mpoeq123dv 7426 |
. . . . . 6
β’ (π€ = π β (π β ((TEndoβπΎ)βπ€), π‘ β ((TEndoβπΎ)βπ€) β¦ (π β π‘)) = (π β πΈ, π‘ β πΈ β¦ (π β π‘))) |
26 | 25 | opeq2d 4835 |
. . . . 5
β’ (π€ = π β β¨(.rβndx),
(π β
((TEndoβπΎ)βπ€), π‘ β ((TEndoβπΎ)βπ€) β¦ (π β π‘))β© = β¨(.rβndx),
(π β πΈ, π‘ β πΈ β¦ (π β π‘))β©) |
27 | 26 | tpeq3d 4706 |
. . . 4
β’ (π€ = π β {β¨(Baseβndx), πΈβ©,
β¨(+gβndx), (π β πΈ, π‘ β πΈ β¦ (π β π β¦ ((π βπ) β (π‘βπ))))β©, β¨(.rβndx),
(π β
((TEndoβπΎ)βπ€), π‘ β ((TEndoβπΎ)βπ€) β¦ (π β π‘))β©} = {β¨(Baseβndx), πΈβ©,
β¨(+gβndx), (π β πΈ, π‘ β πΈ β¦ (π β π β¦ ((π βπ) β (π‘βπ))))β©, β¨(.rβndx),
(π β πΈ, π‘ β πΈ β¦ (π β π‘))β©}) |
28 | 14, 23, 27 | 3eqtrd 2781 |
. . 3
β’ (π€ = π β {β¨(Baseβndx),
((TEndoβπΎ)βπ€)β©, β¨(+gβndx),
(π β
((TEndoβπΎ)βπ€), π‘ β ((TEndoβπΎ)βπ€) β¦ (π β ((LTrnβπΎ)βπ€) β¦ ((π βπ) β (π‘βπ))))β©, β¨(.rβndx),
(π β
((TEndoβπΎ)βπ€), π‘ β ((TEndoβπΎ)βπ€) β¦ (π β π‘))β©} = {β¨(Baseβndx), πΈβ©,
β¨(+gβndx), (π β πΈ, π‘ β πΈ β¦ (π β π β¦ ((π βπ) β (π‘βπ))))β©, β¨(.rβndx),
(π β πΈ, π‘ β πΈ β¦ (π β π‘))β©}) |
29 | | eqid 2737 |
. . 3
β’ (π€ β π» β¦ {β¨(Baseβndx),
((TEndoβπΎ)βπ€)β©, β¨(+gβndx),
(π β
((TEndoβπΎ)βπ€), π‘ β ((TEndoβπΎ)βπ€) β¦ (π β ((LTrnβπΎ)βπ€) β¦ ((π βπ) β (π‘βπ))))β©, β¨(.rβndx),
(π β
((TEndoβπΎ)βπ€), π‘ β ((TEndoβπΎ)βπ€) β¦ (π β π‘))β©}) = (π€ β π» β¦ {β¨(Baseβndx),
((TEndoβπΎ)βπ€)β©, β¨(+gβndx),
(π β
((TEndoβπΎ)βπ€), π‘ β ((TEndoβπΎ)βπ€) β¦ (π β ((LTrnβπΎ)βπ€) β¦ ((π βπ) β (π‘βπ))))β©, β¨(.rβndx),
(π β
((TEndoβπΎ)βπ€), π‘ β ((TEndoβπΎ)βπ€) β¦ (π β π‘))β©}) |
30 | | tpex 7673 |
. . 3
β’
{β¨(Baseβndx), πΈβ©, β¨(+gβndx),
(π β πΈ, π‘ β πΈ β¦ (π β π β¦ ((π βπ) β (π‘βπ))))β©, β¨(.rβndx),
(π β πΈ, π‘ β πΈ β¦ (π β π‘))β©} β V |
31 | 28, 29, 30 | fvmpt 6945 |
. 2
β’ (π β π» β ((π€ β π» β¦ {β¨(Baseβndx),
((TEndoβπΎ)βπ€)β©, β¨(+gβndx),
(π β
((TEndoβπΎ)βπ€), π‘ β ((TEndoβπΎ)βπ€) β¦ (π β ((LTrnβπΎ)βπ€) β¦ ((π βπ) β (π‘βπ))))β©, β¨(.rβndx),
(π β
((TEndoβπΎ)βπ€), π‘ β ((TEndoβπΎ)βπ€) β¦ (π β π‘))β©})βπ) = {β¨(Baseβndx), πΈβ©,
β¨(+gβndx), (π β πΈ, π‘ β πΈ β¦ (π β π β¦ ((π βπ) β (π‘βπ))))β©, β¨(.rβndx),
(π β πΈ, π‘ β πΈ β¦ (π β π‘))β©}) |
32 | 5, 31 | sylan9eq 2797 |
1
β’ ((πΎ β π β§ π β π») β π· = {β¨(Baseβndx), πΈβ©,
β¨(+gβndx), (π β πΈ, π‘ β πΈ β¦ (π β π β¦ ((π βπ) β (π‘βπ))))β©, β¨(.rβndx),
(π β πΈ, π‘ β πΈ β¦ (π β π‘))β©}) |