Metamath Proof Explorer

Theorem parmapco2

Description: Variant of parmapco . (Contributed by Zhi Wang, 14-Sep-2026) (Revised by Zhi Wang, 17-Sep-2026) (New usage is discouraged.) (Proof modification is discouraged.)

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