Step | Hyp | Ref
| Expression |
1 | | dsmmbas2.b |
. 2
⊢ 𝐵 = {𝑓 ∈ (Base‘𝑃) ∣ dom (𝑓 ∖ (0g ∘ 𝑅)) ∈ Fin} |
2 | | dsmmbas2.p |
. . . . . 6
⊢ 𝑃 = (𝑆Xs𝑅) |
3 | 2 | fveq2i 6106 |
. . . . 5
⊢
(Base‘𝑃) =
(Base‘(𝑆Xs𝑅)) |
4 | | rabeq 3166 |
. . . . 5
⊢
((Base‘𝑃) =
(Base‘(𝑆Xs𝑅)) → {𝑓 ∈ (Base‘𝑃) ∣ dom (𝑓 ∖ (0g ∘ 𝑅)) ∈ Fin} = {𝑓 ∈ (Base‘(𝑆Xs𝑅)) ∣ dom (𝑓 ∖ (0g ∘ 𝑅)) ∈ Fin}) |
5 | 3, 4 | ax-mp 5 |
. . . 4
⊢ {𝑓 ∈ (Base‘𝑃) ∣ dom (𝑓 ∖ (0g ∘
𝑅)) ∈ Fin} = {𝑓 ∈ (Base‘(𝑆Xs𝑅)) ∣ dom (𝑓 ∖ (0g ∘ 𝑅)) ∈ Fin} |
6 | | simpll 786 |
. . . . . . . . . 10
⊢ (((𝑅 Fn 𝐼 ∧ 𝐼 ∈ 𝑉) ∧ 𝑓 ∈ (Base‘(𝑆Xs𝑅))) → 𝑅 Fn 𝐼) |
7 | | fvco2 6183 |
. . . . . . . . . 10
⊢ ((𝑅 Fn 𝐼 ∧ 𝑥 ∈ 𝐼) → ((0g ∘ 𝑅)‘𝑥) = (0g‘(𝑅‘𝑥))) |
8 | 6, 7 | sylan 487 |
. . . . . . . . 9
⊢ ((((𝑅 Fn 𝐼 ∧ 𝐼 ∈ 𝑉) ∧ 𝑓 ∈ (Base‘(𝑆Xs𝑅))) ∧ 𝑥 ∈ 𝐼) → ((0g ∘ 𝑅)‘𝑥) = (0g‘(𝑅‘𝑥))) |
9 | 8 | neeq2d 2842 |
. . . . . . . 8
⊢ ((((𝑅 Fn 𝐼 ∧ 𝐼 ∈ 𝑉) ∧ 𝑓 ∈ (Base‘(𝑆Xs𝑅))) ∧ 𝑥 ∈ 𝐼) → ((𝑓‘𝑥) ≠ ((0g ∘ 𝑅)‘𝑥) ↔ (𝑓‘𝑥) ≠ (0g‘(𝑅‘𝑥)))) |
10 | 9 | rabbidva 3163 |
. . . . . . 7
⊢ (((𝑅 Fn 𝐼 ∧ 𝐼 ∈ 𝑉) ∧ 𝑓 ∈ (Base‘(𝑆Xs𝑅))) → {𝑥 ∈ 𝐼 ∣ (𝑓‘𝑥) ≠ ((0g ∘ 𝑅)‘𝑥)} = {𝑥 ∈ 𝐼 ∣ (𝑓‘𝑥) ≠ (0g‘(𝑅‘𝑥))}) |
11 | | eqid 2610 |
. . . . . . . . 9
⊢ (𝑆Xs𝑅) = (𝑆Xs𝑅) |
12 | | eqid 2610 |
. . . . . . . . 9
⊢
(Base‘(𝑆Xs𝑅)) = (Base‘(𝑆Xs𝑅)) |
13 | | noel 3878 |
. . . . . . . . . . . 12
⊢ ¬
𝑓 ∈
∅ |
14 | | reldmprds 15932 |
. . . . . . . . . . . . . . . 16
⊢ Rel dom
Xs |
15 | 14 | ovprc1 6582 |
. . . . . . . . . . . . . . 15
⊢ (¬
𝑆 ∈ V → (𝑆Xs𝑅) = ∅) |
16 | 15 | fveq2d 6107 |
. . . . . . . . . . . . . 14
⊢ (¬
𝑆 ∈ V →
(Base‘(𝑆Xs𝑅)) = (Base‘∅)) |
17 | | base0 15740 |
. . . . . . . . . . . . . 14
⊢ ∅ =
(Base‘∅) |
18 | 16, 17 | syl6eqr 2662 |
. . . . . . . . . . . . 13
⊢ (¬
𝑆 ∈ V →
(Base‘(𝑆Xs𝑅)) = ∅) |
19 | 18 | eleq2d 2673 |
. . . . . . . . . . . 12
⊢ (¬
𝑆 ∈ V → (𝑓 ∈ (Base‘(𝑆Xs𝑅)) ↔ 𝑓 ∈ ∅)) |
20 | 13, 19 | mtbiri 316 |
. . . . . . . . . . 11
⊢ (¬
𝑆 ∈ V → ¬
𝑓 ∈ (Base‘(𝑆Xs𝑅))) |
21 | 20 | con4i 112 |
. . . . . . . . . 10
⊢ (𝑓 ∈ (Base‘(𝑆Xs𝑅)) → 𝑆 ∈ V) |
22 | 21 | adantl 481 |
. . . . . . . . 9
⊢ (((𝑅 Fn 𝐼 ∧ 𝐼 ∈ 𝑉) ∧ 𝑓 ∈ (Base‘(𝑆Xs𝑅))) → 𝑆 ∈ V) |
23 | | simplr 788 |
. . . . . . . . 9
⊢ (((𝑅 Fn 𝐼 ∧ 𝐼 ∈ 𝑉) ∧ 𝑓 ∈ (Base‘(𝑆Xs𝑅))) → 𝐼 ∈ 𝑉) |
24 | | simpr 476 |
. . . . . . . . 9
⊢ (((𝑅 Fn 𝐼 ∧ 𝐼 ∈ 𝑉) ∧ 𝑓 ∈ (Base‘(𝑆Xs𝑅))) → 𝑓 ∈ (Base‘(𝑆Xs𝑅))) |
25 | 11, 12, 22, 23, 6, 24 | prdsbasfn 15954 |
. . . . . . . 8
⊢ (((𝑅 Fn 𝐼 ∧ 𝐼 ∈ 𝑉) ∧ 𝑓 ∈ (Base‘(𝑆Xs𝑅))) → 𝑓 Fn 𝐼) |
26 | | fn0g 17085 |
. . . . . . . . . . . 12
⊢
0g Fn V |
27 | | dffn2 5960 |
. . . . . . . . . . . 12
⊢
(0g Fn V ↔ 0g:V⟶V) |
28 | 26, 27 | mpbi 219 |
. . . . . . . . . . 11
⊢
0g:V⟶V |
29 | | dffn2 5960 |
. . . . . . . . . . . 12
⊢ (𝑅 Fn 𝐼 ↔ 𝑅:𝐼⟶V) |
30 | 29 | biimpi 205 |
. . . . . . . . . . 11
⊢ (𝑅 Fn 𝐼 → 𝑅:𝐼⟶V) |
31 | | fco 5971 |
. . . . . . . . . . 11
⊢
((0g:V⟶V ∧ 𝑅:𝐼⟶V) → (0g ∘
𝑅):𝐼⟶V) |
32 | 28, 30, 31 | sylancr 694 |
. . . . . . . . . 10
⊢ (𝑅 Fn 𝐼 → (0g ∘ 𝑅):𝐼⟶V) |
33 | | ffn 5958 |
. . . . . . . . . 10
⊢
((0g ∘ 𝑅):𝐼⟶V → (0g ∘
𝑅) Fn 𝐼) |
34 | 32, 33 | syl 17 |
. . . . . . . . 9
⊢ (𝑅 Fn 𝐼 → (0g ∘ 𝑅) Fn 𝐼) |
35 | 34 | ad2antrr 758 |
. . . . . . . 8
⊢ (((𝑅 Fn 𝐼 ∧ 𝐼 ∈ 𝑉) ∧ 𝑓 ∈ (Base‘(𝑆Xs𝑅))) → (0g ∘ 𝑅) Fn 𝐼) |
36 | | fndmdif 6229 |
. . . . . . . 8
⊢ ((𝑓 Fn 𝐼 ∧ (0g ∘ 𝑅) Fn 𝐼) → dom (𝑓 ∖ (0g ∘ 𝑅)) = {𝑥 ∈ 𝐼 ∣ (𝑓‘𝑥) ≠ ((0g ∘ 𝑅)‘𝑥)}) |
37 | 25, 35, 36 | syl2anc 691 |
. . . . . . 7
⊢ (((𝑅 Fn 𝐼 ∧ 𝐼 ∈ 𝑉) ∧ 𝑓 ∈ (Base‘(𝑆Xs𝑅))) → dom (𝑓 ∖ (0g ∘ 𝑅)) = {𝑥 ∈ 𝐼 ∣ (𝑓‘𝑥) ≠ ((0g ∘ 𝑅)‘𝑥)}) |
38 | | fndm 5904 |
. . . . . . . . 9
⊢ (𝑅 Fn 𝐼 → dom 𝑅 = 𝐼) |
39 | | rabeq 3166 |
. . . . . . . . 9
⊢ (dom
𝑅 = 𝐼 → {𝑥 ∈ dom 𝑅 ∣ (𝑓‘𝑥) ≠ (0g‘(𝑅‘𝑥))} = {𝑥 ∈ 𝐼 ∣ (𝑓‘𝑥) ≠ (0g‘(𝑅‘𝑥))}) |
40 | 38, 39 | syl 17 |
. . . . . . . 8
⊢ (𝑅 Fn 𝐼 → {𝑥 ∈ dom 𝑅 ∣ (𝑓‘𝑥) ≠ (0g‘(𝑅‘𝑥))} = {𝑥 ∈ 𝐼 ∣ (𝑓‘𝑥) ≠ (0g‘(𝑅‘𝑥))}) |
41 | 40 | ad2antrr 758 |
. . . . . . 7
⊢ (((𝑅 Fn 𝐼 ∧ 𝐼 ∈ 𝑉) ∧ 𝑓 ∈ (Base‘(𝑆Xs𝑅))) → {𝑥 ∈ dom 𝑅 ∣ (𝑓‘𝑥) ≠ (0g‘(𝑅‘𝑥))} = {𝑥 ∈ 𝐼 ∣ (𝑓‘𝑥) ≠ (0g‘(𝑅‘𝑥))}) |
42 | 10, 37, 41 | 3eqtr4d 2654 |
. . . . . 6
⊢ (((𝑅 Fn 𝐼 ∧ 𝐼 ∈ 𝑉) ∧ 𝑓 ∈ (Base‘(𝑆Xs𝑅))) → dom (𝑓 ∖ (0g ∘ 𝑅)) = {𝑥 ∈ dom 𝑅 ∣ (𝑓‘𝑥) ≠ (0g‘(𝑅‘𝑥))}) |
43 | 42 | eleq1d 2672 |
. . . . 5
⊢ (((𝑅 Fn 𝐼 ∧ 𝐼 ∈ 𝑉) ∧ 𝑓 ∈ (Base‘(𝑆Xs𝑅))) → (dom (𝑓 ∖ (0g ∘ 𝑅)) ∈ Fin ↔ {𝑥 ∈ dom 𝑅 ∣ (𝑓‘𝑥) ≠ (0g‘(𝑅‘𝑥))} ∈ Fin)) |
44 | 43 | rabbidva 3163 |
. . . 4
⊢ ((𝑅 Fn 𝐼 ∧ 𝐼 ∈ 𝑉) → {𝑓 ∈ (Base‘(𝑆Xs𝑅)) ∣ dom (𝑓 ∖ (0g ∘ 𝑅)) ∈ Fin} = {𝑓 ∈ (Base‘(𝑆Xs𝑅)) ∣ {𝑥 ∈ dom 𝑅 ∣ (𝑓‘𝑥) ≠ (0g‘(𝑅‘𝑥))} ∈ Fin}) |
45 | 5, 44 | syl5eq 2656 |
. . 3
⊢ ((𝑅 Fn 𝐼 ∧ 𝐼 ∈ 𝑉) → {𝑓 ∈ (Base‘𝑃) ∣ dom (𝑓 ∖ (0g ∘ 𝑅)) ∈ Fin} = {𝑓 ∈ (Base‘(𝑆Xs𝑅)) ∣ {𝑥 ∈ dom 𝑅 ∣ (𝑓‘𝑥) ≠ (0g‘(𝑅‘𝑥))} ∈ Fin}) |
46 | | fnex 6386 |
. . . 4
⊢ ((𝑅 Fn 𝐼 ∧ 𝐼 ∈ 𝑉) → 𝑅 ∈ V) |
47 | | eqid 2610 |
. . . . 5
⊢ {𝑓 ∈ (Base‘(𝑆Xs𝑅)) ∣ {𝑥 ∈ dom 𝑅 ∣ (𝑓‘𝑥) ≠ (0g‘(𝑅‘𝑥))} ∈ Fin} = {𝑓 ∈ (Base‘(𝑆Xs𝑅)) ∣ {𝑥 ∈ dom 𝑅 ∣ (𝑓‘𝑥) ≠ (0g‘(𝑅‘𝑥))} ∈ Fin} |
48 | 47 | dsmmbase 19898 |
. . . 4
⊢ (𝑅 ∈ V → {𝑓 ∈ (Base‘(𝑆Xs𝑅)) ∣ {𝑥 ∈ dom 𝑅 ∣ (𝑓‘𝑥) ≠ (0g‘(𝑅‘𝑥))} ∈ Fin} = (Base‘(𝑆 ⊕m 𝑅))) |
49 | 46, 48 | syl 17 |
. . 3
⊢ ((𝑅 Fn 𝐼 ∧ 𝐼 ∈ 𝑉) → {𝑓 ∈ (Base‘(𝑆Xs𝑅)) ∣ {𝑥 ∈ dom 𝑅 ∣ (𝑓‘𝑥) ≠ (0g‘(𝑅‘𝑥))} ∈ Fin} = (Base‘(𝑆 ⊕m 𝑅))) |
50 | 45, 49 | eqtrd 2644 |
. 2
⊢ ((𝑅 Fn 𝐼 ∧ 𝐼 ∈ 𝑉) → {𝑓 ∈ (Base‘𝑃) ∣ dom (𝑓 ∖ (0g ∘ 𝑅)) ∈ Fin} =
(Base‘(𝑆
⊕m 𝑅))) |
51 | 1, 50 | syl5eq 2656 |
1
⊢ ((𝑅 Fn 𝐼 ∧ 𝐼 ∈ 𝑉) → 𝐵 = (Base‘(𝑆 ⊕m 𝑅))) |