Table of ContentsTable of Contents User Sandbox < Previous   Next >
Related theorems
Unicode version
Theorem idmon 10716
Description: If there exists G such as (GRF) = (J` B) then F is monic. JFM CAT1 th. 63.
Hypotheses
Ref Expression
idmon.1 |- O = dom (id` T)
idmon.2 |- H = (hom` T)
idmon.3 |- R = (o` T)
idmon.4 |- J = (id` T)
Assertion
Ref Expression
idmon |- ((T e. Cat /\ (A e. O /\ B e. O) /\ (G e. (H` <.A, B>.) /\ F e. (H` <.B, A>.))) -> ((GRF) = (J` B) -> F e. (Monic` T)))
Proof of Theorem idmon
StepHypRef Expression
1 idmon.1 . . . . . . . . . . 11 |- O = dom (id` T)
2 idmon.2 . . . . . . . . . . 11 |- H = (hom` T)
3 idmon.3 . . . . . . . . . . 11 |- R = (o` T)
41, 2, 3cmpassoh 10700 . . . . . . . . . 10 |- ((T e. Cat /\ (c e. O /\ B e. O) /\ (A e. O /\ B e. O)) -> ((f e. (H` <.c, B>.) /\ F e. (H` <.B, A>.) /\ G e. (H` <.A, B>.)) -> (GR(FRf)) = ((GRF)Rf)))
5 3simp1 790 . . . . . . . . . . . . 13 |- ((T e. Cat /\ (A e. O /\ B e. O) /\ (G e. (H` <.A, B>.) /\ F e. (H` <.B, A>.))) -> T e. Cat)
65adantr 391 . . . . . . . . . . . 12 |- (((T e. Cat /\ (A e. O /\ B e. O) /\ (G e. (H` <.A, B>.) /\ F e. (H` <.B, A>.))) /\ (GRF) = (J` B)) -> T e. Cat)
76ad2antrr 406 . . . . . . . . . . 11 |- (((((T e. Cat /\ (A e. O /\ B e. O) /\ (G e. (H` <.A, B>.) /\ F e. (H` <.B, A>.))) /\ (GRF) = (J` B)) /\ (c e. O /\ f e. (H` <.c, B>.))) /\ g e. (H` <.c, B>.)) -> T e. Cat)
8 simprl 416 . . . . . . . . . . . . 13 |- ((((T e. Cat /\ (A e. O /\ B e. O) /\ (G e. (H` <.A, B>.) /\ F e. (H` <.B, A>.))) /\ (GRF) = (J` B)) /\ (c e. O /\ f e. (H` <.c, B>.))) -> c e. O)
98adantr 391 . . . . . . . . . . . 12 |- (((((T e. Cat /\ (A e. O /\ B e. O) /\ (G e. (H` <.A, B>.) /\ F e. (H` <.B, A>.))) /\ (GRF) = (J` B)) /\ (c e. O /\ f e. (H` <.c, B>.))) /\ g e. (H` <.c, B>.)) -> c e. O)
10 simplr 415 . . . . . . . . . . . . . 14 |- (((A e. O /\ B e. O) /\ (GRF) = (J` B)) -> B e. O)
11103ad2antl2 812 . . . . . . . . . . . . 13 |- (((T e. Cat /\ (A e. O /\ B e. O) /\ (G e. (H` <.A, B>.) /\ F e. (H` <.B, A>.))) /\ (GRF) = (J` B)) -> B e. O)
1211ad2antrr 406 . . . . . . . . . . . 12 |- (((((T e. Cat /\ (A e. O /\ B e. O) /\ (G e. (H` <.A, B>.) /\ F e. (H` <.B, A>.))) /\ (GRF) = (J` B)) /\ (c e. O /\ f e. (H` <.c, B>.))) /\ g e. (H` <.c, B>.)) -> B e. O)
139, 12jca 288 . . . . . . . . . . 11 |- (((((T e. Cat /\ (A e. O /\ B e. O) /\ (G e. (H` <.A, B>.) /\ F e. (H` <.B, A>.))) /\ (GRF) = (J` B)) /\ (c e. O /\ f e. (H` <.c, B>.))) /\ g e. (H` <.c, B>.)) -> (c e. O /\ B e. O))
14 simpll 414 . . . . . . . . . . . . . 14 |- (((A e. O /\ B e. O) /\ (GRF) = (J` B)) -> A e. O)
15143ad2antl2 812 . . . . . . . . . . . . 13 |- (((T e. Cat /\ (A e. O /\ B e. O) /\ (G e. (H` <.A, B>.) /\ F e. (H` <.B, A>.))) /\ (GRF) = (J` B)) -> A e. O)
1615ad2antrr 406 . . . . . . . . . . . 12 |- (((((T e. Cat /\ (A e. O /\ B e. O) /\ (G e. (H` <.A, B>.) /\ F e. (H` <.B, A>.))) /\ (GRF) = (J` B)) /\ (c e. O /\ f e. (H` <.c, B>.))) /\ g e. (H` <.c, B>.)) -> A e. O)
1716, 12jca 288 . . . . . . . . . . 11 |- (((((T e. Cat /\ (A e. O /\ B e. O) /\ (G e. (H` <.A, B>.) /\ F e. (H` <.B, A>.))) /\ (GRF) = (J` B)) /\ (c e. O /\ f e. (H` <.c, B>.))) /\ g e. (H` <.c, B>.)) -> (A e. O /\ B e. O))
187, 13, 173jca 821 . . . . . . . . . 10 |- (((((T e. Cat /\ (A e. O /\ B e. O) /\ (G e. (H` <.A, B>.) /\ F e. (H` <.B, A>.))) /\ (GRF) = (J` B)) /\ (c e. O /\ f e. (H` <.c, B>.))) /\ g e. (H` <.c, B>.)) -> (T e. Cat /\ (c e. O /\ B e. O) /\ (A e. O /\ B e. O)))
19 simprr 417 . . . . . . . . . . . 12 |- ((((T e. Cat /\ (A e. O /\ B e. O) /\ (G e. (H` <.A, B>.) /\ F e. (H` <.B, A>.))) /\ (GRF) = (J` B)) /\ (c e. O /\ f e. (H` <.c, B>.))) -> f e. (H` <.c, B>.))
2019adantr 391 . . . . . . . . . . 11 |- (((((T e. Cat /\ (A e. O /\ B e. O) /\ (G e. (H` <.A, B>.) /\ F e. (H` <.B, A>.))) /\ (GRF) = (J` B)) /\ (c e. O /\ f e. (H` <.c, B>.))) /\ g e. (H` <.c, B>.)) -> f e. (H` <.c, B>.))
21 simplr 415 . . . . . . . . . . . . 13 |- (((G e. (H` <.A, B>.) /\ F e. (H` <.B, A>.)) /\ (GRF) = (J` B)) -> F e. (H` <.B, A>.))
22213ad2antl3 813 . . . . . . . . . . . 12 |- (((T e. Cat /\ (A e. O /\ B e. O) /\ (G e. (H` <.A, B>.) /\ F e. (H` <.B, A>.))) /\ (GRF) = (J` B)) -> F e. (H` <.B, A>.))
2322ad2antrr 406 . . . . . . . . . . 11 |- (((((T e. Cat /\ (A e. O /\ B e. O) /\ (G e. (H` <.A, B>.) /\ F e. (H` <.B, A>.))) /\ (GRF) = (J` B)) /\ (c e. O /\ f e. (H` <.c, B>.))) /\ g e. (H` <.c, B>.)) -> F e. (H` <.B, A>.))
24 simpll 414 . . . . . . . . . . . . 13 |- (((G e. (H` <.A, B>.) /\ F e. (H` <.B, A>.)) /\ (GRF) = (J` B)) -> G e. (H` <.A, B>.))
25243ad2antl3 813 . . . . . . . . . . . 12 |- (((T e. Cat /\ (A e. O /\ B e. O) /\ (G e. (H` <.A, B>.) /\ F e. (H` <.B, A>.))) /\ (GRF) = (J` B)) -> G e. (H` <.A, B>.))
2625ad2antrr 406 . . . . . . . . . . 11 |- (((((T e. Cat /\ (A e. O /\ B e. O) /\ (G e. (H` <.A, B>.) /\ F e. (H` <.B, A>.))) /\ (GRF) = (J` B)) /\ (c e. O /\ f e. (H` <.c, B>.))) /\ g e. (H` <.c, B>.)) -> G e. (H` <.A, B>.))
2720, 23, 263jca 821 . . . . . . . . . 10 |- (((((T e. Cat /\ (A e. O /\ B e. O) /\ (G e. (H` <.A, B>.) /\ F e. (H` <.B, A>.))) /\ (GRF) = (J` B)) /\ (c e. O /\ f e. (H` <.c, B>.))) /\ g e. (H` <.c, B>.)) -> (f e. (H` <.c, B>.) /\ F e. (H` <.B, A>.) /\ G e. (H` <.A, B>.)))
284, 18, 27sylc 68 . . . . . . . . 9 |- (((((T e. Cat /\ (A e. O /\ B e. O) /\ (G e. (H` <.A, B>.) /\ F e. (H` <.B, A>.))) /\ (GRF) = (J` B)) /\ (c e. O /\ f e. (H` <.c, B>.))) /\ g e. (H`