Proof of Theorem mapdhval
Step | Hyp | Ref
| Expression |
1 | | otex 4933 |
. . 3
⊢
〈𝑋, 𝐹, 𝑌〉 ∈ V |
2 | | fveq2 6191 |
. . . . . 6
⊢ (𝑥 = 〈𝑋, 𝐹, 𝑌〉 → (2nd ‘𝑥) = (2nd
‘〈𝑋, 𝐹, 𝑌〉)) |
3 | 2 | eqeq1d 2624 |
. . . . 5
⊢ (𝑥 = 〈𝑋, 𝐹, 𝑌〉 → ((2nd ‘𝑥) = 0 ↔ (2nd
‘〈𝑋, 𝐹, 𝑌〉) = 0 )) |
4 | 2 | sneqd 4189 |
. . . . . . . . . 10
⊢ (𝑥 = 〈𝑋, 𝐹, 𝑌〉 → {(2nd ‘𝑥)} = {(2nd
‘〈𝑋, 𝐹, 𝑌〉)}) |
5 | 4 | fveq2d 6195 |
. . . . . . . . 9
⊢ (𝑥 = 〈𝑋, 𝐹, 𝑌〉 → (𝑁‘{(2nd ‘𝑥)}) = (𝑁‘{(2nd ‘〈𝑋, 𝐹, 𝑌〉)})) |
6 | 5 | fveq2d 6195 |
. . . . . . . 8
⊢ (𝑥 = 〈𝑋, 𝐹, 𝑌〉 → (𝑀‘(𝑁‘{(2nd ‘𝑥)})) = (𝑀‘(𝑁‘{(2nd ‘〈𝑋, 𝐹, 𝑌〉)}))) |
7 | 6 | eqeq1d 2624 |
. . . . . . 7
⊢ (𝑥 = 〈𝑋, 𝐹, 𝑌〉 → ((𝑀‘(𝑁‘{(2nd ‘𝑥)})) = (𝐽‘{ℎ}) ↔ (𝑀‘(𝑁‘{(2nd ‘〈𝑋, 𝐹, 𝑌〉)})) = (𝐽‘{ℎ}))) |
8 | | fveq2 6191 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 〈𝑋, 𝐹, 𝑌〉 → (1st ‘𝑥) = (1st
‘〈𝑋, 𝐹, 𝑌〉)) |
9 | 8 | fveq2d 6195 |
. . . . . . . . . . . 12
⊢ (𝑥 = 〈𝑋, 𝐹, 𝑌〉 → (1st
‘(1st ‘𝑥)) = (1st ‘(1st
‘〈𝑋, 𝐹, 𝑌〉))) |
10 | 9, 2 | oveq12d 6668 |
. . . . . . . . . . 11
⊢ (𝑥 = 〈𝑋, 𝐹, 𝑌〉 → ((1st
‘(1st ‘𝑥)) − (2nd
‘𝑥)) =
((1st ‘(1st ‘〈𝑋, 𝐹, 𝑌〉)) − (2nd
‘〈𝑋, 𝐹, 𝑌〉))) |
11 | 10 | sneqd 4189 |
. . . . . . . . . 10
⊢ (𝑥 = 〈𝑋, 𝐹, 𝑌〉 → {((1st
‘(1st ‘𝑥)) − (2nd
‘𝑥))} =
{((1st ‘(1st ‘〈𝑋, 𝐹, 𝑌〉)) − (2nd
‘〈𝑋, 𝐹, 𝑌〉))}) |
12 | 11 | fveq2d 6195 |
. . . . . . . . 9
⊢ (𝑥 = 〈𝑋, 𝐹, 𝑌〉 → (𝑁‘{((1st
‘(1st ‘𝑥)) − (2nd
‘𝑥))}) = (𝑁‘{((1st
‘(1st ‘〈𝑋, 𝐹, 𝑌〉)) − (2nd
‘〈𝑋, 𝐹, 𝑌〉))})) |
13 | 12 | fveq2d 6195 |
. . . . . . . 8
⊢ (𝑥 = 〈𝑋, 𝐹, 𝑌〉 → (𝑀‘(𝑁‘{((1st
‘(1st ‘𝑥)) − (2nd
‘𝑥))})) = (𝑀‘(𝑁‘{((1st
‘(1st ‘〈𝑋, 𝐹, 𝑌〉)) − (2nd
‘〈𝑋, 𝐹, 𝑌〉))}))) |
14 | 8 | fveq2d 6195 |
. . . . . . . . . . 11
⊢ (𝑥 = 〈𝑋, 𝐹, 𝑌〉 → (2nd
‘(1st ‘𝑥)) = (2nd ‘(1st
‘〈𝑋, 𝐹, 𝑌〉))) |
15 | 14 | oveq1d 6665 |
. . . . . . . . . 10
⊢ (𝑥 = 〈𝑋, 𝐹, 𝑌〉 → ((2nd
‘(1st ‘𝑥))𝑅ℎ) = ((2nd ‘(1st
‘〈𝑋, 𝐹, 𝑌〉))𝑅ℎ)) |
16 | 15 | sneqd 4189 |
. . . . . . . . 9
⊢ (𝑥 = 〈𝑋, 𝐹, 𝑌〉 → {((2nd
‘(1st ‘𝑥))𝑅ℎ)} = {((2nd ‘(1st
‘〈𝑋, 𝐹, 𝑌〉))𝑅ℎ)}) |
17 | 16 | fveq2d 6195 |
. . . . . . . 8
⊢ (𝑥 = 〈𝑋, 𝐹, 𝑌〉 → (𝐽‘{((2nd
‘(1st ‘𝑥))𝑅ℎ)}) = (𝐽‘{((2nd
‘(1st ‘〈𝑋, 𝐹, 𝑌〉))𝑅ℎ)})) |
18 | 13, 17 | eqeq12d 2637 |
. . . . . . 7
⊢ (𝑥 = 〈𝑋, 𝐹, 𝑌〉 → ((𝑀‘(𝑁‘{((1st
‘(1st ‘𝑥)) − (2nd
‘𝑥))})) = (𝐽‘{((2nd
‘(1st ‘𝑥))𝑅ℎ)}) ↔ (𝑀‘(𝑁‘{((1st
‘(1st ‘〈𝑋, 𝐹, 𝑌〉)) − (2nd
‘〈𝑋, 𝐹, 𝑌〉))})) = (𝐽‘{((2nd
‘(1st ‘〈𝑋, 𝐹, 𝑌〉))𝑅ℎ)}))) |
19 | 7, 18 | anbi12d 747 |
. . . . . 6
⊢ (𝑥 = 〈𝑋, 𝐹, 𝑌〉 → (((𝑀‘(𝑁‘{(2nd ‘𝑥)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1st
‘(1st ‘𝑥)) − (2nd
‘𝑥))})) = (𝐽‘{((2nd
‘(1st ‘𝑥))𝑅ℎ)})) ↔ ((𝑀‘(𝑁‘{(2nd ‘〈𝑋, 𝐹, 𝑌〉)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1st
‘(1st ‘〈𝑋, 𝐹, 𝑌〉)) − (2nd
‘〈𝑋, 𝐹, 𝑌〉))})) = (𝐽‘{((2nd
‘(1st ‘〈𝑋, 𝐹, 𝑌〉))𝑅ℎ)})))) |
20 | 19 | riotabidv 6613 |
. . . . 5
⊢ (𝑥 = 〈𝑋, 𝐹, 𝑌〉 → (℩ℎ ∈ 𝐷 ((𝑀‘(𝑁‘{(2nd ‘𝑥)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1st
‘(1st ‘𝑥)) − (2nd
‘𝑥))})) = (𝐽‘{((2nd
‘(1st ‘𝑥))𝑅ℎ)}))) = (℩ℎ ∈ 𝐷 ((𝑀‘(𝑁‘{(2nd ‘〈𝑋, 𝐹, 𝑌〉)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1st
‘(1st ‘〈𝑋, 𝐹, 𝑌〉)) − (2nd
‘〈𝑋, 𝐹, 𝑌〉))})) = (𝐽‘{((2nd
‘(1st ‘〈𝑋, 𝐹, 𝑌〉))𝑅ℎ)})))) |
21 | 3, 20 | ifbieq2d 4111 |
. . . 4
⊢ (𝑥 = 〈𝑋, 𝐹, 𝑌〉 → if((2nd
‘𝑥) = 0 , 𝑄, (℩ℎ ∈ 𝐷 ((𝑀‘(𝑁‘{(2nd ‘𝑥)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1st
‘(1st ‘𝑥)) − (2nd
‘𝑥))})) = (𝐽‘{((2nd
‘(1st ‘𝑥))𝑅ℎ)})))) = if((2nd ‘〈𝑋, 𝐹, 𝑌〉) = 0 , 𝑄, (℩ℎ ∈ 𝐷 ((𝑀‘(𝑁‘{(2nd ‘〈𝑋, 𝐹, 𝑌〉)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1st
‘(1st ‘〈𝑋, 𝐹, 𝑌〉)) − (2nd
‘〈𝑋, 𝐹, 𝑌〉))})) = (𝐽‘{((2nd
‘(1st ‘〈𝑋, 𝐹, 𝑌〉))𝑅ℎ)}))))) |
22 | | mapdh.i |
. . . 4
⊢ 𝐼 = (𝑥 ∈ V ↦ if((2nd
‘𝑥) = 0 , 𝑄, (℩ℎ ∈ 𝐷 ((𝑀‘(𝑁‘{(2nd ‘𝑥)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1st
‘(1st ‘𝑥)) − (2nd
‘𝑥))})) = (𝐽‘{((2nd
‘(1st ‘𝑥))𝑅ℎ)}))))) |
23 | | mapdh.q |
. . . . . 6
⊢ 𝑄 = (0g‘𝐶) |
24 | | fvex 6201 |
. . . . . 6
⊢
(0g‘𝐶) ∈ V |
25 | 23, 24 | eqeltri 2697 |
. . . . 5
⊢ 𝑄 ∈ V |
26 | | riotaex 6615 |
. . . . 5
⊢
(℩ℎ
∈ 𝐷 ((𝑀‘(𝑁‘{(2nd ‘〈𝑋, 𝐹, 𝑌〉)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1st
‘(1st ‘〈𝑋, 𝐹, 𝑌〉)) − (2nd
‘〈𝑋, 𝐹, 𝑌〉))})) = (𝐽‘{((2nd
‘(1st ‘〈𝑋, 𝐹, 𝑌〉))𝑅ℎ)}))) ∈ V |
27 | 25, 26 | ifex 4156 |
. . . 4
⊢
if((2nd ‘〈𝑋, 𝐹, 𝑌〉) = 0 , 𝑄, (℩ℎ ∈ 𝐷 ((𝑀‘(𝑁‘{(2nd ‘〈𝑋, 𝐹, 𝑌〉)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1st
‘(1st ‘〈𝑋, 𝐹, 𝑌〉)) − (2nd
‘〈𝑋, 𝐹, 𝑌〉))})) = (𝐽‘{((2nd
‘(1st ‘〈𝑋, 𝐹, 𝑌〉))𝑅ℎ)})))) ∈ V |
28 | 21, 22, 27 | fvmpt 6282 |
. . 3
⊢
(〈𝑋, 𝐹, 𝑌〉 ∈ V → (𝐼‘〈𝑋, 𝐹, 𝑌〉) = if((2nd
‘〈𝑋, 𝐹, 𝑌〉) = 0 , 𝑄, (℩ℎ ∈ 𝐷 ((𝑀‘(𝑁‘{(2nd ‘〈𝑋, 𝐹, 𝑌〉)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1st
‘(1st ‘〈𝑋, 𝐹, 𝑌〉)) − (2nd
‘〈𝑋, 𝐹, 𝑌〉))})) = (𝐽‘{((2nd
‘(1st ‘〈𝑋, 𝐹, 𝑌〉))𝑅ℎ)}))))) |
29 | 1, 28 | mp1i 13 |
. 2
⊢ (𝜑 → (𝐼‘〈𝑋, 𝐹, 𝑌〉) = if((2nd
‘〈𝑋, 𝐹, 𝑌〉) = 0 , 𝑄, (℩ℎ ∈ 𝐷 ((𝑀‘(𝑁‘{(2nd ‘〈𝑋, 𝐹, 𝑌〉)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1st
‘(1st ‘〈𝑋, 𝐹, 𝑌〉)) − (2nd
‘〈𝑋, 𝐹, 𝑌〉))})) = (𝐽‘{((2nd
‘(1st ‘〈𝑋, 𝐹, 𝑌〉))𝑅ℎ)}))))) |
30 | | mapdh.y |
. . . . 5
⊢ (𝜑 → 𝑌 ∈ 𝐸) |
31 | | ot3rdg 7184 |
. . . . 5
⊢ (𝑌 ∈ 𝐸 → (2nd ‘〈𝑋, 𝐹, 𝑌〉) = 𝑌) |
32 | 30, 31 | syl 17 |
. . . 4
⊢ (𝜑 → (2nd
‘〈𝑋, 𝐹, 𝑌〉) = 𝑌) |
33 | 32 | eqeq1d 2624 |
. . 3
⊢ (𝜑 → ((2nd
‘〈𝑋, 𝐹, 𝑌〉) = 0 ↔ 𝑌 = 0 )) |
34 | 32 | sneqd 4189 |
. . . . . . . 8
⊢ (𝜑 → {(2nd
‘〈𝑋, 𝐹, 𝑌〉)} = {𝑌}) |
35 | 34 | fveq2d 6195 |
. . . . . . 7
⊢ (𝜑 → (𝑁‘{(2nd ‘〈𝑋, 𝐹, 𝑌〉)}) = (𝑁‘{𝑌})) |
36 | 35 | fveq2d 6195 |
. . . . . 6
⊢ (𝜑 → (𝑀‘(𝑁‘{(2nd ‘〈𝑋, 𝐹, 𝑌〉)})) = (𝑀‘(𝑁‘{𝑌}))) |
37 | 36 | eqeq1d 2624 |
. . . . 5
⊢ (𝜑 → ((𝑀‘(𝑁‘{(2nd ‘〈𝑋, 𝐹, 𝑌〉)})) = (𝐽‘{ℎ}) ↔ (𝑀‘(𝑁‘{𝑌})) = (𝐽‘{ℎ}))) |
38 | | mapdh.x |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑋 ∈ 𝐴) |
39 | | mapdh.f |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐹 ∈ 𝐵) |
40 | | ot1stg 7182 |
. . . . . . . . . . 11
⊢ ((𝑋 ∈ 𝐴 ∧ 𝐹 ∈ 𝐵 ∧ 𝑌 ∈ 𝐸) → (1st
‘(1st ‘〈𝑋, 𝐹, 𝑌〉)) = 𝑋) |
41 | 38, 39, 30, 40 | syl3anc 1326 |
. . . . . . . . . 10
⊢ (𝜑 → (1st
‘(1st ‘〈𝑋, 𝐹, 𝑌〉)) = 𝑋) |
42 | 41, 32 | oveq12d 6668 |
. . . . . . . . 9
⊢ (𝜑 → ((1st
‘(1st ‘〈𝑋, 𝐹, 𝑌〉)) − (2nd
‘〈𝑋, 𝐹, 𝑌〉)) = (𝑋 − 𝑌)) |
43 | 42 | sneqd 4189 |
. . . . . . . 8
⊢ (𝜑 → {((1st
‘(1st ‘〈𝑋, 𝐹, 𝑌〉)) − (2nd
‘〈𝑋, 𝐹, 𝑌〉))} = {(𝑋 − 𝑌)}) |
44 | 43 | fveq2d 6195 |
. . . . . . 7
⊢ (𝜑 → (𝑁‘{((1st
‘(1st ‘〈𝑋, 𝐹, 𝑌〉)) − (2nd
‘〈𝑋, 𝐹, 𝑌〉))}) = (𝑁‘{(𝑋 − 𝑌)})) |
45 | 44 | fveq2d 6195 |
. . . . . 6
⊢ (𝜑 → (𝑀‘(𝑁‘{((1st
‘(1st ‘〈𝑋, 𝐹, 𝑌〉)) − (2nd
‘〈𝑋, 𝐹, 𝑌〉))})) = (𝑀‘(𝑁‘{(𝑋 − 𝑌)}))) |
46 | | ot2ndg 7183 |
. . . . . . . . . 10
⊢ ((𝑋 ∈ 𝐴 ∧ 𝐹 ∈ 𝐵 ∧ 𝑌 ∈ 𝐸) → (2nd
‘(1st ‘〈𝑋, 𝐹, 𝑌〉)) = 𝐹) |
47 | 38, 39, 30, 46 | syl3anc 1326 |
. . . . . . . . 9
⊢ (𝜑 → (2nd
‘(1st ‘〈𝑋, 𝐹, 𝑌〉)) = 𝐹) |
48 | 47 | oveq1d 6665 |
. . . . . . . 8
⊢ (𝜑 → ((2nd
‘(1st ‘〈𝑋, 𝐹, 𝑌〉))𝑅ℎ) = (𝐹𝑅ℎ)) |
49 | 48 | sneqd 4189 |
. . . . . . 7
⊢ (𝜑 → {((2nd
‘(1st ‘〈𝑋, 𝐹, 𝑌〉))𝑅ℎ)} = {(𝐹𝑅ℎ)}) |
50 | 49 | fveq2d 6195 |
. . . . . 6
⊢ (𝜑 → (𝐽‘{((2nd
‘(1st ‘〈𝑋, 𝐹, 𝑌〉))𝑅ℎ)}) = (𝐽‘{(𝐹𝑅ℎ)})) |
51 | 45, 50 | eqeq12d 2637 |
. . . . 5
⊢ (𝜑 → ((𝑀‘(𝑁‘{((1st
‘(1st ‘〈𝑋, 𝐹, 𝑌〉)) − (2nd
‘〈𝑋, 𝐹, 𝑌〉))})) = (𝐽‘{((2nd
‘(1st ‘〈𝑋, 𝐹, 𝑌〉))𝑅ℎ)}) ↔ (𝑀‘(𝑁‘{(𝑋 − 𝑌)})) = (𝐽‘{(𝐹𝑅ℎ)}))) |
52 | 37, 51 | anbi12d 747 |
. . . 4
⊢ (𝜑 → (((𝑀‘(𝑁‘{(2nd ‘〈𝑋, 𝐹, 𝑌〉)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1st
‘(1st ‘〈𝑋, 𝐹, 𝑌〉)) − (2nd
‘〈𝑋, 𝐹, 𝑌〉))})) = (𝐽‘{((2nd
‘(1st ‘〈𝑋, 𝐹, 𝑌〉))𝑅ℎ)})) ↔ ((𝑀‘(𝑁‘{𝑌})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{(𝑋 − 𝑌)})) = (𝐽‘{(𝐹𝑅ℎ)})))) |
53 | 52 | riotabidv 6613 |
. . 3
⊢ (𝜑 → (℩ℎ ∈ 𝐷 ((𝑀‘(𝑁‘{(2nd ‘〈𝑋, 𝐹, 𝑌〉)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1st
‘(1st ‘〈𝑋, 𝐹, 𝑌〉)) − (2nd
‘〈𝑋, 𝐹, 𝑌〉))})) = (𝐽‘{((2nd
‘(1st ‘〈𝑋, 𝐹, 𝑌〉))𝑅ℎ)}))) = (℩ℎ ∈ 𝐷 ((𝑀‘(𝑁‘{𝑌})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{(𝑋 − 𝑌)})) = (𝐽‘{(𝐹𝑅ℎ)})))) |
54 | 33, 53 | ifbieq2d 4111 |
. 2
⊢ (𝜑 → if((2nd
‘〈𝑋, 𝐹, 𝑌〉) = 0 , 𝑄, (℩ℎ ∈ 𝐷 ((𝑀‘(𝑁‘{(2nd ‘〈𝑋, 𝐹, 𝑌〉)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1st
‘(1st ‘〈𝑋, 𝐹, 𝑌〉)) − (2nd
‘〈𝑋, 𝐹, 𝑌〉))})) = (𝐽‘{((2nd
‘(1st ‘〈𝑋, 𝐹, 𝑌〉))𝑅ℎ)})))) = if(𝑌 = 0 , 𝑄, (℩ℎ ∈ 𝐷 ((𝑀‘(𝑁‘{𝑌})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{(𝑋 − 𝑌)})) = (𝐽‘{(𝐹𝑅ℎ)}))))) |
55 | 29, 54 | eqtrd 2656 |
1
⊢ (𝜑 → (𝐼‘〈𝑋, 𝐹, 𝑌〉) = if(𝑌 = 0 , 𝑄, (℩ℎ ∈ 𝐷 ((𝑀‘(𝑁‘{𝑌})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{(𝑋 − 𝑌)})) = (𝐽‘{(𝐹𝑅ℎ)}))))) |