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 𝐶 = ( RingCatALTV ‘ 𝑈 )
ringcsectALTV.b 𝐵 = ( Base ‘ 𝐶 )
ringcsectALTV.u ( 𝜑𝑈𝑉 )
ringcsectALTV.x ( 𝜑𝑋𝐵 )
ringcsectALTV.y ( 𝜑𝑌𝐵 )
ringcsectALTV.e 𝐸 = ( Base ‘ 𝑋 )
ringcsectALTV.n 𝑆 = ( Sect ‘ 𝐶 )
Assertion ringcsectALTV ( 𝜑 → ( 𝐹 ( 𝑋 𝑆 𝑌 ) 𝐺 ↔ ( 𝐹 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RingHom 𝑋 ) ∧ ( 𝐺𝐹 ) = ( I ↾ 𝐸 ) ) ) )

Proof

Step Hyp Ref Expression
1 ringcsectALTV.c 𝐶 = ( RingCatALTV ‘ 𝑈 )
2 ringcsectALTV.b 𝐵 = ( Base ‘ 𝐶 )
3 ringcsectALTV.u ( 𝜑𝑈𝑉 )
4 ringcsectALTV.x ( 𝜑𝑋𝐵 )
5 ringcsectALTV.y ( 𝜑𝑌𝐵 )
6 ringcsectALTV.e 𝐸 = ( Base ‘ 𝑋 )
7 ringcsectALTV.n 𝑆 = ( Sect ‘ 𝐶 )
8 eqid ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
9 eqid ( comp ‘ 𝐶 ) = ( comp ‘ 𝐶 )
10 eqid ( Id ‘ 𝐶 ) = ( Id ‘ 𝐶 )
11 1 ringccatALTV ( 𝑈𝑉𝐶 ∈ 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 ringchomALTV ( 𝜑 → ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) = ( 𝑋 RingHom 𝑌 ) )
15 14 eleq2d ( 𝜑 → ( 𝐹 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) ↔ 𝐹 ∈ ( 𝑋 RingHom 𝑌 ) ) )
16 1 2 3 8 5 4 ringchomALTV ( 𝜑 → ( 𝑌 ( Hom ‘ 𝐶 ) 𝑋 ) = ( 𝑌 RingHom 𝑋 ) )
17 16 eleq2d ( 𝜑 → ( 𝐺 ∈ ( 𝑌 ( Hom ‘ 𝐶 ) 𝑋 ) ↔ 𝐺 ∈ ( 𝑌 RingHom 𝑋 ) ) )
18 15 17 anbi12d ( 𝜑 → ( ( 𝐹 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 ( Hom ‘ 𝐶 ) 𝑋 ) ) ↔ ( 𝐹 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RingHom 𝑋 ) ) ) )
19 18 anbi1d ( 𝜑 → ( ( ( 𝐹 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 ( Hom ‘ 𝐶 ) 𝑋 ) ) ∧ ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) 𝐹 ) = ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ) ↔ ( ( 𝐹 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RingHom 𝑋 ) ) ∧ ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) 𝐹 ) = ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ) ) )
20 3 adantr ( ( 𝜑 ∧ ( 𝐹 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RingHom 𝑋 ) ) ) → 𝑈𝑉 )
21 4 adantr ( ( 𝜑 ∧ ( 𝐹 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RingHom 𝑋 ) ) ) → 𝑋𝐵 )
22 5 adantr ( ( 𝜑 ∧ ( 𝐹 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RingHom 𝑋 ) ) ) → 𝑌𝐵 )
23 simprl ( ( 𝜑 ∧ ( 𝐹 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RingHom 𝑋 ) ) ) → 𝐹 ∈ ( 𝑋 RingHom 𝑌 ) )
24 simprr ( ( 𝜑 ∧ ( 𝐹 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RingHom 𝑋 ) ) ) → 𝐺 ∈ ( 𝑌 RingHom 𝑋 ) )
25 1 2 20 9 21 22 21 23 24 ringccoALTV ( ( 𝜑 ∧ ( 𝐹 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RingHom 𝑋 ) ) ) → ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) 𝐹 ) = ( 𝐺𝐹 ) )
26 1 2 10 3 4 6 ringcidALTV ( 𝜑 → ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) = ( I ↾ 𝐸 ) )
27 26 adantr ( ( 𝜑 ∧ ( 𝐹 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RingHom 𝑋 ) ) ) → ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) = ( I ↾ 𝐸 ) )
28 25 27 eqeq12d ( ( 𝜑 ∧ ( 𝐹 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RingHom 𝑋 ) ) ) → ( ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) 𝐹 ) = ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ↔ ( 𝐺𝐹 ) = ( I ↾ 𝐸 ) ) )
29 28 pm5.32da ( 𝜑 → ( ( ( 𝐹 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RingHom 𝑋 ) ) ∧ ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) 𝐹 ) = ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ) ↔ ( ( 𝐹 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RingHom 𝑋 ) ) ∧ ( 𝐺𝐹 ) = ( I ↾ 𝐸 ) ) ) )
30 19 29 bitrd ( 𝜑 → ( ( ( 𝐹 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 ( Hom ‘ 𝐶 ) 𝑋 ) ) ∧ ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) 𝐹 ) = ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ) ↔ ( ( 𝐹 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RingHom 𝑋 ) ) ∧ ( 𝐺𝐹 ) = ( I ↾ 𝐸 ) ) ) )
31 df-3an ( ( 𝐹 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 ( Hom ‘ 𝐶 ) 𝑋 ) ∧ ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) 𝐹 ) = ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ) ↔ ( ( 𝐹 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 ( Hom ‘ 𝐶 ) 𝑋 ) ) ∧ ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) 𝐹 ) = ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ) )
32 df-3an ( ( 𝐹 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RingHom 𝑋 ) ∧ ( 𝐺𝐹 ) = ( I ↾ 𝐸 ) ) ↔ ( ( 𝐹 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RingHom 𝑋 ) ) ∧ ( 𝐺𝐹 ) = ( I ↾ 𝐸 ) ) )
33 30 31 32 3bitr4g ( 𝜑 → ( ( 𝐹 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 ( Hom ‘ 𝐶 ) 𝑋 ) ∧ ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) 𝐹 ) = ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ) ↔ ( 𝐹 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RingHom 𝑋 ) ∧ ( 𝐺𝐹 ) = ( I ↾ 𝐸 ) ) ) )
34 13 33 bitrd ( 𝜑 → ( 𝐹 ( 𝑋 𝑆 𝑌 ) 𝐺 ↔ ( 𝐹 ∈ ( 𝑋 RingHom 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 RingHom 𝑋 ) ∧ ( 𝐺𝐹 ) = ( I ↾ 𝐸 ) ) ) )