Step | Hyp | Ref
| Expression |
1 | | eqid 2610 |
. . 3
⊢
(Base‘(𝑆
⊕m 𝑅)) =
(Base‘(𝑆
⊕m 𝑅)) |
2 | 1 | dsmmval2 19899 |
. 2
⊢ (𝑆 ⊕m 𝑅) = ((𝑆Xs𝑅) ↾s (Base‘(𝑆 ⊕m 𝑅))) |
3 | | eqid 2610 |
. . . . . . . . . . 11
⊢ (𝑆Xs𝑅) = (𝑆Xs𝑅) |
4 | | eqid 2610 |
. . . . . . . . . . 11
⊢
(Base‘(𝑆Xs𝑅)) = (Base‘(𝑆Xs𝑅)) |
5 | | noel 3878 |
. . . . . . . . . . . . . 14
⊢ ¬
𝑓 ∈
∅ |
6 | | reldmprds 15932 |
. . . . . . . . . . . . . . . . . 18
⊢ Rel dom
Xs |
7 | 6 | ovprc1 6582 |
. . . . . . . . . . . . . . . . 17
⊢ (¬
𝑆 ∈ V → (𝑆Xs𝑅) = ∅) |
8 | 7 | fveq2d 6107 |
. . . . . . . . . . . . . . . 16
⊢ (¬
𝑆 ∈ V →
(Base‘(𝑆Xs𝑅)) = (Base‘∅)) |
9 | | base0 15740 |
. . . . . . . . . . . . . . . 16
⊢ ∅ =
(Base‘∅) |
10 | 8, 9 | syl6eqr 2662 |
. . . . . . . . . . . . . . 15
⊢ (¬
𝑆 ∈ V →
(Base‘(𝑆Xs𝑅)) = ∅) |
11 | 10 | eleq2d 2673 |
. . . . . . . . . . . . . 14
⊢ (¬
𝑆 ∈ V → (𝑓 ∈ (Base‘(𝑆Xs𝑅)) ↔ 𝑓 ∈ ∅)) |
12 | 5, 11 | mtbiri 316 |
. . . . . . . . . . . . 13
⊢ (¬
𝑆 ∈ V → ¬
𝑓 ∈ (Base‘(𝑆Xs𝑅))) |
13 | 12 | con4i 112 |
. . . . . . . . . . . 12
⊢ (𝑓 ∈ (Base‘(𝑆Xs𝑅)) → 𝑆 ∈ V) |
14 | 13 | adantl 481 |
. . . . . . . . . . 11
⊢ (((𝑅 Fn 𝐼 ∧ 𝐼 ∈ Fin) ∧ 𝑓 ∈ (Base‘(𝑆Xs𝑅))) → 𝑆 ∈ V) |
15 | | simplr 788 |
. . . . . . . . . . 11
⊢ (((𝑅 Fn 𝐼 ∧ 𝐼 ∈ Fin) ∧ 𝑓 ∈ (Base‘(𝑆Xs𝑅))) → 𝐼 ∈ Fin) |
16 | | simpll 786 |
. . . . . . . . . . 11
⊢ (((𝑅 Fn 𝐼 ∧ 𝐼 ∈ Fin) ∧ 𝑓 ∈ (Base‘(𝑆Xs𝑅))) → 𝑅 Fn 𝐼) |
17 | | simpr 476 |
. . . . . . . . . . 11
⊢ (((𝑅 Fn 𝐼 ∧ 𝐼 ∈ Fin) ∧ 𝑓 ∈ (Base‘(𝑆Xs𝑅))) → 𝑓 ∈ (Base‘(𝑆Xs𝑅))) |
18 | 3, 4, 14, 15, 16, 17 | prdsbasfn 15954 |
. . . . . . . . . 10
⊢ (((𝑅 Fn 𝐼 ∧ 𝐼 ∈ Fin) ∧ 𝑓 ∈ (Base‘(𝑆Xs𝑅))) → 𝑓 Fn 𝐼) |
19 | | fndm 5904 |
. . . . . . . . . 10
⊢ (𝑓 Fn 𝐼 → dom 𝑓 = 𝐼) |
20 | 18, 19 | syl 17 |
. . . . . . . . 9
⊢ (((𝑅 Fn 𝐼 ∧ 𝐼 ∈ Fin) ∧ 𝑓 ∈ (Base‘(𝑆Xs𝑅))) → dom 𝑓 = 𝐼) |
21 | 20, 15 | eqeltrd 2688 |
. . . . . . . 8
⊢ (((𝑅 Fn 𝐼 ∧ 𝐼 ∈ Fin) ∧ 𝑓 ∈ (Base‘(𝑆Xs𝑅))) → dom 𝑓 ∈ Fin) |
22 | | difss 3699 |
. . . . . . . . 9
⊢ (𝑓 ∖ (0g ∘
𝑅)) ⊆ 𝑓 |
23 | | dmss 5245 |
. . . . . . . . 9
⊢ ((𝑓 ∖ (0g ∘
𝑅)) ⊆ 𝑓 → dom (𝑓 ∖ (0g ∘ 𝑅)) ⊆ dom 𝑓) |
24 | 22, 23 | ax-mp 5 |
. . . . . . . 8
⊢ dom
(𝑓 ∖ (0g
∘ 𝑅)) ⊆ dom
𝑓 |
25 | | ssfi 8065 |
. . . . . . . 8
⊢ ((dom
𝑓 ∈ Fin ∧ dom
(𝑓 ∖ (0g
∘ 𝑅)) ⊆ dom
𝑓) → dom (𝑓 ∖ (0g ∘
𝑅)) ∈
Fin) |
26 | 21, 24, 25 | sylancl 693 |
. . . . . . 7
⊢ (((𝑅 Fn 𝐼 ∧ 𝐼 ∈ Fin) ∧ 𝑓 ∈ (Base‘(𝑆Xs𝑅))) → dom (𝑓 ∖ (0g ∘ 𝑅)) ∈ Fin) |
27 | 26 | ralrimiva 2949 |
. . . . . 6
⊢ ((𝑅 Fn 𝐼 ∧ 𝐼 ∈ Fin) → ∀𝑓 ∈ (Base‘(𝑆Xs𝑅))dom (𝑓 ∖ (0g ∘ 𝑅)) ∈ Fin) |
28 | | rabid2 3096 |
. . . . . 6
⊢
((Base‘(𝑆Xs𝑅)) = {𝑓 ∈ (Base‘(𝑆Xs𝑅)) ∣ dom (𝑓 ∖ (0g ∘ 𝑅)) ∈ Fin} ↔
∀𝑓 ∈
(Base‘(𝑆Xs𝑅))dom (𝑓 ∖ (0g ∘ 𝑅)) ∈ Fin) |
29 | 27, 28 | sylibr 223 |
. . . . 5
⊢ ((𝑅 Fn 𝐼 ∧ 𝐼 ∈ Fin) → (Base‘(𝑆Xs𝑅)) = {𝑓 ∈ (Base‘(𝑆Xs𝑅)) ∣ dom (𝑓 ∖ (0g ∘ 𝑅)) ∈ Fin}) |
30 | | eqid 2610 |
. . . . . 6
⊢ {𝑓 ∈ (Base‘(𝑆Xs𝑅)) ∣ dom (𝑓 ∖ (0g ∘ 𝑅)) ∈ Fin} = {𝑓 ∈ (Base‘(𝑆Xs𝑅)) ∣ dom (𝑓 ∖ (0g ∘ 𝑅)) ∈ Fin} |
31 | 3, 30 | dsmmbas2 19900 |
. . . . 5
⊢ ((𝑅 Fn 𝐼 ∧ 𝐼 ∈ Fin) → {𝑓 ∈ (Base‘(𝑆Xs𝑅)) ∣ dom (𝑓 ∖ (0g ∘ 𝑅)) ∈ Fin} =
(Base‘(𝑆
⊕m 𝑅))) |
32 | 29, 31 | eqtr2d 2645 |
. . . 4
⊢ ((𝑅 Fn 𝐼 ∧ 𝐼 ∈ Fin) → (Base‘(𝑆 ⊕m 𝑅)) = (Base‘(𝑆Xs𝑅))) |
33 | 32 | oveq2d 6565 |
. . 3
⊢ ((𝑅 Fn 𝐼 ∧ 𝐼 ∈ Fin) → ((𝑆Xs𝑅) ↾s (Base‘(𝑆 ⊕m 𝑅))) = ((𝑆Xs𝑅) ↾s (Base‘(𝑆Xs𝑅)))) |
34 | | ovex 6577 |
. . . 4
⊢ (𝑆Xs𝑅) ∈ V |
35 | 4 | ressid 15762 |
. . . 4
⊢ ((𝑆Xs𝑅) ∈ V → ((𝑆Xs𝑅) ↾s (Base‘(𝑆Xs𝑅))) = (𝑆Xs𝑅)) |
36 | 34, 35 | ax-mp 5 |
. . 3
⊢ ((𝑆Xs𝑅) ↾s (Base‘(𝑆Xs𝑅))) = (𝑆Xs𝑅) |
37 | 33, 36 | syl6eq 2660 |
. 2
⊢ ((𝑅 Fn 𝐼 ∧ 𝐼 ∈ Fin) → ((𝑆Xs𝑅) ↾s (Base‘(𝑆 ⊕m 𝑅))) = (𝑆Xs𝑅)) |
38 | 2, 37 | syl5eq 2656 |
1
⊢ ((𝑅 Fn 𝐼 ∧ 𝐼 ∈ Fin) → (𝑆 ⊕m 𝑅) = (𝑆Xs𝑅)) |