Metamath Proof Explorer

Theorem rngcsectALTV

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

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

Proof

Step Hyp Ref Expression
1 rngcsectALTV.c ⊢ C = RngCatALTV ⁡ U
2 rngcsectALTV.b ⊢ B = Base C
3 rngcsectALTV.u ⊢ φ → U ∈ V
4 rngcsectALTV.x ⊢ φ → X ∈ B
5 rngcsectALTV.y ⊢ φ → Y ∈ B
6 rngcsectALTV.e ⊢ E = Base X
7 rngcsectALTV.n ⊢ S = Sect ⁡ C
8 eqid ⊢ Hom ⁡ C = Hom ⁡ C
9 eqid ⊢ comp ⁡ C = comp ⁡ C
10 eqid ⊢ Id ⁡ C = Id ⁡ C
11 1 rngccatALTV ⊢ 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 rngchomALTV ⊢ φ → X Hom ⁡ C Y = X RngHomo Y
15 14 eleq2d ⊢ φ → F ∈ X Hom ⁡ C Y ↔ F ∈ X RngHomo Y
16 1 2 3 8 5 4 rngchomALTV ⊢ φ → Y Hom ⁡ C X = Y RngHomo X
17 16 eleq2d ⊢ φ → G ∈ Y Hom ⁡ C X ↔ G ∈ Y RngHomo X
18 15 17 anbi12d ⊢ φ → F ∈ X Hom ⁡ C Y ∧ G ∈ Y Hom ⁡ C X ↔ F ∈ X RngHomo Y ∧ G ∈ Y RngHomo 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 RngHomo Y ∧ G ∈ Y RngHomo X ∧ G X Y comp ⁡ C X F = Id ⁡ C ⁡ X
20 3 adantr ⊢ φ ∧ F ∈ X RngHomo Y ∧ G ∈ Y RngHomo X → U ∈ V
21 4 adantr ⊢ φ ∧ F ∈ X RngHomo Y ∧ G ∈ Y RngHomo X → X ∈ B
22 5 adantr ⊢ φ ∧ F ∈ X RngHomo Y ∧ G ∈ Y RngHomo X → Y ∈ B
23 simprl ⊢ φ ∧ F ∈ X RngHomo Y ∧ G ∈ Y RngHomo X → F ∈ X RngHomo Y
24 simprr ⊢ φ ∧ F ∈ X RngHomo Y ∧ G ∈ Y RngHomo X → G ∈ Y RngHomo X
25 1 2 20 9 21 22 21 23 24 rngccoALTV ⊢ φ ∧ F ∈ X RngHomo Y ∧ G ∈ Y RngHomo X → G X Y comp ⁡ C X F = G ∘ F
26 1 2 10 3 4 6 rngcidALTV ⊢ φ → Id ⁡ C ⁡ X = I ↾ E
27 26 adantr ⊢ φ ∧ F ∈ X RngHomo Y ∧ G ∈ Y RngHomo X → Id ⁡ C ⁡ X = I ↾ E
28 25 27 eqeq12d ⊢ φ ∧ F ∈ X RngHomo Y ∧ G ∈ Y RngHomo X → G X Y comp ⁡ C X F = Id ⁡ C ⁡ X ↔ G ∘ F = I ↾ E
29 28 pm5.32da ⊢ φ → F ∈ X RngHomo Y ∧ G ∈ Y RngHomo X ∧ G X Y comp ⁡ C X F = Id ⁡ C ⁡ X ↔ F ∈ X RngHomo Y ∧ G ∈ Y RngHomo 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 RngHomo Y ∧ G ∈ Y RngHomo 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 RngHomo Y ∧ G ∈ Y RngHomo X ∧ G ∘ F = I ↾ E ↔ F ∈ X RngHomo Y ∧ G ∈ Y RngHomo 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 RngHomo Y ∧ G ∈ Y RngHomo X ∧ G ∘ F = I ↾ E
34 13 33 bitrd ⊢ φ → F X S Y G ↔ F ∈ X RngHomo Y ∧ G ∈ Y RngHomo X ∧ G ∘ F = I ↾ E