Step | Hyp | Ref
| Expression |
1 | | simpl 484 |
. . . . . 6
β’ ((π = πΈ β§ π = πΉ) β π = πΈ) |
2 | 1 | eleq1d 2819 |
. . . . 5
β’ ((π = πΈ β§ π = πΉ) β (π β Field β πΈ β Field)) |
3 | | simpr 486 |
. . . . . 6
β’ ((π = πΈ β§ π = πΉ) β π = πΉ) |
4 | 3 | eleq1d 2819 |
. . . . 5
β’ ((π = πΈ β§ π = πΉ) β (π β Field β πΉ β Field)) |
5 | 2, 4 | anbi12d 632 |
. . . 4
β’ ((π = πΈ β§ π = πΉ) β ((π β Field β§ π β Field) β (πΈ β Field β§ πΉ β Field))) |
6 | 3 | fveq2d 6847 |
. . . . . . 7
β’ ((π = πΈ β§ π = πΉ) β (Baseβπ) = (BaseβπΉ)) |
7 | 1, 6 | oveq12d 7376 |
. . . . . 6
β’ ((π = πΈ β§ π = πΉ) β (π βΎs (Baseβπ)) = (πΈ βΎs (BaseβπΉ))) |
8 | 3, 7 | eqeq12d 2749 |
. . . . 5
β’ ((π = πΈ β§ π = πΉ) β (π = (π βΎs (Baseβπ)) β πΉ = (πΈ βΎs (BaseβπΉ)))) |
9 | 1 | fveq2d 6847 |
. . . . . 6
β’ ((π = πΈ β§ π = πΉ) β (SubRingβπ) = (SubRingβπΈ)) |
10 | 6, 9 | eleq12d 2828 |
. . . . 5
β’ ((π = πΈ β§ π = πΉ) β ((Baseβπ) β (SubRingβπ) β (BaseβπΉ) β (SubRingβπΈ))) |
11 | 8, 10 | anbi12d 632 |
. . . 4
β’ ((π = πΈ β§ π = πΉ) β ((π = (π βΎs (Baseβπ)) β§ (Baseβπ) β (SubRingβπ)) β (πΉ = (πΈ βΎs (BaseβπΉ)) β§ (BaseβπΉ) β (SubRingβπΈ)))) |
12 | 5, 11 | anbi12d 632 |
. . 3
β’ ((π = πΈ β§ π = πΉ) β (((π β Field β§ π β Field) β§ (π = (π βΎs (Baseβπ)) β§ (Baseβπ) β (SubRingβπ))) β ((πΈ β Field β§ πΉ β Field) β§ (πΉ = (πΈ βΎs (BaseβπΉ)) β§ (BaseβπΉ) β (SubRingβπΈ))))) |
13 | | df-fldext 32388 |
. . 3
β’
/FldExt = {β¨π, πβ© β£ ((π β Field β§ π β Field) β§ (π = (π βΎs (Baseβπ)) β§ (Baseβπ) β (SubRingβπ)))} |
14 | 12, 13 | brabga 5492 |
. 2
β’ ((πΈ β Field β§ πΉ β Field) β (πΈ/FldExtπΉ β ((πΈ β Field β§ πΉ β Field) β§ (πΉ = (πΈ βΎs (BaseβπΉ)) β§ (BaseβπΉ) β (SubRingβπΈ))))) |
15 | 14 | bianabs 543 |
1
β’ ((πΈ β Field β§ πΉ β Field) β (πΈ/FldExtπΉ β (πΉ = (πΈ βΎs (BaseβπΉ)) β§ (BaseβπΉ) β (SubRingβπΈ)))) |