Step | Hyp | Ref
| Expression |
1 | | subrgpropd.1 |
. . . . . 6
β’ (π β π΅ = (BaseβπΎ)) |
2 | | subrgpropd.2 |
. . . . . 6
β’ (π β π΅ = (BaseβπΏ)) |
3 | | subrgpropd.3 |
. . . . . 6
β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β (π₯(+gβπΎ)π¦) = (π₯(+gβπΏ)π¦)) |
4 | | subrgpropd.4 |
. . . . . 6
β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β (π₯(.rβπΎ)π¦) = (π₯(.rβπΏ)π¦)) |
5 | 1, 2, 3, 4 | ringpropd 20013 |
. . . . 5
β’ (π β (πΎ β Ring β πΏ β Ring)) |
6 | 1 | ineq2d 4177 |
. . . . . . 7
β’ (π β (π β© π΅) = (π β© (BaseβπΎ))) |
7 | | eqid 2737 |
. . . . . . . . 9
β’ (πΎ βΎs π ) = (πΎ βΎs π ) |
8 | | eqid 2737 |
. . . . . . . . 9
β’
(BaseβπΎ) =
(BaseβπΎ) |
9 | 7, 8 | ressbas 17125 |
. . . . . . . 8
β’ (π β V β (π β© (BaseβπΎ)) = (Baseβ(πΎ βΎs π ))) |
10 | 9 | elv 3454 |
. . . . . . 7
β’ (π β© (BaseβπΎ)) = (Baseβ(πΎ βΎs π )) |
11 | 6, 10 | eqtrdi 2793 |
. . . . . 6
β’ (π β (π β© π΅) = (Baseβ(πΎ βΎs π ))) |
12 | 2 | ineq2d 4177 |
. . . . . . 7
β’ (π β (π β© π΅) = (π β© (BaseβπΏ))) |
13 | | eqid 2737 |
. . . . . . . . 9
β’ (πΏ βΎs π ) = (πΏ βΎs π ) |
14 | | eqid 2737 |
. . . . . . . . 9
β’
(BaseβπΏ) =
(BaseβπΏ) |
15 | 13, 14 | ressbas 17125 |
. . . . . . . 8
β’ (π β V β (π β© (BaseβπΏ)) = (Baseβ(πΏ βΎs π ))) |
16 | 15 | elv 3454 |
. . . . . . 7
β’ (π β© (BaseβπΏ)) = (Baseβ(πΏ βΎs π )) |
17 | 12, 16 | eqtrdi 2793 |
. . . . . 6
β’ (π β (π β© π΅) = (Baseβ(πΏ βΎs π ))) |
18 | | elinel2 4161 |
. . . . . . . 8
β’ (π₯ β (π β© π΅) β π₯ β π΅) |
19 | | elinel2 4161 |
. . . . . . . 8
β’ (π¦ β (π β© π΅) β π¦ β π΅) |
20 | 18, 19 | anim12i 614 |
. . . . . . 7
β’ ((π₯ β (π β© π΅) β§ π¦ β (π β© π΅)) β (π₯ β π΅ β§ π¦ β π΅)) |
21 | | eqid 2737 |
. . . . . . . . . . 11
β’
(+gβπΎ) = (+gβπΎ) |
22 | 7, 21 | ressplusg 17178 |
. . . . . . . . . 10
β’ (π β V β
(+gβπΎ) =
(+gβ(πΎ
βΎs π ))) |
23 | 22 | elv 3454 |
. . . . . . . . 9
β’
(+gβπΎ) = (+gβ(πΎ βΎs π )) |
24 | 23 | oveqi 7375 |
. . . . . . . 8
β’ (π₯(+gβπΎ)π¦) = (π₯(+gβ(πΎ βΎs π ))π¦) |
25 | | eqid 2737 |
. . . . . . . . . . 11
β’
(+gβπΏ) = (+gβπΏ) |
26 | 13, 25 | ressplusg 17178 |
. . . . . . . . . 10
β’ (π β V β
(+gβπΏ) =
(+gβ(πΏ
βΎs π ))) |
27 | 26 | elv 3454 |
. . . . . . . . 9
β’
(+gβπΏ) = (+gβ(πΏ βΎs π )) |
28 | 27 | oveqi 7375 |
. . . . . . . 8
β’ (π₯(+gβπΏ)π¦) = (π₯(+gβ(πΏ βΎs π ))π¦) |
29 | 3, 24, 28 | 3eqtr3g 2800 |
. . . . . . 7
β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β (π₯(+gβ(πΎ βΎs π ))π¦) = (π₯(+gβ(πΏ βΎs π ))π¦)) |
30 | 20, 29 | sylan2 594 |
. . . . . 6
β’ ((π β§ (π₯ β (π β© π΅) β§ π¦ β (π β© π΅))) β (π₯(+gβ(πΎ βΎs π ))π¦) = (π₯(+gβ(πΏ βΎs π ))π¦)) |
31 | | eqid 2737 |
. . . . . . . . . . 11
β’
(.rβπΎ) = (.rβπΎ) |
32 | 7, 31 | ressmulr 17195 |
. . . . . . . . . 10
β’ (π β V β
(.rβπΎ) =
(.rβ(πΎ
βΎs π ))) |
33 | 32 | elv 3454 |
. . . . . . . . 9
β’
(.rβπΎ) = (.rβ(πΎ βΎs π )) |
34 | 33 | oveqi 7375 |
. . . . . . . 8
β’ (π₯(.rβπΎ)π¦) = (π₯(.rβ(πΎ βΎs π ))π¦) |
35 | | eqid 2737 |
. . . . . . . . . . 11
β’
(.rβπΏ) = (.rβπΏ) |
36 | 13, 35 | ressmulr 17195 |
. . . . . . . . . 10
β’ (π β V β
(.rβπΏ) =
(.rβ(πΏ
βΎs π ))) |
37 | 36 | elv 3454 |
. . . . . . . . 9
β’
(.rβπΏ) = (.rβ(πΏ βΎs π )) |
38 | 37 | oveqi 7375 |
. . . . . . . 8
β’ (π₯(.rβπΏ)π¦) = (π₯(.rβ(πΏ βΎs π ))π¦) |
39 | 4, 34, 38 | 3eqtr3g 2800 |
. . . . . . 7
β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β (π₯(.rβ(πΎ βΎs π ))π¦) = (π₯(.rβ(πΏ βΎs π ))π¦)) |
40 | 20, 39 | sylan2 594 |
. . . . . 6
β’ ((π β§ (π₯ β (π β© π΅) β§ π¦ β (π β© π΅))) β (π₯(.rβ(πΎ βΎs π ))π¦) = (π₯(.rβ(πΏ βΎs π ))π¦)) |
41 | 11, 17, 30, 40 | ringpropd 20013 |
. . . . 5
β’ (π β ((πΎ βΎs π ) β Ring β (πΏ βΎs π ) β Ring)) |
42 | 5, 41 | anbi12d 632 |
. . . 4
β’ (π β ((πΎ β Ring β§ (πΎ βΎs π ) β Ring) β (πΏ β Ring β§ (πΏ βΎs π ) β Ring))) |
43 | 1, 2 | eqtr3d 2779 |
. . . . . 6
β’ (π β (BaseβπΎ) = (BaseβπΏ)) |
44 | 43 | sseq2d 3981 |
. . . . 5
β’ (π β (π β (BaseβπΎ) β π β (BaseβπΏ))) |
45 | 1, 2, 4 | rngidpropd 20133 |
. . . . . 6
β’ (π β (1rβπΎ) = (1rβπΏ)) |
46 | 45 | eleq1d 2823 |
. . . . 5
β’ (π β
((1rβπΎ)
β π β
(1rβπΏ)
β π )) |
47 | 44, 46 | anbi12d 632 |
. . . 4
β’ (π β ((π β (BaseβπΎ) β§ (1rβπΎ) β π ) β (π β (BaseβπΏ) β§ (1rβπΏ) β π ))) |
48 | 42, 47 | anbi12d 632 |
. . 3
β’ (π β (((πΎ β Ring β§ (πΎ βΎs π ) β Ring) β§ (π β (BaseβπΎ) β§ (1rβπΎ) β π )) β ((πΏ β Ring β§ (πΏ βΎs π ) β Ring) β§ (π β (BaseβπΏ) β§ (1rβπΏ) β π )))) |
49 | | eqid 2737 |
. . . 4
β’
(1rβπΎ) = (1rβπΎ) |
50 | 8, 49 | issubrg 20238 |
. . 3
β’ (π β (SubRingβπΎ) β ((πΎ β Ring β§ (πΎ βΎs π ) β Ring) β§ (π β (BaseβπΎ) β§ (1rβπΎ) β π ))) |
51 | | eqid 2737 |
. . . 4
β’
(1rβπΏ) = (1rβπΏ) |
52 | 14, 51 | issubrg 20238 |
. . 3
β’ (π β (SubRingβπΏ) β ((πΏ β Ring β§ (πΏ βΎs π ) β Ring) β§ (π β (BaseβπΏ) β§ (1rβπΏ) β π ))) |
53 | 48, 50, 52 | 3bitr4g 314 |
. 2
β’ (π β (π β (SubRingβπΎ) β π β (SubRingβπΏ))) |
54 | 53 | eqrdv 2735 |
1
β’ (π β (SubRingβπΎ) = (SubRingβπΏ)) |