Step | Hyp | Ref
| Expression |
1 | | df-negs 27323 |
. . 3
⊢
-us = norec ((𝑥
∈ V, 𝑛 ∈ V
↦ ((𝑛 “ ( R
‘𝑥)) |s (𝑛 “ ( L ‘𝑥))))) |
2 | 1 | norecov 27262 |
. 2
⊢ (𝐴 ∈
No → ( -us ‘𝐴) = (𝐴(𝑥 ∈ V, 𝑛 ∈ V ↦ ((𝑛 “ ( R ‘𝑥)) |s (𝑛 “ ( L ‘𝑥))))( -us ↾ (( L
‘𝐴) ∪ ( R
‘𝐴))))) |
3 | | elex 3464 |
. . 3
⊢ (𝐴 ∈
No → 𝐴 ∈
V) |
4 | | negsfn 27325 |
. . . . . 6
⊢
-us Fn No |
5 | | fnfun 6603 |
. . . . . 6
⊢ (
-us Fn No → Fun -us
) |
6 | 4, 5 | ax-mp 5 |
. . . . 5
⊢ Fun
-us |
7 | | fvex 6856 |
. . . . . 6
⊢ ( L
‘𝐴) ∈
V |
8 | | fvex 6856 |
. . . . . 6
⊢ ( R
‘𝐴) ∈
V |
9 | 7, 8 | unex 7681 |
. . . . 5
⊢ (( L
‘𝐴) ∪ ( R
‘𝐴)) ∈
V |
10 | | resfunexg 7166 |
. . . . 5
⊢ ((Fun
-us ∧ (( L ‘𝐴) ∪ ( R ‘𝐴)) ∈ V) → ( -us ↾
(( L ‘𝐴) ∪ ( R
‘𝐴))) ∈
V) |
11 | 6, 9, 10 | mp2an 691 |
. . . 4
⊢ (
-us ↾ (( L ‘𝐴) ∪ ( R ‘𝐴))) ∈ V |
12 | 11 | a1i 11 |
. . 3
⊢ (𝐴 ∈
No → ( -us ↾ (( L ‘𝐴) ∪ ( R ‘𝐴))) ∈ V) |
13 | | ovexd 7393 |
. . 3
⊢ (𝐴 ∈
No → ((( -us ↾ (( L ‘𝐴) ∪ ( R ‘𝐴))) “ ( R ‘𝐴)) |s (( -us ↾ (( L
‘𝐴) ∪ ( R
‘𝐴))) “ ( L
‘𝐴))) ∈
V) |
14 | | fveq2 6843 |
. . . . . 6
⊢ (𝑥 = 𝐴 → ( R ‘𝑥) = ( R ‘𝐴)) |
15 | 14 | imaeq2d 6014 |
. . . . 5
⊢ (𝑥 = 𝐴 → (𝑛 “ ( R ‘𝑥)) = (𝑛 “ ( R ‘𝐴))) |
16 | | fveq2 6843 |
. . . . . 6
⊢ (𝑥 = 𝐴 → ( L ‘𝑥) = ( L ‘𝐴)) |
17 | 16 | imaeq2d 6014 |
. . . . 5
⊢ (𝑥 = 𝐴 → (𝑛 “ ( L ‘𝑥)) = (𝑛 “ ( L ‘𝐴))) |
18 | 15, 17 | oveq12d 7376 |
. . . 4
⊢ (𝑥 = 𝐴 → ((𝑛 “ ( R ‘𝑥)) |s (𝑛 “ ( L ‘𝑥))) = ((𝑛 “ ( R ‘𝐴)) |s (𝑛 “ ( L ‘𝐴)))) |
19 | | imaeq1 6009 |
. . . . 5
⊢ (𝑛 = ( -us ↾ (( L
‘𝐴) ∪ ( R
‘𝐴))) → (𝑛 “ ( R ‘𝐴)) = (( -us ↾
(( L ‘𝐴) ∪ ( R
‘𝐴))) “ ( R
‘𝐴))) |
20 | | imaeq1 6009 |
. . . . 5
⊢ (𝑛 = ( -us ↾ (( L
‘𝐴) ∪ ( R
‘𝐴))) → (𝑛 “ ( L ‘𝐴)) = (( -us ↾
(( L ‘𝐴) ∪ ( R
‘𝐴))) “ ( L
‘𝐴))) |
21 | 19, 20 | oveq12d 7376 |
. . . 4
⊢ (𝑛 = ( -us ↾ (( L
‘𝐴) ∪ ( R
‘𝐴))) → ((𝑛 “ ( R ‘𝐴)) |s (𝑛 “ ( L ‘𝐴))) = ((( -us ↾ (( L
‘𝐴) ∪ ( R
‘𝐴))) “ ( R
‘𝐴)) |s ((
-us ↾ (( L ‘𝐴) ∪ ( R ‘𝐴))) “ ( L ‘𝐴)))) |
22 | | eqid 2737 |
. . . 4
⊢ (𝑥 ∈ V, 𝑛 ∈ V ↦ ((𝑛 “ ( R ‘𝑥)) |s (𝑛 “ ( L ‘𝑥)))) = (𝑥 ∈ V, 𝑛 ∈ V ↦ ((𝑛 “ ( R ‘𝑥)) |s (𝑛 “ ( L ‘𝑥)))) |
23 | 18, 21, 22 | ovmpog 7515 |
. . 3
⊢ ((𝐴 ∈ V ∧ ( -us
↾ (( L ‘𝐴)
∪ ( R ‘𝐴)))
∈ V ∧ ((( -us ↾ (( L ‘𝐴) ∪ ( R ‘𝐴))) “ ( R ‘𝐴)) |s (( -us ↾ (( L
‘𝐴) ∪ ( R
‘𝐴))) “ ( L
‘𝐴))) ∈ V)
→ (𝐴(𝑥 ∈ V, 𝑛 ∈ V ↦ ((𝑛 “ ( R ‘𝑥)) |s (𝑛 “ ( L ‘𝑥))))( -us ↾ (( L
‘𝐴) ∪ ( R
‘𝐴)))) = (((
-us ↾ (( L ‘𝐴) ∪ ( R ‘𝐴))) “ ( R ‘𝐴)) |s (( -us ↾ (( L
‘𝐴) ∪ ( R
‘𝐴))) “ ( L
‘𝐴)))) |
24 | 3, 12, 13, 23 | syl3anc 1372 |
. 2
⊢ (𝐴 ∈
No → (𝐴(𝑥 ∈ V, 𝑛 ∈ V ↦ ((𝑛 “ ( R ‘𝑥)) |s (𝑛 “ ( L ‘𝑥))))( -us ↾ (( L
‘𝐴) ∪ ( R
‘𝐴)))) = (((
-us ↾ (( L ‘𝐴) ∪ ( R ‘𝐴))) “ ( R ‘𝐴)) |s (( -us ↾ (( L
‘𝐴) ∪ ( R
‘𝐴))) “ ( L
‘𝐴)))) |
25 | | ssun2 4134 |
. . . . 5
⊢ ( R
‘𝐴) ⊆ (( L
‘𝐴) ∪ ( R
‘𝐴)) |
26 | | resima2 5973 |
. . . . 5
⊢ (( R
‘𝐴) ⊆ (( L
‘𝐴) ∪ ( R
‘𝐴)) → ((
-us ↾ (( L ‘𝐴) ∪ ( R ‘𝐴))) “ ( R ‘𝐴)) = ( -us “ ( R
‘𝐴))) |
27 | 25, 26 | ax-mp 5 |
. . . 4
⊢ ((
-us ↾ (( L ‘𝐴) ∪ ( R ‘𝐴))) “ ( R ‘𝐴)) = ( -us “ ( R
‘𝐴)) |
28 | | ssun1 4133 |
. . . . 5
⊢ ( L
‘𝐴) ⊆ (( L
‘𝐴) ∪ ( R
‘𝐴)) |
29 | | resima2 5973 |
. . . . 5
⊢ (( L
‘𝐴) ⊆ (( L
‘𝐴) ∪ ( R
‘𝐴)) → ((
-us ↾ (( L ‘𝐴) ∪ ( R ‘𝐴))) “ ( L ‘𝐴)) = ( -us “ ( L
‘𝐴))) |
30 | 28, 29 | ax-mp 5 |
. . . 4
⊢ ((
-us ↾ (( L ‘𝐴) ∪ ( R ‘𝐴))) “ ( L ‘𝐴)) = ( -us “ ( L
‘𝐴)) |
31 | 27, 30 | oveq12i 7370 |
. . 3
⊢ (((
-us ↾ (( L ‘𝐴) ∪ ( R ‘𝐴))) “ ( R ‘𝐴)) |s (( -us ↾ (( L
‘𝐴) ∪ ( R
‘𝐴))) “ ( L
‘𝐴))) = ((
-us “ ( R ‘𝐴)) |s ( -us “ ( L
‘𝐴))) |
32 | 31 | a1i 11 |
. 2
⊢ (𝐴 ∈
No → ((( -us ↾ (( L ‘𝐴) ∪ ( R ‘𝐴))) “ ( R ‘𝐴)) |s (( -us ↾ (( L
‘𝐴) ∪ ( R
‘𝐴))) “ ( L
‘𝐴))) = ((
-us “ ( R ‘𝐴)) |s ( -us “ ( L
‘𝐴)))) |
33 | 2, 24, 32 | 3eqtrd 2781 |
1
⊢ (𝐴 ∈
No → ( -us ‘𝐴) = (( -us “ ( R
‘𝐴)) |s (
-us “ ( L ‘𝐴)))) |