| Step | Hyp | Ref
| Expression |
|---|
| 1 | | elin 3964 |
. . . . . . . . 9
β’ (π₯ β ((SubRingβπ) β© (LSubSpβπ)) β (π₯ β (SubRingβπ) β§ π₯ β (LSubSpβπ))) |
| 2 | 1 | anbi1i 624 |
. . . . . . . 8
β’ ((π₯ β ((SubRingβπ) β© (LSubSpβπ)) β§ π β π₯) β ((π₯ β (SubRingβπ) β§ π₯ β (LSubSpβπ)) β§ π β π₯)) |
| 3 | | anass 469 |
. . . . . . . 8
β’ (((π₯ β (SubRingβπ) β§ π₯ β (LSubSpβπ)) β§ π β π₯) β (π₯ β (SubRingβπ) β§ (π₯ β (LSubSpβπ) β§ π β π₯))) |
| 4 | 2, 3 | bitri 274 |
. . . . . . 7
β’ ((π₯ β ((SubRingβπ) β© (LSubSpβπ)) β§ π β π₯) β (π₯ β (SubRingβπ) β§ (π₯ β (LSubSpβπ) β§ π β π₯))) |
| 5 | | aspval2.c |
. . . . . . . . . . 11
β’ πΆ = (algScβπ) |
| 6 | | eqid 2732 |
. . . . . . . . . . 11
β’
(LSubSpβπ) =
(LSubSpβπ) |
| 7 | 5, 6 | issubassa2 21445 |
. . . . . . . . . 10
β’ ((π β AssAlg β§ π₯ β (SubRingβπ)) β (π₯ β (LSubSpβπ) β ran πΆ β π₯)) |
| 8 | 7 | anbi1d 630 |
. . . . . . . . 9
β’ ((π β AssAlg β§ π₯ β (SubRingβπ)) β ((π₯ β (LSubSpβπ) β§ π β π₯) β (ran πΆ β π₯ β§ π β π₯))) |
| 9 | | unss 4184 |
. . . . . . . . 9
β’ ((ran
πΆ β π₯ β§ π β π₯) β (ran πΆ βͺ π) β π₯) |
| 10 | 8, 9 | bitrdi 286 |
. . . . . . . 8
β’ ((π β AssAlg β§ π₯ β (SubRingβπ)) β ((π₯ β (LSubSpβπ) β§ π β π₯) β (ran πΆ βͺ π) β π₯)) |
| 11 | 10 | pm5.32da 579 |
. . . . . . 7
β’ (π β AssAlg β ((π₯ β (SubRingβπ) β§ (π₯ β (LSubSpβπ) β§ π β π₯)) β (π₯ β (SubRingβπ) β§ (ran πΆ βͺ π) β π₯))) |
| 12 | 4, 11 | bitrid 282 |
. . . . . 6
β’ (π β AssAlg β ((π₯ β ((SubRingβπ) β© (LSubSpβπ)) β§ π β π₯) β (π₯ β (SubRingβπ) β§ (ran πΆ βͺ π) β π₯))) |
| 13 | 12 | abbidv 2801 |
. . . . 5
β’ (π β AssAlg β {π₯ β£ (π₯ β ((SubRingβπ) β© (LSubSpβπ)) β§ π β π₯)} = {π₯ β£ (π₯ β (SubRingβπ) β§ (ran πΆ βͺ π) β π₯)}) |
| 14 | 13 | adantr 481 |
. . . 4
β’ ((π β AssAlg β§ π β π) β {π₯ β£ (π₯ β ((SubRingβπ) β© (LSubSpβπ)) β§ π β π₯)} = {π₯ β£ (π₯ β (SubRingβπ) β§ (ran πΆ βͺ π) β π₯)}) |
| 15 | | df-rab 3433 |
. . . 4
β’ {π₯ β ((SubRingβπ) β© (LSubSpβπ)) β£ π β π₯} = {π₯ β£ (π₯ β ((SubRingβπ) β© (LSubSpβπ)) β§ π β π₯)} |
| 16 | | df-rab 3433 |
. . . 4
β’ {π₯ β (SubRingβπ) β£ (ran πΆ βͺ π) β π₯} = {π₯ β£ (π₯ β (SubRingβπ) β§ (ran πΆ βͺ π) β π₯)} |
| 17 | 14, 15, 16 | 3eqtr4g 2797 |
. . 3
β’ ((π β AssAlg β§ π β π) β {π₯ β ((SubRingβπ) β© (LSubSpβπ)) β£ π β π₯} = {π₯ β (SubRingβπ) β£ (ran πΆ βͺ π) β π₯}) |
| 18 | 17 | inteqd 4955 |
. 2
β’ ((π β AssAlg β§ π β π) β β© {π₯ β ((SubRingβπ) β© (LSubSpβπ)) β£ π β π₯} = β© {π₯ β (SubRingβπ) β£ (ran πΆ βͺ π) β π₯}) |
| 19 | | aspval2.a |
. . 3
β’ π΄ = (AlgSpanβπ) |
| 20 | | aspval2.v |
. . 3
β’ π = (Baseβπ) |
| 21 | 19, 20, 6 | aspval 21426 |
. 2
β’ ((π β AssAlg β§ π β π) β (π΄βπ) = β© {π₯ β ((SubRingβπ) β© (LSubSpβπ)) β£ π β π₯}) |
| 22 | | assaring 21415 |
. . . 4
β’ (π β AssAlg β π β Ring) |
| 23 | 20 | subrgmre 20343 |
. . . 4
β’ (π β Ring β
(SubRingβπ) β
(Mooreβπ)) |
| 24 | 22, 23 | syl 17 |
. . 3
β’ (π β AssAlg β
(SubRingβπ) β
(Mooreβπ)) |
| 25 | | eqid 2732 |
. . . . . . 7
β’
(Scalarβπ) =
(Scalarβπ) |
| 26 | | assalmod 21414 |
. . . . . . 7
β’ (π β AssAlg β π β LMod) |
| 27 | | eqid 2732 |
. . . . . . 7
β’
(Baseβ(Scalarβπ)) = (Baseβ(Scalarβπ)) |
| 28 | 5, 25, 22, 26, 27, 20 | asclf 21435 |
. . . . . 6
β’ (π β AssAlg β πΆ:(Baseβ(Scalarβπ))βΆπ) |
| 29 | 28 | frnd 6725 |
. . . . 5
β’ (π β AssAlg β ran πΆ β π) |
| 30 | 29 | adantr 481 |
. . . 4
β’ ((π β AssAlg β§ π β π) β ran πΆ β π) |
| 31 | | simpr 485 |
. . . 4
β’ ((π β AssAlg β§ π β π) β π β π) |
| 32 | 30, 31 | unssd 4186 |
. . 3
β’ ((π β AssAlg β§ π β π) β (ran πΆ βͺ π) β π) |
| 33 | | aspval2.r |
. . . 4
β’ π
=
(mrClsβ(SubRingβπ)) |
| 34 | 33 | mrcval 17553 |
. . 3
β’
(((SubRingβπ)
β (Mooreβπ)
β§ (ran πΆ βͺ π) β π) β (π
β(ran πΆ βͺ π)) = β© {π₯ β (SubRingβπ) β£ (ran πΆ βͺ π) β π₯}) |
| 35 | 24, 32, 34 | syl2an2r 683 |
. 2
β’ ((π β AssAlg β§ π β π) β (π
β(ran πΆ βͺ π)) = β© {π₯ β (SubRingβπ) β£ (ran πΆ βͺ π) β π₯}) |
| 36 | 18, 21, 35 | 3eqtr4d 2782 |
1
β’ ((π β AssAlg β§ π β π) β (π΄βπ) = (π
β(ran πΆ βͺ π))) |
