Step | Hyp | Ref
| Expression |
1 | | eqid 2737 |
. . . . . 6
β’
(Baseβπ
) =
(Baseβπ
) |
2 | | lnr2i.u |
. . . . . 6
β’ π = (LIdealβπ
) |
3 | | lnr2i.n |
. . . . . 6
β’ π = (RSpanβπ
) |
4 | 1, 2, 3 | islnr2 41470 |
. . . . 5
β’ (π
β LNoeR β (π
β Ring β§ βπ β π βπ β (π« (Baseβπ
) β© Fin)π = (πβπ))) |
5 | 4 | simprbi 498 |
. . . 4
β’ (π
β LNoeR β
βπ β π βπ β (π« (Baseβπ
) β© Fin)π = (πβπ)) |
6 | | eqeq1 2741 |
. . . . . 6
β’ (π = πΌ β (π = (πβπ) β πΌ = (πβπ))) |
7 | 6 | rexbidv 3176 |
. . . . 5
β’ (π = πΌ β (βπ β (π« (Baseβπ
) β© Fin)π = (πβπ) β βπ β (π« (Baseβπ
) β© Fin)πΌ = (πβπ))) |
8 | 7 | rspcva 3582 |
. . . 4
β’ ((πΌ β π β§ βπ β π βπ β (π« (Baseβπ
) β© Fin)π = (πβπ)) β βπ β (π« (Baseβπ
) β© Fin)πΌ = (πβπ)) |
9 | 5, 8 | sylan2 594 |
. . 3
β’ ((πΌ β π β§ π
β LNoeR) β βπ β (π«
(Baseβπ
) β©
Fin)πΌ = (πβπ)) |
10 | 9 | ancoms 460 |
. 2
β’ ((π
β LNoeR β§ πΌ β π) β βπ β (π« (Baseβπ
) β© Fin)πΌ = (πβπ)) |
11 | | lnrring 41468 |
. . . . . . . . . . . 12
β’ (π
β LNoeR β π
β Ring) |
12 | 3, 1 | rspssid 20709 |
. . . . . . . . . . . 12
β’ ((π
β Ring β§ π β (Baseβπ
)) β π β (πβπ)) |
13 | 11, 12 | sylan 581 |
. . . . . . . . . . 11
β’ ((π
β LNoeR β§ π β (Baseβπ
)) β π β (πβπ)) |
14 | 13 | ex 414 |
. . . . . . . . . 10
β’ (π
β LNoeR β (π β (Baseβπ
) β π β (πβπ))) |
15 | | vex 3452 |
. . . . . . . . . . 11
β’ π β V |
16 | 15 | elpw 4569 |
. . . . . . . . . 10
β’ (π β π«
(Baseβπ
) β π β (Baseβπ
)) |
17 | 15 | elpw 4569 |
. . . . . . . . . 10
β’ (π β π« (πβπ) β π β (πβπ)) |
18 | 14, 16, 17 | 3imtr4g 296 |
. . . . . . . . 9
β’ (π
β LNoeR β (π β π«
(Baseβπ
) β π β π« (πβπ))) |
19 | 18 | anim1d 612 |
. . . . . . . 8
β’ (π
β LNoeR β ((π β π«
(Baseβπ
) β§ π β Fin) β (π β π« (πβπ) β§ π β Fin))) |
20 | | elin 3931 |
. . . . . . . 8
β’ (π β (π«
(Baseβπ
) β© Fin)
β (π β π«
(Baseβπ
) β§ π β Fin)) |
21 | | elin 3931 |
. . . . . . . 8
β’ (π β (π« (πβπ) β© Fin) β (π β π« (πβπ) β§ π β Fin)) |
22 | 19, 20, 21 | 3imtr4g 296 |
. . . . . . 7
β’ (π
β LNoeR β (π β (π«
(Baseβπ
) β© Fin)
β π β (π«
(πβπ) β© Fin))) |
23 | | pweq 4579 |
. . . . . . . . . 10
β’ (πΌ = (πβπ) β π« πΌ = π« (πβπ)) |
24 | 23 | ineq1d 4176 |
. . . . . . . . 9
β’ (πΌ = (πβπ) β (π« πΌ β© Fin) = (π« (πβπ) β© Fin)) |
25 | 24 | eleq2d 2824 |
. . . . . . . 8
β’ (πΌ = (πβπ) β (π β (π« πΌ β© Fin) β π β (π« (πβπ) β© Fin))) |
26 | 25 | imbi2d 341 |
. . . . . . 7
β’ (πΌ = (πβπ) β ((π β (π« (Baseβπ
) β© Fin) β π β (π« πΌ β© Fin)) β (π β (π«
(Baseβπ
) β© Fin)
β π β (π«
(πβπ) β© Fin)))) |
27 | 22, 26 | syl5ibrcom 247 |
. . . . . 6
β’ (π
β LNoeR β (πΌ = (πβπ) β (π β (π« (Baseβπ
) β© Fin) β π β (π« πΌ β© Fin)))) |
28 | 27 | imdistand 572 |
. . . . 5
β’ (π
β LNoeR β ((πΌ = (πβπ) β§ π β (π« (Baseβπ
) β© Fin)) β (πΌ = (πβπ) β§ π β (π« πΌ β© Fin)))) |
29 | | ancom 462 |
. . . . 5
β’ ((π β (π«
(Baseβπ
) β© Fin)
β§ πΌ = (πβπ)) β (πΌ = (πβπ) β§ π β (π« (Baseβπ
) β© Fin))) |
30 | | ancom 462 |
. . . . 5
β’ ((π β (π« πΌ β© Fin) β§ πΌ = (πβπ)) β (πΌ = (πβπ) β§ π β (π« πΌ β© Fin))) |
31 | 28, 29, 30 | 3imtr4g 296 |
. . . 4
β’ (π
β LNoeR β ((π β (π«
(Baseβπ
) β© Fin)
β§ πΌ = (πβπ)) β (π β (π« πΌ β© Fin) β§ πΌ = (πβπ)))) |
32 | 31 | reximdv2 3162 |
. . 3
β’ (π
β LNoeR β
(βπ β (π«
(Baseβπ
) β©
Fin)πΌ = (πβπ) β βπ β (π« πΌ β© Fin)πΌ = (πβπ))) |
33 | 32 | adantr 482 |
. 2
β’ ((π
β LNoeR β§ πΌ β π) β (βπ β (π« (Baseβπ
) β© Fin)πΌ = (πβπ) β βπ β (π« πΌ β© Fin)πΌ = (πβπ))) |
34 | 10, 33 | mpd 15 |
1
β’ ((π
β LNoeR β§ πΌ β π) β βπ β (π« πΌ β© Fin)πΌ = (πβπ)) |