Theorem cmpassoh 15150

Description: o is associative. Homset-based version of cmpasso 15120.

Hypotheses

Ref	Expression
cmpassoh.1	|- O = dom (id` T)
cmpassoh.2	|- H = ( hom ` T)
cmpassoh.3	|- R = (o` T)

Assertion

Ref	Expression
cmpassoh	|- ((T e. Cat /\ (A e. O /\ B e. O) /\ (C e. O /\ D e. O)) -> ((L e. (H` <.A, B>.) /\ M e. (H` <.B, C>.) /\ N e. (H` <.C, D>.)) -> (NR(MRL)) = ((NRM)RL)))

Proof of Theorem cmpassoh

Step	Hyp	Ref	Expression
1		simpl1 879	. . . 4 |- (((T e. Cat /\ (A e. O /\ B e. O) /\ (C e. O /\ D e. O)) /\ (L e. (H` <.A, B>.) /\ M e. (H` <.B, C>.) /\ N e. (H` <.C, D>.))) -> T e. Cat )
2		cmpassoh.1	. . . . . . . . . 10 |- O = dom (id` T)
3		eqid 1884	. . . . . . . . . 10 |- dom (dom` T) = dom (dom` T)
4		cmpassoh.2	. . . . . . . . . 10 |- H = ( hom ` T)
5	2, 3, 4	ehm 15140	. . . . . . . . 9 |- ((T e. Cat /\ A e. O /\ B e. O) -> (L e. (H` <.A, B>.) -> L e. dom (dom` T)))
6	5	3expib 1070	. . . . . . . 8 |- (T e. Cat -> ((A e. O /\ B e. O) -> (L e. (H` <.A, B>.) -> L e. dom (dom` T))))
7	6	a1dd 53	. . . . . . 7 |- (T e. Cat -> ((A e. O /\ B e. O) -> ((C e. O /\ D e. O) -> (L e. (H` <.A, B>.) -> L e. dom (dom` T)))))
8	7	3imp 1061	. . . . . 6 |- ((T e. Cat /\ (A e. O /\ B e. O) /\ (C e. O /\ D e. O)) -> (L e. (H` <.A, B>.) -> L e. dom (dom` T)))
9	2, 3, 4	ehm 15140	. . . . . . . . . . . . 13 |- ((T e. Cat /\ B e. O /\ C e. O) -> (M e. (H` <.B, C>.) -> M e. dom (dom` T)))
10	9	3exp 1066	. . . . . . . . . . . 12 |- (T e. Cat -> (B e. O -> (C e. O -> (M e. (H` <.B, C>.) -> M e. dom (dom` T)))))
11	10	com13 37	. . . . . . . . . . 11 |- (C e. O -> (B e. O -> (T e. Cat -> (M e. (H` <.B, C>.) -> M e. dom (dom` T)))))
12	11	adantr 425	. . . . . . . . . 10 |- ((C e. O /\ D e. O) -> (B e. O -> (T e. Cat -> (M e. (H` <.B, C>.) -> M e. dom (dom` T)))))
13	12	com3l 38	. . . . . . . . 9 |- (B e. O -> (T e. Cat -> ((C e. O /\ D e. O) -> (M e. (H` <.B, C>.) -> M e. dom (dom` T)))))
14	13	adantl 424	. . . . . . . 8 |- ((A e. O /\ B e. O) -> (T e. Cat -> ((C e. O /\ D e. O) -> (M e. (H` <.B, C>.) -> M e. dom (dom` T)))))
15	14	com12 14	. . . . . . 7 |- (T e. Cat -> ((A e. O /\ B e. O) -> ((C e. O /\ D e. O) -> (M e. (H` <.B, C>.) -> M e. dom (dom` T)))))
16	15	3imp 1061	. . . . . 6 |- ((T e. Cat /\ (A e. O /\ B e. O) /\ (C e. O /\ D e. O)) -> (M e. (H` <.B, C>.) -> M e. dom (dom` T)))
17	2, 3, 4	ehm 15140	. . . . . . . . 9 |- ((T e. Cat /\ C e. O /\ D e. O) -> (N e. (H` <.C, D>.) -> N e. dom (dom` T)))
18	17	3expib 1070	. . . . . . . 8 |- (T e. Cat -> ((C e. O /\ D e. O) -> (N e. (H` <.C, D>.) -> N e. dom (dom` T))))
19	18	a1d 15	. . . . . . 7 |- (T e. Cat -> ((A e. O /\ B e. O) -> ((C e. O /\ D e. O) -> (N e. (H` <.C, D>.) -> N e. dom (dom` T)))))
20	19	3imp 1061	. . . . . 6 |- ((T e. Cat /\ (A e. O /\ B e. O) /\ (C e. O /\ D e. O)) -> (N e. (H` <.C, D>.) -> N e. dom (dom` T)))
21	8, 16, 20	3anim123d 1175	. . . . 5 |- ((T e. Cat /\ (A e. O /\ B e. O) /\ (C e. O /\ D e. O)) -> ((L e. (H` <.A, B>.) /\ M e. (H` <.B, C>.) /\ N e. (H` <.C, D>.)) -> (L e. dom (dom` T) /\ M e. dom (dom` T) /\ N e. dom (dom` T))))
22	21	imp 377	. . . 4 |- (((T e. Cat /\ (A e. O /\ B e. O) /\ (C e. O /\ D e. O)) /\ (L e. (H` <.A, B>.) /\ M e. (H` <.B, C>.) /\ N e. (H` <.C, D>.))) -> (L e. dom (dom` T) /\ M e. dom (dom` T) /\ N e. dom (dom` T)))
23	1, 22	jca 310	. . 3 |- (((T e. Cat /\ (A e. O /\ B e. O) /\ (C e. O /\ D e. O)) /\ (L e. (H` <.A, B>.) /\ M e. (H` <.B, C>.) /\ N e. (H` <.C, D>.))) -> (T e. Cat /\ (L e. dom (dom` T) /\ M e. dom (dom` T) /\ N e. dom (dom` T))))
24		eqid 1884	. . . . . . . . . . 11 |- (dom` T) = (dom` T)
25	2, 24, 4	dehm 15141	. . . . . . . . . 10 |- ((T e. Cat /\ C e. O /\ D e. O) -> (N e. (H` <.C, D>.) -> ((dom` T)` N) = C))
26	25	3expib 1070	. . . . . . . . 9 |- (T e. Cat -> ((C e. O /\ D e. O) -> (N e. (H` <.C, D>.) -> ((dom` T)` N) = C)))
27	26	a1d 15	. . . . . . . 8 |- (T e. Cat -> ((A e. O /\ B e. O) -> ((C e. O /\ D e. O) -> (N e. (H` <.C, D>.) -> ((dom` T)` N) = C))))
28	27	3imp 1061	. . . . . . 7 |- ((T e. Cat /\ (A e. O /\ B e. O) /\ (C e. O /\ D e. O)) -> (N e. (H` <.C, D>.) -> ((dom` T)` N) = C))
29		simp3 878	. . . . . . 7 |- ((L e. (H` <.A, B>.) /\ M e. (H` <.B, C>.) /\ N e. (H` <.C, D>.)) -> N e. (H` <.C, D>.))
30	28, 29	syl5 20	. . . . . 6 |- ((T e. Cat /\ (A e. O /\ B e. O) /\ (C e. O /\ D e. O)) -> ((L e. (H` <.A, B>.) /\ M e. (H` <.B, C>.) /\ N e. (H` <.C, D>.)) -> ((dom` T)` N) = C))
31	30	imp 377	. . . . 5 |- (((T e. Cat /\ (A e. O /\ B e. O) /\ (C e. O /\ D e. O)) /\ (L e. (H` <.A, B>.) /\ M e. (H` <.B, C>.) /\ N e. (H` <.C, D>.))) -> ((dom` T)` N) = C)
32		eqid 1884	. . . . . . . . . . . . . . 15 |- (cod` T) = (cod` T)
33	2, 32, 4	cehm 15142	. . . . . . . . . . . . . 14 |- ((T e. Cat /\ B e. O /\ C e. O) -> (M e. (H` <.B, C>.) -> ((cod` T)` M) = C))
34	33	3exp 1066	. . . . . . . . . . . . 13 |- (T e. Cat -> (B e. O -> (C e. O -> (M e. (H` <.B, C>.) -> ((cod` T)` M) = C))))
35	34	com13 37	. . . . . . . . . . . 12 |- (C e. O -> (B e. O -> (T e. Cat -> (M e. (H` <.B, C>.) -> ((cod` T)` M) = C))))
36	35	adantr 425	. . . . . . . . . . 11 |- ((C e. O /\ D e. O) -> (B e. O -> (T e. Cat -> (M e. (H` <.B, C>.) -> ((cod` T)` M) = C))))
37	36	com3l 38	. . . . . . . . . 10 |- (B e. O -> (T e. Cat -> ((C e. O /\ D e. O) -> (M e. (H` <.B, C>.) -> ((cod` T)` M) = C))))
38	37	adantl 424	. . . . . . . . 9 |- ((A e. O /\ B e. O) -> (T e. Cat -> ((C e. O /\ D e. O) -> (M e. (H` <.B, C>.) -> ((cod` T)` M) = C))))
39	38	com12 14	. . . . . . . 8 |- (T e. Cat -> ((A e. O /\ B e. O) -> ((C e. O /\ D e. O) -> (M e. (H` <.B, C>.) -> ((cod` T)` M) = C))))
40	39	3imp 1061	. . . . . . 7 |- ((T e. Cat /\ (A e. O /\ B e. O) /\ (C e. O /\ D e. O)) -> (M e. (H` <.B, C>.) -> ((cod` T)` M) = C))
41		simp2 877	. . . . . . 7 |- ((L e. (H` <.A, B>.) /\ M e. (H` <.B, C>.) /\ N e. (H` <.C, D>.)) -> M e. (H` <.B, C>.))
42	40, 41	syl5 20	. . . . . 6 |- ((T e. Cat /\ (A e. O /\ B e. O) /\ (C e. O /\ D e. O)) -> ((L e. (H` <.A, B>.) /\ M e. (H` <.B, C>.) /\ N e. (H` <.C, D>.)) -> ((cod` T)` M) = C))
43	42	imp 377	. . . . 5 |- (((T e. Cat /\ (A e. O /\ B e. O) /\ (C e. O /\ D e. O)) /\ (L e. (H` <.A, B>.) /\ M e. (H` <.B, C>.) /\ N e. (H` <.C, D>.))) -> ((cod` T)` M) = C)
44	31, 43	eqtr4d 1928	. . . 4 |- (((T e. Cat /\ (A e. O /\ B e. O) /\ (C e. O /\ D e. O)) /\ (L e. (H` <.A, B>.) /\ M e. (H` <.B, C>.) /\ N e. (H` <.C, D>.))) -> ((dom` T)` N) = ((cod` T)` M))
45	2, 24, 4	dehm 15141	. . . . . . . . . . . . . . . . 17 |- ((T e. Cat /\ B e. O /\ C e. O) -> (M e. (H` <.B, C>.) -> ((dom` T)` M) = B))
46	45	3adant3r1 1077	. . . . . . . . . . . . . . . 16 |- ((T e. Cat /\ (A e. O /\ B e. O /\ C e. O)) -> (M e. (H` <.B, C>.) -> ((dom` T)` M) = B))
47	46	adantld 426	. . . . . . . . . . . . . . 15 |- ((T e. Cat /\ (A e. O /\ B e. O /\ C e. O)) -> ((L e. (H` <.A, B>.) /\ M e. (H` <.B, C>.)) -> ((dom` T)` M) = B))
48	47	3impia 1064	. . . . . . . . . . . . . 14 |- ((T e. Cat /\ (A e. O /\ B e. O /\ C e. O) /\ (L e. (H` <.A, B>.) /\ M e. (H` <.B, C>.))) -> ((dom` T)` M) = B)
49	2, 32, 4	cehm 15142	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((T e. Cat /\ A e. O /\ B e. O) -> (L e. (H` <.A, B>.) -> ((cod` T)` L) = B))
50	49	imp 377	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((T e. Cat /\ A e. O /\ B e. O) /\ L e. (H` <.A, B>.)) -> ((cod` T)` L) = B)
51	50	eqcomd 1889	. . . . . . . . . . . . . . . . . . . . . 22 |- (((T e. Cat /\ A e. O /\ B e. O) /\ L e. (H` <.A, B>.)) -> B = ((cod` T)` L))
52	51	ex 402	. . . . . . . . . . . . . . . . . . . . 21 |- ((T e. Cat /\ A e. O /\ B e. O) -> (L e. (H` <.A, B>.) -> B = ((cod` T)` L)))
53	52	3expib 1070	. . . . . . . . . . . . . . . . . . . 20 |- (T e. Cat -> ((A e. O /\ B e. O) -> (L e. (H` <.A, B>.) -> B = ((cod` T)` L))))
54	53	com3r 39	. . . . . . . . . . . . . . . . . . 19 |- (L e. (H` <.A, B>.) -> (T e. Cat -> ((A e. O /\ B e. O) -> B = ((cod` T)` L))))
55	54	adantr 425	. . . . . . . . . . . . . . . . . 18 |- ((L e. (H` <.A, B>.) /\ M e. (H` <.B, C>.)) -> (T e. Cat -> ((A e. O /\ B e. O) -> B = ((cod` T)` L))))
56	55	com13 37	. . . . . . . . . . . . . . . . 17 |- ((A e. O /\ B e. O) -> (T e. Cat -> ((L e. (H` <.A, B>.) /\ M e. (H` <.B, C>.)) -> B = ((cod` T)` L))))
57	56	3adant3 896	. . . . . . . . . . . . . . . 16 |- ((A e. O /\ B e. O /\ C e. O) -> (T e. Cat -> ((L e. (H` <.A, B>.) /\ M e. (H` <.B, C>.)) -> B = ((cod` T)` L))))
58	57	com12 14	. . . . . . . . . . . . . . 15 |- (T e. Cat -> ((A e. O /\ B e. O /\ C e. O) -> ((L e. (H` <.A, B>.) /\ M e. (H` <.B, C>.)) -> B = ((cod` T)` L))))
59	58	3imp 1061	. . . . . . . . . . . . . 14 |- ((T e. Cat /\ (A e. O /\ B e. O /\ C e. O) /\ (L e. (H` <.A, B>.) /\ M e. (H` <.B, C>.))) -> B = ((cod` T)` L))
60	48, 59	eqtrd 1925	. . . . . . . . . . . . 13 |- ((T e. Cat /\ (A e. O /\ B e. O /\ C e. O) /\ (L e. (H` <.A, B>.) /\ M e. (H` <.B, C>.))) -> ((dom` T)` M) = ((cod` T)` L))
61	60	3exp 1066	. . . . . . . . . . . 12 |- (T e. Cat -> ((A e. O /\ B e. O /\ C e. O) -> ((L e. (H` <.A, B>.) /\ M e. (H` <.B, C>.)) -> ((dom` T)` M) = ((cod` T)` L))))
62	61	com12 14	. . . . . . . . . . 11 |- ((A e. O /\ B e. O /\ C e. O) -> (T e. Cat -> ((L e. (H` <.A, B>.) /\ M e. (H` <.B, C>.)) -> ((dom` T)` M) = ((cod` T)` L))))
63	62	3expia 1069	. . . . . . . . . 10 |- ((A e. O /\ B e. O) -> (C e. O -> (T e. Cat -> ((L e. (H` <.A, B>.) /\ M e. (H` <.B, C>.)) -> ((dom` T)` M) = ((cod` T)` L)))))
64	63	com12 14	. . . . . . . . 9 |- (C e. O -> ((A e. O /\ B e. O) -> (T e. Cat -> ((L e. (H` <.A, B>.) /\ M e. (H` <.B, C>.)) -> ((dom` T)` M) = ((cod` T)` L)))))
65	64	adantr 425	. . . . . . . 8 |- ((C e. O /\ D e. O) -> ((A e. O /\ B e. O) -> (T e. Cat -> ((L e. (H` <.A, B>.) /\ M e. (H` <.B, C>.)) -> ((dom` T)` M) = ((cod` T)` L)))))
66	65	com13 37	. . . . . . 7 |- (T e. Cat -> ((A e. O /\ B e. O) -> ((C e. O /\ D e. O) -> ((L e. (H` <.A, B>.) /\ M e. (H` <.B, C>.)) -> ((dom` T)` M) = ((cod` T)` L)))))
67	66	3imp 1061	. . . . . 6 |- ((T e. Cat /\ (A e. O /\ B e. O) /\ (C e. O /\ D e. O)) -> ((L e. (H` <.A, B>.) /\ M e. (H` <.B, C>.)) -> ((dom` T)` M) = ((cod` T)` L)))
68		3simpa 872	. . . . . 6 |- ((L e. (H` <.A, B>.) /\ M e. (H` <.B, C>.) /\ N e. (H` <.C, D>.)) -> (L e. (H` <.A, B>.) /\ M e. (H` <.B, C>.)))
69	67, 68	syl5 20	. . . . 5 |- ((T e. Cat /\ (A e. O /\ B e. O) /\ (C e. O /\ D e. O)) -> ((L e. (H` <.A, B>.) /\ M e. (H` <.B, C>.) /\ N e. (H` <.C, D>.)) -> ((dom` T)` M) = ((cod` T)` L)))
70	69	imp 377	. . . 4 |- (((T e. Cat /\ (A e. O /\ B e. O) /\ (C e. O /\ D e. O)) /\ (L e. (H` <.A, B>.) /\ M e. (H` <.B, C>.) /\ N e. (H` <.C, D>.))) -> ((dom` T)` M) = ((cod` T)` L))
71	44, 70	jca 310	. . 3 |- (((T e. Cat /\ (A e. O /\ B e. O) /\ (C e. O /\ D e. O)) /\ (L e. (H` <.A, B>.) /\ M e. (H` <.B, C>.) /\ N e. (H` <.C, D>.))) -> (((dom` T)` N) = ((cod` T)` M) /\ ((dom` T)` M) = ((cod` T)` L)))
72		cmpassoh.3	. . . 4 |- R = (o` T)
73	3, 24, 32, 72	cmpasso 15120	. . 3 |- ((T e. Cat /\ (L e. dom (dom` T) /\ M e. dom (dom` T) /\ N e. dom (dom` T))) -> ((((dom` T)` N) = ((cod` T)` M) /\ ((dom` T)` M) = ((cod` T)` L)) -> (NR(MRL)) = ((NRM)RL)))
74	23, 71, 73	sylc 83	. 2 |- (((T e. Cat /\ (A e. O /\ B e. O) /\ (C e. O /\ D e. O)) /\ (L e. (H` <.A, B>.) /\ M e. (H` <.B, C>.) /\ N e. (H` <.C, D>.))) -> (NR(MRL)) = ((NRM)RL))
75	74	ex 402	1 |- ((T e. Cat /\ (A e. O /\ B e. O) /\ (C e. O /\ D e. O)) -> ((L e. (H` <.A, B>.) /\ M e. (H` <.B, C>.) /\ N e. (H` <.C, D>.)) -> (NR(MRL)) = ((NRM)RL)))

Syntax hints:   -> wi 3   /\ wa 240   /\ w3a 858   = wceq 1298   e. wcel 1300  <.cop 3046  dom cdm 3986  ` cfv 3998  (class class class)co 4884  domcdom_ 15059  codccod_ 15060  idcid_ 15061  oco_ 15062   Cat ccat 15099   hom chom 15134

This theorem is referenced by:  cmpmon 15164  icmpmon 15165  idmon 15166

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-13 1311  ax-14 1312  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865  ax-rep 3428  ax-sep 3438  ax-nul 3445  ax-pow 3481  ax-pr 3524  ax-un 3790

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-3an 860  df-ex 1327  df-sb 1536  df-eu 1775  df-mo 1776  df-clab 1872  df-cleq 1877  df-clel 1880  df-ne 2019  df-ral 2109  df-rex 2110  df-v 2294  df-sbc 2454  df-csb 2541  df-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-nul 2876  df-if 2983  df-pw 3035  df-sn 3049  df-pr 3050  df-op 3053  df-uni 3178  df-br 3339  df-opab 3396  df-id 3586  df-xp 4000  df-rel 4001  df-cnv 4002  df-co 4003  df-dm 4004  df-rn 4005  df-res 4006  df-ima 4007  df-fun 4008  df-fn 4009  df-f 4010  df-f1 4011  df-fo 4012  df-f1o 4013  df-fv 4014  df-opr 4886  df-oprab 4887  df-1st 5020  df-2nd 5021  df-alg 15063  df-doma 15064  df-coda 15065  df-ida 15066  df-cmpa 15067  df-ded 15082  df-cat 15100  df-hom 15135

Copyright terms: Public domain