Metamath Proof Explorer


Theorem funcestrcsetclem9

Description: Lemma 9 for funcestrcsetc . (Contributed by AV, 23-Mar-2020)

Ref Expression
Hypotheses funcestrcsetc.e E = ExtStrCat U
funcestrcsetc.s S = SetCat U
funcestrcsetc.b B = Base E
funcestrcsetc.c C = Base S
funcestrcsetc.u φ U WUni
funcestrcsetc.f φ F = x B Base x
funcestrcsetc.g φ G = x B , y B I Base y Base x
Assertion funcestrcsetclem9 φ X B Y B Z B H X Hom E Y K Y Hom E Z X G Z K X Y comp E Z H = Y G Z K F X F Y comp S F Z X G Y H

Proof

Step Hyp Ref Expression
1 funcestrcsetc.e E = ExtStrCat U
2 funcestrcsetc.s S = SetCat U
3 funcestrcsetc.b B = Base E
4 funcestrcsetc.c C = Base S
5 funcestrcsetc.u φ U WUni
6 funcestrcsetc.f φ F = x B Base x
7 funcestrcsetc.g φ G = x B , y B I Base y Base x
8 5 adantr φ X B Y B Z B U WUni
9 eqid Hom E = Hom E
10 1 5 estrcbas φ U = Base E
11 3 10 eqtr4id φ B = U
12 11 eleq2d φ X B X U
13 12 biimpcd X B φ X U
14 13 3ad2ant1 X B Y B Z B φ X U
15 14 impcom φ X B Y B Z B X U
16 11 eleq2d φ Y B Y U
17 16 biimpcd Y B φ Y U
18 17 3ad2ant2 X B Y B Z B φ Y U
19 18 impcom φ X B Y B Z B Y U
20 eqid Base X = Base X
21 eqid Base Y = Base Y
22 1 8 9 15 19 20 21 estrchom φ X B Y B Z B X Hom E Y = Base Y Base X
23 22 eleq2d φ X B Y B Z B H X Hom E Y H Base Y Base X
24 11 eleq2d φ Z B Z U
25 24 biimpcd Z B φ Z U
26 25 3ad2ant3 X B Y B Z B φ Z U
27 26 impcom φ X B Y B Z B Z U
28 eqid Base Z = Base Z
29 1 8 9 19 27 21 28 estrchom φ X B Y B Z B Y Hom E Z = Base Z Base Y
30 29 eleq2d φ X B Y B Z B K Y Hom E Z K Base Z Base Y
31 23 30 anbi12d φ X B Y B Z B H X Hom E Y K Y Hom E Z H Base Y Base X K Base Z Base Y
32 elmapi K Base Z Base Y K : Base Y Base Z
33 elmapi H Base Y Base X H : Base X Base Y
34 fco K : Base Y Base Z H : Base X Base Y K H : Base X Base Z
35 32 33 34 syl2an K Base Z Base Y H Base Y Base X K H : Base X Base Z
36 fvex Base Z V
37 fvex Base X V
38 36 37 elmap K H Base Z Base X K H : Base X Base Z
39 35 38 sylibr K Base Z Base Y H Base Y Base X K H Base Z Base X
40 39 ancoms H Base Y Base X K Base Z Base Y K H Base Z Base X
41 40 adantl φ X B Y B Z B H Base Y Base X K Base Z Base Y K H Base Z Base X
42 fvresi K H Base Z Base X I Base Z Base X K H = K H
43 41 42 syl φ X B Y B Z B H Base Y Base X K Base Z Base Y I Base Z Base X K H = K H
44 1 2 3 4 5 6 7 20 28 funcestrcsetclem5 φ X B Z B X G Z = I Base Z Base X
45 44 3adantr2 φ X B Y B Z B X G Z = I Base Z Base X
46 45 adantr φ X B Y B Z B H Base Y Base X K Base Z Base Y X G Z = I Base Z Base X
47 8 adantr φ X B Y B Z B H Base Y Base X K Base Z Base Y U WUni
48 eqid comp E = comp E
49 15 adantr φ X B Y B Z B H Base Y Base X K Base Z Base Y X U
50 19 adantr φ X B Y B Z B H Base Y Base X K Base Z Base Y Y U
51 27 adantr φ X B Y B Z B H Base Y Base X K Base Z Base Y Z U
52 33 ad2antrl φ X B Y B Z B H Base Y Base X K Base Z Base Y H : Base X Base Y
53 32 ad2antll φ X B Y B Z B H Base Y Base X K Base Z Base Y K : Base Y Base Z
54 1 47 48 49 50 51 20 21 28 52 53 estrcco φ X B Y B Z B H Base Y Base X K Base Z Base Y K X Y comp E Z H = K H
55 46 54 fveq12d φ X B Y B Z B H Base Y Base X K Base Z Base Y X G Z K X Y comp E Z H = I Base Z Base X K H
56 eqid comp S = comp S
57 1 2 3 4 5 6 funcestrcsetclem2 φ X B F X U
58 57 3ad2antr1 φ X B Y B Z B F X U
59 58 adantr φ X B Y B Z B H Base Y Base X K Base Z Base Y F X U
60 1 2 3 4 5 6 funcestrcsetclem2 φ Y B F Y U
61 60 3ad2antr2 φ X B Y B Z B F Y U
62 61 adantr φ X B Y B Z B H Base Y Base X K Base Z Base Y F Y U
63 1 2 3 4 5 6 funcestrcsetclem2 φ Z B F Z U
64 63 3ad2antr3 φ X B Y B Z B F Z U
65 64 adantr φ X B Y B Z B H Base Y Base X K Base Z Base Y F Z U
66 1 2 3 4 5 6 funcestrcsetclem1 φ X B F X = Base X
67 66 3ad2antr1 φ X B Y B Z B F X = Base X
68 1 2 3 4 5 6 funcestrcsetclem1 φ Y B F Y = Base Y
69 68 3ad2antr2 φ X B Y B Z B F Y = Base Y
70 67 69 feq23d φ X B Y B Z B H : F X F Y H : Base X Base Y
71 70 adantr φ X B Y B Z B H Base Y Base X K Base Z Base Y H : F X F Y H : Base X Base Y
72 52 71 mpbird φ X B Y B Z B H Base Y Base X K Base Z Base Y H : F X F Y
73 simpll φ X B Y B Z B H Base Y Base X K Base Z Base Y φ
74 3simpa X B Y B Z B X B Y B
75 74 ad2antlr φ X B Y B Z B H Base Y Base X K Base Z Base Y X B Y B
76 simprl φ X B Y B Z B H Base Y Base X K Base Z Base Y H Base Y Base X
77 1 2 3 4 5 6 7 20 21 funcestrcsetclem6 φ X B Y B H Base Y Base X X G Y H = H
78 73 75 76 77 syl3anc φ X B Y B Z B H Base Y Base X K Base Z Base Y X G Y H = H
79 78 feq1d φ X B Y B Z B H Base Y Base X K Base Z Base Y X G Y H : F X F Y H : F X F Y
80 72 79 mpbird φ X B Y B Z B H Base Y Base X K Base Z Base Y X G Y H : F X F Y
81 1 2 3 4 5 6 funcestrcsetclem1 φ Z B F Z = Base Z
82 81 3ad2antr3 φ X B Y B Z B F Z = Base Z
83 69 82 feq23d φ X B Y B Z B K : F Y F Z K : Base Y Base Z
84 83 adantr φ X B Y B Z B H Base Y Base X K Base Z Base Y K : F Y F Z K : Base Y Base Z
85 53 84 mpbird φ X B Y B Z B H Base Y Base X K Base Z Base Y K : F Y F Z
86 3simpc X B Y B Z B Y B Z B
87 86 ad2antlr φ X B Y B Z B H Base Y Base X K Base Z Base Y Y B Z B
88 simprr φ X B Y B Z B H Base Y Base X K Base Z Base Y K Base Z Base Y
89 1 2 3 4 5 6 7 21 28 funcestrcsetclem6 φ Y B Z B K Base Z Base Y Y G Z K = K
90 73 87 88 89 syl3anc φ X B Y B Z B H Base Y Base X K Base Z Base Y Y G Z K = K
91 90 feq1d φ X B Y B Z B H Base Y Base X K Base Z Base Y Y G Z K : F Y F Z K : F Y F Z
92 85 91 mpbird φ X B Y B Z B H Base Y Base X K Base Z Base Y Y G Z K : F Y F Z
93 2 47 56 59 62 65 80 92 setcco φ X B Y B Z B H Base Y Base X K Base Z Base Y Y G Z K F X F Y comp S F Z X G Y H = Y G Z K X G Y H
94 90 78 coeq12d φ X B Y B Z B H Base Y Base X K Base Z Base Y Y G Z K X G Y H = K H
95 93 94 eqtrd φ X B Y B Z B H Base Y Base X K Base Z Base Y Y G Z K F X F Y comp S F Z X G Y H = K H
96 43 55 95 3eqtr4d φ X B Y B Z B H Base Y Base X K Base Z Base Y X G Z K X Y comp E Z H = Y G Z K F X F Y comp S F Z X G Y H
97 96 ex φ X B Y B Z B H Base Y Base X K Base Z Base Y X G Z K X Y comp E Z H = Y G Z K F X F Y comp S F Z X G Y H
98 31 97 sylbid φ X B Y B Z B H X Hom E Y K Y Hom E Z X G Z K X Y comp E Z H = Y G Z K F X F Y comp S F Z X G Y H
99 98 3impia φ X B Y B Z B H X Hom E Y K Y Hom E Z X G Z K X Y comp E Z H = Y G Z K F X F Y comp S F Z X G Y H