Metamath Proof Explorer

Theorem ringcsectALTV

Description: A section in the category of rings, written out. (Contributed by AV, 14-Feb-2020) (New usage is discouraged.)

Ref Expression
Hypotheses ringcsectALTV.c ⊢ C = RingCatALTV ⁡ U
ringcsectALTV.b ⊢ B = Base C
ringcsectALTV.u ⊢ φ → U ∈ V
ringcsectALTV.x ⊢ φ → X ∈ B
ringcsectALTV.y ⊢ φ → Y ∈ B
ringcsectALTV.e ⊢ E = Base X
ringcsectALTV.n ⊢ S = Sect ⁡ C
Assertion ringcsectALTV ⊢ φ → F X S Y G ↔ F ∈ X RingHom Y ∧ G ∈ Y RingHom X ∧ G ∘ F = I ↾ E

Proof

Step Hyp Ref Expression
1 ringcsectALTV.c ⊢ C = RingCatALTV ⁡ U
2 ringcsectALTV.b ⊢ B = Base C
3 ringcsectALTV.u ⊢ φ → U ∈ V
4 ringcsectALTV.x ⊢ φ → X ∈ B
5 ringcsectALTV.y ⊢ φ → Y ∈ B
6 ringcsectALTV.e ⊢ E = Base X
7 ringcsectALTV.n ⊢ S = Sect ⁡ C
8 eqid ⊢ Hom ⁡ C = Hom ⁡ C
9 eqid ⊢ comp ⁡ C = comp ⁡ C
10 eqid ⊢ Id ⁡ C = Id ⁡ C
11 1 ringccatALTV ⊢ U ∈ V → C ∈ Cat
12 3 11 syl ⊢ φ → C ∈ Cat
13 2 8 9 10 7 12 4 5 issect ⊢ φ → F X S Y G ↔ F ∈ X Hom ⁡ C Y ∧ G ∈ Y Hom ⁡ C X ∧ G X Y comp ⁡ C X F = Id ⁡ C ⁡ X
14 1 2 3 8 4 5 ringchomALTV ⊢ φ → X Hom ⁡ C Y = X RingHom Y
15 14 eleq2d ⊢ φ → F ∈ X Hom ⁡ C Y ↔ F ∈ X RingHom Y
16 1 2 3 8 5 4 ringchomALTV ⊢ φ → Y Hom ⁡ C X = Y RingHom X
17 16 eleq2d ⊢ φ → G ∈ Y Hom ⁡ C X ↔ G ∈ Y RingHom X
18 15 17 anbi12d ⊢ φ → F ∈ X Hom ⁡ C Y ∧ G ∈ Y Hom ⁡ C X ↔ F ∈ X RingHom Y ∧ G ∈ Y RingHom X
19 18 anbi1d ⊢ φ → F ∈ X Hom ⁡ C Y ∧ G ∈ Y Hom ⁡ C X ∧ G X Y comp ⁡ C X F = Id ⁡ C ⁡ X ↔ F ∈ X RingHom Y ∧ G ∈ Y RingHom X ∧ G X Y comp ⁡ C X F = Id ⁡ C ⁡ X
20 3 adantr ⊢ φ ∧ F ∈ X RingHom Y ∧ G ∈ Y RingHom X → U ∈ V
21 4 adantr ⊢ φ ∧ F ∈ X RingHom Y ∧ G ∈ Y RingHom X → X ∈ B
22 5 adantr ⊢ φ ∧ F ∈ X RingHom Y ∧ G ∈ Y RingHom X → Y ∈ B
23 simprl ⊢ φ ∧ F ∈ X RingHom Y ∧ G ∈ Y RingHom X → F ∈ X RingHom Y
24 simprr ⊢ φ ∧ F ∈ X RingHom Y ∧ G ∈ Y RingHom X → G ∈ Y RingHom X
25 1 2 20 9 21 22 21 23 24 ringccoALTV ⊢ φ ∧ F ∈ X RingHom Y ∧ G ∈ Y RingHom X → G X Y comp ⁡ C X F = G ∘ F
26 1 2 10 3 4 6 ringcidALTV ⊢ φ → Id ⁡ C ⁡ X = I ↾ E
27 26 adantr ⊢ φ ∧ F ∈ X RingHom Y ∧ G ∈ Y RingHom X → Id ⁡ C ⁡ X = I ↾ E
28 25 27 eqeq12d ⊢ φ ∧ F ∈ X RingHom Y ∧ G ∈ Y RingHom X → G X Y comp ⁡ C X F = Id ⁡ C ⁡ X ↔ G ∘ F = I ↾ E
29 28 pm5.32da ⊢ φ → F ∈ X RingHom Y ∧ G ∈ Y RingHom X ∧ G X Y comp ⁡ C X F = Id ⁡ C ⁡ X ↔ F ∈ X RingHom Y ∧ G ∈ Y RingHom X ∧ G ∘ F = I ↾ E
30 19 29 bitrd ⊢ φ → F ∈ X Hom ⁡ C Y ∧ G ∈ Y Hom ⁡ C X ∧ G X Y comp ⁡ C X F = Id ⁡ C ⁡ X ↔ F ∈ X RingHom Y ∧ G ∈ Y RingHom X ∧ G ∘ F = I ↾ E
31 df-3an ⊢ F ∈ X Hom ⁡ C Y ∧ G ∈ Y Hom ⁡ C X ∧ G X Y comp ⁡ C X F = Id ⁡ C ⁡ X ↔ F ∈ X Hom ⁡ C Y ∧ G ∈ Y Hom ⁡ C X ∧ G X Y comp ⁡ C X F = Id ⁡ C ⁡ X
32 df-3an ⊢ F ∈ X RingHom Y ∧ G ∈ Y RingHom X ∧ G ∘ F = I ↾ E ↔ F ∈ X RingHom Y ∧ G ∈ Y RingHom X ∧ G ∘ F = I ↾ E
33 30 31 32 3bitr4g ⊢ φ → F ∈ X Hom ⁡ C Y ∧ G ∈ Y Hom ⁡ C X ∧ G X Y comp ⁡ C X F = Id ⁡ C ⁡ X ↔ F ∈ X RingHom Y ∧ G ∈ Y RingHom X ∧ G ∘ F = I ↾ E
34 13 33 bitrd ⊢ φ → F X S Y G ↔ F ∈ X RingHom Y ∧ G ∈ Y RingHom X ∧ G ∘ F = I ↾ E