Step | Hyp | Ref
| Expression |
1 | | df-pprod 34151 |
. . 3
⊢
pprod(𝐴, 𝐵) = ((𝐴 ∘ (1st ↾ (V ×
V))) ⊗ (𝐵 ∘
(2nd ↾ (V × V)))) |
2 | 1 | breqi 5085 |
. 2
⊢
(〈𝑋, 𝑌〉pprod(𝐴, 𝐵)〈𝑍, 𝑊〉 ↔ 〈𝑋, 𝑌〉((𝐴 ∘ (1st ↾ (V ×
V))) ⊗ (𝐵 ∘
(2nd ↾ (V × V))))〈𝑍, 𝑊〉) |
3 | | opex 5382 |
. . 3
⊢
〈𝑋, 𝑌〉 ∈ V |
4 | | brpprod.3 |
. . 3
⊢ 𝑍 ∈ V |
5 | | brpprod.4 |
. . 3
⊢ 𝑊 ∈ V |
6 | 3, 4, 5 | brtxp 34176 |
. 2
⊢
(〈𝑋, 𝑌〉((𝐴 ∘ (1st ↾ (V ×
V))) ⊗ (𝐵 ∘
(2nd ↾ (V × V))))〈𝑍, 𝑊〉 ↔ (〈𝑋, 𝑌〉(𝐴 ∘ (1st ↾ (V ×
V)))𝑍 ∧ 〈𝑋, 𝑌〉(𝐵 ∘ (2nd ↾ (V ×
V)))𝑊)) |
7 | 3, 4 | brco 5777 |
. . . 4
⊢
(〈𝑋, 𝑌〉(𝐴 ∘ (1st ↾ (V ×
V)))𝑍 ↔ ∃𝑥(〈𝑋, 𝑌〉(1st ↾ (V ×
V))𝑥 ∧ 𝑥𝐴𝑍)) |
8 | | brpprod.1 |
. . . . . . . . 9
⊢ 𝑋 ∈ V |
9 | | brpprod.2 |
. . . . . . . . 9
⊢ 𝑌 ∈ V |
10 | 8, 9 | opelvv 5628 |
. . . . . . . 8
⊢
〈𝑋, 𝑌〉 ∈ (V ×
V) |
11 | | vex 3435 |
. . . . . . . . 9
⊢ 𝑥 ∈ V |
12 | 11 | brresi 5898 |
. . . . . . . 8
⊢
(〈𝑋, 𝑌〉(1st ↾ (V
× V))𝑥 ↔
(〈𝑋, 𝑌〉 ∈ (V × V) ∧
〈𝑋, 𝑌〉1st 𝑥)) |
13 | 10, 12 | mpbiran 706 |
. . . . . . 7
⊢
(〈𝑋, 𝑌〉(1st ↾ (V
× V))𝑥 ↔
〈𝑋, 𝑌〉1st 𝑥) |
14 | 8, 9 | br1steq 33739 |
. . . . . . 7
⊢
(〈𝑋, 𝑌〉1st 𝑥 ↔ 𝑥 = 𝑋) |
15 | 13, 14 | bitri 274 |
. . . . . 6
⊢
(〈𝑋, 𝑌〉(1st ↾ (V
× V))𝑥 ↔ 𝑥 = 𝑋) |
16 | 15 | anbi1i 624 |
. . . . 5
⊢
((〈𝑋, 𝑌〉(1st ↾ (V
× V))𝑥 ∧ 𝑥𝐴𝑍) ↔ (𝑥 = 𝑋 ∧ 𝑥𝐴𝑍)) |
17 | 16 | exbii 1854 |
. . . 4
⊢
(∃𝑥(〈𝑋, 𝑌〉(1st ↾ (V ×
V))𝑥 ∧ 𝑥𝐴𝑍) ↔ ∃𝑥(𝑥 = 𝑋 ∧ 𝑥𝐴𝑍)) |
18 | | breq1 5082 |
. . . . 5
⊢ (𝑥 = 𝑋 → (𝑥𝐴𝑍 ↔ 𝑋𝐴𝑍)) |
19 | 8, 18 | ceqsexv 3478 |
. . . 4
⊢
(∃𝑥(𝑥 = 𝑋 ∧ 𝑥𝐴𝑍) ↔ 𝑋𝐴𝑍) |
20 | 7, 17, 19 | 3bitri 297 |
. . 3
⊢
(〈𝑋, 𝑌〉(𝐴 ∘ (1st ↾ (V ×
V)))𝑍 ↔ 𝑋𝐴𝑍) |
21 | 3, 5 | brco 5777 |
. . . 4
⊢
(〈𝑋, 𝑌〉(𝐵 ∘ (2nd ↾ (V ×
V)))𝑊 ↔ ∃𝑦(〈𝑋, 𝑌〉(2nd ↾ (V ×
V))𝑦 ∧ 𝑦𝐵𝑊)) |
22 | | vex 3435 |
. . . . . . . . 9
⊢ 𝑦 ∈ V |
23 | 22 | brresi 5898 |
. . . . . . . 8
⊢
(〈𝑋, 𝑌〉(2nd ↾ (V
× V))𝑦 ↔
(〈𝑋, 𝑌〉 ∈ (V × V) ∧
〈𝑋, 𝑌〉2nd 𝑦)) |
24 | 10, 23 | mpbiran 706 |
. . . . . . 7
⊢
(〈𝑋, 𝑌〉(2nd ↾ (V
× V))𝑦 ↔
〈𝑋, 𝑌〉2nd 𝑦) |
25 | 8, 9 | br2ndeq 33740 |
. . . . . . 7
⊢
(〈𝑋, 𝑌〉2nd 𝑦 ↔ 𝑦 = 𝑌) |
26 | 24, 25 | bitri 274 |
. . . . . 6
⊢
(〈𝑋, 𝑌〉(2nd ↾ (V
× V))𝑦 ↔ 𝑦 = 𝑌) |
27 | 26 | anbi1i 624 |
. . . . 5
⊢
((〈𝑋, 𝑌〉(2nd ↾ (V
× V))𝑦 ∧ 𝑦𝐵𝑊) ↔ (𝑦 = 𝑌 ∧ 𝑦𝐵𝑊)) |
28 | 27 | exbii 1854 |
. . . 4
⊢
(∃𝑦(〈𝑋, 𝑌〉(2nd ↾ (V ×
V))𝑦 ∧ 𝑦𝐵𝑊) ↔ ∃𝑦(𝑦 = 𝑌 ∧ 𝑦𝐵𝑊)) |
29 | | breq1 5082 |
. . . . 5
⊢ (𝑦 = 𝑌 → (𝑦𝐵𝑊 ↔ 𝑌𝐵𝑊)) |
30 | 9, 29 | ceqsexv 3478 |
. . . 4
⊢
(∃𝑦(𝑦 = 𝑌 ∧ 𝑦𝐵𝑊) ↔ 𝑌𝐵𝑊) |
31 | 21, 28, 30 | 3bitri 297 |
. . 3
⊢
(〈𝑋, 𝑌〉(𝐵 ∘ (2nd ↾ (V ×
V)))𝑊 ↔ 𝑌𝐵𝑊) |
32 | 20, 31 | anbi12i 627 |
. 2
⊢
((〈𝑋, 𝑌〉(𝐴 ∘ (1st ↾ (V ×
V)))𝑍 ∧ 〈𝑋, 𝑌〉(𝐵 ∘ (2nd ↾ (V ×
V)))𝑊) ↔ (𝑋𝐴𝑍 ∧ 𝑌𝐵𝑊)) |
33 | 2, 6, 32 | 3bitri 297 |
1
⊢
(〈𝑋, 𝑌〉pprod(𝐴, 𝐵)〈𝑍, 𝑊〉 ↔ (𝑋𝐴𝑍 ∧ 𝑌𝐵𝑊)) |