Proof of Theorem ixpsnbasval
Step | Hyp | Ref
| Expression |
1 | | ixpsnval 8184 |
. . 3
⊢ (𝑋 ∈ 𝑊 → X𝑥 ∈ {𝑋} (Base‘(({𝑋} × {(ringLMod‘𝑅)})‘𝑥)) = {𝑓 ∣ (𝑓 Fn {𝑋} ∧ (𝑓‘𝑋) ∈ ⦋𝑋 / 𝑥⦌(Base‘(({𝑋} × {(ringLMod‘𝑅)})‘𝑥)))}) |
2 | 1 | adantl 475 |
. 2
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑋 ∈ 𝑊) → X𝑥 ∈ {𝑋} (Base‘(({𝑋} × {(ringLMod‘𝑅)})‘𝑥)) = {𝑓 ∣ (𝑓 Fn {𝑋} ∧ (𝑓‘𝑋) ∈ ⦋𝑋 / 𝑥⦌(Base‘(({𝑋} × {(ringLMod‘𝑅)})‘𝑥)))}) |
3 | | csbfv2g 6482 |
. . . . . . . . 9
⊢ (𝑋 ∈ 𝑊 → ⦋𝑋 / 𝑥⦌(Base‘(({𝑋} × {(ringLMod‘𝑅)})‘𝑥)) = (Base‘⦋𝑋 / 𝑥⦌(({𝑋} × {(ringLMod‘𝑅)})‘𝑥))) |
4 | | csbfv2g 6482 |
. . . . . . . . . . 11
⊢ (𝑋 ∈ 𝑊 → ⦋𝑋 / 𝑥⦌(({𝑋} × {(ringLMod‘𝑅)})‘𝑥) = (({𝑋} × {(ringLMod‘𝑅)})‘⦋𝑋 / 𝑥⦌𝑥)) |
5 | | csbvarg 4229 |
. . . . . . . . . . . 12
⊢ (𝑋 ∈ 𝑊 → ⦋𝑋 / 𝑥⦌𝑥 = 𝑋) |
6 | 5 | fveq2d 6441 |
. . . . . . . . . . 11
⊢ (𝑋 ∈ 𝑊 → (({𝑋} × {(ringLMod‘𝑅)})‘⦋𝑋 / 𝑥⦌𝑥) = (({𝑋} × {(ringLMod‘𝑅)})‘𝑋)) |
7 | 4, 6 | eqtrd 2861 |
. . . . . . . . . 10
⊢ (𝑋 ∈ 𝑊 → ⦋𝑋 / 𝑥⦌(({𝑋} × {(ringLMod‘𝑅)})‘𝑥) = (({𝑋} × {(ringLMod‘𝑅)})‘𝑋)) |
8 | 7 | fveq2d 6441 |
. . . . . . . . 9
⊢ (𝑋 ∈ 𝑊 → (Base‘⦋𝑋 / 𝑥⦌(({𝑋} × {(ringLMod‘𝑅)})‘𝑥)) = (Base‘(({𝑋} × {(ringLMod‘𝑅)})‘𝑋))) |
9 | 3, 8 | eqtrd 2861 |
. . . . . . . 8
⊢ (𝑋 ∈ 𝑊 → ⦋𝑋 / 𝑥⦌(Base‘(({𝑋} × {(ringLMod‘𝑅)})‘𝑥)) = (Base‘(({𝑋} × {(ringLMod‘𝑅)})‘𝑋))) |
10 | 9 | adantl 475 |
. . . . . . 7
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑋 ∈ 𝑊) → ⦋𝑋 / 𝑥⦌(Base‘(({𝑋} × {(ringLMod‘𝑅)})‘𝑥)) = (Base‘(({𝑋} × {(ringLMod‘𝑅)})‘𝑋))) |
11 | | fvexd 6452 |
. . . . . . . . . . . . 13
⊢ (𝑅 ∈ 𝑉 → (ringLMod‘𝑅) ∈ V) |
12 | 11 | anim1i 608 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑋 ∈ 𝑊) → ((ringLMod‘𝑅) ∈ V ∧ 𝑋 ∈ 𝑊)) |
13 | 12 | ancomd 455 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑋 ∈ 𝑊) → (𝑋 ∈ 𝑊 ∧ (ringLMod‘𝑅) ∈ V)) |
14 | | xpsng 6661 |
. . . . . . . . . . 11
⊢ ((𝑋 ∈ 𝑊 ∧ (ringLMod‘𝑅) ∈ V) → ({𝑋} × {(ringLMod‘𝑅)}) = {〈𝑋, (ringLMod‘𝑅)〉}) |
15 | 13, 14 | syl 17 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑋 ∈ 𝑊) → ({𝑋} × {(ringLMod‘𝑅)}) = {〈𝑋, (ringLMod‘𝑅)〉}) |
16 | 15 | fveq1d 6439 |
. . . . . . . . 9
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑋 ∈ 𝑊) → (({𝑋} × {(ringLMod‘𝑅)})‘𝑋) = ({〈𝑋, (ringLMod‘𝑅)〉}‘𝑋)) |
17 | | fvsng 6703 |
. . . . . . . . . 10
⊢ ((𝑋 ∈ 𝑊 ∧ (ringLMod‘𝑅) ∈ V) → ({〈𝑋, (ringLMod‘𝑅)〉}‘𝑋) = (ringLMod‘𝑅)) |
18 | 13, 17 | syl 17 |
. . . . . . . . 9
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑋 ∈ 𝑊) → ({〈𝑋, (ringLMod‘𝑅)〉}‘𝑋) = (ringLMod‘𝑅)) |
19 | 16, 18 | eqtrd 2861 |
. . . . . . . 8
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑋 ∈ 𝑊) → (({𝑋} × {(ringLMod‘𝑅)})‘𝑋) = (ringLMod‘𝑅)) |
20 | 19 | fveq2d 6441 |
. . . . . . 7
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑋 ∈ 𝑊) → (Base‘(({𝑋} × {(ringLMod‘𝑅)})‘𝑋)) = (Base‘(ringLMod‘𝑅))) |
21 | 10, 20 | eqtrd 2861 |
. . . . . 6
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑋 ∈ 𝑊) → ⦋𝑋 / 𝑥⦌(Base‘(({𝑋} × {(ringLMod‘𝑅)})‘𝑥)) = (Base‘(ringLMod‘𝑅))) |
22 | | rlmbas 19563 |
. . . . . 6
⊢
(Base‘𝑅) =
(Base‘(ringLMod‘𝑅)) |
23 | 21, 22 | syl6eqr 2879 |
. . . . 5
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑋 ∈ 𝑊) → ⦋𝑋 / 𝑥⦌(Base‘(({𝑋} × {(ringLMod‘𝑅)})‘𝑥)) = (Base‘𝑅)) |
24 | 23 | eleq2d 2892 |
. . . 4
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑋 ∈ 𝑊) → ((𝑓‘𝑋) ∈ ⦋𝑋 / 𝑥⦌(Base‘(({𝑋} × {(ringLMod‘𝑅)})‘𝑥)) ↔ (𝑓‘𝑋) ∈ (Base‘𝑅))) |
25 | 24 | anbi2d 622 |
. . 3
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑋 ∈ 𝑊) → ((𝑓 Fn {𝑋} ∧ (𝑓‘𝑋) ∈ ⦋𝑋 / 𝑥⦌(Base‘(({𝑋} × {(ringLMod‘𝑅)})‘𝑥))) ↔ (𝑓 Fn {𝑋} ∧ (𝑓‘𝑋) ∈ (Base‘𝑅)))) |
26 | 25 | abbidv 2946 |
. 2
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑋 ∈ 𝑊) → {𝑓 ∣ (𝑓 Fn {𝑋} ∧ (𝑓‘𝑋) ∈ ⦋𝑋 / 𝑥⦌(Base‘(({𝑋} × {(ringLMod‘𝑅)})‘𝑥)))} = {𝑓 ∣ (𝑓 Fn {𝑋} ∧ (𝑓‘𝑋) ∈ (Base‘𝑅))}) |
27 | 2, 26 | eqtrd 2861 |
1
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑋 ∈ 𝑊) → X𝑥 ∈ {𝑋} (Base‘(({𝑋} × {(ringLMod‘𝑅)})‘𝑥)) = {𝑓 ∣ (𝑓 Fn {𝑋} ∧ (𝑓‘𝑋) ∈ (Base‘𝑅))}) |