Metamath Proof Explorer


Theorem funcringcsetcALTV2lem7

Description: Lemma 7 for funcringcsetcALTV2 . (Contributed by AV, 15-Feb-2020) (New usage is discouraged.)

Ref Expression
Hypotheses funcringcsetcALTV2.r R = RingCat U
funcringcsetcALTV2.s S = SetCat U
funcringcsetcALTV2.b B = Base R
funcringcsetcALTV2.c C = Base S
funcringcsetcALTV2.u φ U WUni
funcringcsetcALTV2.f φ F = x B Base x
funcringcsetcALTV2.g φ G = x B , y B I x RingHom y
Assertion funcringcsetcALTV2lem7 φ X B X G X Id R X = Id S F X

Proof

Step Hyp Ref Expression
1 funcringcsetcALTV2.r R = RingCat U
2 funcringcsetcALTV2.s S = SetCat U
3 funcringcsetcALTV2.b B = Base R
4 funcringcsetcALTV2.c C = Base S
5 funcringcsetcALTV2.u φ U WUni
6 funcringcsetcALTV2.f φ F = x B Base x
7 funcringcsetcALTV2.g φ G = x B , y B I x RingHom y
8 1 2 3 4 5 6 7 funcringcsetcALTV2lem5 φ X B X B X G X = I X RingHom X
9 8 anabsan2 φ X B X G X = I X RingHom X
10 eqid Id R = Id R
11 5 adantr φ X B U WUni
12 simpr φ X B X B
13 eqid Base X = Base X
14 1 3 10 11 12 13 ringcid φ X B Id R X = I Base X
15 9 14 fveq12d φ X B X G X Id R X = I X RingHom X I Base X
16 1 3 5 ringcbas φ B = U Ring
17 16 eleq2d φ X B X U Ring
18 elin X U Ring X U X Ring
19 18 simprbi X U Ring X Ring
20 17 19 syl6bi φ X B X Ring
21 20 imp φ X B X Ring
22 13 idrhm X Ring I Base X X RingHom X
23 fvresi I Base X X RingHom X I X RingHom X I Base X = I Base X
24 21 22 23 3syl φ X B I X RingHom X I Base X = I Base X
25 1 2 3 4 5 6 funcringcsetcALTV2lem1 φ X B F X = Base X
26 25 fveq2d φ X B Id S F X = Id S Base X
27 eqid Id S = Id S
28 1 3 5 ringcbasbas φ X B Base X U
29 2 27 11 28 setcid φ X B Id S Base X = I Base X
30 26 29 eqtr2d φ X B I Base X = Id S F X
31 15 24 30 3eqtrd φ X B X G X Id R X = Id S F X