Theorem cmpassoh 10729

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

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		eqid 1475	. . . 4 |- dom (dom` T) = dom (dom` T)
2		eqid 1475	. . . 4 |- (dom` T) = (dom` T)
3		eqid 1475	. . . 4 |- (cod` T) = (cod` T)
4		cmpassoh.3	. . . 4 |- R = (o` T)
5	1, 2, 3, 4	cmpasso 10706	. . 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)))
6		3simp1 788	. . . . 5 |- ((T e. Cat /\ (A e. O /\ B e. O) /\ (C e. O /\ D e. O)) -> T e. Cat)
7	6	adantr 389	. . . 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)
8		cmpassoh.1	. . . . . . . . . 10 |- O = dom (id` T)
9		cmpassoh.2	. . . . . . . . . 10 |- H = (hom` T)
10	8, 1, 9	ehm 10719	. . . . . . . . 9 |- ((T e. Cat /\ A e. O /\ B e. O) -> (L e. (H` <.A, B>.) -> L e. dom (dom` T)))
11	10	3expib 836	. . . . . . . 8 |- (T e. Cat -> ((A e. O /\ B e. O) -> (L e. (H` <.A, B>.) -> L e. dom (dom` T))))
12	11	a1dd 42	. . . . . . 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)))))
13	12	3imp 827	. . . . . 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)))
14	8, 1, 9	ehm 10719	. . . . . . . . . . . . 13 |- ((T e. Cat /\ B e. O /\ C e. O) -> (M e. (H` <.B, C>.) -> M e. dom (dom` T)))
15	14	3exp 832	. . . . . . . . . . . 12 |- (T e. Cat -> (B e. O -> (C e. O -> (M e. (H` <.B, C>.) -> M e. dom (dom` T)))))
16	15	com13 33	. . . . . . . . . . 11 |- (C e. O -> (B e. O -> (T e. Cat -> (M e. (H` <.B, C>.) -> M e. dom (dom` T)))))
17	16	adantr 389	. . . . . . . . . 10 |- ((C e. O /\ D e. O) -> (B e. O -> (T e. Cat -> (M e. (H` <.B, C>.) -> M e. dom (dom` T)))))
18	17	com3l 34	. . . . . . . . 9 |- (B e. O -> (T e. Cat -> ((C e. O /\ D e. O) -> (M e. (H` <.B, C>.) -> M e. dom (dom` T)))))
19	18	adantl 388	. . . . . . . 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)))))
20	19	com12 11	. . . . . . 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)))))
21	20	3imp 827	. . . . . 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)))
22	8, 1, 9	ehm 10719	. . . . . . . . 9 |- ((T e. Cat /\ C e. O /\ D e. O) -> (N e. (H` <.C, D>.) -> N e. dom (dom` T)))
23	22	3expib 836	. . . . . . . 8 |- (T e. Cat -> ((C e. O /\ D e. O) -> (N e. (H` <.C, D>.) -> N e. dom (dom` T))))
24	23	a1d 12	. . . . . . 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)))))
25	24	3imp 827	. . . . . 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)))
26	13, 21, 25	3anim123d 900	. . . . 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))))
27	26	imp 350	. . . 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)))
28	7, 27	jca 288	. . 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))))
29	8, 2, 9	dehm 10720	. . . . . . . . . 10 |- ((T e. Cat /\ C e. O /\ D e. O) -> (N e. (H` <.C, D>.) -> ((dom` T)` N) = C))
30	29	3expib 836	. . . . . . . . 9 |- (T e. Cat -> ((C e. O /\ D e. O) -> (N e. (H` <.C, D>.) -> ((dom` T)` N) = C)))
31	30	a1d 12	. . . . . . . 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))))
32	31	3imp 827	. . . . . . 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))
33		3simp3 790	. . . . . . 7 |- ((L e. (H` <.A, B>.) /\ M e. (H` <.B, C>.) /\ N e. (H` <.C, D>.)) -> N e. (H` <.C, D>.))
34	32, 33	syl5 21	. . . . . 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))
35	34	imp 350	. . . . 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)
36	8, 3, 9	cehm 10721	. . . . . . . . . . . . . 14 |- ((T e. Cat /\ B e. O /\ C e. O) -> (M e. (H` <.B, C>.) -> ((cod` T)` M) = C))
37	36	3exp 832	. . . . . . . . . . . . 13 |- (T e. Cat -> (B e. O -> (C e. O -> (M e. (H` <.B, C>.) -> ((cod` T)` M) = C))))
38	37	com13 33	. . . . . . . . . . . 12 |- (C e. O -> (B e. O -> (T e. Cat -> (M e. (H` <.B, C>.) -> ((cod` T)` M) = C))))
39	38	adantr 389	. . . . . . . . . . 11 |- ((C e. O /\ D e. O) -> (B e. O -> (T e. Cat -> (M e. (H` <.B, C>.) -> ((cod` T)` M) = C))))
40	39	com3l 34	. . . . . . . . . 10 |- (B e. O -> (T e. Cat -> ((C e. O /\ D e. O) -> (M e. (H` <.B, C>.) -> ((cod` T)` M) = C))))
41	40	adantl 388	. . . . . . . . 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))))
42	41	com12 11	. . . . . . . 8 |- (T e. Cat -> ((A e. O /\ B e. O) -> ((C e. O /\ D e. O) -> (M e. (H` <.B, C>.) -> ((cod` T)` M)