Step | Hyp | Ref
| Expression |
1 | | subrgrcl 20466 |
. . . . 5
β’ (π΄ β (SubRingβπ
) β π
β Ring) |
2 | 1 | adantr 479 |
. . . 4
β’ ((π΄ β (SubRingβπ
) β§ π΅ β (SubRingβπ)) β π
β Ring) |
3 | | eqid 2730 |
. . . . . . . . 9
β’
(Baseβπ) =
(Baseβπ) |
4 | 3 | subrgss 20462 |
. . . . . . . 8
β’ (π΅ β (SubRingβπ) β π΅ β (Baseβπ)) |
5 | 4 | adantl 480 |
. . . . . . 7
β’ ((π΄ β (SubRingβπ
) β§ π΅ β (SubRingβπ)) β π΅ β (Baseβπ)) |
6 | | subsubrg.s |
. . . . . . . . 9
β’ π = (π
βΎs π΄) |
7 | 6 | subrgbas 20471 |
. . . . . . . 8
β’ (π΄ β (SubRingβπ
) β π΄ = (Baseβπ)) |
8 | 7 | adantr 479 |
. . . . . . 7
β’ ((π΄ β (SubRingβπ
) β§ π΅ β (SubRingβπ)) β π΄ = (Baseβπ)) |
9 | 5, 8 | sseqtrrd 4022 |
. . . . . 6
β’ ((π΄ β (SubRingβπ
) β§ π΅ β (SubRingβπ)) β π΅ β π΄) |
10 | 6 | oveq1i 7421 |
. . . . . . 7
β’ (π βΎs π΅) = ((π
βΎs π΄) βΎs π΅) |
11 | | ressabs 17198 |
. . . . . . 7
β’ ((π΄ β (SubRingβπ
) β§ π΅ β π΄) β ((π
βΎs π΄) βΎs π΅) = (π
βΎs π΅)) |
12 | 10, 11 | eqtrid 2782 |
. . . . . 6
β’ ((π΄ β (SubRingβπ
) β§ π΅ β π΄) β (π βΎs π΅) = (π
βΎs π΅)) |
13 | 9, 12 | syldan 589 |
. . . . 5
β’ ((π΄ β (SubRingβπ
) β§ π΅ β (SubRingβπ)) β (π βΎs π΅) = (π
βΎs π΅)) |
14 | | eqid 2730 |
. . . . . . 7
β’ (π βΎs π΅) = (π βΎs π΅) |
15 | 14 | subrgring 20464 |
. . . . . 6
β’ (π΅ β (SubRingβπ) β (π βΎs π΅) β Ring) |
16 | 15 | adantl 480 |
. . . . 5
β’ ((π΄ β (SubRingβπ
) β§ π΅ β (SubRingβπ)) β (π βΎs π΅) β Ring) |
17 | 13, 16 | eqeltrrd 2832 |
. . . 4
β’ ((π΄ β (SubRingβπ
) β§ π΅ β (SubRingβπ)) β (π
βΎs π΅) β Ring) |
18 | | eqid 2730 |
. . . . . . . 8
β’
(Baseβπ
) =
(Baseβπ
) |
19 | 18 | subrgss 20462 |
. . . . . . 7
β’ (π΄ β (SubRingβπ
) β π΄ β (Baseβπ
)) |
20 | 19 | adantr 479 |
. . . . . 6
β’ ((π΄ β (SubRingβπ
) β§ π΅ β (SubRingβπ)) β π΄ β (Baseβπ
)) |
21 | 9, 20 | sstrd 3991 |
. . . . 5
β’ ((π΄ β (SubRingβπ
) β§ π΅ β (SubRingβπ)) β π΅ β (Baseβπ
)) |
22 | | eqid 2730 |
. . . . . . . 8
β’
(1rβπ
) = (1rβπ
) |
23 | 6, 22 | subrg1 20472 |
. . . . . . 7
β’ (π΄ β (SubRingβπ
) β
(1rβπ
) =
(1rβπ)) |
24 | 23 | adantr 479 |
. . . . . 6
β’ ((π΄ β (SubRingβπ
) β§ π΅ β (SubRingβπ)) β (1rβπ
) = (1rβπ)) |
25 | | eqid 2730 |
. . . . . . . 8
β’
(1rβπ) = (1rβπ) |
26 | 25 | subrg1cl 20470 |
. . . . . . 7
β’ (π΅ β (SubRingβπ) β
(1rβπ)
β π΅) |
27 | 26 | adantl 480 |
. . . . . 6
β’ ((π΄ β (SubRingβπ
) β§ π΅ β (SubRingβπ)) β (1rβπ) β π΅) |
28 | 24, 27 | eqeltrd 2831 |
. . . . 5
β’ ((π΄ β (SubRingβπ
) β§ π΅ β (SubRingβπ)) β (1rβπ
) β π΅) |
29 | 21, 28 | jca 510 |
. . . 4
β’ ((π΄ β (SubRingβπ
) β§ π΅ β (SubRingβπ)) β (π΅ β (Baseβπ
) β§ (1rβπ
) β π΅)) |
30 | 18, 22 | issubrg 20461 |
. . . 4
β’ (π΅ β (SubRingβπ
) β ((π
β Ring β§ (π
βΎs π΅) β Ring) β§ (π΅ β (Baseβπ
) β§ (1rβπ
) β π΅))) |
31 | 2, 17, 29, 30 | syl21anbrc 1342 |
. . 3
β’ ((π΄ β (SubRingβπ
) β§ π΅ β (SubRingβπ)) β π΅ β (SubRingβπ
)) |
32 | 31, 9 | jca 510 |
. 2
β’ ((π΄ β (SubRingβπ
) β§ π΅ β (SubRingβπ)) β (π΅ β (SubRingβπ
) β§ π΅ β π΄)) |
33 | 6 | subrgring 20464 |
. . . 4
β’ (π΄ β (SubRingβπ
) β π β Ring) |
34 | 33 | adantr 479 |
. . 3
β’ ((π΄ β (SubRingβπ
) β§ (π΅ β (SubRingβπ
) β§ π΅ β π΄)) β π β Ring) |
35 | 12 | adantrl 712 |
. . . 4
β’ ((π΄ β (SubRingβπ
) β§ (π΅ β (SubRingβπ
) β§ π΅ β π΄)) β (π βΎs π΅) = (π
βΎs π΅)) |
36 | | eqid 2730 |
. . . . . 6
β’ (π
βΎs π΅) = (π
βΎs π΅) |
37 | 36 | subrgring 20464 |
. . . . 5
β’ (π΅ β (SubRingβπ
) β (π
βΎs π΅) β Ring) |
38 | 37 | ad2antrl 724 |
. . . 4
β’ ((π΄ β (SubRingβπ
) β§ (π΅ β (SubRingβπ
) β§ π΅ β π΄)) β (π
βΎs π΅) β Ring) |
39 | 35, 38 | eqeltrd 2831 |
. . 3
β’ ((π΄ β (SubRingβπ
) β§ (π΅ β (SubRingβπ
) β§ π΅ β π΄)) β (π βΎs π΅) β Ring) |
40 | | simprr 769 |
. . . . 5
β’ ((π΄ β (SubRingβπ
) β§ (π΅ β (SubRingβπ
) β§ π΅ β π΄)) β π΅ β π΄) |
41 | 7 | adantr 479 |
. . . . 5
β’ ((π΄ β (SubRingβπ
) β§ (π΅ β (SubRingβπ
) β§ π΅ β π΄)) β π΄ = (Baseβπ)) |
42 | 40, 41 | sseqtrd 4021 |
. . . 4
β’ ((π΄ β (SubRingβπ
) β§ (π΅ β (SubRingβπ
) β§ π΅ β π΄)) β π΅ β (Baseβπ)) |
43 | 23 | adantr 479 |
. . . . 5
β’ ((π΄ β (SubRingβπ
) β§ (π΅ β (SubRingβπ
) β§ π΅ β π΄)) β (1rβπ
) = (1rβπ)) |
44 | 22 | subrg1cl 20470 |
. . . . . 6
β’ (π΅ β (SubRingβπ
) β
(1rβπ
)
β π΅) |
45 | 44 | ad2antrl 724 |
. . . . 5
β’ ((π΄ β (SubRingβπ
) β§ (π΅ β (SubRingβπ
) β§ π΅ β π΄)) β (1rβπ
) β π΅) |
46 | 43, 45 | eqeltrrd 2832 |
. . . 4
β’ ((π΄ β (SubRingβπ
) β§ (π΅ β (SubRingβπ
) β§ π΅ β π΄)) β (1rβπ) β π΅) |
47 | 42, 46 | jca 510 |
. . 3
β’ ((π΄ β (SubRingβπ
) β§ (π΅ β (SubRingβπ
) β§ π΅ β π΄)) β (π΅ β (Baseβπ) β§ (1rβπ) β π΅)) |
48 | 3, 25 | issubrg 20461 |
. . 3
β’ (π΅ β (SubRingβπ) β ((π β Ring β§ (π βΎs π΅) β Ring) β§ (π΅ β (Baseβπ) β§ (1rβπ) β π΅))) |
49 | 34, 39, 47, 48 | syl21anbrc 1342 |
. 2
β’ ((π΄ β (SubRingβπ
) β§ (π΅ β (SubRingβπ
) β§ π΅ β π΄)) β π΅ β (SubRingβπ)) |
50 | 32, 49 | impbida 797 |
1
β’ (π΄ β (SubRingβπ
) β (π΅ β (SubRingβπ) β (π΅ β (SubRingβπ
) β§ π΅ β π΄))) |