Theorem enq0tr 6417

Description: The equivalence relation for non-negative fractions is transitive. Lemma for enq0er 6418. (Contributed by Jim Kingdon, 14-Nov-2019.)

Assertion

Ref	Expression
enq0tr	|- ((f ~Q0 g /\ g ~Q0 h) -> f ~Q0 h)

Proof of Theorem enq0tr

Dummy variables a b c d e s t u v w x y z are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		vex 2554	. . . . . . . . . 10 |- f e. _V
2		vex 2554	. . . . . . . . . 10 |- g e. _V
3		eleq1 2097	. . . . . . . . . . . 12 |- (x = f -> (x e. ( om X. N.) <-> f e. ( om X. N.)))
4	3	anbi1d 438	. . . . . . . . . . 11 |- (x = f -> ((x e. ( om X. N.) /\ y e. ( om X. N.)) <-> (f e. ( om X. N.) /\ y e. ( om X. N.))))
5		eqeq1 2043	. . . . . . . . . . . . . 14 |- (x = f -> (x = <.z , w >. <-> f = <.z , w >.))
6	5	anbi1d 438	. . . . . . . . . . . . 13 |- (x = f -> ((x = <.z , w >. /\ y = <.v , u >.) <-> (f = <.z , w >. /\ y = <.v , u >.)))
7	6	anbi1d 438	. . . . . . . . . . . 12 |- (x = f -> (((x = <.z , w >. /\ y = <.v , u >.) /\ (z .o u) = (w .o v)) <-> ((f = <.z , w >. /\ y = <.v , u >.) /\ (z .o u) = (w .o v))))
8	7	4exbidv 1747	. . . . . . . . . . 11 |- (x = f -> (E.zE.wE.vE.u((x = <.z , w >. /\ y = <.v , u >.) /\ (z .o u) = (w .o v)) <-> E.zE.wE.vE.u((f = <.z , w >. /\ y = <.v , u >.) /\ (z .o u) = (w .o v))))
9	4, 8	anbi12d 442	. . . . . . . . . 10 |- (x = f -> (((x e. ( om X. N.) /\ y e. ( om X. N.)) /\ E.zE.wE.vE.u((x = <.z , w >. /\ y = <.v , u >.) /\ (z .o u) = (w .o v))) <-> ((f e. ( om X. N.) /\ y e. ( om X. N.)) /\ E.zE.wE.vE.u((f = <.z , w >. /\ y = <.v , u >.) /\ (z .o u) = (w .o v)))))
10		eleq1 2097	. . . . . . . . . . . 12 |- (y = g -> (y e. ( om X. N.) <-> g e. ( om X. N.)))
11	10	anbi2d 437	. . . . . . . . . . 11 |- (y = g -> ((f e. ( om X. N.) /\ y e. ( om X. N.)) <-> (f e. ( om X. N.) /\ g e. ( om X. N.))))
12		eqeq1 2043	. . . . . . . . . . . . . 14 |- (y = g -> (y = <.v , u >. <-> g = <.v , u >.))
13	12	anbi2d 437	. . . . . . . . . . . . 13 |- (y = g -> ((f = <.z , w >. /\ y = <.v , u >.) <-> (f = <.z , w >. /\ g = <.v , u >.)))
14	13	anbi1d 438	. . . . . . . . . . . 12 |- (y = g -> (((f = <.z , w >. /\ y = <.v , u >.) /\ (z .o u) = (w .o v)) <-> ((f = <.z , w >. /\ g = <.v , u >.) /\ (z .o u) = (w .o v))))
15	14	4exbidv 1747	. . . . . . . . . . 11 |- (y = g -> (E.zE.wE.vE.u((f = <.z , w >. /\ y = <.v , u >.) /\ (z .o u) = (w .o v)) <-> E.zE.wE.vE.u((f = <.z , w >. /\ g = <.v , u >.) /\ (z .o u) = (w .o v))))
16	11, 15	anbi12d 442	. . . . . . . . . 10 |- (y = g -> (((f e. ( om X. N.) /\ y e. ( om X. N.)) /\ E.zE.wE.vE.u((f = <.z , w >. /\ y = <.v , u >.) /\ (z .o u) = (w .o v))) <-> ((f e. ( om X. N.) /\ g e. ( om X. N.)) /\ E.zE.wE.vE.u((f = <.z , w >. /\ g = <.v , u >.) /\ (z .o u) = (w .o v)))))
17		df-enq0 6407	. . . . . . . . . 10 |- ~Q0 = { <.x , y >. | ((x e. ( om X. N.) /\ y e. ( om X. N.)) /\ E.zE.wE.vE.u((x = <.z , w >. /\ y = <.v , u >.) /\ (z .o u) = (w .o v))) }
18	1, 2, 9, 16, 17	brab 4000	. . . . . . . . 9 |- (f ~Q0 g <-> ((f e. ( om X. N.) /\ g e. ( om X. N.)) /\ E.zE.wE.vE.u((f = <.z , w >. /\ g = <.v , u >.) /\ (z .o u) = (w .o v))))
19		vex 2554	. . . . . . . . . 10 |- h e. _V
20		eleq1 2097	. . . . . . . . . . . 12 |- (x = g -> (x e. ( om X. N.) <-> g e. ( om X. N.)))
21	20	anbi1d 438	. . . . . . . . . . 11 |- (x = g -> ((x e. ( om X. N.) /\ y e. ( om X. N.)) <-> (g e. ( om X. N.) /\ y e. ( om X. N.))))
22		eqeq1 2043	. . . . . . . . . . . . . 14 |- (x = g -> (x = <. a , b >. <-> g = <. a , b >.))
23	22	anbi1d 438	. . . . . . . . . . . . 13 |- (x = g -> ((x = <. a , b >. /\ y = <. s , t >.) <-> (g = <. a , b >. /\ y = <. s , t >.)))
24	23	anbi1d 438	. . . . . . . . . . . 12 |- (x = g -> (((x = <. a , b >. /\ y = <. s , t >.) /\ ( a .o t) = ( b .o s)) <-> ((g = <. a , b >. /\ y = <. s , t >.) /\ ( a .o t) = ( b .o s))))
25	24	4exbidv 1747	. . . . . . . . . . 11 |- (x = g -> (E. aE. bE. sE. t((x = <. a , b >. /\ y = <. s , t >.) /\ ( a .o t) = ( b .o s)) <-> E. aE. bE. sE. t((g = <. a , b >. /\ y = <. s , t >.) /\ ( a .o t) = ( b .o s))))
26	21, 25	anbi12d 442	. . . . . . . . . 10 |- (x = g -> (((x e. ( om X. N.) /\ y e. ( om X. N.)) /\ E. aE. bE. sE. t((x = <. a , b >. /\ y = <. s , t >.) /\ ( a .o t) = ( b .o s))) <-> ((g e. ( om X. N.) /\ y e. ( om X. N.)) /\ E. aE. bE. sE. t((g = <. a , b >. /\ y = <. s , t >.) /\ ( a .o t) = ( b .o s)))))
27		eleq1 2097	. . . . . . . . . . . 12 |- (y = h -> (y e. ( om X. N.) <-> h e. ( om X. N.)))
28	27	anbi2d 437	. . . . . . . . . . 11 |- (y = h -> ((g e. ( om X. N.) /\ y e. ( om X. N.)) <-> (g e. ( om X. N.) /\ h e. ( om X. N.))))
29		eqeq1 2043	. . . . . . . . . . . . . 14 |- (y = h -> (y = <. s , t >. <-> h = <. s , t >.))
30	29	anbi2d 437	. . . . . . . . . . . . 13 |- (y = h -> ((g = <. a , b >. /\ y = <. s , t >.) <-> (g = <. a , b >. /\ h = <. s , t >.)))
31	30	anbi1d 438	. . . . . . . . . . . 12 |- (y = h -> (((g = <. a , b >. /\ y = <. s , t >.) /\ ( a .o t) = ( b .o s)) <-> ((g = <. a , b >. /\ h = <. s , t >.) /\ ( a .o t) = ( b .o s))))
32	31	4exbidv 1747	. . . . . . . . . . 11 |- (y = h -> (E. aE. bE. sE. t((g = <. a , b >. /\ y = <. s , t >.) /\ ( a .o t) = ( b .o s)) <-> E. aE. bE. sE. t((g = <. a , b >. /\ h = <. s , t >.) /\ ( a .o t) = ( b .o s))))
33	28, 32	anbi12d 442	. . . . . . . . . 10 |- (y = h -> (((g e. ( om X. N.) /\ y e. ( om X. N.)) /\ E. aE. bE. sE. t((g = <. a , b >. /\ y = <. s , t >.) /\ ( a .o t) = ( b .o s))) <-> ((g e. ( om X. N.) /\ h e. ( om X. N.)) /\ E. aE. bE. sE. t((g = <. a , b >. /\ h = <. s , t >.) /\ ( a .o t) = ( b .o s)))))
34		df-enq0 6407	. . . . . . . . . 10 |- ~Q0 = { <.x , y >. | ((x e. ( om X. N.) /\ y e. ( om X. N.)) /\ E. aE. bE. sE. t((x = <. a , b >. /\ y = <. s , t >.) /\ ( a .o t) = ( b .o s))) }
35	2, 19, 26, 33, 34	brab 4000	. . . . . . . . 9 |- (g ~Q0 h <-> ((g e. ( om X. N.) /\ h e. ( om X. N.)) /\ E. aE. bE. sE. t((g = <. a , b >. /\ h = <. s , t >.) /\ ( a .o t) = ( b .o s))))
36	18, 35	anbi12i 433	. . . . . . . 8 |- ((f ~Q0 g /\ g ~Q0 h) <-> (((f e. ( om X. N.) /\ g e. ( om X. N.)) /\ E.zE.wE.vE.u((f = <.z , w >. /\ g = <.v , u >.) /\ (z .o u) = (w .o v))) /\ ((g e. ( om X. N.) /\ h e. ( om X. N.)) /\ E. aE. bE. sE. t((g = <. a , b >. /\ h = <. s , t >.) /\ ( a .o t) = ( b .o s)))))
37	36	biimpi 113	. . . . . . 7 |- ((f ~Q0 g /\ g ~Q0 h) -> (((f e. ( om X. N.) /\ g e. ( om X. N.)) /\ E.zE.wE.vE.u((f = <.z , w >. /\ g = <.v , u >.) /\ (z .o u) = (w .o v))) /\ ((g e. ( om X. N.) /\ h e. ( om X. N.)) /\ E. aE. bE. sE. t((g = <. a , b >. /\ h = <. s , t >.) /\ ( a .o t) = ( b .o s)))))
38		an4 520	. . . . . . 7 |- ((((f e. ( om X. N.) /\ g e. ( om X. N.)) /\ E.zE.wE.vE.u((f = <.z , w >. /\ g = <.v , u >.) /\ (z .o u) = (w .o v))) /\ ((g e. ( om X. N.) /\ h e. ( om X. N.)) /\ E. aE. bE. sE. t((g = <. a , b >. /\ h = <. s , t >.) /\ ( a .o t) = ( b .o s)))) <-> (((f e. ( om X. N.) /\ g e. ( om X. N.)) /\ (g e. ( om X. N.) /\ h e. ( om X. N.))) /\ (E.zE.wE.vE.u((f = <.z , w >. /\ g = <.v , u >.) /\ (z .o u) = (w .o v)) /\ E. aE. bE. sE. t((g = <. a , b >. /\ h = <. s , t >.) /\ ( a .o t) = ( b .o s)))))
39	37, 38	sylib 127	. . . . . 6 |- ((f ~Q0 g /\ g ~Q0 h) -> (((f e. ( om X. N.) /\ g e. ( om X. N.)) /\ (g e. ( om X. N.) /\ h e. ( om X. N.))) /\ (E.zE.wE.vE.u((f = <.z , w >. /\ g = <.v , u >.) /\ (z .o u) = (w .o v)) /\ E. aE. bE. sE. t((g = <. a , b >. /\ h = <. s , t >.) /\ ( a .o t) = ( b .o s)))))
40		3anass 888	. . . . . . . 8 |- ((f e. ( om X. N.) /\ g e. ( om X. N.) /\ h e. ( om X. N.)) <-> (f e. ( om X. N.) /\ (g e. ( om X. N.) /\ h e. ( om X. N.))))
41		anass 381	. . . . . . . . 9 |- (((f e. ( om X. N.) /\ g e. ( om X. N.)) /\ (g e. ( om X. N.) /\ h e. ( om X. N.))) <-> (f e. ( om X. N.) /\ (g e. ( om X. N.) /\ (g e. ( om X. N.) /\ h e. ( om X. N.)))))
42		anass 381	. . . . . . . . . 10 |- (((g e. ( om X. N.) /\ g e. ( om X. N.)) /\ h e. ( om X. N.)) <-> (g e. ( om X. N.) /\ (g e. ( om X. N.) /\ h e. ( om X. N.))))
43	42	anbi2i 430	. . . . . . . . 9 |- ((f e. ( om X. N.) /\ ((g e. ( om X. N.) /\ g e. ( om X. N.)) /\ h e. ( om X. N.))) <-> (f e. ( om X. N.) /\ (g e. ( om X. N.) /\ (g e. ( om X. N.) /\ h e. ( om X. N.)))))
44		anidm 376	. . . . . . . . . . 11 |- ((g e. ( om X. N.) /\ g e. ( om X. N.)) <-> g e. ( om X. N.))
45	44	anbi1i 431	. . . . . . . . . 10 |- (((g e. ( om X. N.) /\ g e. ( om X. N.)) /\ h e. ( om X. N.)) <-> (g e. ( om X. N.) /\ h e. ( om X. N.)))
46	45	anbi2i 430	. . . . . . . . 9 |- ((f e. ( om X. N.) /\ ((g e. ( om X. N.) /\ g e. ( om X. N.)) /\ h e. ( om X. N.))) <-> (f e. ( om X. N.) /\ (g e. ( om X. N.) /\ h e. ( om X. N.))))
47	41, 43, 46	3bitr2i 197	. . . . . . . 8 |- (((f e. ( om X. N.) /\ g e. ( om X. N.)) /\ (g e. ( om X. N.) /\ h e. ( om X. N.))) <-> (f e. ( om X. N.) /\ (g e. ( om X. N.) /\ h e. ( om X. N.))))
48	40, 47	bitr4i 176	. . . . . . 7 |- ((f e. ( om X. N.) /\ g e. ( om X. N.) /\ h e. ( om X. N.)) <-> ((f e. ( om X. N.) /\ g e. ( om X. N.)) /\ (g e. ( om X. N.) /\ h e. ( om X. N.))))
49	48	anbi1i 431	. . . . . 6 |- (((f e. ( om X. N.) /\ g e. ( om X. N.) /\ h e. ( om X. N.)) /\ (E.zE.wE.vE.u((f = <.z , w >. /\ g = <.v , u >.) /\ (z .o u) = (w .o v)) /\ E. aE. bE. sE. t((g = <. a , b >. /\ h = <. s , t >.) /\ ( a .o t) = ( b .o s)))) <-> (((f e. ( om X. N.) /\ g e. ( om X. N.)) /\ (g e. ( om X. N.) /\ h e. ( om X. N.))) /\ (E.zE.wE.vE.u((f = <.z , w >. /\ g = <.v , u >.) /\ (z .o u) = (w .o v)) /\ E. aE. bE. sE. t((g = <. a , b >. /\ h = <. s , t >.) /\ ( a .o t) = ( b .o s)))))
50	39, 49	sylibr 137	. . . . 5 |- ((f ~Q0 g /\ g ~Q0 h) -> ((f e. ( om X. N.) /\ g e. ( om X. N.) /\ h e. ( om X. N.)) /\ (E.zE.wE.vE.u((f = <.z , w >. /\ g = <.v , u >.) /\ (z .o u) = (w .o v)) /\ E. aE. bE. sE. t((g = <. a , b >. /\ h = <. s , t >.) /\ ( a .o t) = ( b .o s)))))
51		ee8anv 1807	. . . . . 6 |- (E.zE.wE.vE.uE. aE. bE. sE. t(((f = <.z , w >. /\ g = <.v , u >.) /\ (z .o u) = (w .o v)) /\ ((g = <. a , b >. /\ h = <. s , t >.) /\ ( a .o t) = ( b .o s))) <-> (E.zE.wE.vE.u((f = <.z , w >. /\ g = <.v , u >.) /\ (z .o u) = (w .o v)) /\ E. aE. bE. sE. t((g = <. a , b >. /\ h = <. s , t >.) /\ ( a .o t) = ( b .o s))))
52	51	anbi2i 430	. . . . 5 |- (((f e. ( om X. N.) /\ g e. ( om X. N.) /\ h e. ( om X. N.)) /\ E.zE.wE.vE.uE. aE. bE. sE. t(((f = <.z , w >. /\ g = <.v , u >.) /\ (z .o u) = (w .o v)) /\ ((g = <. a , b >. /\ h = <. s , t >.) /\ ( a .o t) = ( b .o s)))) <-> ((f e. ( om X. N.) /\ g e. ( om X. N.) /\ h e. ( om X. N.)) /\ (E.zE.wE.vE.u((f = <.z , w >. /\ g = <.v , u >.) /\ (z .o u) = (w .o v)) /\ E. aE. bE. sE. t((g = <. a , b >. /\ h = <. s , t >.) /\ ( a .o t) = ( b .o s)))))
53	50, 52	sylibr 137	. . . 4 |- ((f ~Q0 g /\ g ~Q0 h) -> ((f e. ( om X. N.) /\ g e. ( om X. N.) /\ h e. ( om X. N.)) /\ E.zE.wE.vE.uE. aE. bE. sE. t(((f = <.z , w >. /\ g = <.v , u >.) /\ (z .o u) = (w .o v)) /\ ((g = <. a , b >. /\ h = <. s , t >.) /\ ( a .o t) = ( b .o s)))))
54		19.42vvvv 1787	. . . . . . 7 |- (E. aE. bE. sE. t((f e. ( om X. N.) /\ g e. ( om X. N.) /\ h e. ( om X. N.)) /\ (((f = <.z , w >. /\ g = <.v , u >.) /\ (z .o u) = (w .o v)) /\ ((g = <. a , b >. /\ h = <. s , t >.) /\ ( a .o t) = ( b .o s)))) <-> ((f e. ( om X. N.) /\ g e. ( om X. N.) /\ h e. ( om X. N.)) /\ E. aE. bE. sE. t(((f = <.z , w >. /\ g = <.v , u >.) /\ (z .o u) = (w .o v)) /\ ((g = <. a , b >. /\ h = <. s , t >.) /\ ( a .o t) = ( b .o s)))))
55	54	2exbii 1494	. . . . . 6 |- (E.vE.uE. aE. bE. sE. t((f e. ( om X. N.) /\ g e. ( om X. N.) /\ h e. ( om X. N.)) /\ (((f = <.z , w >. /\ g = <.v , u >.) /\ (z .o u) = (w .o v)) /\ ((g = <. a , b >. /\ h = <. s , t >.) /\ ( a .o t) = ( b .o s)))) <-> E.vE.u((f e. ( om X. N.) /\ g e. ( om X. N.) /\ h e. ( om X. N.)) /\ E. aE. bE. sE. t(((f = <.z , w >. /\ g = <.v , u >.) /\ (z .o u) = (w .o v)) /\ ((g = <. a , b >. /\ h = <. s , t >.) /\ ( a .o t) = ( b .o s)))))
56	55	2exbii 1494	. . . . 5 |- (E.zE.wE.vE.uE. aE. bE. sE. t((f e. ( om X. N.) /\ g e. ( om X. N.) /\ h e. ( om X. N.)) /\ (((f = <.z , w >. /\ g = <.v , u >.) /\ (z .o u) = (w .o v)) /\ ((g = <. a , b >. /\ h = <. s , t >.) /\ ( a .o t) = ( b .o s)))) <-> E.zE.wE.vE.u((f e. ( om X. N.) /\ g e. ( om X. N.) /\ h e. ( om X. N.)) /\ E. aE. bE. sE. t(((f = <.z , w >. /\ g = <.v , u >.) /\ (z .o u) = (w .o v)) /\ ((g = <. a , b >. /\ h = <. s , t >.) /\ ( a .o t) = ( b .o s)))))
57		19.42vvvv 1787	. . . . 5 |- (E.zE.wE.vE.u((f e. ( om X. N.) /\ g e. ( om X. N.) /\ h e. ( om X. N.)) /\ E. aE. bE. sE. t(((f = <.z , w >. /\ g = <.v , u >.) /\ (z .o u) = (w .o v)) /\ ((g = <. a , b >. /\ h = <. s , t >.) /\ ( a .o t) = ( b .o s)))) <-> ((f e. ( om X. N.) /\ g e. ( om X. N.) /\ h e. ( om X. N.)) /\ E.zE.wE.vE.uE. aE. bE. sE. t(((f = <.z , w >. /\ g = <.v , u >.) /\ (z .o u) = (w .o v)) /\ ((g = <. a , b >. /\ h = <. s , t >.) /\ ( a .o t) = ( b .o s)))))
58	56, 57	bitri 173	. . . 4 |- (E.zE.wE.vE.uE. aE. bE. sE. t((f e. ( om X. N.) /\ g e. ( om X. N.) /\ h e. ( om X. N.)) /\ (((f = <.z , w >. /\ g = <.v , u >.) /\ (z .o u) = (w .o v)) /\ ((g = <. a , b >. /\ h = <. s , t >.) /\ ( a .o t) = ( b .o s)))) <-> ((f e. ( om X. N.) /\ g e. ( om X. N.) /\ h e. ( om X. N.)) /\ E.zE.wE.vE.uE. aE. bE. sE. t(((f = <.z , w >. /\ g = <.v , u >.) /\ (z .o u) = (w .o v)) /\ ((g = <. a , b >. /\ h = <. s , t >.) /\ ( a .o t) = ( b .o s)))))
59	53, 58	sylibr 137	. . 3 |- ((f ~Q0 g /\ g ~Q0 h) -> E.zE.wE.vE.uE. aE. bE. sE. t((f e. ( om X. N.) /\ g e. ( om X. N.) /\ h e. ( om X. N.)) /\ (((f = <.z , w >. /\ g = <.v , u >.) /\ (z .o u) = (w .o v)) /\ ((g = <. a , b >. /\ h = <. s , t >.) /\ ( a .o t) = ( b .o s)))))
60		3simpb 901	. . . . . . . . 9 |- ((f e. ( om X. N.) /\ g e. ( om X. N.) /\ h e. ( om X. N.)) -> (f e. ( om X. N.) /\ h e. ( om X. N.)))
61	60	adantr 261	. . . . . . . 8 |- (((f e. ( om X. N.) /\ g e. ( om X. N.) /\ h e. ( om X. N.)) /\ (((f = <.z , w >. /\ g = <.v , u >.) /\ (z .o u) = (w .o v)) /\ ((g = <. a , b >. /\ h = <. s , t >.) /\ ( a .o t) = ( b .o s)))) -> (f e. ( om X. N.) /\ h e. ( om X. N.)))
62		simplll 485	. . . . . . . . . 10 |- ((((f = <.z , w >. /\ g = <.v , u >.) /\ (z .o u) = (w .o v)) /\ ((g = <. a , b >. /\ h = <. s , t >.) /\ ( a .o t) = ( b .o s))) -> f = <.z , w >.)
63		simprlr 490	. . . . . . . . . 10 |- ((((f = <.z , w >. /\ g = <.v , u >.) /\ (z .o u) = (w .o v)) /\ ((g = <. a , b >. /\ h = <. s , t >.) /\ ( a .o t) = ( b .o s))) -> h = <. s , t >.)
64	62, 63	jca 290	. . . . . . . . 9 |- ((((f = <.z , w >. /\ g = <.v , u >.) /\ (z .o u) = (w .o v)) /\ ((g = <. a , b >. /\ h = <. s , t >.) /\ ( a .o t) = ( b .o s))) -> (f = <.z , w >. /\ h = <. s , t >.))
65	64	adantl 262	. . . . . . . 8 |- (((f e. ( om X. N.) /\ g e. ( om X. N.) /\ h e. ( om X. N.)) /\ (((f = <.z , w >. /\ g = <.v , u >.) /\ (z .o u) = (w .o v)) /\ ((g = <. a , b >. /\ h = <. s , t >.) /\ ( a .o t) = ( b .o s)))) -> (f = <.z , w >. /\ h = <. s , t >.))
66		oveq1 5462	. . . . . . . . . . . . . . . 16 |- (v = (/) -> (v .o t) = ( (/) .o t))
67	63	adantl 262	. . . . . . . . . . . . . . . . . . . . . 22 |- (((f e. ( om X. N.) /\ g e. ( om X. N.) /\ h e. ( om X. N.)) /\ (((f = <.z , w >. /\ g = <.v , u >.) /\ (z .o u) = (w .o v)) /\ ((g = <. a , b >. /\ h = <. s , t >.) /\ ( a .o t) = ( b .o s)))) -> h = <. s , t >.)
68		simpl3 908	. . . . . . . . . . . . . . . . . . . . . 22 |- (((f e. ( om X. N.) /\ g e. ( om X. N.) /\ h e. ( om X. N.)) /\ (((f = <.z , w >. /\ g = <.v , u >.) /\ (z .o u) = (w .o v)) /\ ((g = <. a , b >. /\ h = <. s , t >.) /\ ( a .o t) = ( b .o s)))) -> h e. ( om X. N.))
69	67, 68	eqeltrrd 2112	. . . . . . . . . . . . . . . . . . . . 21 |- (((f e. ( om X. N.) /\ g e. ( om X. N.) /\ h e. ( om X. N.)) /\ (((f = <.z , w >. /\ g = <.v , u >.) /\ (z .o u) = (w .o v)) /\ ((g = <. a , b >. /\ h = <. s , t >.) /\ ( a .o t) = ( b .o s)))) -> <. s , t >. e. ( om X. N.))
70		opelxp 4317	. . . . . . . . . . . . . . . . . . . . 21 |- ( <. s , t >. e. ( om X. N.) <-> ( s e. om /\ t e. N.))
71	69, 70	sylib 127	. . . . . . . . . . . . . . . . . . . 20 |- (((f e. ( om X. N.) /\ g e. ( om X. N.) /\ h e. ( om X. N.)) /\ (((f = <.z , w >. /\ g = <.v , u >.) /\ (z .o u) = (w .o v)) /\ ((g = <. a , b >. /\ h = <. s , t >.) /\ ( a .o t) = ( b .o s)))) -> ( s e. om /\ t e. N.))
72	71	simprd 107	. . . . . . . . . . . . . . . . . . 19 |- (((f e. ( om X. N.) /\ g e. ( om X. N.) /\ h e. ( om X. N.)) /\ (((f = <.z , w >. /\ g = <.v , u >.) /\ (z .o u) = (w .o v)) /\ ((g = <. a , b >. /\ h = <. s , t >.) /\ ( a .o t) = ( b .o s)))) -> t e. N.)
73		pinn 6293	. . . . . . . . . . . . . . . . . . 19 |- ( t e. N. -> t e. om)
74	72, 73	syl 14	. . . . . . . . . . . . . . . . . 18 |- (((f e. ( om X. N.) /\ g e. ( om X. N.) /\ h e. ( om X. N.)) /\ (((f = <.z , w >. /\ g = <.v , u >.) /\ (z .o u) = (w .o v)) /\ ((g = <. a , b >. /\ h = <. s , t >.) /\ ( a .o t) = ( b .o s)))) -> t e. om)
75		nnm0r 5997	. . . . . . . . . . . . . . . . . 18 |- ( t e. om -> ( (/) .o t) = (/))
76	74, 75	syl 14	. . . . . . . . . . . . . . . . 17 |- (((f e. ( om X. N.) /\ g e. ( om X. N.) /\ h e. ( om X. N.)) /\ (((f = <.z , w >. /\ g = <.v , u >.) /\ (z .o u) = (w .o v)) /\ ((g = <. a , b >. /\ h = <. s , t >.) /\ ( a .o t) = ( b .o s)))) -> ( (/) .o t) = (/))
77	76	eqeq2d 2048	. . . . . . . . . . . . . . . 16 |- (((f e. ( om X. N.) /\ g e. ( om X. N.) /\ h e. ( om X. N.)) /\ (((f = <.z , w >. /\ g = <.v , u >.) /\ (z .o u) = (w .o v)) /\ ((g = <. a , b >. /\ h = <. s , t >.) /\ ( a .o t) = ( b .o s)))) -> ((v .o t) = ( (/) .o t) <-> (v .o t) = (/)))
78	66, 77	syl5ib 143	. . . . . . . . . . . . . . 15 |- (((f e. ( om X. N.) /\ g e. ( om X. N.) /\ h e. ( om X. N.)) /\ (((f = <.z , w >. /\ g = <.v , u >.) /\ (z .o u) = (w .o v)) /\ ((g = <. a , b >. /\ h = <. s , t >.) /\ ( a .o t) = ( b .o s)))) -> (v = (/) -> (v .o t) = (/)))
79		simprr 484	. . . . . . . . . . . . . . . . . 18 |- ((((f = <.z , w >. /\ g = <.v , u >.) /\ (z .o u) = (w .o v)) /\ ((g = <. a , b >. /\ h = <. s , t >.) /\ ( a .o t) = ( b .o s))) -> ( a .o t) = ( b .o s))
80		eqtr2 2055	. . . . . . . . . . . . . . . . . . . . . 22 |- ((g = <.v , u >. /\ g = <. a , b >.) -> <.v , u >. = <. a , b >.)
81		vex 2554	. . . . . . . . . . . . . . . . . . . . . . 23 |- v e. _V
82		vex 2554	. . . . . . . . . . . . . . . . . . . . . . 23 |- u e. _V
83	81, 82	opth 3965	. . . . . . . . . . . . . . . . . . . . . 22 |- ( <.v , u >. = <. a , b >. <-> (v = a /\ u = b))
84	80, 83	sylib 127	. . . . . . . . . . . . . . . . . . . . 21 |- ((g = <.v , u >. /\ g = <. a , b >.) -> (v = a /\ u = b))
85		oveq1 5462	. . . . . . . . . . . . . . . . . . . . . 22 |- (v = a -> (v .o t) = ( a .o t))
86		oveq1 5462	. . . . . . . . . . . . . . . . . . . . . 22 |- (u = b -> (u .o s) = ( b .o s))
87	85, 86	eqeqan12d 2052	. . . . . . . . . . . . . . . . . . . . 21 |- ((v = a /\ u = b) -> ((v .o t) = (u .o s) <-> ( a .o t) = ( b .o s)))
88	84, 87	syl 14	. . . . . . . . . . . . . . . . . . . 20 |- ((g = <.v , u >. /\ g = <. a , b >.) -> ((v .o t) = (u .o s) <-> ( a .o t) = ( b .o s)))
89	88	ad2ant2lr 479	. . . . . . . . . . . . . . . . . . 19 |- (((f = <.z , w >. /\ g = <.v , u >.) /\ (g = <. a , b >. /\ h = <. s , t >.)) -> ((v .o t) = (u .o s) <-> ( a .o t) = ( b .o s)))
90	89	ad2ant2r 478	. . . . . . . . . . . . . . . . . 18 |- ((((f = <.z , w >. /\ g = <.v , u >.) /\ (z .o u) = (w .o v)) /\ ((g = <. a , b >. /\ h = <. s , t >.) /\ ( a .o t) = ( b .o s))) -> ((v .o t) = (u .o s) <-> ( a .o t) = ( b .o s)))
91	79, 90	mpbird 156	. . . . . . . . . . . . . . . . 17 |- ((((f = <.z , w >. /\ g = <.v , u >.) /\ (z .o u) = (w .o v)) /\ ((g = <. a , b >. /\ h = <. s , t >.) /\ ( a .o t) = ( b .o s))) -> (v .o t) = (u .o s))
92	91	eqeq1d 2045	. . . . . . . . . . . . . . . 16 |- ((((f = <.z , w >. /\ g = <.v , u >.) /\ (z .o u) = (w .o v)) /\ ((g = <. a , b >. /\ h = <. s , t >.) /\ ( a .o t) = ( b .o s))) -> ((v .o t) = (/) <-> (u .o s) = (/)))
93	92	adantl 262	. . . . . . . . . . . . . . 15 |- (((f e. ( om X. N.) /\ g e. ( om X. N.) /\ h e. ( om X. N.)) /\ (((f = <.z , w >. /\ g = <.v , u >.) /\ (z .o u) = (w .o v)) /\ ((g = <. a , b >. /\ h = <. s , t >.) /\ ( a .o t) = ( b .o s)))) -> ((v .o t) = (/) <-> (u .o s) = (/)))
94	78, 93	sylibd 138	. . . . . . . . . . . . . 14 |- (((f e. ( om X. N.) /\ g e. ( om X. N.) /\ h e. ( om X. N.)) /\ (((f = <.z , w >. /\ g = <.v , u >.) /\ (z .o u) = (w .o v)) /\ ((g = <. a , b >. /\ h = <. s , t >.) /\ ( a .o t) = ( b .o s)))) -> (v = (/) -> (u .o s) = (/)))
95		simpllr 486	. . . . . . . . . . . . . . . . . . . 20 |- ((((f = <.z , w >. /\ g = <.v , u >.) /\ (z .o u) = (w .o v)) /\ ((g = <. a , b >. /\ h = <. s , t >.) /\ ( a .o t) = ( b .o s))) -> g = <.v , u >.)
96	95	adantl 262	. . . . . . . . . . . . . . . . . . 19 |- (((f e. ( om X. N.) /\ g e. ( om X. N.) /\ h e. ( om X. N.)) /\ (((f = <.z , w >. /\ g = <.v , u >.) /\ (z .o u) = (w .o v)) /\ ((g = <. a , b >. /\ h = <. s , t >.) /\ ( a .o t) = ( b .o s)))) -> g = <.v , u >.)
97		simpl2 907	. . . . . . . . . . . . . . . . . . 19 |- (((f e. ( om X. N.) /\ g e. ( om X. N.) /\ h e. ( om X. N.)) /\ (((f = <.z , w >. /\ g = <.v , u >.) /\ (z .o u) = (w .o v)) /\ ((g = <. a , b >. /\ h = <. s , t >.) /\ ( a .o t) = ( b .o s)))) -> g e. ( om X. N.))
98	96, 97	eqeltrrd 2112	. . . . . . . . . . . . . . . . . 18 |- (((f e. ( om X. N.) /\ g e. ( om X. N.) /\ h e. ( om X. N.)) /\ (((f = <.z , w >. /\ g = <.v , u >.) /\ (z .o u) = (w .o v)) /\ ((g = <. a , b >. /\ h = <. s , t >.) /\ ( a .o t) = ( b .o s)))) -> <.v , u >. e. ( om X. N.))
99		opelxp 4317	. . . . . . . . . . . . . . . . . 18 |- ( <.v , u >. e. ( om X. N.) <-> (v e. om /\ u e. N.))
100	98, 99	sylib 127	. . . . . . . . . . . . . . . . 17 |- (((f e. ( om X. N.) /\ g e. ( om X. N.) /\ h e. ( om X. N.)) /\ (((f = <.z , w >. /\ g = <.v , u >.) /\ (z .o u) = (w .o v)) /\ ((g = <. a , b >. /\ h = <. s , t >.) /\ ( a .o t) = ( b .o s)))) -> (v e. om /\ u e. N.))
101	100	simprd 107	. . . . . . . . . . . . . . . 16 |- (((f e. ( om X. N.) /\ g e. ( om X. N.) /\ h e. ( om X. N.)) /\ (((f = <.z , w >. /\ g = <.v , u >.) /\ (z .o u) = (w .o v)) /\ ((g = <. a , b >. /\ h = <. s , t >.) /\ ( a .o t) = ( b .o s)))) -> u e. N.)
102		pinn 6293	. . . . . . . . . . . . . . . 16 |- (u e. N. -> u e. om)
103	101, 102	syl 14	. . . . . . . . . . . . . . 15 |- (((f e. ( om X. N.) /\ g e. ( om X. N.) /\ h e. ( om X. N.)) /\ (((f = <.z , w >. /\ g = <.v , u >.) /\ (z .o u) = (w .o v)) /\ ((g = <. a , b >. /\ h = <. s , t >.) /\ ( a .o t) = ( b .o s)))) -> u e. om)
104	71	simpld 105	. . . . . . . . . . . . . . 15 |- (((f e. ( om X. N.) /\ g e. ( om X. N.) /\ h e. ( om X. N.)) /\ (((f = <.z , w >. /\ g = <.v , u >.) /\ (z .o u) = (w .o v)) /\ ((g = <. a , b >. /\ h = <. s , t >.) /\ ( a .o t) = ( b .o s)))) -> s e. om)
105		nnm00 6038	. . . . . . . . . . . . . . 15 |- ((u e. om /\ s e. om) -> ((u .o s) = (/) <-> (u = (/) \/ s = (/))))
106	103, 104, 105	syl2anc 391	. . . . . . . . . . . . . 14 |- (((f e. ( om X. N.) /\ g e. ( om X. N.) /\ h e. ( om X. N.)) /\ (((f = <.z , w >. /\ g = <.v , u >.) /\ (z .o u) = (w .o v)) /\ ((g = <. a , b >. /\ h = <. s , t >.) /\ ( a .o t) = ( b .o s)))) -> ((u .o s) = (/) <-> (u = (/) \/ s = (/))))
107	94, 106	sylibd 138	. . . . . . . . . . . . 13 |- (((f e. ( om X. N.) /\ g e. ( om X. N.) /\ h e. ( om X. N.)) /\ (((f = <.z , w >. /\ g = <.v , u >.) /\ (z .o u) = (w .o v)) /\ ((g = <. a , b >. /\ h = <. s , t >.) /\ ( a .o t) = ( b .o s)))) -> (v = (/) -> (u = (/) \/ s = (/))))
108		elni2 6298	. . . . . . . . . . . . . . . 16 |- (u e. N. <-> (u e. om /\ (/) e. u))
109	108	simprbi 260	. . . . . . . . . . . . . . 15 |- (u e. N. -> (/) e. u)
110	101, 109	syl 14	. . . . . . . . . . . . . 14 |- (((f e. ( om X. N.) /\ g e. ( om X. N.) /\ h e. ( om X. N.)) /\ (((f = <.z , w >. /\ g = <.v , u >.) /\ (z .o u) = (w .o v)) /\ ((g = <. a , b >. /\ h = <. s , t >.) /\ ( a .o t) = ( b .o s)))) -> (/) e. u)
111		n0i 3223	. . . . . . . . . . . . . 14 |- ( (/) e. u -> -. u = (/))
112		biorf 662	. . . . . . . . . . . . . 14 |- (-. u = (/) -> ( s = (/) <-> (u = (/) \/ s = (/))))
113	110, 111, 112	3syl 17	. . . . . . . . . . . . 13 |- (((f e. ( om X. N.) /\ g e. ( om X. N.) /\ h e. ( om X. N.)) /\ (((f = <.z , w >. /\ g = <.v , u >.) /\ (z .o u) = (w .o v)) /\ ((g = <. a , b >. /\ h = <. s , t >.) /\ ( a .o t) = ( b .o s)))) -> ( s = (/) <-> (u = (/) \/ s = (/))))
114	107, 113	sylibrd 158	. . . . . . . . . . . 12 |- (((f e. ( om X. N.) /\ g e. ( om X. N.) /\ h e. ( om X. N.)) /\ (((f = <.z , w >. /\ g = <.v , u >.) /\ (z .o u) = (w .o v)) /\ ((g = <. a , b >. /\ h = <. s , t >.) /\ ( a .o t) = ( b .o s)))) -> (v = (/) -> s = (/)))
115	62	adantl 262	. . . . . . . . . . . . . . . . . 18 |- (((f e. ( om X. N.) /\ g e. ( om X. N.) /\ h e. ( om X. N.)) /\ (((f = <.z , w >. /\ g = <.v , u >.) /\ (z .o u) = (w .o v)) /\ ((g = <. a , b >. /\ h = <. s , t >.) /\ ( a .o t) = ( b .o s)))) -> f = <.z , w >.)
116		simpl1 906	. . . . . . . . . . . . . . . . . 18 |- (((f e. ( om X. N.) /\ g e. ( om X. N.) /\ h e. ( om X. N.)) /\ (((f = <.z , w >. /\ g = <.v , u >.) /\ (z .o u) = (w .o v)) /\ ((g = <. a , b >. /\ h = <. s , t >.) /\ ( a .o t) = ( b .o s)))) -> f e. ( om X. N.))
117	115, 116	eqeltrrd 2112	. . . . . . . . . . . . . . . . 17 |- (((f e. ( om X. N.) /\ g e. ( om X. N.) /\ h e. ( om X. N.)) /\ (((f = <.z , w >. /\ g = <.v , u >.) /\ (z .o u) = (w .o v)) /\ ((g = <. a , b >. /\ h = <. s , t >.) /\ ( a .o t) = ( b .o s)))) -> <.z , w >. e. ( om X. N.))
118		opelxp 4317	. . . . . . . . . . . . . . . . 17 |- ( <.z , w >. e. ( om X. N.) <-> (z e. om /\ w e. N.))
119	117, 118	sylib 127	. . . . . . . . . . . . . . . 16 |- (((f e. ( om X. N.) /\ g e. ( om X. N.) /\ h e. ( om X. N.)) /\ (((f = <.z , w >. /\ g = <.v , u >.) /\ (z .o u) = (w .o v)) /\ ((g = <. a , b >. /\ h = <. s , t >.) /\ ( a .o t) = ( b .o s)))) -> (z e. om /\ w e. N.))
120	119	simprd 107	. . . . . . . . . . . . . . 15 |- (((f e. ( om X. N.) /\ g e. ( om X. N.) /\ h e. ( om X. N.)) /\ (((f = <.z , w >. /\ g = <.v , u >.) /\ (z .o u) = (w .o v)) /\ ((g = <. a , b >. /\ h = <. s , t >.) /\ ( a .o t) = ( b .o s)))) -> w e. N.)
121		pinn 6293	. . . . . . . . . . . . . . 15 |- (w e. N. -> w e. om)
122	120, 121	syl 14	. . . . . . . . . . . . . 14 |- (((f e. ( om X. N.) /\ g e. ( om X. N.) /\ h e. ( om X. N.)) /\ (((f = <.z , w >. /\ g = <.v , u >.) /\ (z .o u) = (w .o v)) /\ ((g = <. a , b >. /\ h = <. s , t >.) /\ ( a .o t) = ( b .o s)))) -> w e. om)
123		nnm0 5993	. . . . . . . . . . . . . 14 |- (w e. om -> (w .o (/)) = (/))
124	122, 123	syl 14	. . . . . . . . . . . . 13 |- (((f e. ( om X. N.) /\ g e. ( om X. N.) /\ h e. ( om X. N.)) /\ (((f = <.z , w >. /\ g = <.v , u >.) /\ (z .o u) = (w .o v)) /\ ((g = <. a , b >. /\ h = <. s , t >.) /\ ( a .o t) = ( b .o s)))) -> (w .o (/)) = (/))
125		oveq2 5463	. . . . . . . . . . . . . 14 |- ( s = (/) -> (w .o s) = (w .o (/)))
126	125	eqeq1d 2045	. . . . . . . . . . . . 13 |- ( s = (/) -> ((w .o s) = (/) <-> (w .o (/)) = (/)))
127	124, 126	syl5ibrcom 146	. . . . . . . . . . . 12 |- (((f e. ( om X. N.) /\ g e. ( om X. N.) /\ h e. ( om X. N.)) /\ (((f = <.z , w >. /\ g = <.v , u >.) /\ (z .o u) = (w .o v)) /\ ((g = <. a , b >. /\ h = <. s , t >.) /\ ( a .o t) = ( b .o s)))) -> ( s = (/) -> (w .o s) = (/)))
128	114, 127	syld 40	. . . . . . . . . . 11 |- (((f e. ( om X. N.) /\ g e. ( om X. N.) /\ h e. ( om X. N.)) /\ (((f = <.z , w >. /\ g = <.v , u >.) /\ (z .o u) = (w .o v)) /\ ((g = <. a , b >. /\ h = <. s , t >.) /\ ( a .o t) = ( b .o s)))) -> (v = (/) -> (w .o s) = (/)))
129		oveq2 5463	. . . . . . . . . . . . . . . 16 |- (v = (/) -> (w .o v) = (w .o (/)))
130	124	eqeq2d 2048	. . . . . . . . . . . . . . . 16 |- (((f e. ( om X. N.) /\ g e. ( om X. N.) /\ h e. ( om X. N.)) /\ (((f = <.z , w >. /\ g = <.v , u >.) /\ (z .o u) = (w .o v)) /\ ((g = <. a , b >. /\ h = <. s , t >.) /\ ( a .o t) = ( b .o s)))) -> ((w .o v) = (w .o (/)) <-> (w .o v) = (/)))
131	129, 130	syl5ib 143	. . . . . . . . . . . . . . 15 |- (((f e. ( om X. N.) /\ g e. ( om X. N.) /\ h e. ( om X. N.)) /\ (((f = <.z , w >. /\ g = <.v , u >.) /\ (z .o u) = (w .o v)) /\ ((g = <. a , b >. /\ h = <. s , t >.) /\ ( a .o t) = ( b .o s)))) -> (v = (/) -> (w .o v) = (/)))
132		simprlr 490	. . . . . . . . . . . . . . . 16 |- (((f e. ( om X. N.) /\ g e. ( om X. N.) /\ h e. ( om X. N.)) /\ (((f = <.z , w >. /\ g = <.v , u >.) /\ (z .o u) = (w .o v)) /\ ((g = <. a , b >. /\ h = <. s , t >.) /\ ( a .o t) = ( b .o s)))) -> (z .o u) = (w .o v))
133	132	eqeq1d 2045	. . . . . . . . . . . . . . 15 |- (((f e. ( om X. N.) /\ g e. ( om X. N.) /\ h e. ( om X. N.)) /\ (((f = <.z , w >. /\ g = <.v , u >.) /\ (z .o u) = (w .o v)) /\ ((g = <. a , b >. /\ h = <. s , t >.) /\ ( a .o t) = ( b .o s)))) -> ((z .o u) = (/) <-> (w .o v) = (/)))
134	131, 133	sylibrd 158	. . . . . . . . . . . . . 14 |- (((f e. ( om X. N.) /\ g e. ( om X. N.) /\ h e. ( om X. N.)) /\ (((f = <.z , w >. /\ g = <.v , u >.) /\ (z .o u) = (w .o v)) /\ ((g = <. a , b >. /\ h = <. s , t >.) /\ ( a .o t) = ( b .o s)))) -> (v = (/) -> (z .o u) = (/)))
135	119	simpld 105	. . . . . . . . . . . . . . 15 |- (((f e. ( om X. N.) /\ g e. ( om X. N.) /\ h e. ( om X. N.)) /\ (((f = <.z , w >. /\ g = <.v , u >.) /\ (z .o u) = (w .o v)) /\ ((g = <. a , b >. /\ h = <. s , t >.) /\ ( a .o t) = ( b .o s)))) -> z e. om)
136		nnm00 6038	. . . . . . . . . . . . . . 15 |- ((z e. om /\ u e. om) -> ((z .o u) = (/) <-> (z = (/) \/ u = (/))))
137	135, 103, 136	syl2anc 391	. . . . . . . . . . . . . 14 |- (((f e. ( om X. N.) /\ g e. ( om X. N.) /\ h e. ( om X. N.)) /\ (((f = <.z , w >. /\ g = <.v , u >.) /\ (z .o u) = (w .o v)) /\ ((g = <. a , b >. /\ h = <. s , t >.) /\ ( a .o t) = ( b .o s)))) -> ((z .o u) = (/) <-> (z = (/) \/ u = (/))))
138	134, 137	sylibd 138	. . . . . . . . . . . . 13 |- (((f e. ( om X. N.) /\ g e. ( om X. N.) /\ h e. ( om X. N.)) /\ (((f = <.z , w >. /\ g = <.v , u >.) /\ (z .o u) = (w .o v)) /\ ((g = <. a , b >. /\ h = <. s , t >.) /\ ( a .o t) = ( b .o s)))) -> (v = (/) -> (z = (/) \/ u = (/))))
139		biorf 662	. . . . . . . . . . . . . . 15 |- (-. u = (/) -> (z = (/) <-> (u = (/) \/ z = (/))))
140		orcom 646	. . . . . . . . . . . . . . 15 |- ((u = (/) \/ z = (/)) <-> (z = (/) \/ u = (/)))
141	139, 140	syl6bb 185	. . . . . . . . . . . . . 14 |- (-. u = (/) -> (z = (/) <-> (z = (/) \/ u = (/))))
142	110, 111, 141	3syl 17	. . . . . . . . . . . . 13 |- (((f e. ( om X. N.) /\ g e. ( om X. N.) /\ h e. ( om X. N.)) /\ (((f = <.z , w >. /\ g = <.v , u >.) /\ (z .o u) = (w .o v)) /\ ((g = <. a , b >. /\ h = <. s , t >.) /\ ( a .o t) = ( b .o s)))) -> (z = (/) <-> (z = (/) \/ u = (/))))
143	138, 142	sylibrd 158	. . . . . . . . . . . 12 |- (((f e. ( om X. N.) /\ g e. ( om X. N.) /\ h e. ( om X. N.)) /\ (((f = <.z , w >. /\ g = <.v , u >.) /\ (z .o u) = (w .o v)) /\ ((g = <. a , b >. /\ h = <. s , t >.) /\ ( a .o t) = ( b .o s)))) -> (v = (/) -> z = (/)))
144		oveq1 5462	. . . . . . . . . . . . . 14 |- (z = (/) -> (z .o t) = ( (/) .o t))
145	144	eqeq1d 2045	. . . . . . . . . . . . 13 |- (z = (/) -> ((z .o t) = (/) <-> ( (/) .o t) = (/)))
146	76, 145	syl5ibrcom 146	. . . . . . . . . . . 12 |- (((f e. ( om X. N.) /\ g e. ( om X. N.) /\ h e. ( om X. N.)) /\ (((f = <.z , w >. /\ g = <.v , u >.) /\ (z .o u) = (w .o v)) /\ ((g = <. a , b >. /\ h = <. s , t >.) /\ ( a .o t) = ( b .o s)))) -> (z = (/) -> (z .o t) = (/)))
147	143, 146	syld 40	. . . . . . . . . . 11 |- (((f e. ( om X. N.) /\ g e. ( om X. N.) /\ h e. ( om X. N.)) /\ (((f = <.z , w >. /\ g = <.v , u >.) /\ (z .o u) = (w .o v)) /\ ((g = <. a , b >. /\ h = <. s , t >.) /\ ( a .o t) = ( b .o s)))) -> (v = (/) -> (z .o t) = (/)))
148	128, 147	jcad 291	. . . . . . . . . 10 |- (((f e. ( om X. N.) /\ g e. ( om X. N.) /\ h e. ( om X. N.)) /\ (((f = <.z , w >. /\ g = <.v , u >.) /\ (z .o u) = (w .o v)) /\ ((g = <. a , b >. /\ h = <. s , t >.) /\ ( a .o t) = ( b .o s)))) -> (v = (/) -> ((w .o s) = (/) /\ (z .o t) = (/))))
149		eqtr3 2056	. . . . . . . . . . 11 |- (((w .o s) = (/) /\ (z .o t) = (/)) -> (w .o s) = (z .o t))
150	149	eqcomd 2042	. . . . . . . . . 10 |- (((w .o s) = (/) /\ (z .o t) = (/)) -> (z .o t) = (w .o s))
151	148, 150	syl6 29	. . . . . . . . 9 |- (((f e. ( om X. N.) /\ g e. ( om X. N.) /\ h e. ( om X. N.)) /\ (((f = <.z , w >. /\ g = <.v , u >.) /\ (z .o u) = (w .o v)) /\ ((g = <. a , b >. /\ h = <. s , t >.) /\ ( a .o t) = ( b .o s)))) -> (v = (/) -> (z .o t) = (w .o s)))
152		simplr 482	. . . . . . . . . . . . . . . . 17 |- ((((f = <.z , w >. /\ g = <.v , u >.) /\ (z .o u) = (w .o v)) /\ ((g = <. a , b >. /\ h = <. s , t >.) /\ ( a .o t) = ( b .o s))) -> (z .o u) = (w .o v))
153	91, 152	oveq12d 5473	. . . . . . . . . . . . . . . 16 |- ((((f = <.z , w >. /\ g = <.v , u >.) /\ (z .o u) = (w .o v)) /\ ((g = <. a , b >. /\ h = <. s , t >.) /\ ( a .o t) = ( b .o s))) -> ((v .o t) .o (z .o u)) = ((u .o s) .o (w .o v)))
154	153	adantl 262	. . . . . . . . . . . . . . 15 |- (((f e. ( om X. N.) /\ g e. ( om X. N.) /\ h e. ( om X. N.)) /\ (((f = <.z , w >. /\ g = <.v , u >.) /\ (z .o u) = (w .o v)) /\ ((g = <. a , b >. /\ h = <. s , t >.) /\ ( a .o t) = ( b .o s)))) -> ((v .o t) .o (z .o u)) = ((u .o s) .o (w .o v)))
155	100	simpld 105	. . . . . . . . . . . . . . . . 17 |- (((f e. ( om X. N.) /\ g e. ( om X. N.) /\ h e. ( om X. N.)) /\ (((f = <.z , w >. /\ g = <.v , u >.) /\ (z .o u) = (w .o v)) /\ ((g = <. a , b >. /\ h = <. s , t >.) /\ ( a .o t) = ( b .o s)))) -> v e. om)
156		nnmcl 5999	. . . . . . . . . . . . . . . . 17 |- ((v e. om /\ t e. om) -> (v .o t) e. om)
157	155, 74, 156	syl2anc 391	. . . . . . . . . . . . . . . 16 |- (((f e. ( om X. N.) /\ g e. ( om X. N.) /\ h e. ( om X. N.)) /\ (((f = <.z , w >. /\ g = <.v , u >.) /\ (z .o u) = (w .o v)) /\ ((g = <. a , b >. /\ h = <. s , t >.) /\ ( a .o t) = ( b .o s)))) -> (v .o t) e. om)
158		nnmcom 6007	. . . . . . . . . . . . . . . . 17 |- (( c e. om /\ d e. om) -> ( c .o d) = ( d .o c))
159	158	adantl 262	. . . . . . . . . . . . . . . 16 |- ((((f e. ( om X. N.) /\ g e. ( om X. N.) /\ h e. ( om X. N.)) /\ (((f = <.z , w >. /\ g = <.v , u >.) /\ (z .o u) = (w .o v)) /\ ((g = <. a , b >. /\ h = <. s , t >.) /\ ( a .o t) = ( b .o s)))) /\ ( c e. om /\ d e. om)) -> ( c .o d) = ( d .o c))
160		nnmass 6005	. . . . . . . . . . . . . . . . 17 |- (( c e. om /\ d e. om /\ e e. om) -> (( c .o d) .o e) = ( c .o ( d .o e)))
161	160	adantl 262	. . . . . . . . . . . . . . . 16 |- ((((f e. ( om X. N.) /\ g e. ( om X. N.) /\ h e. ( om X. N.)) /\ (((f = <.z , w >. /\ g = <.v , u >.) /\ (z .o u) = (w .o v)) /\ ((g = <. a , b >. /\ h = <. s , t >.) /\ ( a .o t) = ( b .o s)))) /\ ( c e. om /\ d e. om /\ e e. om)) -> (( c .o d) .o e) = ( c .o ( d .o e)))
162	157, 135, 103, 159, 161	caov13d 5626	. . . . . . . . . . . . . . 15 |- (((f e. ( om X. N.) /\ g e. ( om X. N.) /\ h e. ( om X. N.)) /\ (((f = <.z , w >. /\ g = <.v , u >.) /\ (z .o u) = (w .o v)) /\ ((g = <. a , b >. /\ h = <. s , t >.) /\ ( a .o t) = ( b .o s)))) -> ((v .o t) .o (z .o u)) = (u .o (z .o (v .o t))))
163		nnmcl 5999	. . . . . . . . . . . . . . . . 17 |- ((w e. om /\ v e. om) -> (w .o v) e. om)
164	122, 155, 163	syl2anc 391	. . . . . . . . . . . . . . . 16 |- (((f e. ( om X. N.) /\ g e. ( om X. N.) /\ h e. ( om X. N.)) /\ (((f = <.z , w >. /\ g = <.v , u >.) /\ (z .o u) = (w .o v)) /\ ((g = <. a , b >. /\ h = <. s , t >.) /\ ( a .o t) = ( b .o s)))) -> (w .o v) e. om)
165	161, 103, 104, 164	caovassd 5602	. . . . . . . . . . . . . . 15 |- (((f e. ( om X. N.) /\ g e. ( om X. N.) /\ h e. ( om X. N.)) /\ (((f = <.z , w >. /\ g = <.v , u >.) /\ (z .o u) = (w .o v)) /\ ((g = <. a , b >. /\ h = <. s , t >.) /\ ( a .o t) = ( b .o s)))) -> ((u .o s) .o (w .o v)) = (u .o ( s .o (w .o v))))
166	154, 162, 165	3eqtr3d 2077	. . . . . . . . . . . . . 14 |- (((f e. ( om X. N.) /\ g e. ( om X. N.) /\ h e. ( om X. N.)) /\ (((f = <.z , w >. /\ g = <.v , u >.) /\ (z .o u) = (w .o v)) /\ ((g = <. a , b >. /\ h = <. s , t >.) /\ ( a .o t) = ( b .o s)))) -> (u .o (z .o (v .o t))) = (u .o ( s .o (w .o v))))
167		nnmcl 5999	. . . . . . . . . . . . . . . 16 |- ((z e. om /\ (v .o t) e. om) -> (z .o (v .o t)) e. om)
168	135, 157, 167	syl2anc 391	. . . . . . . . . . . . . . 15 |- (((f e. ( om X. N.) /\ g e. ( om X. N.) /\ h e. ( om X. N.)) /\ (((f = <.z , w >. /\ g = <.v , u >.) /\ (z .o u) = (w .o v)) /\ ((g = <. a , b >. /\ h = <. s , t >.) /\ ( a .o t) = ( b .o s)))) -> (z .o (v .o t)) e. om)
169		nnmcl 5999	. . . . . . . . . . . . . . . 16 |- (( s e. om /\ (w .o v) e. om) -> ( s .o (w .o v)) e. om)
170	104, 164, 169	syl2anc 391	. . . . . . . . . . . . . . 15 |- (((f e. ( om X. N.) /\ g e. ( om X. N.) /\ h e. ( om X. N.)) /\ (((f = <.z , w >. /\ g = <.v , u >.) /\ (z .o u) = (w .o v)) /\ ((g = <. a , b >. /\ h = <. s , t >.) /\ ( a .o t) = ( b .o s)))) -> ( s .o (w .o v)) e. om)
171		nnmcan 6028	. . . . . . . . . . . . . . 15 |- (((u e. om /\ (z .o (v .o t)) e. om /\ ( s .o (w .o v)) e. om) /\ (/) e. u) -> ((u .o (z .o (v .o t))) = (u .o ( s .o (w .o v))) <-> (z .o (v .o t)) = ( s .o (w .o v))))
172	103, 168, 170, 110, 171	syl31anc 1137	. . . . . . . . . . . . . 14 |- (((f e. ( om X. N.) /\ g e. ( om X. N.) /\ h e. ( om X. N.)) /\ (((f = <.z , w >. /\ g = <.v , u >.) /\ (z .o u) = (w .o v)) /\ ((g = <. a , b >. /\ h = <. s , t >.) /\ ( a .o t) = ( b .o s)))) -> ((u .o (z .o (v .o t))) = (u .o ( s .o (w .o v))) <-> (z .o (v .o t)) = ( s .o (w .o v))))
173	166, 172	mpbid 135	. . . . . . . . . . . . 13 |- (((f e. ( om X. N.) /\ g e. ( om X. N.) /\ h e. ( om X. N.)) /\ (((f = <.z , w >. /\ g = <.v , u >.) /\ (z .o u) = (w .o v)) /\ ((g = <. a , b >. /\ h = <. s , t >.) /\ ( a .o t) = ( b .o s)))) -> (z .o (v .o t)) = ( s .o (w .o v)))
174	135, 155, 74, 159, 161	caov12d 5624	. . . . . . . . . . . . 13 |- (((f e. ( om X. N.) /\ g e. ( om X. N.) /\ h e. ( om X. N.)) /\ (((f = <.z , w >. /\ g = <.v , u >.) /\ (z .o u) = (w .o v)) /\ ((g = <. a , b >. /\ h = <. s , t >.) /\ ( a .o t) = ( b .o s)))) -> (z .o (v .o t)) = (v .o (z .o t)))
175	104, 122, 155, 159, 161	caov13d 5626	. . . . . . . . . . . . 13 |- (((f e. ( om X. N.) /\ g e. ( om X. N.) /\ h e. ( om X. N.)) /\ (((f = <.z , w >. /\ g = <.v , u >.) /\ (z .o u) = (w .o v)) /\ ((g = <. a , b >. /\ h = <. s , t >.) /\ ( a .o t) = ( b .o s)))) -> ( s .o (w .o v)) = (v .o (w .o s)))
176	173, 174, 175	3eqtr3d 2077	. . . . . . . . . . . 12 |- (((f e. ( om X. N.) /\ g e. ( om X. N.) /\ h e. ( om X. N.)) /\ (((f = <.z , w >. /\ g = <.v , u >.) /\ (z .o u) = (w .o v)) /\ ((g = <. a , b >. /\ h = <. s , t >.) /\ ( a .o t) = ( b .o s)))) -> (v .o (z .o t)) = (v .o (w .o s)))
177	176	adantr 261	. . . . . . . . . . 11 |- ((((f e. ( om X. N.) /\ g e. ( om X. N.) /\ h e. ( om X. N.)) /\ (((f = <.z , w >. /\ g = <.v , u >.) /\ (z .o u) = (w .o v)) /\ ((g = <. a , b >. /\ h = <. s , t >.) /\ ( a .o t) = ( b .o s)))) /\ (/) e. v) -> (v .o (z .o t)) = (v .o (w .o s)))
178		nnmcl 5999	. . . . . . . . . . . . . 14 |- ((z e. om /\ t e. om) -> (z .o t) e. om)
179	135, 74, 178	syl2anc 391	. . . . . . . . . . . . 13 |- (((f e. ( om X. N.) /\ g e. ( om X. N.) /\ h e. ( om X. N.)) /\ (((f = <.z , w >. /\ g = <.v , u >.) /\ (z .o u) = (w .o v)) /\ ((g = <. a , b >. /\ h = <. s , t >.) /\ ( a .o t) = ( b .o s)))) -> (z .o t) e. om)
180		nnmcl 5999	. . . . . . . . . . . . . 14 |- ((w e. om /\ s e. om) -> (w .o s) e. om)
181	122, 104, 180	syl2anc 391	. . . . . . . . . . . . 13 |- (((f e. ( om X. N.) /\ g e. ( om X. N.) /\ h e. ( om X. N.)) /\ (((f = <.z , w >. /\ g = <.v , u >.) /\ (z .o u) = (w .o v)) /\ ((g = <. a , b >. /\ h = <. s , t >.) /\ ( a .o t) = ( b .o s)))) -> (w .o s) e. om)
182	155, 179, 181	3jca 1083	. . . . . . . . . . . 12 |- (((f e. ( om X. N.) /\ g e. ( om X. N.) /\ h e. ( om X. N.)) /\ (((f = <.z , w >. /\ g = <.v , u >.) /\ (z .o u) = (w .o v)) /\ ((g = <. a , b >. /\ h = <. s , t >.) /\ ( a .o t) = ( b .o s)))) -> (v e. om /\ (z .o t) e. om /\ (w .o s) e. om))
183		nnmcan 6028	. . . . . . . . . . . 12 |- (((v e. om /\ (z .o t) e. om /\ (w .o s) e. om) /\ (/) e. v) -> ((v .o (z .o t)) = (v .o (w .o s)) <-> (z .o t) = (w .o s)))
184	182, 183	sylan 267	. . . . . . . . . . 11 |- ((((f e. ( om X. N.) /\ g e. ( om X. N.) /\ h e. ( om X. N.)) /\ (((f = <.z , w >. /\ g = <.v , u >.) /\ (z .o u) = (w .o v)) /\ ((g = <. a , b >. /\ h = <. s , t >.) /\ ( a .o t) = ( b .o s)))) /\ (/) e. v) -> ((v .o (z .o t)) = (v .o (w .o s)) <-> (z .o t) = (w .o s)))
185	177, 184	mpbid 135	. . . . . . . . . 10 |- ((((f e. ( om X. N.) /\ g e. ( om X. N.) /\ h e. ( om X. N.)) /\ (((f = <.z , w >. /\ g = <.v , u >.) /\ (z .o u) = (w .o v)) /\ ((g = <. a , b >. /\ h = <. s , t >.) /\ ( a .o t) = ( b .o s)))) /\ (/) e. v) -> (z .o t) = (w .o s))
186	185	ex 108	. . . . . . . . 9 |- (((f e. ( om X. N.) /\ g e. ( om X. N.) /\ h e. ( om X. N.)) /\ (((f = <.z , w >. /\ g = <.v , u >.) /\ (z .o u) = (w .o v)) /\ ((g = <. a , b >. /\ h = <. s , t >.) /\ ( a .o t) = ( b .o s)))) -> ( (/) e. v -> (z .o t) = (w .o s)))
187		0elnn 4283	. . . . . . . . . 10 |- (v e. om -> (v = (/) \/ (/) e. v))
188	155, 187	syl 14	. . . . . . . . 9 |- (((f e. ( om X. N.) /\ g e. ( om X. N.) /\ h e. ( om X. N.)) /\ (((f = <.z , w >. /\ g = <.v , u >.) /\ (z .o u) = (w .o v)) /\ ((g = <. a , b >. /\ h = <. s , t >.) /\ ( a .o t) = ( b .o s)))) -> (v = (/) \/ (/) e. v))
189	151, 186, 188	mpjaod 637	. . . . . . . 8 |- (((f e. ( om X. N.) /\ g e. ( om X. N.) /\ h e. ( om X. N.)) /\ (((f = <.z , w >. /\ g = <.v , u >.) /\ (z .o u) = (w .o v)) /\ ((g = <. a , b >. /\ h = <. s , t >.) /\ ( a .o t) = ( b .o s)))) -> (z .o t) = (w .o s))
190	61, 65, 189	jca32 293	. . . . . . 7 |- (((f e. ( om X. N.) /\ g e. ( om X. N.) /\ h e. ( om X. N.)) /\ (((f = <.z , w >. /\ g = <.v , u >.) /\ (z .o u) = (w .o v)) /\ ((g = <. a , b >. /\ h = <. s , t >.) /\ ( a .o t) = ( b .o s)))) -> ((f e. ( om X. N.) /\ h e. ( om X. N.)) /\ ((f = <.z , w >. /\ h = <. s , t >.) /\ (z .o t) = (w .o s))))
191	190	2eximi 1489	. . . . . 6 |- (E. sE. t((f e. ( om X. N.) /\ g e. ( om X. N.) /\ h e. ( om X. N.)) /\ (((f = <.z , w >. /\ g = <.v , u >.) /\ (z .o u) = (w .o v)) /\ ((g = <. a , b >. /\ h = <. s , t >.) /\ ( a .o t) = ( b .o s)))) -> E. sE. t((f e. ( om X. N.) /\ h e. ( om X. N.)) /\ ((f = <.z , w >. /\ h = <. s , t >.) /\ (z .o t) = (w .o s))))
192	191	exlimivv 1773	. . . . 5 |- (E. aE. bE. sE. t((f e. ( om X. N.) /\ g e. ( om X. N.) /\ h e. ( om X. N.)) /\ (((f = <.z , w >. /\ g = <.v , u >.) /\ (z .o u) = (w .o v)) /\ ((g = <. a , b >. /\ h = <. s , t >.) /\ ( a .o t) = ( b .o s)))) -> E. sE. t((f e. ( om X. N.) /\ h e. ( om X. N.)) /\ ((f = <.z , w >. /\ h = <. s , t >.) /\ (z .o t) = (w .o s))))
193	192	exlimivv 1773	. . . 4 |- (E.vE.uE. aE. bE. sE. t((f e. ( om X. N.) /\ g e. ( om X. N.) /\ h e. ( om X. N.)) /\ (((f = <.z , w >. /\ g = <.v , u >.) /\ (z .o u) = (w .o v)) /\ ((g = <. a , b >. /\ h = <. s , t >.) /\ ( a .o t) = ( b .o s)))) -> E. sE. t((f e. ( om X. N.) /\ h e. ( om X. N.)) /\ ((f = <.z , w >. /\ h = <. s , t >.) /\ (z .o t) = (w .o s))))
194	193	2eximi 1489	. . 3 |- (E.zE.wE.vE.uE. aE. bE. sE. t((f e. ( om X. N.) /\ g e. ( om X. N.) /\ h e. ( om X. N.)) /\ (((f = <.z , w >. /\ g = <.v , u >.) /\ (z .o u) = (w .o v)) /\ ((g = <. a , b >. /\ h = <. s , t >.) /\ ( a .o t) = ( b .o s)))) -> E.zE.wE. sE. t((f e. ( om X. N.) /\ h e. ( om X. N.)) /\ ((f = <.z , w >. /\ h = <. s , t >.) /\ (z .o t) = (w .o s))))
195	59, 194	syl 14	. 2 |- ((f ~Q0 g /\ g ~Q0 h) -> E.zE.wE. sE. t((f e. ( om X. N.) /\ h e. ( om X. N.)) /\ ((f = <.z , w >. /\ h = <. s , t >.) /\ (z .o t) = (w .o s))))
196		19.42vvvv 1787	. . 3 |- (E.zE.wE. sE. t((f e. ( om X. N.) /\ h e. ( om X. N.)) /\ ((f = <.z , w >. /\ h = <. s , t >.) /\ (z .o t) = (w .o s))) <-> ((f e. ( om X. N.) /\ h e. ( om X. N.)) /\ E.zE.wE. sE. t((f = <.z , w >. /\ h = <. s , t >.) /\ (z .o t) = (w .o s))))
197	5	anbi1d 438	. . . . . . 7 |- (x = f -> ((x = <.z , w >. /\ y = <. s , t >.) <-> (f = <.z , w >. /\ y = <. s , t >.)))
198	197	anbi1d 438	. . . . . 6 |- (x = f -> (((x = <.z , w >. /\ y = <. s , t >.) /\ (z .o t) = (w .o s)) <-> ((f = <.z , w >. /\ y = <. s , t >.) /\ (z .o t) = (w .o s))))
199	198	4exbidv 1747	. . . . 5 |- (x = f -> (E.zE.wE. sE. t((x = <.z , w >. /\ y = <. s , t >.) /\ (z .o t) = (w .o s)) <-> E.zE.wE. sE. t((f = <.z , w >. /\ y = <. s , t >.) /\ (z .o t) = (w .o s))))
200	4, 199	anbi12d 442	. . . 4 |- (x = f -> (((x e. ( om X. N.) /\ y e. ( om X. N.)) /\ E.zE.wE. sE. t((x = <.z , w >. /\ y = <. s , t >.) /\ (z .o t) = (w .o s))) <-> ((f e. ( om X. N.) /\ y e. ( om X. N.)) /\ E.zE.w