Proof of Theorem pprodcnveq
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | dfpprod2 35883 | . 2
⊢
pprod(𝑅, 𝑆) = ((◡(1st ↾ (V × V))
∘ (𝑅 ∘
(1st ↾ (V × V)))) ∩ (◡(2nd ↾ (V × V))
∘ (𝑆 ∘
(2nd ↾ (V × V))))) | 
| 2 |  | dfpprod2 35883 | . . . 4
⊢
pprod(◡𝑅, ◡𝑆) = ((◡(1st ↾ (V × V))
∘ (◡𝑅 ∘ (1st ↾ (V ×
V)))) ∩ (◡(2nd ↾
(V × V)) ∘ (◡𝑆 ∘ (2nd ↾
(V × V))))) | 
| 3 | 2 | cnveqi 5885 | . . 3
⊢ ◡pprod(◡𝑅, ◡𝑆) = ◡((◡(1st ↾ (V × V))
∘ (◡𝑅 ∘ (1st ↾ (V ×
V)))) ∩ (◡(2nd ↾
(V × V)) ∘ (◡𝑆 ∘ (2nd ↾
(V × V))))) | 
| 4 |  | cnvin 6164 | . . 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 35759 | . . . . 5
⊢ ◡(◡(1st ↾ (V × V))
∘ (◡𝑅 ∘ (1st ↾ (V ×
V)))) = (◡(◡𝑅 ∘ (1st ↾ (V ×
V))) ∘ (1st ↾ (V × V))) | 
| 6 |  | cnvco1 35759 | . . . . . 6
⊢ ◡(◡𝑅 ∘ (1st ↾ (V ×
V))) = (◡(1st ↾ (V
× V)) ∘ 𝑅) | 
| 7 | 6 | coeq1i 5870 | . . . . 5
⊢ (◡(◡𝑅 ∘ (1st ↾ (V ×
V))) ∘ (1st ↾ (V × V))) = ((◡(1st ↾ (V × V))
∘ 𝑅) ∘
(1st ↾ (V × V))) | 
| 8 |  | coass 6285 | . . . . 5
⊢ ((◡(1st ↾ (V × V))
∘ 𝑅) ∘
(1st ↾ (V × V))) = (◡(1st ↾ (V × V))
∘ (𝑅 ∘
(1st ↾ (V × V)))) | 
| 9 | 5, 7, 8 | 3eqtri 2769 | . . . 4
⊢ ◡(◡(1st ↾ (V × V))
∘ (◡𝑅 ∘ (1st ↾ (V ×
V)))) = (◡(1st ↾ (V
× V)) ∘ (𝑅
∘ (1st ↾ (V × V)))) | 
| 10 |  | cnvco1 35759 | . . . . 5
⊢ ◡(◡(2nd ↾ (V × V))
∘ (◡𝑆 ∘ (2nd ↾ (V ×
V)))) = (◡(◡𝑆 ∘ (2nd ↾ (V ×
V))) ∘ (2nd ↾ (V × V))) | 
| 11 |  | cnvco1 35759 | . . . . . 6
⊢ ◡(◡𝑆 ∘ (2nd ↾ (V ×
V))) = (◡(2nd ↾ (V
× V)) ∘ 𝑆) | 
| 12 | 11 | coeq1i 5870 | . . . . 5
⊢ (◡(◡𝑆 ∘ (2nd ↾ (V ×
V))) ∘ (2nd ↾ (V × V))) = ((◡(2nd ↾ (V × V))
∘ 𝑆) ∘
(2nd ↾ (V × V))) | 
| 13 |  | coass 6285 | . . . . 5
⊢ ((◡(2nd ↾ (V × V))
∘ 𝑆) ∘
(2nd ↾ (V × V))) = (◡(2nd ↾ (V × V))
∘ (𝑆 ∘
(2nd ↾ (V × V)))) | 
| 14 | 10, 12, 13 | 3eqtri 2769 | . . . 4
⊢ ◡(◡(2nd ↾ (V × V))
∘ (◡𝑆 ∘ (2nd ↾ (V ×
V)))) = (◡(2nd ↾ (V
× V)) ∘ (𝑆
∘ (2nd ↾ (V × V)))) | 
| 15 | 9, 14 | ineq12i 4218 | . . 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 2769 | . 2
⊢ ◡pprod(◡𝑅, ◡𝑆) = ((◡(1st ↾ (V × V))
∘ (𝑅 ∘
(1st ↾ (V × V)))) ∩ (◡(2nd ↾ (V × V))
∘ (𝑆 ∘
(2nd ↾ (V × V))))) | 
| 17 | 1, 16 | eqtr4i 2768 | 1
⊢
pprod(𝑅, 𝑆) = ◡pprod(◡𝑅, ◡𝑆) |