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 
|- H = ( x e. B , y e. B |-> if ( x = y , { J } , if ( ( x = X /\ y = Y ) , S , (/) ) ) )
parmapco.p 
|- S C_ ~P J
parmapco.f 
|- ( ph -> F e. ( U H V ) )
parmapco.g 
|- ( ph -> G e. ( V H W ) )
parmapco.i 
|- ( ph -> ( A ` J ) = J )
parmapco.a 
|- ( ( ph /\ F e. S ) -> ( A ` F ) e. S )
parmapco.b 
|- ( ( ph /\ G e. S ) -> ( A ` G ) e. S )
Assertion parmapco 
|- ( ph -> ( A ` ( G i^i F ) ) = ( ( A ` G ) i^i ( A ` F ) ) )

Proof

Step Hyp Ref Expression
1 parmapcl.h 
 |-  H = ( x e. B , y e. B |-> if ( x = y , { J } , if ( ( x = X /\ y = Y ) , S , (/) ) ) )
2 parmapco.p 
 |-  S C_ ~P J
3 parmapco.f 
 |-  ( ph -> F e. ( U H V ) )
4 parmapco.g 
 |-  ( ph -> G e. ( V H W ) )
5 parmapco.i 
 |-  ( ph -> ( A ` J ) = J )
6 parmapco.a 
 |-  ( ( ph /\ F e. S ) -> ( A ` F ) e. S )
7 parmapco.b 
 |-  ( ( ph /\ G e. S ) -> ( A ` G ) e. S )
8 1 4 5 7 parmapcl 
 |-  ( ph -> ( A ` G ) e. ( V H W ) )
9 1 2 8 parhomss 
 |-  ( ph -> ( A ` G ) C_ J )
10 9 adantr 
 |-  ( ( ph /\ U = V ) -> ( A ` G ) C_ J )
11 dfss2 
 |-  ( ( A ` G ) C_ J <-> ( ( A ` G ) i^i J ) = ( A ` G ) )
12 10 11 sylib 
 |-  ( ( ph /\ U = V ) -> ( ( A ` G ) i^i J ) = ( A ` G ) )
13 3 adantr 
 |-  ( ( ph /\ U = V ) -> F e. ( U H V ) )
14 simpr 
 |-  ( ( ph /\ U = V ) -> U = V )
15 1 13 14 parhomideq 
 |-  ( ( ph /\ U = V ) -> F = J )
16 15 fveq2d 
 |-  ( ( ph /\ U = V ) -> ( A ` F ) = ( A ` J ) )
17 5 adantr 
 |-  ( ( ph /\ U = V ) -> ( A ` J ) = J )
18 16 17 eqtrd 
 |-  ( ( ph /\ U = V ) -> ( A ` F ) = J )
19 18 ineq2d 
 |-  ( ( ph /\ U = V ) -> ( ( A ` G ) i^i ( A ` F ) ) = ( ( A ` G ) i^i J ) )
20 15 ineq2d 
 |-  ( ( ph /\ U = V ) -> ( G i^i F ) = ( G i^i J ) )
21 1 2 4 parhomss 
 |-  ( ph -> G C_ J )
22 21 adantr 
 |-  ( ( ph /\ U = V ) -> G C_ J )
23 dfss2 
 |-  ( G C_ J <-> ( G i^i J ) = G )
24 22 23 sylib 
 |-  ( ( ph /\ U = V ) -> ( G i^i J ) = G )
25 20 24 eqtrd 
 |-  ( ( ph /\ U = V ) -> ( G i^i F ) = G )
26 25 fveq2d 
 |-  ( ( ph /\ U = V ) -> ( A ` ( G i^i F ) ) = ( A ` G ) )
27 12 19 26 3eqtr4rd 
 |-  ( ( ph /\ U = V ) -> ( A ` ( G i^i F ) ) = ( ( A ` G ) i^i ( A ` F ) ) )
28 1 3 5 6 parmapcl 
 |-  ( ph -> ( A ` F ) e. ( U H V ) )
29 1 2 28 parhomss 
 |-  ( ph -> ( A ` F ) C_ J )
30 29 adantr 
 |-  ( ( ph /\ V = W ) -> ( A ` F ) C_ J )
31 sseqin2 
 |-  ( ( A ` F ) C_ J <-> ( J i^i ( A ` F ) ) = ( A ` F ) )
32 30 31 sylib 
 |-  ( ( ph /\ V = W ) -> ( J i^i ( A ` F ) ) = ( A ` F ) )
33 4 adantr 
 |-  ( ( ph /\ V = W ) -> G e. ( V H W ) )
34 simpr 
 |-  ( ( ph /\ V = W ) -> V = W )
35 1 33 34 parhomideq 
 |-  ( ( ph /\ V = W ) -> G = J )
36 35 fveq2d 
 |-  ( ( ph /\ V = W ) -> ( A ` G ) = ( A ` J ) )
37 5 adantr 
 |-  ( ( ph /\ V = W ) -> ( A ` J ) = J )
38 36 37 eqtrd 
 |-  ( ( ph /\ V = W ) -> ( A ` G ) = J )
39 38 ineq1d 
 |-  ( ( ph /\ V = W ) -> ( ( A ` G ) i^i ( A ` F ) ) = ( J i^i ( A ` F ) ) )
40 35 ineq1d 
 |-  ( ( ph /\ V = W ) -> ( G i^i F ) = ( J i^i F ) )
41 1 2 3 parhomss 
 |-  ( ph -> F C_ J )
42 41 adantr 
 |-  ( ( ph /\ V = W ) -> F C_ J )
43 sseqin2 
 |-  ( F C_ J <-> ( J i^i F ) = F )
44 42 43 sylib 
 |-  ( ( ph /\ V = W ) -> ( J i^i F ) = F )
45 40 44 eqtrd 
 |-  ( ( ph /\ V = W ) -> ( G i^i F ) = F )
46 45 fveq2d 
 |-  ( ( ph /\ V = W ) -> ( A ` ( G i^i F ) ) = ( A ` F ) )
47 32 39 46 3eqtr4rd 
 |-  ( ( ph /\ V = W ) -> ( A ` ( G i^i F ) ) = ( ( A ` G ) i^i ( A ` F ) ) )
48 1 3 4 parhomeqor 
 |-  ( ph -> ( U = V \/ V = W ) )
49 27 47 48 mpjaodan 
 |-  ( ph -> ( A ` ( G i^i F ) ) = ( ( A ` G ) i^i ( A ` F ) ) )