Metamath Proof Explorer

Theorem rngcsect

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

Ref Expression
Hypotheses rngcsect.c ⊢ 𝐶 = ( RngCat ‘ 𝑈 )
rngcsect.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
rngcsect.u ⊢ ( 𝜑 → 𝑈 ∈ 𝑉 )
rngcsect.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
rngcsect.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
rngcsect.e ⊢ 𝐸 = ( Base ‘ 𝑋 )
rngcsect.n ⊢ 𝑆 = ( Sect ‘ 𝐶 )
Assertion rngcsect ( 𝜑 → ( 𝐹 ( 𝑋 𝑆 𝑌 ) 𝐺 ↔ ( 𝐹 ∈ ( 𝑋 RngHomo 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RngHomo 𝑋 ) ∧ ( 𝐺 ∘ 𝐹 ) = ( I ↾ 𝐸 ) ) ) )

Proof

Step Hyp Ref Expression
1 rngcsect.c ⊢ 𝐶 = ( RngCat ‘ 𝑈 )
2 rngcsect.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
3 rngcsect.u ⊢ ( 𝜑 → 𝑈 ∈ 𝑉 )
4 rngcsect.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
5 rngcsect.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
6 rngcsect.e ⊢ 𝐸 = ( Base ‘ 𝑋 )
7 rngcsect.n ⊢ 𝑆 = ( Sect ‘ 𝐶 )
8 eqid ⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
9 eqid ⊢ ( comp ‘ 𝐶 ) = ( comp ‘ 𝐶 )
10 eqid ⊢ ( Id ‘ 𝐶 ) = ( Id ‘ 𝐶 )
11 1 rngccat ⊢ ( 𝑈 ∈ 𝑉 → 𝐶 ∈ Cat )
12 3 11 syl ⊢ ( 𝜑 → 𝐶 ∈ Cat )
13 2 8 9 10 7 12 4 5 issect ⊢ ( 𝜑 → ( 𝐹 ( 𝑋 𝑆 𝑌 ) 𝐺 ↔ ( 𝐹 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 ( Hom ‘ 𝐶 ) 𝑋 ) ∧ ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) 𝐹 ) = ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ) ) )
14 1 2 3 8 4 5 rngchom ⊢ ( 𝜑 → ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) = ( 𝑋 RngHomo 𝑌 ) )
15 14 eleq2d ⊢ ( 𝜑 → ( 𝐹 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) ↔ 𝐹 ∈ ( 𝑋 RngHomo 𝑌 ) ) )
16 1 2 3 8 5 4 rngchom ⊢ ( 𝜑 → ( 𝑌 ( Hom ‘ 𝐶 ) 𝑋 ) = ( 𝑌 RngHomo 𝑋 ) )
17 16 eleq2d ⊢ ( 𝜑 → ( 𝐺 ∈ ( 𝑌 ( Hom ‘ 𝐶 ) 𝑋 ) ↔ 𝐺 ∈ ( 𝑌 RngHomo 𝑋 ) ) )
18 15 17 anbi12d ⊢ ( 𝜑 → ( ( 𝐹 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 ( Hom ‘ 𝐶 ) 𝑋 ) ) ↔ ( 𝐹 ∈ ( 𝑋 RngHomo 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RngHomo 𝑋 ) ) ) )
19 18 anbi1d ⊢ ( 𝜑 → ( ( ( 𝐹 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 ( Hom ‘ 𝐶 ) 𝑋 ) ) ∧ ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) 𝐹 ) = ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ) ↔ ( ( 𝐹 ∈ ( 𝑋 RngHomo 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RngHomo 𝑋 ) ) ∧ ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) 𝐹 ) = ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ) ) )
20 3 adantr ⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ ( 𝑋 RngHomo 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RngHomo 𝑋 ) ) ) → 𝑈 ∈ 𝑉 )
21 4 adantr ⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ ( 𝑋 RngHomo 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RngHomo 𝑋 ) ) ) → 𝑋 ∈ 𝐵 )
22 1 2 3 rngcbas ⊢ ( 𝜑 → 𝐵 = ( 𝑈 ∩ Rng ) )
23 22 eleq2d ⊢ ( 𝜑 → ( 𝑋 ∈ 𝐵 ↔ 𝑋 ∈ ( 𝑈 ∩ Rng ) ) )
24 inss1 ⊢ ( 𝑈 ∩ Rng ) ⊆ 𝑈
25 24 a1i ⊢ ( 𝜑 → ( 𝑈 ∩ Rng ) ⊆ 𝑈 )
26 25 sseld ⊢ ( 𝜑 → ( 𝑋 ∈ ( 𝑈 ∩ Rng ) → 𝑋 ∈ 𝑈 ) )
27 23 26 sylbid ⊢ ( 𝜑 → ( 𝑋 ∈ 𝐵 → 𝑋 ∈ 𝑈 ) )
28 27 adantr ⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ ( 𝑋 RngHomo 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RngHomo 𝑋 ) ) ) → ( 𝑋 ∈ 𝐵 → 𝑋 ∈ 𝑈 ) )
29 21 28 mpd ⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ ( 𝑋 RngHomo 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RngHomo 𝑋 ) ) ) → 𝑋 ∈ 𝑈 )
30 5 adantr ⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ ( 𝑋 RngHomo 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RngHomo 𝑋 ) ) ) → 𝑌 ∈ 𝐵 )
31 22 eleq2d ⊢ ( 𝜑 → ( 𝑌 ∈ 𝐵 ↔ 𝑌 ∈ ( 𝑈 ∩ Rng ) ) )
32 25 sseld ⊢ ( 𝜑 → ( 𝑌 ∈ ( 𝑈 ∩ Rng ) → 𝑌 ∈ 𝑈 ) )
33 31 32 sylbid ⊢ ( 𝜑 → ( 𝑌 ∈ 𝐵 → 𝑌 ∈ 𝑈 ) )
34 33 adantr ⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ ( 𝑋 RngHomo 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RngHomo 𝑋 ) ) ) → ( 𝑌 ∈ 𝐵 → 𝑌 ∈ 𝑈 ) )
35 30 34 mpd ⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ ( 𝑋 RngHomo 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RngHomo 𝑋 ) ) ) → 𝑌 ∈ 𝑈 )
36 eqid ⊢ ( Base ‘ 𝑋 ) = ( Base ‘ 𝑋 )
37 eqid ⊢ ( Base ‘ 𝑌 ) = ( Base ‘ 𝑌 )
38 36 37 rnghmf ⊢ ( 𝐹 ∈ ( 𝑋 RngHomo 𝑌 ) → 𝐹 : ( Base ‘ 𝑋 ) ⟶ ( Base ‘ 𝑌 ) )
39 38 adantr ⊢ ( ( 𝐹 ∈ ( 𝑋 RngHomo 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RngHomo 𝑋 ) ) → 𝐹 : ( Base ‘ 𝑋 ) ⟶ ( Base ‘ 𝑌 ) )
40 39 adantl ⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ ( 𝑋 RngHomo 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RngHomo 𝑋 ) ) ) → 𝐹 : ( Base ‘ 𝑋 ) ⟶ ( Base ‘ 𝑌 ) )
41 37 36 rnghmf ⊢ ( 𝐺 ∈ ( 𝑌 RngHomo 𝑋 ) → 𝐺 : ( Base ‘ 𝑌 ) ⟶ ( Base ‘ 𝑋 ) )
42 41 adantl ⊢ ( ( 𝐹 ∈ ( 𝑋 RngHomo 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RngHomo 𝑋 ) ) → 𝐺 : ( Base ‘ 𝑌 ) ⟶ ( Base ‘ 𝑋 ) )
43 42 adantl ⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ ( 𝑋 RngHomo 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RngHomo 𝑋 ) ) ) → 𝐺 : ( Base ‘ 𝑌 ) ⟶ ( Base ‘ 𝑋 ) )
44 1 20 9 29 35 29 40 43 rngcco ⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ ( 𝑋 RngHomo 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RngHomo 𝑋 ) ) ) → ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) 𝐹 ) = ( 𝐺 ∘ 𝐹 ) )
45 1 2 10 3 4 6 rngcid ⊢ ( 𝜑 → ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) = ( I ↾ 𝐸 ) )
46 45 adantr ⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ ( 𝑋 RngHomo 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RngHomo 𝑋 ) ) ) → ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) = ( I ↾ 𝐸 ) )
47 44 46 eqeq12d ⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ ( 𝑋 RngHomo 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RngHomo 𝑋 ) ) ) → ( ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) 𝐹 ) = ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ↔ ( 𝐺 ∘ 𝐹 ) = ( I ↾ 𝐸 ) ) )
48 47 pm5.32da ⊢ ( 𝜑 → ( ( ( 𝐹 ∈ ( 𝑋 RngHomo 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RngHomo 𝑋 ) ) ∧ ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) 𝐹 ) = ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ) ↔ ( ( 𝐹 ∈ ( 𝑋 RngHomo 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RngHomo 𝑋 ) ) ∧ ( 𝐺 ∘ 𝐹 ) = ( I ↾ 𝐸 ) ) ) )
49 19 48 bitrd ⊢ ( 𝜑 → ( ( ( 𝐹 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 ( Hom ‘ 𝐶 ) 𝑋 ) ) ∧ ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) 𝐹 ) = ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ) ↔ ( ( 𝐹 ∈ ( 𝑋 RngHomo 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RngHomo 𝑋 ) ) ∧ ( 𝐺 ∘ 𝐹 ) = ( I ↾ 𝐸 ) ) ) )
50 df-3an ⊢ ( ( 𝐹 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 ( Hom ‘ 𝐶 ) 𝑋 ) ∧ ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) 𝐹 ) = ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ) ↔ ( ( 𝐹 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 ( Hom ‘ 𝐶 ) 𝑋 ) ) ∧ ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) 𝐹 ) = ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ) )
51 df-3an ⊢ ( ( 𝐹 ∈ ( 𝑋 RngHomo 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RngHomo 𝑋 ) ∧ ( 𝐺 ∘ 𝐹 ) = ( I ↾ 𝐸 ) ) ↔ ( ( 𝐹 ∈ ( 𝑋 RngHomo 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RngHomo 𝑋 ) ) ∧ ( 𝐺 ∘ 𝐹 ) = ( I ↾ 𝐸 ) ) )
52 49 50 51 3bitr4g ⊢ ( 𝜑 → ( ( 𝐹 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 ( Hom ‘ 𝐶 ) 𝑋 ) ∧ ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) 𝐹 ) = ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ) ↔ ( 𝐹 ∈ ( 𝑋 RngHomo 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RngHomo 𝑋 ) ∧ ( 𝐺 ∘ 𝐹 ) = ( I ↾ 𝐸 ) ) ) )
53 13 52 bitrd ⊢ ( 𝜑 → ( 𝐹 ( 𝑋 𝑆 𝑌 ) 𝐺 ↔ ( 𝐹 ∈ ( 𝑋 RngHomo 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RngHomo 𝑋 ) ∧ ( 𝐺 ∘ 𝐹 ) = ( I ↾ 𝐸 ) ) ) )