Proof of Theorem xpcco2
Step | Hyp | Ref
| Expression |
1 | | xpcco2.t |
. . 3
⊢ 𝑇 = (𝐶 ×c 𝐷) |
2 | | xpcco2.x |
. . . 4
⊢ 𝑋 = (Base‘𝐶) |
3 | | xpcco2.y |
. . . 4
⊢ 𝑌 = (Base‘𝐷) |
4 | 1, 2, 3 | xpcbas 16818 |
. . 3
⊢ (𝑋 × 𝑌) = (Base‘𝑇) |
5 | | eqid 2622 |
. . 3
⊢ (Hom
‘𝑇) = (Hom
‘𝑇) |
6 | | xpcco2.o1 |
. . 3
⊢ · =
(comp‘𝐶) |
7 | | xpcco2.o2 |
. . 3
⊢ ∙ =
(comp‘𝐷) |
8 | | xpcco2.o |
. . 3
⊢ 𝑂 = (comp‘𝑇) |
9 | | xpcco2.m |
. . . 4
⊢ (𝜑 → 𝑀 ∈ 𝑋) |
10 | | xpcco2.n |
. . . 4
⊢ (𝜑 → 𝑁 ∈ 𝑌) |
11 | | opelxpi 5148 |
. . . 4
⊢ ((𝑀 ∈ 𝑋 ∧ 𝑁 ∈ 𝑌) → 〈𝑀, 𝑁〉 ∈ (𝑋 × 𝑌)) |
12 | 9, 10, 11 | syl2anc 693 |
. . 3
⊢ (𝜑 → 〈𝑀, 𝑁〉 ∈ (𝑋 × 𝑌)) |
13 | | xpcco2.p |
. . . 4
⊢ (𝜑 → 𝑃 ∈ 𝑋) |
14 | | xpcco2.q |
. . . 4
⊢ (𝜑 → 𝑄 ∈ 𝑌) |
15 | | opelxpi 5148 |
. . . 4
⊢ ((𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑌) → 〈𝑃, 𝑄〉 ∈ (𝑋 × 𝑌)) |
16 | 13, 14, 15 | syl2anc 693 |
. . 3
⊢ (𝜑 → 〈𝑃, 𝑄〉 ∈ (𝑋 × 𝑌)) |
17 | | xpcco2.r |
. . . 4
⊢ (𝜑 → 𝑅 ∈ 𝑋) |
18 | | xpcco2.s |
. . . 4
⊢ (𝜑 → 𝑆 ∈ 𝑌) |
19 | | opelxpi 5148 |
. . . 4
⊢ ((𝑅 ∈ 𝑋 ∧ 𝑆 ∈ 𝑌) → 〈𝑅, 𝑆〉 ∈ (𝑋 × 𝑌)) |
20 | 17, 18, 19 | syl2anc 693 |
. . 3
⊢ (𝜑 → 〈𝑅, 𝑆〉 ∈ (𝑋 × 𝑌)) |
21 | | xpcco2.f |
. . . . 5
⊢ (𝜑 → 𝐹 ∈ (𝑀𝐻𝑃)) |
22 | | xpcco2.g |
. . . . 5
⊢ (𝜑 → 𝐺 ∈ (𝑁𝐽𝑄)) |
23 | | opelxpi 5148 |
. . . . 5
⊢ ((𝐹 ∈ (𝑀𝐻𝑃) ∧ 𝐺 ∈ (𝑁𝐽𝑄)) → 〈𝐹, 𝐺〉 ∈ ((𝑀𝐻𝑃) × (𝑁𝐽𝑄))) |
24 | 21, 22, 23 | syl2anc 693 |
. . . 4
⊢ (𝜑 → 〈𝐹, 𝐺〉 ∈ ((𝑀𝐻𝑃) × (𝑁𝐽𝑄))) |
25 | | xpcco2.h |
. . . . 5
⊢ 𝐻 = (Hom ‘𝐶) |
26 | | xpcco2.j |
. . . . 5
⊢ 𝐽 = (Hom ‘𝐷) |
27 | 1, 2, 3, 25, 26, 9, 10, 13, 14, 5 | xpchom2 16826 |
. . . 4
⊢ (𝜑 → (〈𝑀, 𝑁〉(Hom ‘𝑇)〈𝑃, 𝑄〉) = ((𝑀𝐻𝑃) × (𝑁𝐽𝑄))) |
28 | 24, 27 | eleqtrrd 2704 |
. . 3
⊢ (𝜑 → 〈𝐹, 𝐺〉 ∈ (〈𝑀, 𝑁〉(Hom ‘𝑇)〈𝑃, 𝑄〉)) |
29 | | xpcco2.k |
. . . . 5
⊢ (𝜑 → 𝐾 ∈ (𝑃𝐻𝑅)) |
30 | | xpcco2.l |
. . . . 5
⊢ (𝜑 → 𝐿 ∈ (𝑄𝐽𝑆)) |
31 | | opelxpi 5148 |
. . . . 5
⊢ ((𝐾 ∈ (𝑃𝐻𝑅) ∧ 𝐿 ∈ (𝑄𝐽𝑆)) → 〈𝐾, 𝐿〉 ∈ ((𝑃𝐻𝑅) × (𝑄𝐽𝑆))) |
32 | 29, 30, 31 | syl2anc 693 |
. . . 4
⊢ (𝜑 → 〈𝐾, 𝐿〉 ∈ ((𝑃𝐻𝑅) × (𝑄𝐽𝑆))) |
33 | 1, 2, 3, 25, 26, 13, 14, 17, 18, 5 | xpchom2 16826 |
. . . 4
⊢ (𝜑 → (〈𝑃, 𝑄〉(Hom ‘𝑇)〈𝑅, 𝑆〉) = ((𝑃𝐻𝑅) × (𝑄𝐽𝑆))) |
34 | 32, 33 | eleqtrrd 2704 |
. . 3
⊢ (𝜑 → 〈𝐾, 𝐿〉 ∈ (〈𝑃, 𝑄〉(Hom ‘𝑇)〈𝑅, 𝑆〉)) |
35 | 1, 4, 5, 6, 7, 8, 12, 16, 20, 28, 34 | xpcco 16823 |
. 2
⊢ (𝜑 → (〈𝐾, 𝐿〉(〈〈𝑀, 𝑁〉, 〈𝑃, 𝑄〉〉𝑂〈𝑅, 𝑆〉)〈𝐹, 𝐺〉) = 〈((1st
‘〈𝐾, 𝐿〉)(〈(1st
‘〈𝑀, 𝑁〉), (1st
‘〈𝑃, 𝑄〉)〉 · (1st
‘〈𝑅, 𝑆〉))(1st
‘〈𝐹, 𝐺〉)), ((2nd
‘〈𝐾, 𝐿〉)(〈(2nd
‘〈𝑀, 𝑁〉), (2nd
‘〈𝑃, 𝑄〉)〉 ∙ (2nd
‘〈𝑅, 𝑆〉))(2nd
‘〈𝐹, 𝐺〉))〉) |
36 | | op1stg 7180 |
. . . . . . 7
⊢ ((𝑀 ∈ 𝑋 ∧ 𝑁 ∈ 𝑌) → (1st ‘〈𝑀, 𝑁〉) = 𝑀) |
37 | 9, 10, 36 | syl2anc 693 |
. . . . . 6
⊢ (𝜑 → (1st
‘〈𝑀, 𝑁〉) = 𝑀) |
38 | | op1stg 7180 |
. . . . . . 7
⊢ ((𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑌) → (1st ‘〈𝑃, 𝑄〉) = 𝑃) |
39 | 13, 14, 38 | syl2anc 693 |
. . . . . 6
⊢ (𝜑 → (1st
‘〈𝑃, 𝑄〉) = 𝑃) |
40 | 37, 39 | opeq12d 4410 |
. . . . 5
⊢ (𝜑 → 〈(1st
‘〈𝑀, 𝑁〉), (1st
‘〈𝑃, 𝑄〉)〉 = 〈𝑀, 𝑃〉) |
41 | | op1stg 7180 |
. . . . . 6
⊢ ((𝑅 ∈ 𝑋 ∧ 𝑆 ∈ 𝑌) → (1st ‘〈𝑅, 𝑆〉) = 𝑅) |
42 | 17, 18, 41 | syl2anc 693 |
. . . . 5
⊢ (𝜑 → (1st
‘〈𝑅, 𝑆〉) = 𝑅) |
43 | 40, 42 | oveq12d 6668 |
. . . 4
⊢ (𝜑 → (〈(1st
‘〈𝑀, 𝑁〉), (1st
‘〈𝑃, 𝑄〉)〉 · (1st
‘〈𝑅, 𝑆〉)) = (〈𝑀, 𝑃〉 · 𝑅)) |
44 | | op1stg 7180 |
. . . . 5
⊢ ((𝐾 ∈ (𝑃𝐻𝑅) ∧ 𝐿 ∈ (𝑄𝐽𝑆)) → (1st ‘〈𝐾, 𝐿〉) = 𝐾) |
45 | 29, 30, 44 | syl2anc 693 |
. . . 4
⊢ (𝜑 → (1st
‘〈𝐾, 𝐿〉) = 𝐾) |
46 | | op1stg 7180 |
. . . . 5
⊢ ((𝐹 ∈ (𝑀𝐻𝑃) ∧ 𝐺 ∈ (𝑁𝐽𝑄)) → (1st ‘〈𝐹, 𝐺〉) = 𝐹) |
47 | 21, 22, 46 | syl2anc 693 |
. . . 4
⊢ (𝜑 → (1st
‘〈𝐹, 𝐺〉) = 𝐹) |
48 | 43, 45, 47 | oveq123d 6671 |
. . 3
⊢ (𝜑 → ((1st
‘〈𝐾, 𝐿〉)(〈(1st
‘〈𝑀, 𝑁〉), (1st
‘〈𝑃, 𝑄〉)〉 · (1st
‘〈𝑅, 𝑆〉))(1st
‘〈𝐹, 𝐺〉)) = (𝐾(〈𝑀, 𝑃〉 · 𝑅)𝐹)) |
49 | | op2ndg 7181 |
. . . . . . 7
⊢ ((𝑀 ∈ 𝑋 ∧ 𝑁 ∈ 𝑌) → (2nd ‘〈𝑀, 𝑁〉) = 𝑁) |
50 | 9, 10, 49 | syl2anc 693 |
. . . . . 6
⊢ (𝜑 → (2nd
‘〈𝑀, 𝑁〉) = 𝑁) |
51 | | op2ndg 7181 |
. . . . . . 7
⊢ ((𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑌) → (2nd ‘〈𝑃, 𝑄〉) = 𝑄) |
52 | 13, 14, 51 | syl2anc 693 |
. . . . . 6
⊢ (𝜑 → (2nd
‘〈𝑃, 𝑄〉) = 𝑄) |
53 | 50, 52 | opeq12d 4410 |
. . . . 5
⊢ (𝜑 → 〈(2nd
‘〈𝑀, 𝑁〉), (2nd
‘〈𝑃, 𝑄〉)〉 = 〈𝑁, 𝑄〉) |
54 | | op2ndg 7181 |
. . . . . 6
⊢ ((𝑅 ∈ 𝑋 ∧ 𝑆 ∈ 𝑌) → (2nd ‘〈𝑅, 𝑆〉) = 𝑆) |
55 | 17, 18, 54 | syl2anc 693 |
. . . . 5
⊢ (𝜑 → (2nd
‘〈𝑅, 𝑆〉) = 𝑆) |
56 | 53, 55 | oveq12d 6668 |
. . . 4
⊢ (𝜑 → (〈(2nd
‘〈𝑀, 𝑁〉), (2nd
‘〈𝑃, 𝑄〉)〉 ∙ (2nd
‘〈𝑅, 𝑆〉)) = (〈𝑁, 𝑄〉 ∙ 𝑆)) |
57 | | op2ndg 7181 |
. . . . 5
⊢ ((𝐾 ∈ (𝑃𝐻𝑅) ∧ 𝐿 ∈ (𝑄𝐽𝑆)) → (2nd ‘〈𝐾, 𝐿〉) = 𝐿) |
58 | 29, 30, 57 | syl2anc 693 |
. . . 4
⊢ (𝜑 → (2nd
‘〈𝐾, 𝐿〉) = 𝐿) |
59 | | op2ndg 7181 |
. . . . 5
⊢ ((𝐹 ∈ (𝑀𝐻𝑃) ∧ 𝐺 ∈ (𝑁𝐽𝑄)) → (2nd ‘〈𝐹, 𝐺〉) = 𝐺) |
60 | 21, 22, 59 | syl2anc 693 |
. . . 4
⊢ (𝜑 → (2nd
‘〈𝐹, 𝐺〉) = 𝐺) |
61 | 56, 58, 60 | oveq123d 6671 |
. . 3
⊢ (𝜑 → ((2nd
‘〈𝐾, 𝐿〉)(〈(2nd
‘〈𝑀, 𝑁〉), (2nd
‘〈𝑃, 𝑄〉)〉 ∙ (2nd
‘〈𝑅, 𝑆〉))(2nd
‘〈𝐹, 𝐺〉)) = (𝐿(〈𝑁, 𝑄〉 ∙ 𝑆)𝐺)) |
62 | 48, 61 | opeq12d 4410 |
. 2
⊢ (𝜑 → 〈((1st
‘〈𝐾, 𝐿〉)(〈(1st
‘〈𝑀, 𝑁〉), (1st
‘〈𝑃, 𝑄〉)〉 · (1st
‘〈𝑅, 𝑆〉))(1st
‘〈𝐹, 𝐺〉)), ((2nd
‘〈𝐾, 𝐿〉)(〈(2nd
‘〈𝑀, 𝑁〉), (2nd
‘〈𝑃, 𝑄〉)〉 ∙ (2nd
‘〈𝑅, 𝑆〉))(2nd
‘〈𝐹, 𝐺〉))〉 = 〈(𝐾(〈𝑀, 𝑃〉 · 𝑅)𝐹), (𝐿(〈𝑁, 𝑄〉 ∙ 𝑆)𝐺)〉) |
63 | 35, 62 | eqtrd 2656 |
1
⊢ (𝜑 → (〈𝐾, 𝐿〉(〈〈𝑀, 𝑁〉, 〈𝑃, 𝑄〉〉𝑂〈𝑅, 𝑆〉)〈𝐹, 𝐺〉) = 〈(𝐾(〈𝑀, 𝑃〉 · 𝑅)𝐹), (𝐿(〈𝑁, 𝑄〉 ∙ 𝑆)𝐺)〉) |