Metamath Proof Explorer

Theorem parmapco

Description: An identity-fixing map preserving parallel arrows preserves every typed composition. (Contributed by Zhi Wang, 14-Sep-2026) (Revised by Zhi Wang, 17-Sep-2026)

Ref Expression
Hypotheses parmapcl.h ⊢ 𝐻 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ if ( 𝑥 = 𝑦 , { 𝐽 } , if ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) , 𝑆 , ∅ ) ) )
parmapco.p ⊢ 𝑆 ⊆ 𝒫 𝐽
parmapco.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝑈 𝐻 𝑉 ) )
parmapco.g ⊢ ( 𝜑 → 𝐺 ∈ ( 𝑉 𝐻 𝑊 ) )
parmapco.i ⊢ ( 𝜑 → ( 𝐴 ‘ 𝐽 ) = 𝐽 )
parmapco.a ⊢ ( ( 𝜑 ∧ 𝐹 ∈ 𝑆 ) → ( 𝐴 ‘ 𝐹 ) ∈ 𝑆 )
parmapco.b ⊢ ( ( 𝜑 ∧ 𝐺 ∈ 𝑆 ) → ( 𝐴 ‘ 𝐺 ) ∈ 𝑆 )
Assertion parmapco ( 𝜑 → ( 𝐴 ‘ ( 𝐺 ∩ 𝐹 ) ) = ( ( 𝐴 ‘ 𝐺 ) ∩ ( 𝐴 ‘ 𝐹 ) ) )

Proof

Step Hyp Ref Expression
1 parmapcl.h ⊢ 𝐻 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ if ( 𝑥 = 𝑦 , { 𝐽 } , if ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) , 𝑆 , ∅ ) ) )
2 parmapco.p ⊢ 𝑆 ⊆ 𝒫 𝐽
3 parmapco.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝑈 𝐻 𝑉 ) )
4 parmapco.g ⊢ ( 𝜑 → 𝐺 ∈ ( 𝑉 𝐻 𝑊 ) )
5 parmapco.i ⊢ ( 𝜑 → ( 𝐴 ‘ 𝐽 ) = 𝐽 )
6 parmapco.a ⊢ ( ( 𝜑 ∧ 𝐹 ∈ 𝑆 ) → ( 𝐴 ‘ 𝐹 ) ∈ 𝑆 )
7 parmapco.b ⊢ ( ( 𝜑 ∧ 𝐺 ∈ 𝑆 ) → ( 𝐴 ‘ 𝐺 ) ∈ 𝑆 )
8 1 4 5 7 parmapcl ⊢ ( 𝜑 → ( 𝐴 ‘ 𝐺 ) ∈ ( 𝑉 𝐻 𝑊 ) )
9 1 2 8 parhomss ⊢ ( 𝜑 → ( 𝐴 ‘ 𝐺 ) ⊆ 𝐽 )
10 9 adantr ⊢ ( ( 𝜑 ∧ 𝑈 = 𝑉 ) → ( 𝐴 ‘ 𝐺 ) ⊆ 𝐽 )
11 dfss2 ⊢ ( ( 𝐴 ‘ 𝐺 ) ⊆ 𝐽 ↔ ( ( 𝐴 ‘ 𝐺 ) ∩ 𝐽 ) = ( 𝐴 ‘ 𝐺 ) )
12 10 11 sylib ⊢ ( ( 𝜑 ∧ 𝑈 = 𝑉 ) → ( ( 𝐴 ‘ 𝐺 ) ∩ 𝐽 ) = ( 𝐴 ‘ 𝐺 ) )
13 3 adantr ⊢ ( ( 𝜑 ∧ 𝑈 = 𝑉 ) → 𝐹 ∈ ( 𝑈 𝐻 𝑉 ) )
14 simpr ⊢ ( ( 𝜑 ∧ 𝑈 = 𝑉 ) → 𝑈 = 𝑉 )
15 1 13 14 parhomideq ⊢ ( ( 𝜑 ∧ 𝑈 = 𝑉 ) → 𝐹 = 𝐽 )
16 15 fveq2d ⊢ ( ( 𝜑 ∧ 𝑈 = 𝑉 ) → ( 𝐴 ‘ 𝐹 ) = ( 𝐴 ‘ 𝐽 ) )
17 5 adantr ⊢ ( ( 𝜑 ∧ 𝑈 = 𝑉 ) → ( 𝐴 ‘ 𝐽 ) = 𝐽 )
18 16 17 eqtrd ⊢ ( ( 𝜑 ∧ 𝑈 = 𝑉 ) → ( 𝐴 ‘ 𝐹 ) = 𝐽 )
19 18 ineq2d ⊢ ( ( 𝜑 ∧ 𝑈 = 𝑉 ) → ( ( 𝐴 ‘ 𝐺 ) ∩ ( 𝐴 ‘ 𝐹 ) ) = ( ( 𝐴 ‘ 𝐺 ) ∩ 𝐽 ) )
20 15 ineq2d ⊢ ( ( 𝜑 ∧ 𝑈 = 𝑉 ) → ( 𝐺 ∩ 𝐹 ) = ( 𝐺 ∩ 𝐽 ) )
21 1 2 4 parhomss ⊢ ( 𝜑 → 𝐺 ⊆ 𝐽 )
22 21 adantr ⊢ ( ( 𝜑 ∧ 𝑈 = 𝑉 ) → 𝐺 ⊆ 𝐽 )
23 dfss2 ⊢ ( 𝐺 ⊆ 𝐽 ↔ ( 𝐺 ∩ 𝐽 ) = 𝐺 )
24 22 23 sylib ⊢ ( ( 𝜑 ∧ 𝑈 = 𝑉 ) → ( 𝐺 ∩ 𝐽 ) = 𝐺 )
25 20 24 eqtrd ⊢ ( ( 𝜑 ∧ 𝑈 = 𝑉 ) → ( 𝐺 ∩ 𝐹 ) = 𝐺 )
26 25 fveq2d ⊢ ( ( 𝜑 ∧ 𝑈 = 𝑉 ) → ( 𝐴 ‘ ( 𝐺 ∩ 𝐹 ) ) = ( 𝐴 ‘ 𝐺 ) )
27 12 19 26 3eqtr4rd ⊢ ( ( 𝜑 ∧ 𝑈 = 𝑉 ) → ( 𝐴 ‘ ( 𝐺 ∩ 𝐹 ) ) = ( ( 𝐴 ‘ 𝐺 ) ∩ ( 𝐴 ‘ 𝐹 ) ) )
28 1 3 5 6 parmapcl ⊢ ( 𝜑 → ( 𝐴 ‘ 𝐹 ) ∈ ( 𝑈 𝐻 𝑉 ) )
29 1 2 28 parhomss ⊢ ( 𝜑 → ( 𝐴 ‘ 𝐹 ) ⊆ 𝐽 )
30 29 adantr ⊢ ( ( 𝜑 ∧ 𝑉 = 𝑊 ) → ( 𝐴 ‘ 𝐹 ) ⊆ 𝐽 )
31 sseqin2 ⊢ ( ( 𝐴 ‘ 𝐹 ) ⊆ 𝐽 ↔ ( 𝐽 ∩ ( 𝐴 ‘ 𝐹 ) ) = ( 𝐴 ‘ 𝐹 ) )
32 30 31 sylib ⊢ ( ( 𝜑 ∧ 𝑉 = 𝑊 ) → ( 𝐽 ∩ ( 𝐴 ‘ 𝐹 ) ) = ( 𝐴 ‘ 𝐹 ) )
33 4 adantr ⊢ ( ( 𝜑 ∧ 𝑉 = 𝑊 ) → 𝐺 ∈ ( 𝑉 𝐻 𝑊 ) )
34 simpr ⊢ ( ( 𝜑 ∧ 𝑉 = 𝑊 ) → 𝑉 = 𝑊 )
35 1 33 34 parhomideq ⊢ ( ( 𝜑 ∧ 𝑉 = 𝑊 ) → 𝐺 = 𝐽 )
36 35 fveq2d ⊢ ( ( 𝜑 ∧ 𝑉 = 𝑊 ) → ( 𝐴 ‘ 𝐺 ) = ( 𝐴 ‘ 𝐽 ) )
37 5 adantr ⊢ ( ( 𝜑 ∧ 𝑉 = 𝑊 ) → ( 𝐴 ‘ 𝐽 ) = 𝐽 )
38 36 37 eqtrd ⊢ ( ( 𝜑 ∧ 𝑉 = 𝑊 ) → ( 𝐴 ‘ 𝐺 ) = 𝐽 )
39 38 ineq1d ⊢ ( ( 𝜑 ∧ 𝑉 = 𝑊 ) → ( ( 𝐴 ‘ 𝐺 ) ∩ ( 𝐴 ‘ 𝐹 ) ) = ( 𝐽 ∩ ( 𝐴 ‘ 𝐹 ) ) )
40 35 ineq1d ⊢ ( ( 𝜑 ∧ 𝑉 = 𝑊 ) → ( 𝐺 ∩ 𝐹 ) = ( 𝐽 ∩ 𝐹 ) )
41 1 2 3 parhomss ⊢ ( 𝜑 → 𝐹 ⊆ 𝐽 )
42 41 adantr ⊢ ( ( 𝜑 ∧ 𝑉 = 𝑊 ) → 𝐹 ⊆ 𝐽 )
43 sseqin2 ⊢ ( 𝐹 ⊆ 𝐽 ↔ ( 𝐽 ∩ 𝐹 ) = 𝐹 )
44 42 43 sylib ⊢ ( ( 𝜑 ∧ 𝑉 = 𝑊 ) → ( 𝐽 ∩ 𝐹 ) = 𝐹 )
45 40 44 eqtrd ⊢ ( ( 𝜑 ∧ 𝑉 = 𝑊 ) → ( 𝐺 ∩ 𝐹 ) = 𝐹 )
46 45 fveq2d ⊢ ( ( 𝜑 ∧ 𝑉 = 𝑊 ) → ( 𝐴 ‘ ( 𝐺 ∩ 𝐹 ) ) = ( 𝐴 ‘ 𝐹 ) )
47 32 39 46 3eqtr4rd ⊢ ( ( 𝜑 ∧ 𝑉 = 𝑊 ) → ( 𝐴 ‘ ( 𝐺 ∩ 𝐹 ) ) = ( ( 𝐴 ‘ 𝐺 ) ∩ ( 𝐴 ‘ 𝐹 ) ) )
48 1 3 4 parhomeqor ⊢ ( 𝜑 → ( 𝑈 = 𝑉 ∨ 𝑉 = 𝑊 ) )
49 27 47 48 mpjaodan ⊢ ( 𝜑 → ( 𝐴 ‘ ( 𝐺 ∩ 𝐹 ) ) = ( ( 𝐴 ‘ 𝐺 ) ∩ ( 𝐴 ‘ 𝐹 ) ) )