Proof of Theorem ixpsnbasval
Step | Hyp | Ref
| Expression |
1 | | ixpsnval 8651 |
. . 3
⊢ (𝑋 ∈ 𝑊 → X𝑥 ∈ {𝑋} (Base‘(({𝑋} × {(ringLMod‘𝑅)})‘𝑥)) = {𝑓 ∣ (𝑓 Fn {𝑋} ∧ (𝑓‘𝑋) ∈ ⦋𝑋 / 𝑥⦌(Base‘(({𝑋} × {(ringLMod‘𝑅)})‘𝑥)))}) |
2 | 1 | adantl 481 |
. 2
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑋 ∈ 𝑊) → X𝑥 ∈ {𝑋} (Base‘(({𝑋} × {(ringLMod‘𝑅)})‘𝑥)) = {𝑓 ∣ (𝑓 Fn {𝑋} ∧ (𝑓‘𝑋) ∈ ⦋𝑋 / 𝑥⦌(Base‘(({𝑋} × {(ringLMod‘𝑅)})‘𝑥)))}) |
3 | | csbfv2g 6805 |
. . . . . . . . 9
⊢ (𝑋 ∈ 𝑊 → ⦋𝑋 / 𝑥⦌(Base‘(({𝑋} × {(ringLMod‘𝑅)})‘𝑥)) = (Base‘⦋𝑋 / 𝑥⦌(({𝑋} × {(ringLMod‘𝑅)})‘𝑥))) |
4 | | csbfv2g 6805 |
. . . . . . . . . . 11
⊢ (𝑋 ∈ 𝑊 → ⦋𝑋 / 𝑥⦌(({𝑋} × {(ringLMod‘𝑅)})‘𝑥) = (({𝑋} × {(ringLMod‘𝑅)})‘⦋𝑋 / 𝑥⦌𝑥)) |
5 | | csbvarg 4367 |
. . . . . . . . . . . 12
⊢ (𝑋 ∈ 𝑊 → ⦋𝑋 / 𝑥⦌𝑥 = 𝑋) |
6 | 5 | fveq2d 6765 |
. . . . . . . . . . 11
⊢ (𝑋 ∈ 𝑊 → (({𝑋} × {(ringLMod‘𝑅)})‘⦋𝑋 / 𝑥⦌𝑥) = (({𝑋} × {(ringLMod‘𝑅)})‘𝑋)) |
7 | 4, 6 | eqtrd 2777 |
. . . . . . . . . 10
⊢ (𝑋 ∈ 𝑊 → ⦋𝑋 / 𝑥⦌(({𝑋} × {(ringLMod‘𝑅)})‘𝑥) = (({𝑋} × {(ringLMod‘𝑅)})‘𝑋)) |
8 | 7 | fveq2d 6765 |
. . . . . . . . 9
⊢ (𝑋 ∈ 𝑊 → (Base‘⦋𝑋 / 𝑥⦌(({𝑋} × {(ringLMod‘𝑅)})‘𝑥)) = (Base‘(({𝑋} × {(ringLMod‘𝑅)})‘𝑋))) |
9 | 3, 8 | eqtrd 2777 |
. . . . . . . 8
⊢ (𝑋 ∈ 𝑊 → ⦋𝑋 / 𝑥⦌(Base‘(({𝑋} × {(ringLMod‘𝑅)})‘𝑥)) = (Base‘(({𝑋} × {(ringLMod‘𝑅)})‘𝑋))) |
10 | 9 | adantl 481 |
. . . . . . 7
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑋 ∈ 𝑊) → ⦋𝑋 / 𝑥⦌(Base‘(({𝑋} × {(ringLMod‘𝑅)})‘𝑥)) = (Base‘(({𝑋} × {(ringLMod‘𝑅)})‘𝑋))) |
11 | | fvexd 6776 |
. . . . . . . . . . . 12
⊢ (𝑅 ∈ 𝑉 → (ringLMod‘𝑅) ∈ V) |
12 | 11 | anim1ci 615 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑋 ∈ 𝑊) → (𝑋 ∈ 𝑊 ∧ (ringLMod‘𝑅) ∈ V)) |
13 | | xpsng 6998 |
. . . . . . . . . . 11
⊢ ((𝑋 ∈ 𝑊 ∧ (ringLMod‘𝑅) ∈ V) → ({𝑋} × {(ringLMod‘𝑅)}) = {〈𝑋, (ringLMod‘𝑅)〉}) |
14 | 12, 13 | syl 17 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑋 ∈ 𝑊) → ({𝑋} × {(ringLMod‘𝑅)}) = {〈𝑋, (ringLMod‘𝑅)〉}) |
15 | 14 | fveq1d 6763 |
. . . . . . . . 9
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑋 ∈ 𝑊) → (({𝑋} × {(ringLMod‘𝑅)})‘𝑋) = ({〈𝑋, (ringLMod‘𝑅)〉}‘𝑋)) |
16 | | fvsng 7039 |
. . . . . . . . . 10
⊢ ((𝑋 ∈ 𝑊 ∧ (ringLMod‘𝑅) ∈ V) → ({〈𝑋, (ringLMod‘𝑅)〉}‘𝑋) = (ringLMod‘𝑅)) |
17 | 12, 16 | syl 17 |
. . . . . . . . 9
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑋 ∈ 𝑊) → ({〈𝑋, (ringLMod‘𝑅)〉}‘𝑋) = (ringLMod‘𝑅)) |
18 | 15, 17 | eqtrd 2777 |
. . . . . . . 8
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑋 ∈ 𝑊) → (({𝑋} × {(ringLMod‘𝑅)})‘𝑋) = (ringLMod‘𝑅)) |
19 | 18 | fveq2d 6765 |
. . . . . . 7
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑋 ∈ 𝑊) → (Base‘(({𝑋} × {(ringLMod‘𝑅)})‘𝑋)) = (Base‘(ringLMod‘𝑅))) |
20 | 10, 19 | eqtrd 2777 |
. . . . . 6
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑋 ∈ 𝑊) → ⦋𝑋 / 𝑥⦌(Base‘(({𝑋} × {(ringLMod‘𝑅)})‘𝑥)) = (Base‘(ringLMod‘𝑅))) |
21 | | rlmbas 20409 |
. . . . . 6
⊢
(Base‘𝑅) =
(Base‘(ringLMod‘𝑅)) |
22 | 20, 21 | eqtr4di 2795 |
. . . . 5
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑋 ∈ 𝑊) → ⦋𝑋 / 𝑥⦌(Base‘(({𝑋} × {(ringLMod‘𝑅)})‘𝑥)) = (Base‘𝑅)) |
23 | 22 | eleq2d 2822 |
. . . 4
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑋 ∈ 𝑊) → ((𝑓‘𝑋) ∈ ⦋𝑋 / 𝑥⦌(Base‘(({𝑋} × {(ringLMod‘𝑅)})‘𝑥)) ↔ (𝑓‘𝑋) ∈ (Base‘𝑅))) |
24 | 23 | anbi2d 628 |
. . 3
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑋 ∈ 𝑊) → ((𝑓 Fn {𝑋} ∧ (𝑓‘𝑋) ∈ ⦋𝑋 / 𝑥⦌(Base‘(({𝑋} × {(ringLMod‘𝑅)})‘𝑥))) ↔ (𝑓 Fn {𝑋} ∧ (𝑓‘𝑋) ∈ (Base‘𝑅)))) |
25 | 24 | abbidv 2806 |
. 2
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑋 ∈ 𝑊) → {𝑓 ∣ (𝑓 Fn {𝑋} ∧ (𝑓‘𝑋) ∈ ⦋𝑋 / 𝑥⦌(Base‘(({𝑋} × {(ringLMod‘𝑅)})‘𝑥)))} = {𝑓 ∣ (𝑓 Fn {𝑋} ∧ (𝑓‘𝑋) ∈ (Base‘𝑅))}) |
26 | 2, 25 | eqtrd 2777 |
1
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑋 ∈ 𝑊) → X𝑥 ∈ {𝑋} (Base‘(({𝑋} × {(ringLMod‘𝑅)})‘𝑥)) = {𝑓 ∣ (𝑓 Fn {𝑋} ∧ (𝑓‘𝑋) ∈ (Base‘𝑅))}) |