Proof of Theorem pprodcnveq
Step | Hyp | Ref
| Expression |
1 | | dfpprod2 34184 |
. 2
⊢
pprod(𝑅, 𝑆) = ((◡(1st ↾ (V × V))
∘ (𝑅 ∘
(1st ↾ (V × V)))) ∩ (◡(2nd ↾ (V × V))
∘ (𝑆 ∘
(2nd ↾ (V × V))))) |
2 | | dfpprod2 34184 |
. . . 4
⊢
pprod(◡𝑅, ◡𝑆) = ((◡(1st ↾ (V × V))
∘ (◡𝑅 ∘ (1st ↾ (V ×
V)))) ∩ (◡(2nd ↾
(V × V)) ∘ (◡𝑆 ∘ (2nd ↾
(V × V))))) |
3 | 2 | cnveqi 5783 |
. . 3
⊢ ◡pprod(◡𝑅, ◡𝑆) = ◡((◡(1st ↾ (V × V))
∘ (◡𝑅 ∘ (1st ↾ (V ×
V)))) ∩ (◡(2nd ↾
(V × V)) ∘ (◡𝑆 ∘ (2nd ↾
(V × V))))) |
4 | | cnvin 6048 |
. . 3
⊢ ◡((◡(1st ↾ (V × V))
∘ (◡𝑅 ∘ (1st ↾ (V ×
V)))) ∩ (◡(2nd ↾
(V × V)) ∘ (◡𝑆 ∘ (2nd ↾
(V × V))))) = (◡(◡(1st ↾ (V × V))
∘ (◡𝑅 ∘ (1st ↾ (V ×
V)))) ∩ ◡(◡(2nd ↾ (V × V))
∘ (◡𝑆 ∘ (2nd ↾ (V ×
V))))) |
5 | | cnvco1 33726 |
. . . . 5
⊢ ◡(◡(1st ↾ (V × V))
∘ (◡𝑅 ∘ (1st ↾ (V ×
V)))) = (◡(◡𝑅 ∘ (1st ↾ (V ×
V))) ∘ (1st ↾ (V × V))) |
6 | | cnvco1 33726 |
. . . . . 6
⊢ ◡(◡𝑅 ∘ (1st ↾ (V ×
V))) = (◡(1st ↾ (V
× V)) ∘ 𝑅) |
7 | 6 | coeq1i 5768 |
. . . . 5
⊢ (◡(◡𝑅 ∘ (1st ↾ (V ×
V))) ∘ (1st ↾ (V × V))) = ((◡(1st ↾ (V × V))
∘ 𝑅) ∘
(1st ↾ (V × V))) |
8 | | coass 6169 |
. . . . 5
⊢ ((◡(1st ↾ (V × V))
∘ 𝑅) ∘
(1st ↾ (V × V))) = (◡(1st ↾ (V × V))
∘ (𝑅 ∘
(1st ↾ (V × V)))) |
9 | 5, 7, 8 | 3eqtri 2770 |
. . . 4
⊢ ◡(◡(1st ↾ (V × V))
∘ (◡𝑅 ∘ (1st ↾ (V ×
V)))) = (◡(1st ↾ (V
× V)) ∘ (𝑅
∘ (1st ↾ (V × V)))) |
10 | | cnvco1 33726 |
. . . . 5
⊢ ◡(◡(2nd ↾ (V × V))
∘ (◡𝑆 ∘ (2nd ↾ (V ×
V)))) = (◡(◡𝑆 ∘ (2nd ↾ (V ×
V))) ∘ (2nd ↾ (V × V))) |
11 | | cnvco1 33726 |
. . . . . 6
⊢ ◡(◡𝑆 ∘ (2nd ↾ (V ×
V))) = (◡(2nd ↾ (V
× V)) ∘ 𝑆) |
12 | 11 | coeq1i 5768 |
. . . . 5
⊢ (◡(◡𝑆 ∘ (2nd ↾ (V ×
V))) ∘ (2nd ↾ (V × V))) = ((◡(2nd ↾ (V × V))
∘ 𝑆) ∘
(2nd ↾ (V × V))) |
13 | | coass 6169 |
. . . . 5
⊢ ((◡(2nd ↾ (V × V))
∘ 𝑆) ∘
(2nd ↾ (V × V))) = (◡(2nd ↾ (V × V))
∘ (𝑆 ∘
(2nd ↾ (V × V)))) |
14 | 10, 12, 13 | 3eqtri 2770 |
. . . 4
⊢ ◡(◡(2nd ↾ (V × V))
∘ (◡𝑆 ∘ (2nd ↾ (V ×
V)))) = (◡(2nd ↾ (V
× V)) ∘ (𝑆
∘ (2nd ↾ (V × V)))) |
15 | 9, 14 | ineq12i 4144 |
. . 3
⊢ (◡(◡(1st ↾ (V × V))
∘ (◡𝑅 ∘ (1st ↾ (V ×
V)))) ∩ ◡(◡(2nd ↾ (V × V))
∘ (◡𝑆 ∘ (2nd ↾ (V ×
V))))) = ((◡(1st ↾ (V
× V)) ∘ (𝑅
∘ (1st ↾ (V × V)))) ∩ (◡(2nd ↾ (V × V))
∘ (𝑆 ∘
(2nd ↾ (V × V))))) |
16 | 3, 4, 15 | 3eqtri 2770 |
. 2
⊢ ◡pprod(◡𝑅, ◡𝑆) = ((◡(1st ↾ (V × V))
∘ (𝑅 ∘
(1st ↾ (V × V)))) ∩ (◡(2nd ↾ (V × V))
∘ (𝑆 ∘
(2nd ↾ (V × V))))) |
17 | 1, 16 | eqtr4i 2769 |
1
⊢
pprod(𝑅, 𝑆) = ◡pprod(◡𝑅, ◡𝑆) |