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 18223 |
. . 3
⊢ (𝑋 × 𝑌) = (Base‘𝑇) |
| 5 | | eqid 2737 |
. . 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 | 9, 10 | opelxpd 5724 |
. . 3
⊢ (𝜑 → 〈𝑀, 𝑁〉 ∈ (𝑋 × 𝑌)) |
| 12 | | xpcco2.p |
. . . 4
⊢ (𝜑 → 𝑃 ∈ 𝑋) |
| 13 | | xpcco2.q |
. . . 4
⊢ (𝜑 → 𝑄 ∈ 𝑌) |
| 14 | 12, 13 | opelxpd 5724 |
. . 3
⊢ (𝜑 → 〈𝑃, 𝑄〉 ∈ (𝑋 × 𝑌)) |
| 15 | | xpcco2.r |
. . . 4
⊢ (𝜑 → 𝑅 ∈ 𝑋) |
| 16 | | xpcco2.s |
. . . 4
⊢ (𝜑 → 𝑆 ∈ 𝑌) |
| 17 | 15, 16 | opelxpd 5724 |
. . 3
⊢ (𝜑 → 〈𝑅, 𝑆〉 ∈ (𝑋 × 𝑌)) |
| 18 | | xpcco2.f |
. . . . 5
⊢ (𝜑 → 𝐹 ∈ (𝑀𝐻𝑃)) |
| 19 | | xpcco2.g |
. . . . 5
⊢ (𝜑 → 𝐺 ∈ (𝑁𝐽𝑄)) |
| 20 | 18, 19 | opelxpd 5724 |
. . . 4
⊢ (𝜑 → 〈𝐹, 𝐺〉 ∈ ((𝑀𝐻𝑃) × (𝑁𝐽𝑄))) |
| 21 | | xpcco2.h |
. . . . 5
⊢ 𝐻 = (Hom ‘𝐶) |
| 22 | | xpcco2.j |
. . . . 5
⊢ 𝐽 = (Hom ‘𝐷) |
| 23 | 1, 2, 3, 21, 22, 9, 10, 12, 13, 5 | xpchom2 18231 |
. . . 4
⊢ (𝜑 → (〈𝑀, 𝑁〉(Hom ‘𝑇)〈𝑃, 𝑄〉) = ((𝑀𝐻𝑃) × (𝑁𝐽𝑄))) |
| 24 | 20, 23 | eleqtrrd 2844 |
. . 3
⊢ (𝜑 → 〈𝐹, 𝐺〉 ∈ (〈𝑀, 𝑁〉(Hom ‘𝑇)〈𝑃, 𝑄〉)) |
| 25 | | xpcco2.k |
. . . . 5
⊢ (𝜑 → 𝐾 ∈ (𝑃𝐻𝑅)) |
| 26 | | xpcco2.l |
. . . . 5
⊢ (𝜑 → 𝐿 ∈ (𝑄𝐽𝑆)) |
| 27 | 25, 26 | opelxpd 5724 |
. . . 4
⊢ (𝜑 → 〈𝐾, 𝐿〉 ∈ ((𝑃𝐻𝑅) × (𝑄𝐽𝑆))) |
| 28 | 1, 2, 3, 21, 22, 12, 13, 15, 16, 5 | xpchom2 18231 |
. . . 4
⊢ (𝜑 → (〈𝑃, 𝑄〉(Hom ‘𝑇)〈𝑅, 𝑆〉) = ((𝑃𝐻𝑅) × (𝑄𝐽𝑆))) |
| 29 | 27, 28 | eleqtrrd 2844 |
. . 3
⊢ (𝜑 → 〈𝐾, 𝐿〉 ∈ (〈𝑃, 𝑄〉(Hom ‘𝑇)〈𝑅, 𝑆〉)) |
| 30 | 1, 4, 5, 6, 7, 8, 11, 14, 17, 24, 29 | xpcco 18228 |
. 2
⊢ (𝜑 → (〈𝐾, 𝐿〉(〈〈𝑀, 𝑁〉, 〈𝑃, 𝑄〉〉𝑂〈𝑅, 𝑆〉)〈𝐹, 𝐺〉) = 〈((1st
‘〈𝐾, 𝐿〉)(〈(1st
‘〈𝑀, 𝑁〉), (1st
‘〈𝑃, 𝑄〉)〉 · (1st
‘〈𝑅, 𝑆〉))(1st
‘〈𝐹, 𝐺〉)), ((2nd
‘〈𝐾, 𝐿〉)(〈(2nd
‘〈𝑀, 𝑁〉), (2nd
‘〈𝑃, 𝑄〉)〉 ∙ (2nd
‘〈𝑅, 𝑆〉))(2nd
‘〈𝐹, 𝐺〉))〉) |
| 31 | | op1stg 8026 |
. . . . . . 7
⊢ ((𝑀 ∈ 𝑋 ∧ 𝑁 ∈ 𝑌) → (1st ‘〈𝑀, 𝑁〉) = 𝑀) |
| 32 | 9, 10, 31 | syl2anc 584 |
. . . . . 6
⊢ (𝜑 → (1st
‘〈𝑀, 𝑁〉) = 𝑀) |
| 33 | | op1stg 8026 |
. . . . . . 7
⊢ ((𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑌) → (1st ‘〈𝑃, 𝑄〉) = 𝑃) |
| 34 | 12, 13, 33 | syl2anc 584 |
. . . . . 6
⊢ (𝜑 → (1st
‘〈𝑃, 𝑄〉) = 𝑃) |
| 35 | 32, 34 | opeq12d 4881 |
. . . . 5
⊢ (𝜑 → 〈(1st
‘〈𝑀, 𝑁〉), (1st
‘〈𝑃, 𝑄〉)〉 = 〈𝑀, 𝑃〉) |
| 36 | | op1stg 8026 |
. . . . . 6
⊢ ((𝑅 ∈ 𝑋 ∧ 𝑆 ∈ 𝑌) → (1st ‘〈𝑅, 𝑆〉) = 𝑅) |
| 37 | 15, 16, 36 | syl2anc 584 |
. . . . 5
⊢ (𝜑 → (1st
‘〈𝑅, 𝑆〉) = 𝑅) |
| 38 | 35, 37 | oveq12d 7449 |
. . . 4
⊢ (𝜑 → (〈(1st
‘〈𝑀, 𝑁〉), (1st
‘〈𝑃, 𝑄〉)〉 · (1st
‘〈𝑅, 𝑆〉)) = (〈𝑀, 𝑃〉 · 𝑅)) |
| 39 | | op1stg 8026 |
. . . . 5
⊢ ((𝐾 ∈ (𝑃𝐻𝑅) ∧ 𝐿 ∈ (𝑄𝐽𝑆)) → (1st ‘〈𝐾, 𝐿〉) = 𝐾) |
| 40 | 25, 26, 39 | syl2anc 584 |
. . . 4
⊢ (𝜑 → (1st
‘〈𝐾, 𝐿〉) = 𝐾) |
| 41 | | op1stg 8026 |
. . . . 5
⊢ ((𝐹 ∈ (𝑀𝐻𝑃) ∧ 𝐺 ∈ (𝑁𝐽𝑄)) → (1st ‘〈𝐹, 𝐺〉) = 𝐹) |
| 42 | 18, 19, 41 | syl2anc 584 |
. . . 4
⊢ (𝜑 → (1st
‘〈𝐹, 𝐺〉) = 𝐹) |
| 43 | 38, 40, 42 | oveq123d 7452 |
. . 3
⊢ (𝜑 → ((1st
‘〈𝐾, 𝐿〉)(〈(1st
‘〈𝑀, 𝑁〉), (1st
‘〈𝑃, 𝑄〉)〉 · (1st
‘〈𝑅, 𝑆〉))(1st
‘〈𝐹, 𝐺〉)) = (𝐾(〈𝑀, 𝑃〉 · 𝑅)𝐹)) |
| 44 | | op2ndg 8027 |
. . . . . . 7
⊢ ((𝑀 ∈ 𝑋 ∧ 𝑁 ∈ 𝑌) → (2nd ‘〈𝑀, 𝑁〉) = 𝑁) |
| 45 | 9, 10, 44 | syl2anc 584 |
. . . . . 6
⊢ (𝜑 → (2nd
‘〈𝑀, 𝑁〉) = 𝑁) |
| 46 | | op2ndg 8027 |
. . . . . . 7
⊢ ((𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑌) → (2nd ‘〈𝑃, 𝑄〉) = 𝑄) |
| 47 | 12, 13, 46 | syl2anc 584 |
. . . . . 6
⊢ (𝜑 → (2nd
‘〈𝑃, 𝑄〉) = 𝑄) |
| 48 | 45, 47 | opeq12d 4881 |
. . . . 5
⊢ (𝜑 → 〈(2nd
‘〈𝑀, 𝑁〉), (2nd
‘〈𝑃, 𝑄〉)〉 = 〈𝑁, 𝑄〉) |
| 49 | | op2ndg 8027 |
. . . . . 6
⊢ ((𝑅 ∈ 𝑋 ∧ 𝑆 ∈ 𝑌) → (2nd ‘〈𝑅, 𝑆〉) = 𝑆) |
| 50 | 15, 16, 49 | syl2anc 584 |
. . . . 5
⊢ (𝜑 → (2nd
‘〈𝑅, 𝑆〉) = 𝑆) |
| 51 | 48, 50 | oveq12d 7449 |
. . . 4
⊢ (𝜑 → (〈(2nd
‘〈𝑀, 𝑁〉), (2nd
‘〈𝑃, 𝑄〉)〉 ∙ (2nd
‘〈𝑅, 𝑆〉)) = (〈𝑁, 𝑄〉 ∙ 𝑆)) |
| 52 | | op2ndg 8027 |
. . . . 5
⊢ ((𝐾 ∈ (𝑃𝐻𝑅) ∧ 𝐿 ∈ (𝑄𝐽𝑆)) → (2nd ‘〈𝐾, 𝐿〉) = 𝐿) |
| 53 | 25, 26, 52 | syl2anc 584 |
. . . 4
⊢ (𝜑 → (2nd
‘〈𝐾, 𝐿〉) = 𝐿) |
| 54 | | op2ndg 8027 |
. . . . 5
⊢ ((𝐹 ∈ (𝑀𝐻𝑃) ∧ 𝐺 ∈ (𝑁𝐽𝑄)) → (2nd ‘〈𝐹, 𝐺〉) = 𝐺) |
| 55 | 18, 19, 54 | syl2anc 584 |
. . . 4
⊢ (𝜑 → (2nd
‘〈𝐹, 𝐺〉) = 𝐺) |
| 56 | 51, 53, 55 | oveq123d 7452 |
. . 3
⊢ (𝜑 → ((2nd
‘〈𝐾, 𝐿〉)(〈(2nd
‘〈𝑀, 𝑁〉), (2nd
‘〈𝑃, 𝑄〉)〉 ∙ (2nd
‘〈𝑅, 𝑆〉))(2nd
‘〈𝐹, 𝐺〉)) = (𝐿(〈𝑁, 𝑄〉 ∙ 𝑆)𝐺)) |
| 57 | 43, 56 | opeq12d 4881 |
. 2
⊢ (𝜑 → 〈((1st
‘〈𝐾, 𝐿〉)(〈(1st
‘〈𝑀, 𝑁〉), (1st
‘〈𝑃, 𝑄〉)〉 · (1st
‘〈𝑅, 𝑆〉))(1st
‘〈𝐹, 𝐺〉)), ((2nd
‘〈𝐾, 𝐿〉)(〈(2nd
‘〈𝑀, 𝑁〉), (2nd
‘〈𝑃, 𝑄〉)〉 ∙ (2nd
‘〈𝑅, 𝑆〉))(2nd
‘〈𝐹, 𝐺〉))〉 = 〈(𝐾(〈𝑀, 𝑃〉 · 𝑅)𝐹), (𝐿(〈𝑁, 𝑄〉 ∙ 𝑆)𝐺)〉) |
| 58 | 30, 57 | eqtrd 2777 |
1
⊢ (𝜑 → (〈𝐾, 𝐿〉(〈〈𝑀, 𝑁〉, 〈𝑃, 𝑄〉〉𝑂〈𝑅, 𝑆〉)〈𝐹, 𝐺〉) = 〈(𝐾(〈𝑀, 𝑃〉 · 𝑅)𝐹), (𝐿(〈𝑁, 𝑄〉 ∙ 𝑆)𝐺)〉) |