This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem nati

Description: Naturality property of a natural transformation. (Contributed by Mario Carneiro, 6-Jan-2017)

Ref Expression
Hypotheses natrcl.1 ⊢ 𝑁 = ( 𝐶 Nat 𝐷 )
natixp.2 ⊢ ( 𝜑 → 𝐴 ∈ ( ⟨ 𝐹 , 𝐺 ⟩ 𝑁 ⟨ 𝐾 , 𝐿 ⟩ ) )
natixp.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
nati.h ⊢ 𝐻 = ( Hom ‘ 𝐶 )
nati.o ⊢ · = ( comp ‘ 𝐷 )
nati.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
nati.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
nati.r ⊢ ( 𝜑 → 𝑅 ∈ ( 𝑋 𝐻 𝑌 ) )
Assertion nati ( 𝜑 → ( ( 𝐴 ‘ 𝑌 ) ( ⟨ ( 𝐹 ‘ 𝑋 ) , ( 𝐹 ‘ 𝑌 ) ⟩ · ( 𝐾 ‘ 𝑌 ) ) ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑅 ) ) = ( ( ( 𝑋 𝐿 𝑌 ) ‘ 𝑅 ) ( ⟨ ( 𝐹 ‘ 𝑋 ) , ( 𝐾 ‘ 𝑋 ) ⟩ · ( 𝐾 ‘ 𝑌 ) ) ( 𝐴 ‘ 𝑋 ) ) )

Proof

Step Hyp Ref Expression
1 natrcl.1 ⊢ 𝑁 = ( 𝐶 Nat 𝐷 )
2 natixp.2 ⊢ ( 𝜑 → 𝐴 ∈ ( ⟨ 𝐹 , 𝐺 ⟩ 𝑁 ⟨ 𝐾 , 𝐿 ⟩ ) )
3 natixp.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
4 nati.h ⊢ 𝐻 = ( Hom ‘ 𝐶 )
5 nati.o ⊢ · = ( comp ‘ 𝐷 )
6 nati.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
7 nati.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
8 nati.r ⊢ ( 𝜑 → 𝑅 ∈ ( 𝑋 𝐻 𝑌 ) )
9 eqid ⊢ ( Hom ‘ 𝐷 ) = ( Hom ‘ 𝐷 )
10 1 natrcl ⊢ ( 𝐴 ∈ ( ⟨ 𝐹 , 𝐺 ⟩ 𝑁 ⟨ 𝐾 , 𝐿 ⟩ ) → ( ⟨ 𝐹 , 𝐺 ⟩ ∈ ( 𝐶 Func 𝐷 ) ∧ ⟨ 𝐾 , 𝐿 ⟩ ∈ ( 𝐶 Func 𝐷 ) ) )
11 2 10 syl ⊢ ( 𝜑 → ( ⟨ 𝐹 , 𝐺 ⟩ ∈ ( 𝐶 Func 𝐷 ) ∧ ⟨ 𝐾 , 𝐿 ⟩ ∈ ( 𝐶 Func 𝐷 ) ) )
12 11 simpld ⊢ ( 𝜑 → ⟨ 𝐹 , 𝐺 ⟩ ∈ ( 𝐶 Func 𝐷 ) )
13 df-br ⊢ ( 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 ↔ ⟨ 𝐹 , 𝐺 ⟩ ∈ ( 𝐶 Func 𝐷 ) )
14 12 13 sylibr ⊢ ( 𝜑 → 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 )
15 11 simprd ⊢ ( 𝜑 → ⟨ 𝐾 , 𝐿 ⟩ ∈ ( 𝐶 Func 𝐷 ) )
16 df-br ⊢ ( 𝐾 ( 𝐶 Func 𝐷 ) 𝐿 ↔ ⟨ 𝐾 , 𝐿 ⟩ ∈ ( 𝐶 Func 𝐷 ) )
17 15 16 sylibr ⊢ ( 𝜑 → 𝐾 ( 𝐶 Func 𝐷 ) 𝐿 )
18 1 3 4 9 5 14 17 isnat ⊢ ( 𝜑 → ( 𝐴 ∈ ( ⟨ 𝐹 , 𝐺 ⟩ 𝑁 ⟨ 𝐾 , 𝐿 ⟩ ) ↔ ( 𝐴 ∈ X 𝑥 ∈ 𝐵 ( ( 𝐹 ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( 𝐾 ‘ 𝑥 ) ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ( ( 𝐴 ‘ 𝑦 ) ( ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ · ( 𝐾 ‘ 𝑦 ) ) ( ( 𝑥 𝐺 𝑦 ) ‘ 𝑓 ) ) = ( ( ( 𝑥 𝐿 𝑦 ) ‘ 𝑓 ) ( ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐾 ‘ 𝑥 ) ⟩ · ( 𝐾 ‘ 𝑦 ) ) ( 𝐴 ‘ 𝑥 ) ) ) ) )
19 2 18 mpbid ⊢ ( 𝜑 → ( 𝐴 ∈ X 𝑥 ∈ 𝐵 ( ( 𝐹 ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( 𝐾 ‘ 𝑥 ) ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ( ( 𝐴 ‘ 𝑦 ) ( ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ · ( 𝐾 ‘ 𝑦 ) ) ( ( 𝑥 𝐺 𝑦 ) ‘ 𝑓 ) ) = ( ( ( 𝑥 𝐿 𝑦 ) ‘ 𝑓 ) ( ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐾 ‘ 𝑥 ) ⟩ · ( 𝐾 ‘ 𝑦 ) ) ( 𝐴 ‘ 𝑥 ) ) ) )
20 19 simprd ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ( ( 𝐴 ‘ 𝑦 ) ( ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ · ( 𝐾 ‘ 𝑦 ) ) ( ( 𝑥 𝐺 𝑦 ) ‘ 𝑓 ) ) = ( ( ( 𝑥 𝐿 𝑦 ) ‘ 𝑓 ) ( ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐾 ‘ 𝑥 ) ⟩ · ( 𝐾 ‘ 𝑦 ) ) ( 𝐴 ‘ 𝑥 ) ) )
21 7 adantr ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → 𝑌 ∈ 𝐵 )
22 8 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑌 ) → 𝑅 ∈ ( 𝑋 𝐻 𝑌 ) )
23 simplr ⊢ ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑌 ) → 𝑥 = 𝑋 )
24 simpr ⊢ ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑌 ) → 𝑦 = 𝑌 )
25 23 24 oveq12d ⊢ ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑌 ) → ( 𝑥 𝐻 𝑦 ) = ( 𝑋 𝐻 𝑌 ) )
26 22 25 eleqtrrd ⊢ ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑌 ) → 𝑅 ∈ ( 𝑥 𝐻 𝑦 ) )
27 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑌 ) ∧ 𝑓 = 𝑅 ) → 𝑥 = 𝑋 )
28 27 fveq2d ⊢ ( ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑌 ) ∧ 𝑓 = 𝑅 ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑋 ) )
29 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑌 ) ∧ 𝑓 = 𝑅 ) → 𝑦 = 𝑌 )
30 29 fveq2d ⊢ ( ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑌 ) ∧ 𝑓 = 𝑅 ) → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑌 ) )
31 28 30 opeq12d ⊢ ( ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑌 ) ∧ 𝑓 = 𝑅 ) → ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ = ⟨ ( 𝐹 ‘ 𝑋 ) , ( 𝐹 ‘ 𝑌 ) ⟩ )
32 29 fveq2d ⊢ ( ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑌 ) ∧ 𝑓 = 𝑅 ) → ( 𝐾 ‘ 𝑦 ) = ( 𝐾 ‘ 𝑌 ) )
33 31 32 oveq12d ⊢ ( ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑌 ) ∧ 𝑓 = 𝑅 ) → ( ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ · ( 𝐾 ‘ 𝑦 ) ) = ( ⟨ ( 𝐹 ‘ 𝑋 ) , ( 𝐹 ‘ 𝑌 ) ⟩ · ( 𝐾 ‘ 𝑌 ) ) )
34 29 fveq2d ⊢ ( ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑌 ) ∧ 𝑓 = 𝑅 ) → ( 𝐴 ‘ 𝑦 ) = ( 𝐴 ‘ 𝑌 ) )
35 27 29 oveq12d ⊢ ( ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑌 ) ∧ 𝑓 = 𝑅 ) → ( 𝑥 𝐺 𝑦 ) = ( 𝑋 𝐺 𝑌 ) )
36 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑌 ) ∧ 𝑓 = 𝑅 ) → 𝑓 = 𝑅 )
37 35 36 fveq12d ⊢ ( ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑌 ) ∧ 𝑓 = 𝑅 ) → ( ( 𝑥 𝐺 𝑦 ) ‘ 𝑓 ) = ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑅 ) )
38 33 34 37 oveq123d ⊢ ( ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑌 ) ∧ 𝑓 = 𝑅 ) → ( ( 𝐴 ‘ 𝑦 ) ( ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ · ( 𝐾 ‘ 𝑦 ) ) ( ( 𝑥 𝐺 𝑦 ) ‘ 𝑓 ) ) = ( ( 𝐴 ‘ 𝑌 ) ( ⟨ ( 𝐹 ‘ 𝑋 ) , ( 𝐹 ‘ 𝑌 ) ⟩ · ( 𝐾 ‘ 𝑌 ) ) ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑅 ) ) )
39 27 fveq2d ⊢ ( ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑌 ) ∧ 𝑓 = 𝑅 ) → ( 𝐾 ‘ 𝑥 ) = ( 𝐾 ‘ 𝑋 ) )
40 28 39 opeq12d ⊢ ( ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑌 ) ∧ 𝑓 = 𝑅 ) → ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐾 ‘ 𝑥 ) ⟩ = ⟨ ( 𝐹 ‘ 𝑋 ) , ( 𝐾 ‘ 𝑋 ) ⟩ )
41 40 32 oveq12d ⊢ ( ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑌 ) ∧ 𝑓 = 𝑅 ) → ( ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐾 ‘ 𝑥 ) ⟩ · ( 𝐾 ‘ 𝑦 ) ) = ( ⟨ ( 𝐹 ‘ 𝑋 ) , ( 𝐾 ‘ 𝑋 ) ⟩ · ( 𝐾 ‘ 𝑌 ) ) )
42 27 29 oveq12d ⊢ ( ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑌 ) ∧ 𝑓 = 𝑅 ) → ( 𝑥 𝐿 𝑦 ) = ( 𝑋 𝐿 𝑌 ) )
43 42 36 fveq12d ⊢ ( ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑌 ) ∧ 𝑓 = 𝑅 ) → ( ( 𝑥 𝐿 𝑦 ) ‘ 𝑓 ) = ( ( 𝑋 𝐿 𝑌 ) ‘ 𝑅 ) )
44 27 fveq2d ⊢ ( ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑌 ) ∧ 𝑓 = 𝑅 ) → ( 𝐴 ‘ 𝑥 ) = ( 𝐴 ‘ 𝑋 ) )
45 41 43 44 oveq123d ⊢ ( ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑌 ) ∧ 𝑓 = 𝑅 ) → ( ( ( 𝑥 𝐿 𝑦 ) ‘ 𝑓 ) ( ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐾 ‘ 𝑥 ) ⟩ · ( 𝐾 ‘ 𝑦 ) ) ( 𝐴 ‘ 𝑥 ) ) = ( ( ( 𝑋 𝐿 𝑌 ) ‘ 𝑅 ) ( ⟨ ( 𝐹 ‘ 𝑋 ) , ( 𝐾 ‘ 𝑋 ) ⟩ · ( 𝐾 ‘ 𝑌 ) ) ( 𝐴 ‘ 𝑋 ) ) )
46 38 45 eqeq12d ⊢ ( ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑌 ) ∧ 𝑓 = 𝑅 ) → ( ( ( 𝐴 ‘ 𝑦 ) ( ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ · ( 𝐾 ‘ 𝑦 ) ) ( ( 𝑥 𝐺 𝑦 ) ‘ 𝑓 ) ) = ( ( ( 𝑥 𝐿 𝑦 ) ‘ 𝑓 ) ( ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐾 ‘ 𝑥 ) ⟩ · ( 𝐾 ‘ 𝑦 ) ) ( 𝐴 ‘ 𝑥 ) ) ↔ ( ( 𝐴 ‘ 𝑌 ) ( ⟨ ( 𝐹 ‘ 𝑋 ) , ( 𝐹 ‘ 𝑌 ) ⟩ · ( 𝐾 ‘ 𝑌 ) ) ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑅 ) ) = ( ( ( 𝑋 𝐿 𝑌 ) ‘ 𝑅 ) ( ⟨ ( 𝐹 ‘ 𝑋 ) , ( 𝐾 ‘ 𝑋 ) ⟩ · ( 𝐾 ‘ 𝑌 ) ) ( 𝐴 ‘ 𝑋 ) ) ) )
47 26 46 rspcdv ⊢ ( ( ( 𝜑 ∧ 𝑥 = 𝑋 ) ∧ 𝑦 = 𝑌 ) → ( ∀ 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ( ( 𝐴 ‘ 𝑦 ) ( ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ · ( 𝐾 ‘ 𝑦 ) ) ( ( 𝑥 𝐺 𝑦 ) ‘ 𝑓 ) ) = ( ( ( 𝑥 𝐿 𝑦 ) ‘ 𝑓 ) ( ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐾 ‘ 𝑥 ) ⟩ · ( 𝐾 ‘ 𝑦 ) ) ( 𝐴 ‘ 𝑥 ) ) → ( ( 𝐴 ‘ 𝑌 ) ( ⟨ ( 𝐹 ‘ 𝑋 ) , ( 𝐹 ‘ 𝑌 ) ⟩ · ( 𝐾 ‘ 𝑌 ) ) ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑅 ) ) = ( ( ( 𝑋 𝐿 𝑌 ) ‘ 𝑅 ) ( ⟨ ( 𝐹 ‘ 𝑋 ) , ( 𝐾 ‘ 𝑋 ) ⟩ · ( 𝐾 ‘ 𝑌 ) ) ( 𝐴 ‘ 𝑋 ) ) ) )
48 21 47 rspcimdv ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → ( ∀ 𝑦 ∈ 𝐵 ∀ 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ( ( 𝐴 ‘ 𝑦 ) ( ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ · ( 𝐾 ‘ 𝑦 ) ) ( ( 𝑥 𝐺 𝑦 ) ‘ 𝑓 ) ) = ( ( ( 𝑥 𝐿 𝑦 ) ‘ 𝑓 ) ( ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐾 ‘ 𝑥 ) ⟩ · ( 𝐾 ‘ 𝑦 ) ) ( 𝐴 ‘ 𝑥 ) ) → ( ( 𝐴 ‘ 𝑌 ) ( ⟨ ( 𝐹 ‘ 𝑋 ) , ( 𝐹 ‘ 𝑌 ) ⟩ · ( 𝐾 ‘ 𝑌 ) ) ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑅 ) ) = ( ( ( 𝑋 𝐿 𝑌 ) ‘ 𝑅 ) ( ⟨ ( 𝐹 ‘ 𝑋 ) , ( 𝐾 ‘ 𝑋 ) ⟩ · ( 𝐾 ‘ 𝑌 ) ) ( 𝐴 ‘ 𝑋 ) ) ) )
49 6 48 rspcimdv ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ( ( 𝐴 ‘ 𝑦 ) ( ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ · ( 𝐾 ‘ 𝑦 ) ) ( ( 𝑥 𝐺 𝑦 ) ‘ 𝑓 ) ) = ( ( ( 𝑥 𝐿 𝑦 ) ‘ 𝑓 ) ( ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐾 ‘ 𝑥 ) ⟩ · ( 𝐾 ‘ 𝑦 ) ) ( 𝐴 ‘ 𝑥 ) ) → ( ( 𝐴 ‘ 𝑌 ) ( ⟨ ( 𝐹 ‘ 𝑋 ) , ( 𝐹 ‘ 𝑌 ) ⟩ · ( 𝐾 ‘ 𝑌 ) ) ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑅 ) ) = ( ( ( 𝑋 𝐿 𝑌 ) ‘ 𝑅 ) ( ⟨ ( 𝐹 ‘ 𝑋 ) , ( 𝐾 ‘ 𝑋 ) ⟩ · ( 𝐾 ‘ 𝑌 ) ) ( 𝐴 ‘ 𝑋 ) ) ) )
50 20 49 mpd ⊢ ( 𝜑 → ( ( 𝐴 ‘ 𝑌 ) ( ⟨ ( 𝐹 ‘ 𝑋 ) , ( 𝐹 ‘ 𝑌 ) ⟩ · ( 𝐾 ‘ 𝑌 ) ) ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑅 ) ) = ( ( ( 𝑋 𝐿 𝑌 ) ‘ 𝑅 ) ( ⟨ ( 𝐹 ‘ 𝑋 ) , ( 𝐾 ‘ 𝑋 ) ⟩ · ( 𝐾 ‘ 𝑌 ) ) ( 𝐴 ‘ 𝑋 ) ) )