Step | Hyp | Ref
| Expression |
1 | | subrgdvds.3 |
. . . 4
β’ πΈ =
(β₯rβπ) |
2 | 1 | reldvdsr 20252 |
. . 3
β’ Rel πΈ |
3 | 2 | a1i 11 |
. 2
β’ (π΄ β (SubRingβπ
) β Rel πΈ) |
4 | | subrgdvds.1 |
. . . . . . . 8
β’ π = (π
βΎs π΄) |
5 | 4 | subrgbas 20472 |
. . . . . . 7
β’ (π΄ β (SubRingβπ
) β π΄ = (Baseβπ)) |
6 | | eqid 2731 |
. . . . . . . 8
β’
(Baseβπ
) =
(Baseβπ
) |
7 | 6 | subrgss 20463 |
. . . . . . 7
β’ (π΄ β (SubRingβπ
) β π΄ β (Baseβπ
)) |
8 | 5, 7 | eqsstrrd 4022 |
. . . . . 6
β’ (π΄ β (SubRingβπ
) β (Baseβπ) β (Baseβπ
)) |
9 | 8 | sseld 3982 |
. . . . 5
β’ (π΄ β (SubRingβπ
) β (π₯ β (Baseβπ) β π₯ β (Baseβπ
))) |
10 | | eqid 2731 |
. . . . . . . . . 10
β’
(.rβπ
) = (.rβπ
) |
11 | 4, 10 | ressmulr 17257 |
. . . . . . . . 9
β’ (π΄ β (SubRingβπ
) β
(.rβπ
) =
(.rβπ)) |
12 | 11 | oveqd 7429 |
. . . . . . . 8
β’ (π΄ β (SubRingβπ
) β (π§(.rβπ
)π₯) = (π§(.rβπ)π₯)) |
13 | 12 | eqeq1d 2733 |
. . . . . . 7
β’ (π΄ β (SubRingβπ
) β ((π§(.rβπ
)π₯) = π¦ β (π§(.rβπ)π₯) = π¦)) |
14 | 13 | rexbidv 3177 |
. . . . . 6
β’ (π΄ β (SubRingβπ
) β (βπ§ β (Baseβπ)(π§(.rβπ
)π₯) = π¦ β βπ§ β (Baseβπ)(π§(.rβπ)π₯) = π¦)) |
15 | | ssrexv 4052 |
. . . . . . 7
β’
((Baseβπ)
β (Baseβπ
)
β (βπ§ β
(Baseβπ)(π§(.rβπ
)π₯) = π¦ β βπ§ β (Baseβπ
)(π§(.rβπ
)π₯) = π¦)) |
16 | 8, 15 | syl 17 |
. . . . . 6
β’ (π΄ β (SubRingβπ
) β (βπ§ β (Baseβπ)(π§(.rβπ
)π₯) = π¦ β βπ§ β (Baseβπ
)(π§(.rβπ
)π₯) = π¦)) |
17 | 14, 16 | sylbird 259 |
. . . . 5
β’ (π΄ β (SubRingβπ
) β (βπ§ β (Baseβπ)(π§(.rβπ)π₯) = π¦ β βπ§ β (Baseβπ
)(π§(.rβπ
)π₯) = π¦)) |
18 | 9, 17 | anim12d 608 |
. . . 4
β’ (π΄ β (SubRingβπ
) β ((π₯ β (Baseβπ) β§ βπ§ β (Baseβπ)(π§(.rβπ)π₯) = π¦) β (π₯ β (Baseβπ
) β§ βπ§ β (Baseβπ
)(π§(.rβπ
)π₯) = π¦))) |
19 | | eqid 2731 |
. . . . 5
β’
(Baseβπ) =
(Baseβπ) |
20 | | eqid 2731 |
. . . . 5
β’
(.rβπ) = (.rβπ) |
21 | 19, 1, 20 | dvdsr 20254 |
. . . 4
β’ (π₯πΈπ¦ β (π₯ β (Baseβπ) β§ βπ§ β (Baseβπ)(π§(.rβπ)π₯) = π¦)) |
22 | | subrgdvds.2 |
. . . . 5
β’ β₯ =
(β₯rβπ
) |
23 | 6, 22, 10 | dvdsr 20254 |
. . . 4
β’ (π₯ β₯ π¦ β (π₯ β (Baseβπ
) β§ βπ§ β (Baseβπ
)(π§(.rβπ
)π₯) = π¦)) |
24 | 18, 21, 23 | 3imtr4g 295 |
. . 3
β’ (π΄ β (SubRingβπ
) β (π₯πΈπ¦ β π₯ β₯ π¦)) |
25 | | df-br 5150 |
. . 3
β’ (π₯πΈπ¦ β β¨π₯, π¦β© β πΈ) |
26 | | df-br 5150 |
. . 3
β’ (π₯ β₯ π¦ β β¨π₯, π¦β© β β₯ ) |
27 | 24, 25, 26 | 3imtr3g 294 |
. 2
β’ (π΄ β (SubRingβπ
) β (β¨π₯, π¦β© β πΈ β β¨π₯, π¦β© β β₯ )) |
28 | 3, 27 | relssdv 5789 |
1
β’ (π΄ β (SubRingβπ
) β πΈ β β₯ ) |