Step | Hyp | Ref
| Expression |
1 | | rgspnval.sp |
. 2
β’ (π β π = (πβπ΄)) |
2 | | rgspnval.n |
. . 3
β’ (π β π = (RingSpanβπ
)) |
3 | 2 | fveq1d 6849 |
. 2
β’ (π β (πβπ΄) = ((RingSpanβπ
)βπ΄)) |
4 | | rgspnval.r |
. . . . 5
β’ (π β π
β Ring) |
5 | | elex 3466 |
. . . . 5
β’ (π
β Ring β π
β V) |
6 | | fveq2 6847 |
. . . . . . . 8
β’ (π = π
β (Baseβπ) = (Baseβπ
)) |
7 | 6 | pweqd 4582 |
. . . . . . 7
β’ (π = π
β π« (Baseβπ) = π« (Baseβπ
)) |
8 | | fveq2 6847 |
. . . . . . . . 9
β’ (π = π
β (SubRingβπ) = (SubRingβπ
)) |
9 | | rabeq 3424 |
. . . . . . . . 9
β’
((SubRingβπ) =
(SubRingβπ
) β
{π‘ β
(SubRingβπ) β£
π β π‘} = {π‘ β (SubRingβπ
) β£ π β π‘}) |
10 | 8, 9 | syl 17 |
. . . . . . . 8
β’ (π = π
β {π‘ β (SubRingβπ) β£ π β π‘} = {π‘ β (SubRingβπ
) β£ π β π‘}) |
11 | 10 | inteqd 4917 |
. . . . . . 7
β’ (π = π
β β© {π‘ β (SubRingβπ) β£ π β π‘} = β© {π‘ β (SubRingβπ
) β£ π β π‘}) |
12 | 7, 11 | mpteq12dv 5201 |
. . . . . 6
β’ (π = π
β (π β π« (Baseβπ) β¦ β© {π‘
β (SubRingβπ)
β£ π β π‘}) = (π β π« (Baseβπ
) β¦ β© {π‘
β (SubRingβπ
)
β£ π β π‘})) |
13 | | df-rgspn 20237 |
. . . . . 6
β’ RingSpan
= (π β V β¦
(π β π«
(Baseβπ) β¦
β© {π‘ β (SubRingβπ) β£ π β π‘})) |
14 | | fvex 6860 |
. . . . . . . 8
β’
(Baseβπ
)
β V |
15 | 14 | pwex 5340 |
. . . . . . 7
β’ π«
(Baseβπ
) β
V |
16 | 15 | mptex 7178 |
. . . . . 6
β’ (π β π«
(Baseβπ
) β¦
β© {π‘ β (SubRingβπ
) β£ π β π‘}) β V |
17 | 12, 13, 16 | fvmpt 6953 |
. . . . 5
β’ (π
β V β
(RingSpanβπ
) = (π β π«
(Baseβπ
) β¦
β© {π‘ β (SubRingβπ
) β£ π β π‘})) |
18 | 4, 5, 17 | 3syl 18 |
. . . 4
β’ (π β (RingSpanβπ
) = (π β π« (Baseβπ
) β¦ β© {π‘
β (SubRingβπ
)
β£ π β π‘})) |
19 | 18 | fveq1d 6849 |
. . 3
β’ (π β ((RingSpanβπ
)βπ΄) = ((π β π« (Baseβπ
) β¦ β© {π‘
β (SubRingβπ
)
β£ π β π‘})βπ΄)) |
20 | | eqid 2737 |
. . . 4
β’ (π β π«
(Baseβπ
) β¦
β© {π‘ β (SubRingβπ
) β£ π β π‘}) = (π β π« (Baseβπ
) β¦ β© {π‘
β (SubRingβπ
)
β£ π β π‘}) |
21 | | sseq1 3974 |
. . . . . 6
β’ (π = π΄ β (π β π‘ β π΄ β π‘)) |
22 | 21 | rabbidv 3418 |
. . . . 5
β’ (π = π΄ β {π‘ β (SubRingβπ
) β£ π β π‘} = {π‘ β (SubRingβπ
) β£ π΄ β π‘}) |
23 | 22 | inteqd 4917 |
. . . 4
β’ (π = π΄ β β© {π‘ β (SubRingβπ
) β£ π β π‘} = β© {π‘ β (SubRingβπ
) β£ π΄ β π‘}) |
24 | | rgspnval.ss |
. . . . . 6
β’ (π β π΄ β π΅) |
25 | | rgspnval.b |
. . . . . 6
β’ (π β π΅ = (Baseβπ
)) |
26 | 24, 25 | sseqtrd 3989 |
. . . . 5
β’ (π β π΄ β (Baseβπ
)) |
27 | 14 | elpw2 5307 |
. . . . 5
β’ (π΄ β π«
(Baseβπ
) β π΄ β (Baseβπ
)) |
28 | 26, 27 | sylibr 233 |
. . . 4
β’ (π β π΄ β π« (Baseβπ
)) |
29 | | eqid 2737 |
. . . . . . . . 9
β’
(Baseβπ
) =
(Baseβπ
) |
30 | 29 | subrgid 20240 |
. . . . . . . 8
β’ (π
β Ring β
(Baseβπ
) β
(SubRingβπ
)) |
31 | 4, 30 | syl 17 |
. . . . . . 7
β’ (π β (Baseβπ
) β (SubRingβπ
)) |
32 | 25, 31 | eqeltrd 2838 |
. . . . . 6
β’ (π β π΅ β (SubRingβπ
)) |
33 | | sseq2 3975 |
. . . . . . 7
β’ (π‘ = π΅ β (π΄ β π‘ β π΄ β π΅)) |
34 | 33 | rspcev 3584 |
. . . . . 6
β’ ((π΅ β (SubRingβπ
) β§ π΄ β π΅) β βπ‘ β (SubRingβπ
)π΄ β π‘) |
35 | 32, 24, 34 | syl2anc 585 |
. . . . 5
β’ (π β βπ‘ β (SubRingβπ
)π΄ β π‘) |
36 | | intexrab 5302 |
. . . . 5
β’
(βπ‘ β
(SubRingβπ
)π΄ β π‘ β β© {π‘ β (SubRingβπ
) β£ π΄ β π‘} β V) |
37 | 35, 36 | sylib 217 |
. . . 4
β’ (π β β© {π‘
β (SubRingβπ
)
β£ π΄ β π‘} β V) |
38 | 20, 23, 28, 37 | fvmptd3 6976 |
. . 3
β’ (π β ((π β π« (Baseβπ
) β¦ β© {π‘
β (SubRingβπ
)
β£ π β π‘})βπ΄) = β© {π‘ β (SubRingβπ
) β£ π΄ β π‘}) |
39 | 19, 38 | eqtrd 2777 |
. 2
β’ (π β ((RingSpanβπ
)βπ΄) = β© {π‘ β (SubRingβπ
) β£ π΄ β π‘}) |
40 | 1, 3, 39 | 3eqtrd 2781 |
1
β’ (π β π = β© {π‘ β (SubRingβπ
) β£ π΄ β π‘}) |