Proof of Theorem ixpsnbasval
Step | Hyp | Ref
| Expression |
1 | | ixpsnval 7797 |
. . 3
⊢ (𝑋 ∈ 𝑊 → X𝑥 ∈ {𝑋} (Base‘(({𝑋} × {(ringLMod‘𝑅)})‘𝑥)) = {𝑓 ∣ (𝑓 Fn {𝑋} ∧ (𝑓‘𝑋) ∈ ⦋𝑋 / 𝑥⦌(Base‘(({𝑋} × {(ringLMod‘𝑅)})‘𝑥)))}) |
2 | 1 | adantl 481 |
. 2
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑋 ∈ 𝑊) → X𝑥 ∈ {𝑋} (Base‘(({𝑋} × {(ringLMod‘𝑅)})‘𝑥)) = {𝑓 ∣ (𝑓 Fn {𝑋} ∧ (𝑓‘𝑋) ∈ ⦋𝑋 / 𝑥⦌(Base‘(({𝑋} × {(ringLMod‘𝑅)})‘𝑥)))}) |
3 | | csbfv2g 6142 |
. . . . . . . . 9
⊢ (𝑋 ∈ 𝑊 → ⦋𝑋 / 𝑥⦌(Base‘(({𝑋} × {(ringLMod‘𝑅)})‘𝑥)) = (Base‘⦋𝑋 / 𝑥⦌(({𝑋} × {(ringLMod‘𝑅)})‘𝑥))) |
4 | | csbfv2g 6142 |
. . . . . . . . . . 11
⊢ (𝑋 ∈ 𝑊 → ⦋𝑋 / 𝑥⦌(({𝑋} × {(ringLMod‘𝑅)})‘𝑥) = (({𝑋} × {(ringLMod‘𝑅)})‘⦋𝑋 / 𝑥⦌𝑥)) |
5 | | csbvarg 3955 |
. . . . . . . . . . . 12
⊢ (𝑋 ∈ 𝑊 → ⦋𝑋 / 𝑥⦌𝑥 = 𝑋) |
6 | 5 | fveq2d 6107 |
. . . . . . . . . . 11
⊢ (𝑋 ∈ 𝑊 → (({𝑋} × {(ringLMod‘𝑅)})‘⦋𝑋 / 𝑥⦌𝑥) = (({𝑋} × {(ringLMod‘𝑅)})‘𝑋)) |
7 | 4, 6 | eqtrd 2644 |
. . . . . . . . . 10
⊢ (𝑋 ∈ 𝑊 → ⦋𝑋 / 𝑥⦌(({𝑋} × {(ringLMod‘𝑅)})‘𝑥) = (({𝑋} × {(ringLMod‘𝑅)})‘𝑋)) |
8 | 7 | fveq2d 6107 |
. . . . . . . . 9
⊢ (𝑋 ∈ 𝑊 → (Base‘⦋𝑋 / 𝑥⦌(({𝑋} × {(ringLMod‘𝑅)})‘𝑥)) = (Base‘(({𝑋} × {(ringLMod‘𝑅)})‘𝑋))) |
9 | 3, 8 | eqtrd 2644 |
. . . . . . . 8
⊢ (𝑋 ∈ 𝑊 → ⦋𝑋 / 𝑥⦌(Base‘(({𝑋} × {(ringLMod‘𝑅)})‘𝑥)) = (Base‘(({𝑋} × {(ringLMod‘𝑅)})‘𝑋))) |
10 | 9 | adantl 481 |
. . . . . . 7
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑋 ∈ 𝑊) → ⦋𝑋 / 𝑥⦌(Base‘(({𝑋} × {(ringLMod‘𝑅)})‘𝑥)) = (Base‘(({𝑋} × {(ringLMod‘𝑅)})‘𝑋))) |
11 | | fvex 6113 |
. . . . . . . . . . . . . 14
⊢
(ringLMod‘𝑅)
∈ V |
12 | 11 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝑅 ∈ 𝑉 → (ringLMod‘𝑅) ∈ V) |
13 | 12 | anim1i 590 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑋 ∈ 𝑊) → ((ringLMod‘𝑅) ∈ V ∧ 𝑋 ∈ 𝑊)) |
14 | 13 | ancomd 466 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑋 ∈ 𝑊) → (𝑋 ∈ 𝑊 ∧ (ringLMod‘𝑅) ∈ V)) |
15 | | xpsng 6312 |
. . . . . . . . . . 11
⊢ ((𝑋 ∈ 𝑊 ∧ (ringLMod‘𝑅) ∈ V) → ({𝑋} × {(ringLMod‘𝑅)}) = {〈𝑋, (ringLMod‘𝑅)〉}) |
16 | 14, 15 | syl 17 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑋 ∈ 𝑊) → ({𝑋} × {(ringLMod‘𝑅)}) = {〈𝑋, (ringLMod‘𝑅)〉}) |
17 | 16 | fveq1d 6105 |
. . . . . . . . 9
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑋 ∈ 𝑊) → (({𝑋} × {(ringLMod‘𝑅)})‘𝑋) = ({〈𝑋, (ringLMod‘𝑅)〉}‘𝑋)) |
18 | | fvsng 6352 |
. . . . . . . . . 10
⊢ ((𝑋 ∈ 𝑊 ∧ (ringLMod‘𝑅) ∈ V) → ({〈𝑋, (ringLMod‘𝑅)〉}‘𝑋) = (ringLMod‘𝑅)) |
19 | 14, 18 | syl 17 |
. . . . . . . . 9
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑋 ∈ 𝑊) → ({〈𝑋, (ringLMod‘𝑅)〉}‘𝑋) = (ringLMod‘𝑅)) |
20 | 17, 19 | eqtrd 2644 |
. . . . . . . 8
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑋 ∈ 𝑊) → (({𝑋} × {(ringLMod‘𝑅)})‘𝑋) = (ringLMod‘𝑅)) |
21 | 20 | fveq2d 6107 |
. . . . . . 7
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑋 ∈ 𝑊) → (Base‘(({𝑋} × {(ringLMod‘𝑅)})‘𝑋)) = (Base‘(ringLMod‘𝑅))) |
22 | 10, 21 | eqtrd 2644 |
. . . . . 6
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑋 ∈ 𝑊) → ⦋𝑋 / 𝑥⦌(Base‘(({𝑋} × {(ringLMod‘𝑅)})‘𝑥)) = (Base‘(ringLMod‘𝑅))) |
23 | | rlmbas 19016 |
. . . . . 6
⊢
(Base‘𝑅) =
(Base‘(ringLMod‘𝑅)) |
24 | 22, 23 | syl6eqr 2662 |
. . . . 5
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑋 ∈ 𝑊) → ⦋𝑋 / 𝑥⦌(Base‘(({𝑋} × {(ringLMod‘𝑅)})‘𝑥)) = (Base‘𝑅)) |
25 | 24 | eleq2d 2673 |
. . . 4
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑋 ∈ 𝑊) → ((𝑓‘𝑋) ∈ ⦋𝑋 / 𝑥⦌(Base‘(({𝑋} × {(ringLMod‘𝑅)})‘𝑥)) ↔ (𝑓‘𝑋) ∈ (Base‘𝑅))) |
26 | 25 | anbi2d 736 |
. . 3
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑋 ∈ 𝑊) → ((𝑓 Fn {𝑋} ∧ (𝑓‘𝑋) ∈ ⦋𝑋 / 𝑥⦌(Base‘(({𝑋} × {(ringLMod‘𝑅)})‘𝑥))) ↔ (𝑓 Fn {𝑋} ∧ (𝑓‘𝑋) ∈ (Base‘𝑅)))) |
27 | 26 | abbidv 2728 |
. 2
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑋 ∈ 𝑊) → {𝑓 ∣ (𝑓 Fn {𝑋} ∧ (𝑓‘𝑋) ∈ ⦋𝑋 / 𝑥⦌(Base‘(({𝑋} × {(ringLMod‘𝑅)})‘𝑥)))} = {𝑓 ∣ (𝑓 Fn {𝑋} ∧ (𝑓‘𝑋) ∈ (Base‘𝑅))}) |
28 | 2, 27 | eqtrd 2644 |
1
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑋 ∈ 𝑊) → X𝑥 ∈ {𝑋} (Base‘(({𝑋} × {(ringLMod‘𝑅)})‘𝑥)) = {𝑓 ∣ (𝑓 Fn {𝑋} ∧ (𝑓‘𝑋) ∈ (Base‘𝑅))}) |