Metamath Proof Explorer


Theorem rngccoALTV

Description: Composition in the category of non-unital rings. (New usage is discouraged.) (Contributed by AV, 27-Feb-2020)

Ref Expression
Hypotheses rngcbasALTV.c 𝐶 = ( RngCatALTV ‘ 𝑈 )
rngcbasALTV.b 𝐵 = ( Base ‘ 𝐶 )
rngcbasALTV.u ( 𝜑𝑈𝑉 )
rngccofvalALTV.o · = ( comp ‘ 𝐶 )
rngccoALTV.x ( 𝜑𝑋𝐵 )
rngccoALTV.y ( 𝜑𝑌𝐵 )
rngccoALTV.z ( 𝜑𝑍𝐵 )
rngccoALTV.f ( 𝜑𝐹 ∈ ( 𝑋 RngHomo 𝑌 ) )
rngccoALTV.g ( 𝜑𝐺 ∈ ( 𝑌 RngHomo 𝑍 ) )
Assertion rngccoALTV ( 𝜑 → ( 𝐺 ( ⟨ 𝑋 , 𝑌· 𝑍 ) 𝐹 ) = ( 𝐺𝐹 ) )

Proof

Step Hyp Ref Expression
1 rngcbasALTV.c 𝐶 = ( RngCatALTV ‘ 𝑈 )
2 rngcbasALTV.b 𝐵 = ( Base ‘ 𝐶 )
3 rngcbasALTV.u ( 𝜑𝑈𝑉 )
4 rngccofvalALTV.o · = ( comp ‘ 𝐶 )
5 rngccoALTV.x ( 𝜑𝑋𝐵 )
6 rngccoALTV.y ( 𝜑𝑌𝐵 )
7 rngccoALTV.z ( 𝜑𝑍𝐵 )
8 rngccoALTV.f ( 𝜑𝐹 ∈ ( 𝑋 RngHomo 𝑌 ) )
9 rngccoALTV.g ( 𝜑𝐺 ∈ ( 𝑌 RngHomo 𝑍 ) )
10 1 2 3 4 rngccofvalALTV ( 𝜑· = ( 𝑣 ∈ ( 𝐵 × 𝐵 ) , 𝑧𝐵 ↦ ( 𝑔 ∈ ( ( 2nd𝑣 ) RngHomo 𝑧 ) , 𝑓 ∈ ( ( 1st𝑣 ) RngHomo ( 2nd𝑣 ) ) ↦ ( 𝑔𝑓 ) ) ) )
11 simprl ( ( 𝜑 ∧ ( 𝑣 = ⟨ 𝑋 , 𝑌 ⟩ ∧ 𝑧 = 𝑍 ) ) → 𝑣 = ⟨ 𝑋 , 𝑌 ⟩ )
12 11 fveq2d ( ( 𝜑 ∧ ( 𝑣 = ⟨ 𝑋 , 𝑌 ⟩ ∧ 𝑧 = 𝑍 ) ) → ( 2nd𝑣 ) = ( 2nd ‘ ⟨ 𝑋 , 𝑌 ⟩ ) )
13 op2ndg ( ( 𝑋𝐵𝑌𝐵 ) → ( 2nd ‘ ⟨ 𝑋 , 𝑌 ⟩ ) = 𝑌 )
14 5 6 13 syl2anc ( 𝜑 → ( 2nd ‘ ⟨ 𝑋 , 𝑌 ⟩ ) = 𝑌 )
15 14 adantr ( ( 𝜑 ∧ ( 𝑣 = ⟨ 𝑋 , 𝑌 ⟩ ∧ 𝑧 = 𝑍 ) ) → ( 2nd ‘ ⟨ 𝑋 , 𝑌 ⟩ ) = 𝑌 )
16 12 15 eqtrd ( ( 𝜑 ∧ ( 𝑣 = ⟨ 𝑋 , 𝑌 ⟩ ∧ 𝑧 = 𝑍 ) ) → ( 2nd𝑣 ) = 𝑌 )
17 simprr ( ( 𝜑 ∧ ( 𝑣 = ⟨ 𝑋 , 𝑌 ⟩ ∧ 𝑧 = 𝑍 ) ) → 𝑧 = 𝑍 )
18 16 17 oveq12d ( ( 𝜑 ∧ ( 𝑣 = ⟨ 𝑋 , 𝑌 ⟩ ∧ 𝑧 = 𝑍 ) ) → ( ( 2nd𝑣 ) RngHomo 𝑧 ) = ( 𝑌 RngHomo 𝑍 ) )
19 11 fveq2d ( ( 𝜑 ∧ ( 𝑣 = ⟨ 𝑋 , 𝑌 ⟩ ∧ 𝑧 = 𝑍 ) ) → ( 1st𝑣 ) = ( 1st ‘ ⟨ 𝑋 , 𝑌 ⟩ ) )
20 op1stg ( ( 𝑋𝐵𝑌𝐵 ) → ( 1st ‘ ⟨ 𝑋 , 𝑌 ⟩ ) = 𝑋 )
21 5 6 20 syl2anc ( 𝜑 → ( 1st ‘ ⟨ 𝑋 , 𝑌 ⟩ ) = 𝑋 )
22 21 adantr ( ( 𝜑 ∧ ( 𝑣 = ⟨ 𝑋 , 𝑌 ⟩ ∧ 𝑧 = 𝑍 ) ) → ( 1st ‘ ⟨ 𝑋 , 𝑌 ⟩ ) = 𝑋 )
23 19 22 eqtrd ( ( 𝜑 ∧ ( 𝑣 = ⟨ 𝑋 , 𝑌 ⟩ ∧ 𝑧 = 𝑍 ) ) → ( 1st𝑣 ) = 𝑋 )
24 23 16 oveq12d ( ( 𝜑 ∧ ( 𝑣 = ⟨ 𝑋 , 𝑌 ⟩ ∧ 𝑧 = 𝑍 ) ) → ( ( 1st𝑣 ) RngHomo ( 2nd𝑣 ) ) = ( 𝑋 RngHomo 𝑌 ) )
25 eqidd ( ( 𝜑 ∧ ( 𝑣 = ⟨ 𝑋 , 𝑌 ⟩ ∧ 𝑧 = 𝑍 ) ) → ( 𝑔𝑓 ) = ( 𝑔𝑓 ) )
26 18 24 25 mpoeq123dv ( ( 𝜑 ∧ ( 𝑣 = ⟨ 𝑋 , 𝑌 ⟩ ∧ 𝑧 = 𝑍 ) ) → ( 𝑔 ∈ ( ( 2nd𝑣 ) RngHomo 𝑧 ) , 𝑓 ∈ ( ( 1st𝑣 ) RngHomo ( 2nd𝑣 ) ) ↦ ( 𝑔𝑓 ) ) = ( 𝑔 ∈ ( 𝑌 RngHomo 𝑍 ) , 𝑓 ∈ ( 𝑋 RngHomo 𝑌 ) ↦ ( 𝑔𝑓 ) ) )
27 opelxpi ( ( 𝑋𝐵𝑌𝐵 ) → ⟨ 𝑋 , 𝑌 ⟩ ∈ ( 𝐵 × 𝐵 ) )
28 5 6 27 syl2anc ( 𝜑 → ⟨ 𝑋 , 𝑌 ⟩ ∈ ( 𝐵 × 𝐵 ) )
29 ovex ( 𝑌 RngHomo 𝑍 ) ∈ V
30 ovex ( 𝑋 RngHomo 𝑌 ) ∈ V
31 29 30 mpoex ( 𝑔 ∈ ( 𝑌 RngHomo 𝑍 ) , 𝑓 ∈ ( 𝑋 RngHomo 𝑌 ) ↦ ( 𝑔𝑓 ) ) ∈ V
32 31 a1i ( 𝜑 → ( 𝑔 ∈ ( 𝑌 RngHomo 𝑍 ) , 𝑓 ∈ ( 𝑋 RngHomo 𝑌 ) ↦ ( 𝑔𝑓 ) ) ∈ V )
33 10 26 28 7 32 ovmpod ( 𝜑 → ( ⟨ 𝑋 , 𝑌· 𝑍 ) = ( 𝑔 ∈ ( 𝑌 RngHomo 𝑍 ) , 𝑓 ∈ ( 𝑋 RngHomo 𝑌 ) ↦ ( 𝑔𝑓 ) ) )
34 simprl ( ( 𝜑 ∧ ( 𝑔 = 𝐺𝑓 = 𝐹 ) ) → 𝑔 = 𝐺 )
35 simprr ( ( 𝜑 ∧ ( 𝑔 = 𝐺𝑓 = 𝐹 ) ) → 𝑓 = 𝐹 )
36 34 35 coeq12d ( ( 𝜑 ∧ ( 𝑔 = 𝐺𝑓 = 𝐹 ) ) → ( 𝑔𝑓 ) = ( 𝐺𝐹 ) )
37 coexg ( ( 𝐺 ∈ ( 𝑌 RngHomo 𝑍 ) ∧ 𝐹 ∈ ( 𝑋 RngHomo 𝑌 ) ) → ( 𝐺𝐹 ) ∈ V )
38 9 8 37 syl2anc ( 𝜑 → ( 𝐺𝐹 ) ∈ V )
39 33 36 9 8 38 ovmpod ( 𝜑 → ( 𝐺 ( ⟨ 𝑋 , 𝑌· 𝑍 ) 𝐹 ) = ( 𝐺𝐹 ) )