Step | Hyp | Ref
| Expression |
1 | | eqid 2733 |
. . . 4
β’
(1st βπ
) = (1st βπ
) |
2 | | unmnd.1 |
. . . 4
β’ π» = (2nd βπ
) |
3 | | eqid 2733 |
. . . 4
β’ ran
(1st βπ
) =
ran (1st βπ
) |
4 | 1, 2, 3 | rngosm 36409 |
. . 3
β’ (π
β RingOps β π»:(ran (1st
βπ
) Γ ran
(1st βπ
))βΆran (1st βπ
)) |
5 | 1, 2, 3 | rngoass 36415 |
. . . 4
β’ ((π
β RingOps β§ (π₯ β ran (1st
βπ
) β§ π¦ β ran (1st
βπ
) β§ π§ β ran (1st
βπ
))) β ((π₯π»π¦)π»π§) = (π₯π»(π¦π»π§))) |
6 | 5 | ralrimivvva 3197 |
. . 3
β’ (π
β RingOps β
βπ₯ β ran
(1st βπ
)βπ¦ β ran (1st βπ
)βπ§ β ran (1st βπ
)((π₯π»π¦)π»π§) = (π₯π»(π¦π»π§))) |
7 | 1, 2, 3 | rngoi 36408 |
. . . 4
β’ (π
β RingOps β
(((1st βπ
)
β AbelOp β§ π»:(ran
(1st βπ
)
Γ ran (1st βπ
))βΆran (1st βπ
)) β§ (βπ₯ β ran (1st
βπ
)βπ¦ β ran (1st
βπ
)βπ§ β ran (1st
βπ
)(((π₯π»π¦)π»π§) = (π₯π»(π¦π»π§)) β§ (π₯π»(π¦(1st βπ
)π§)) = ((π₯π»π¦)(1st βπ
)(π₯π»π§)) β§ ((π₯(1st βπ
)π¦)π»π§) = ((π₯π»π§)(1st βπ
)(π¦π»π§))) β§ βπ₯ β ran (1st βπ
)βπ¦ β ran (1st βπ
)((π₯π»π¦) = π¦ β§ (π¦π»π₯) = π¦)))) |
8 | 7 | simprrd 773 |
. . 3
β’ (π
β RingOps β
βπ₯ β ran
(1st βπ
)βπ¦ β ran (1st βπ
)((π₯π»π¦) = π¦ β§ (π¦π»π₯) = π¦)) |
9 | 2, 1 | rngorn1 36442 |
. . . 4
β’ (π
β RingOps β ran
(1st βπ
) =
dom dom π») |
10 | | xpid11 5891 |
. . . . . . . 8
β’ ((dom dom
π» Γ dom dom π») = (ran (1st
βπ
) Γ ran
(1st βπ
))
β dom dom π» = ran
(1st βπ
)) |
11 | 10 | biimpri 227 |
. . . . . . 7
β’ (dom dom
π» = ran (1st
βπ
) β (dom dom
π» Γ dom dom π») = (ran (1st
βπ
) Γ ran
(1st βπ
))) |
12 | | feq23 6656 |
. . . . . . 7
β’ (((dom
dom π» Γ dom dom π») = (ran (1st
βπ
) Γ ran
(1st βπ
))
β§ dom dom π» = ran
(1st βπ
))
β (π»:(dom dom π» Γ dom dom π»)βΆdom dom π» β π»:(ran (1st βπ
) Γ ran (1st
βπ
))βΆran
(1st βπ
))) |
13 | 11, 12 | mpancom 687 |
. . . . . 6
β’ (dom dom
π» = ran (1st
βπ
) β (π»:(dom dom π» Γ dom dom π»)βΆdom dom π» β π»:(ran (1st βπ
) Γ ran (1st
βπ
))βΆran
(1st βπ
))) |
14 | | raleq 3308 |
. . . . . . . 8
β’ (dom dom
π» = ran (1st
βπ
) β
(βπ§ β dom dom
π»((π₯π»π¦)π»π§) = (π₯π»(π¦π»π§)) β βπ§ β ran (1st βπ
)((π₯π»π¦)π»π§) = (π₯π»(π¦π»π§)))) |
15 | 14 | raleqbi1dv 3306 |
. . . . . . 7
β’ (dom dom
π» = ran (1st
βπ
) β
(βπ¦ β dom dom
π»βπ§ β dom dom π»((π₯π»π¦)π»π§) = (π₯π»(π¦π»π§)) β βπ¦ β ran (1st βπ
)βπ§ β ran (1st βπ
)((π₯π»π¦)π»π§) = (π₯π»(π¦π»π§)))) |
16 | 15 | raleqbi1dv 3306 |
. . . . . 6
β’ (dom dom
π» = ran (1st
βπ
) β
(βπ₯ β dom dom
π»βπ¦ β dom dom π»βπ§ β dom dom π»((π₯π»π¦)π»π§) = (π₯π»(π¦π»π§)) β βπ₯ β ran (1st βπ
)βπ¦ β ran (1st βπ
)βπ§ β ran (1st βπ
)((π₯π»π¦)π»π§) = (π₯π»(π¦π»π§)))) |
17 | | raleq 3308 |
. . . . . . 7
β’ (dom dom
π» = ran (1st
βπ
) β
(βπ¦ β dom dom
π»((π₯π»π¦) = π¦ β§ (π¦π»π₯) = π¦) β βπ¦ β ran (1st βπ
)((π₯π»π¦) = π¦ β§ (π¦π»π₯) = π¦))) |
18 | 17 | rexeqbi1dv 3307 |
. . . . . 6
β’ (dom dom
π» = ran (1st
βπ
) β
(βπ₯ β dom dom
π»βπ¦ β dom dom π»((π₯π»π¦) = π¦ β§ (π¦π»π₯) = π¦) β βπ₯ β ran (1st βπ
)βπ¦ β ran (1st βπ
)((π₯π»π¦) = π¦ β§ (π¦π»π₯) = π¦))) |
19 | 13, 16, 18 | 3anbi123d 1437 |
. . . . 5
β’ (dom dom
π» = ran (1st
βπ
) β ((π»:(dom dom π» Γ dom dom π»)βΆdom dom π» β§ βπ₯ β dom dom π»βπ¦ β dom dom π»βπ§ β dom dom π»((π₯π»π¦)π»π§) = (π₯π»(π¦π»π§)) β§ βπ₯ β dom dom π»βπ¦ β dom dom π»((π₯π»π¦) = π¦ β§ (π¦π»π₯) = π¦)) β (π»:(ran (1st βπ
) Γ ran (1st
βπ
))βΆran
(1st βπ
)
β§ βπ₯ β ran
(1st βπ
)βπ¦ β ran (1st βπ
)βπ§ β ran (1st βπ
)((π₯π»π¦)π»π§) = (π₯π»(π¦π»π§)) β§ βπ₯ β ran (1st βπ
)βπ¦ β ran (1st βπ
)((π₯π»π¦) = π¦ β§ (π¦π»π₯) = π¦)))) |
20 | 19 | eqcoms 2741 |
. . . 4
β’ (ran
(1st βπ
) =
dom dom π» β ((π»:(dom dom π» Γ dom dom π»)βΆdom dom π» β§ βπ₯ β dom dom π»βπ¦ β dom dom π»βπ§ β dom dom π»((π₯π»π¦)π»π§) = (π₯π»(π¦π»π§)) β§ βπ₯ β dom dom π»βπ¦ β dom dom π»((π₯π»π¦) = π¦ β§ (π¦π»π₯) = π¦)) β (π»:(ran (1st βπ
) Γ ran (1st
βπ
))βΆran
(1st βπ
)
β§ βπ₯ β ran
(1st βπ
)βπ¦ β ran (1st βπ
)βπ§ β ran (1st βπ
)((π₯π»π¦)π»π§) = (π₯π»(π¦π»π§)) β§ βπ₯ β ran (1st βπ
)βπ¦ β ran (1st βπ
)((π₯π»π¦) = π¦ β§ (π¦π»π₯) = π¦)))) |
21 | 9, 20 | syl 17 |
. . 3
β’ (π
β RingOps β ((π»:(dom dom π» Γ dom dom π»)βΆdom dom π» β§ βπ₯ β dom dom π»βπ¦ β dom dom π»βπ§ β dom dom π»((π₯π»π¦)π»π§) = (π₯π»(π¦π»π§)) β§ βπ₯ β dom dom π»βπ¦ β dom dom π»((π₯π»π¦) = π¦ β§ (π¦π»π₯) = π¦)) β (π»:(ran (1st βπ
) Γ ran (1st
βπ
))βΆran
(1st βπ
)
β§ βπ₯ β ran
(1st βπ
)βπ¦ β ran (1st βπ
)βπ§ β ran (1st βπ
)((π₯π»π¦)π»π§) = (π₯π»(π¦π»π§)) β§ βπ₯ β ran (1st βπ
)βπ¦ β ran (1st βπ
)((π₯π»π¦) = π¦ β§ (π¦π»π₯) = π¦)))) |
22 | 4, 6, 8, 21 | mpbir3and 1343 |
. 2
β’ (π
β RingOps β (π»:(dom dom π» Γ dom dom π»)βΆdom dom π» β§ βπ₯ β dom dom π»βπ¦ β dom dom π»βπ§ β dom dom π»((π₯π»π¦)π»π§) = (π₯π»(π¦π»π§)) β§ βπ₯ β dom dom π»βπ¦ β dom dom π»((π₯π»π¦) = π¦ β§ (π¦π»π₯) = π¦))) |
23 | | fvex 6859 |
. . . 4
β’
(2nd βπ
) β V |
24 | | eleq1 2822 |
. . . 4
β’ (π» = (2nd βπ
) β (π» β V β (2nd
βπ
) β
V)) |
25 | 23, 24 | mpbiri 258 |
. . 3
β’ (π» = (2nd βπ
) β π» β V) |
26 | | eqid 2733 |
. . . 4
β’ dom dom
π» = dom dom π» |
27 | 26 | ismndo1 36382 |
. . 3
β’ (π» β V β (π» β MndOp β (π»:(dom dom π» Γ dom dom π»)βΆdom dom π» β§ βπ₯ β dom dom π»βπ¦ β dom dom π»βπ§ β dom dom π»((π₯π»π¦)π»π§) = (π₯π»(π¦π»π§)) β§ βπ₯ β dom dom π»βπ¦ β dom dom π»((π₯π»π¦) = π¦ β§ (π¦π»π₯) = π¦)))) |
28 | 2, 25, 27 | mp2b 10 |
. 2
β’ (π» β MndOp β (π»:(dom dom π» Γ dom dom π»)βΆdom dom π» β§ βπ₯ β dom dom π»βπ¦ β dom dom π»βπ§ β dom dom π»((π₯π»π¦)π»π§) = (π₯π»(π¦π»π§)) β§ βπ₯ β dom dom π»βπ¦ β dom dom π»((π₯π»π¦) = π¦ β§ (π¦π»π₯) = π¦))) |
29 | 22, 28 | sylibr 233 |
1
β’ (π
β RingOps β π» β MndOp) |