Metamath Proof Explorer


Theorem gass

Description: A subset of a group action is a group action iff it is closed under the group action operation. (Contributed by Mario Carneiro, 17-Jan-2015)

Ref Expression
Hypothesis gass.1 𝑋 = ( Base ‘ 𝐺 )
Assertion gass ( ( ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑍𝑌 ) → ( ( ↾ ( 𝑋 × 𝑍 ) ) ∈ ( 𝐺 GrpAct 𝑍 ) ↔ ∀ 𝑥𝑋𝑦𝑍 ( 𝑥 𝑦 ) ∈ 𝑍 ) )

Proof

Step Hyp Ref Expression
1 gass.1 𝑋 = ( Base ‘ 𝐺 )
2 ovres ( ( 𝑥𝑋𝑦𝑍 ) → ( 𝑥 ( ↾ ( 𝑋 × 𝑍 ) ) 𝑦 ) = ( 𝑥 𝑦 ) )
3 2 adantl ( ( ( ( ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑍𝑌 ) ∧ ( ↾ ( 𝑋 × 𝑍 ) ) ∈ ( 𝐺 GrpAct 𝑍 ) ) ∧ ( 𝑥𝑋𝑦𝑍 ) ) → ( 𝑥 ( ↾ ( 𝑋 × 𝑍 ) ) 𝑦 ) = ( 𝑥 𝑦 ) )
4 1 gaf ( ( ↾ ( 𝑋 × 𝑍 ) ) ∈ ( 𝐺 GrpAct 𝑍 ) → ( ↾ ( 𝑋 × 𝑍 ) ) : ( 𝑋 × 𝑍 ) ⟶ 𝑍 )
5 4 adantl ( ( ( ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑍𝑌 ) ∧ ( ↾ ( 𝑋 × 𝑍 ) ) ∈ ( 𝐺 GrpAct 𝑍 ) ) → ( ↾ ( 𝑋 × 𝑍 ) ) : ( 𝑋 × 𝑍 ) ⟶ 𝑍 )
6 5 fovrnda ( ( ( ( ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑍𝑌 ) ∧ ( ↾ ( 𝑋 × 𝑍 ) ) ∈ ( 𝐺 GrpAct 𝑍 ) ) ∧ ( 𝑥𝑋𝑦𝑍 ) ) → ( 𝑥 ( ↾ ( 𝑋 × 𝑍 ) ) 𝑦 ) ∈ 𝑍 )
7 3 6 eqeltrrd ( ( ( ( ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑍𝑌 ) ∧ ( ↾ ( 𝑋 × 𝑍 ) ) ∈ ( 𝐺 GrpAct 𝑍 ) ) ∧ ( 𝑥𝑋𝑦𝑍 ) ) → ( 𝑥 𝑦 ) ∈ 𝑍 )
8 7 ralrimivva ( ( ( ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑍𝑌 ) ∧ ( ↾ ( 𝑋 × 𝑍 ) ) ∈ ( 𝐺 GrpAct 𝑍 ) ) → ∀ 𝑥𝑋𝑦𝑍 ( 𝑥 𝑦 ) ∈ 𝑍 )
9 gagrp ( ∈ ( 𝐺 GrpAct 𝑌 ) → 𝐺 ∈ Grp )
10 9 ad2antrr ( ( ( ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑍𝑌 ) ∧ ∀ 𝑥𝑋𝑦𝑍 ( 𝑥 𝑦 ) ∈ 𝑍 ) → 𝐺 ∈ Grp )
11 gaset ( ∈ ( 𝐺 GrpAct 𝑌 ) → 𝑌 ∈ V )
12 11 adantr ( ( ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑍𝑌 ) → 𝑌 ∈ V )
13 simpr ( ( ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑍𝑌 ) → 𝑍𝑌 )
14 12 13 ssexd ( ( ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑍𝑌 ) → 𝑍 ∈ V )
15 14 adantr ( ( ( ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑍𝑌 ) ∧ ∀ 𝑥𝑋𝑦𝑍 ( 𝑥 𝑦 ) ∈ 𝑍 ) → 𝑍 ∈ V )
16 10 15 jca ( ( ( ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑍𝑌 ) ∧ ∀ 𝑥𝑋𝑦𝑍 ( 𝑥 𝑦 ) ∈ 𝑍 ) → ( 𝐺 ∈ Grp ∧ 𝑍 ∈ V ) )
17 1 gaf ( ∈ ( 𝐺 GrpAct 𝑌 ) → : ( 𝑋 × 𝑌 ) ⟶ 𝑌 )
18 17 ad2antrr ( ( ( ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑍𝑌 ) ∧ ∀ 𝑥𝑋𝑦𝑍 ( 𝑥 𝑦 ) ∈ 𝑍 ) → : ( 𝑋 × 𝑌 ) ⟶ 𝑌 )
19 18 ffnd ( ( ( ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑍𝑌 ) ∧ ∀ 𝑥𝑋𝑦𝑍 ( 𝑥 𝑦 ) ∈ 𝑍 ) → Fn ( 𝑋 × 𝑌 ) )
20 simplr ( ( ( ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑍𝑌 ) ∧ ∀ 𝑥𝑋𝑦𝑍 ( 𝑥 𝑦 ) ∈ 𝑍 ) → 𝑍𝑌 )
21 xpss2 ( 𝑍𝑌 → ( 𝑋 × 𝑍 ) ⊆ ( 𝑋 × 𝑌 ) )
22 20 21 syl ( ( ( ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑍𝑌 ) ∧ ∀ 𝑥𝑋𝑦𝑍 ( 𝑥 𝑦 ) ∈ 𝑍 ) → ( 𝑋 × 𝑍 ) ⊆ ( 𝑋 × 𝑌 ) )
23 fnssres ( ( Fn ( 𝑋 × 𝑌 ) ∧ ( 𝑋 × 𝑍 ) ⊆ ( 𝑋 × 𝑌 ) ) → ( ↾ ( 𝑋 × 𝑍 ) ) Fn ( 𝑋 × 𝑍 ) )
24 19 22 23 syl2anc ( ( ( ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑍𝑌 ) ∧ ∀ 𝑥𝑋𝑦𝑍 ( 𝑥 𝑦 ) ∈ 𝑍 ) → ( ↾ ( 𝑋 × 𝑍 ) ) Fn ( 𝑋 × 𝑍 ) )
25 simpr ( ( ( ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑍𝑌 ) ∧ ∀ 𝑥𝑋𝑦𝑍 ( 𝑥 𝑦 ) ∈ 𝑍 ) → ∀ 𝑥𝑋𝑦𝑍 ( 𝑥 𝑦 ) ∈ 𝑍 )
26 2 eleq1d ( ( 𝑥𝑋𝑦𝑍 ) → ( ( 𝑥 ( ↾ ( 𝑋 × 𝑍 ) ) 𝑦 ) ∈ 𝑍 ↔ ( 𝑥 𝑦 ) ∈ 𝑍 ) )
27 26 ralbidva ( 𝑥𝑋 → ( ∀ 𝑦𝑍 ( 𝑥 ( ↾ ( 𝑋 × 𝑍 ) ) 𝑦 ) ∈ 𝑍 ↔ ∀ 𝑦𝑍 ( 𝑥 𝑦 ) ∈ 𝑍 ) )
28 27 ralbiia ( ∀ 𝑥𝑋𝑦𝑍 ( 𝑥 ( ↾ ( 𝑋 × 𝑍 ) ) 𝑦 ) ∈ 𝑍 ↔ ∀ 𝑥𝑋𝑦𝑍 ( 𝑥 𝑦 ) ∈ 𝑍 )
29 25 28 sylibr ( ( ( ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑍𝑌 ) ∧ ∀ 𝑥𝑋𝑦𝑍 ( 𝑥 𝑦 ) ∈ 𝑍 ) → ∀ 𝑥𝑋𝑦𝑍 ( 𝑥 ( ↾ ( 𝑋 × 𝑍 ) ) 𝑦 ) ∈ 𝑍 )
30 ffnov ( ( ↾ ( 𝑋 × 𝑍 ) ) : ( 𝑋 × 𝑍 ) ⟶ 𝑍 ↔ ( ( ↾ ( 𝑋 × 𝑍 ) ) Fn ( 𝑋 × 𝑍 ) ∧ ∀ 𝑥𝑋𝑦𝑍 ( 𝑥 ( ↾ ( 𝑋 × 𝑍 ) ) 𝑦 ) ∈ 𝑍 ) )
31 24 29 30 sylanbrc ( ( ( ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑍𝑌 ) ∧ ∀ 𝑥𝑋𝑦𝑍 ( 𝑥 𝑦 ) ∈ 𝑍 ) → ( ↾ ( 𝑋 × 𝑍 ) ) : ( 𝑋 × 𝑍 ) ⟶ 𝑍 )
32 eqid ( 0g𝐺 ) = ( 0g𝐺 )
33 1 32 grpidcl ( 𝐺 ∈ Grp → ( 0g𝐺 ) ∈ 𝑋 )
34 10 33 syl ( ( ( ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑍𝑌 ) ∧ ∀ 𝑥𝑋𝑦𝑍 ( 𝑥 𝑦 ) ∈ 𝑍 ) → ( 0g𝐺 ) ∈ 𝑋 )
35 ovres ( ( ( 0g𝐺 ) ∈ 𝑋𝑧𝑍 ) → ( ( 0g𝐺 ) ( ↾ ( 𝑋 × 𝑍 ) ) 𝑧 ) = ( ( 0g𝐺 ) 𝑧 ) )
36 34 35 sylan ( ( ( ( ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑍𝑌 ) ∧ ∀ 𝑥𝑋𝑦𝑍 ( 𝑥 𝑦 ) ∈ 𝑍 ) ∧ 𝑧𝑍 ) → ( ( 0g𝐺 ) ( ↾ ( 𝑋 × 𝑍 ) ) 𝑧 ) = ( ( 0g𝐺 ) 𝑧 ) )
37 simpll ( ( ( ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑍𝑌 ) ∧ ∀ 𝑥𝑋𝑦𝑍 ( 𝑥 𝑦 ) ∈ 𝑍 ) → ∈ ( 𝐺 GrpAct 𝑌 ) )
38 20 sselda ( ( ( ( ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑍𝑌 ) ∧ ∀ 𝑥𝑋𝑦𝑍 ( 𝑥 𝑦 ) ∈ 𝑍 ) ∧ 𝑧𝑍 ) → 𝑧𝑌 )
39 32 gagrpid ( ( ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑧𝑌 ) → ( ( 0g𝐺 ) 𝑧 ) = 𝑧 )
40 37 38 39 syl2an2r ( ( ( ( ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑍𝑌 ) ∧ ∀ 𝑥𝑋𝑦𝑍 ( 𝑥 𝑦 ) ∈ 𝑍 ) ∧ 𝑧𝑍 ) → ( ( 0g𝐺 ) 𝑧 ) = 𝑧 )
41 36 40 eqtrd ( ( ( ( ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑍𝑌 ) ∧ ∀ 𝑥𝑋𝑦𝑍 ( 𝑥 𝑦 ) ∈ 𝑍 ) ∧ 𝑧𝑍 ) → ( ( 0g𝐺 ) ( ↾ ( 𝑋 × 𝑍 ) ) 𝑧 ) = 𝑧 )
42 37 ad2antrr ( ( ( ( ( ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑍𝑌 ) ∧ ∀ 𝑥𝑋𝑦𝑍 ( 𝑥 𝑦 ) ∈ 𝑍 ) ∧ 𝑧𝑍 ) ∧ ( 𝑢𝑋𝑣𝑋 ) ) → ∈ ( 𝐺 GrpAct 𝑌 ) )
43 simprl ( ( ( ( ( ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑍𝑌 ) ∧ ∀ 𝑥𝑋𝑦𝑍 ( 𝑥 𝑦 ) ∈ 𝑍 ) ∧ 𝑧𝑍 ) ∧ ( 𝑢𝑋𝑣𝑋 ) ) → 𝑢𝑋 )
44 simprr ( ( ( ( ( ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑍𝑌 ) ∧ ∀ 𝑥𝑋𝑦𝑍 ( 𝑥 𝑦 ) ∈ 𝑍 ) ∧ 𝑧𝑍 ) ∧ ( 𝑢𝑋𝑣𝑋 ) ) → 𝑣𝑋 )
45 38 adantr ( ( ( ( ( ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑍𝑌 ) ∧ ∀ 𝑥𝑋𝑦𝑍 ( 𝑥 𝑦 ) ∈ 𝑍 ) ∧ 𝑧𝑍 ) ∧ ( 𝑢𝑋𝑣𝑋 ) ) → 𝑧𝑌 )
46 eqid ( +g𝐺 ) = ( +g𝐺 )
47 1 46 gaass ( ( ∈ ( 𝐺 GrpAct 𝑌 ) ∧ ( 𝑢𝑋𝑣𝑋𝑧𝑌 ) ) → ( ( 𝑢 ( +g𝐺 ) 𝑣 ) 𝑧 ) = ( 𝑢 ( 𝑣 𝑧 ) ) )
48 42 43 44 45 47 syl13anc ( ( ( ( ( ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑍𝑌 ) ∧ ∀ 𝑥𝑋𝑦𝑍 ( 𝑥 𝑦 ) ∈ 𝑍 ) ∧ 𝑧𝑍 ) ∧ ( 𝑢𝑋𝑣𝑋 ) ) → ( ( 𝑢 ( +g𝐺 ) 𝑣 ) 𝑧 ) = ( 𝑢 ( 𝑣 𝑧 ) ) )
49 simplr ( ( ( ( ( ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑍𝑌 ) ∧ ∀ 𝑥𝑋𝑦𝑍 ( 𝑥 𝑦 ) ∈ 𝑍 ) ∧ 𝑧𝑍 ) ∧ ( 𝑢𝑋𝑣𝑋 ) ) → 𝑧𝑍 )
50 simpllr ( ( ( ( ( ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑍𝑌 ) ∧ ∀ 𝑥𝑋𝑦𝑍 ( 𝑥 𝑦 ) ∈ 𝑍 ) ∧ 𝑧𝑍 ) ∧ ( 𝑢𝑋𝑣𝑋 ) ) → ∀ 𝑥𝑋𝑦𝑍 ( 𝑥 𝑦 ) ∈ 𝑍 )
51 ovrspc2v ( ( ( 𝑣𝑋𝑧𝑍 ) ∧ ∀ 𝑥𝑋𝑦𝑍 ( 𝑥 𝑦 ) ∈ 𝑍 ) → ( 𝑣 𝑧 ) ∈ 𝑍 )
52 44 49 50 51 syl21anc ( ( ( ( ( ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑍𝑌 ) ∧ ∀ 𝑥𝑋𝑦𝑍 ( 𝑥 𝑦 ) ∈ 𝑍 ) ∧ 𝑧𝑍 ) ∧ ( 𝑢𝑋𝑣𝑋 ) ) → ( 𝑣 𝑧 ) ∈ 𝑍 )
53 ovres ( ( 𝑢𝑋 ∧ ( 𝑣 𝑧 ) ∈ 𝑍 ) → ( 𝑢 ( ↾ ( 𝑋 × 𝑍 ) ) ( 𝑣 𝑧 ) ) = ( 𝑢 ( 𝑣 𝑧 ) ) )
54 43 52 53 syl2anc ( ( ( ( ( ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑍𝑌 ) ∧ ∀ 𝑥𝑋𝑦𝑍 ( 𝑥 𝑦 ) ∈ 𝑍 ) ∧ 𝑧𝑍 ) ∧ ( 𝑢𝑋𝑣𝑋 ) ) → ( 𝑢 ( ↾ ( 𝑋 × 𝑍 ) ) ( 𝑣 𝑧 ) ) = ( 𝑢 ( 𝑣 𝑧 ) ) )
55 48 54 eqtr4d ( ( ( ( ( ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑍𝑌 ) ∧ ∀ 𝑥𝑋𝑦𝑍 ( 𝑥 𝑦 ) ∈ 𝑍 ) ∧ 𝑧𝑍 ) ∧ ( 𝑢𝑋𝑣𝑋 ) ) → ( ( 𝑢 ( +g𝐺 ) 𝑣 ) 𝑧 ) = ( 𝑢 ( ↾ ( 𝑋 × 𝑍 ) ) ( 𝑣 𝑧 ) ) )
56 10 ad2antrr ( ( ( ( ( ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑍𝑌 ) ∧ ∀ 𝑥𝑋𝑦𝑍 ( 𝑥 𝑦 ) ∈ 𝑍 ) ∧ 𝑧𝑍 ) ∧ ( 𝑢𝑋𝑣𝑋 ) ) → 𝐺 ∈ Grp )
57 1 46 grpcl ( ( 𝐺 ∈ Grp ∧ 𝑢𝑋𝑣𝑋 ) → ( 𝑢 ( +g𝐺 ) 𝑣 ) ∈ 𝑋 )
58 56 43 44 57 syl3anc ( ( ( ( ( ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑍𝑌 ) ∧ ∀ 𝑥𝑋𝑦𝑍 ( 𝑥 𝑦 ) ∈ 𝑍 ) ∧ 𝑧𝑍 ) ∧ ( 𝑢𝑋𝑣𝑋 ) ) → ( 𝑢 ( +g𝐺 ) 𝑣 ) ∈ 𝑋 )
59 ovres ( ( ( 𝑢 ( +g𝐺 ) 𝑣 ) ∈ 𝑋𝑧𝑍 ) → ( ( 𝑢 ( +g𝐺 ) 𝑣 ) ( ↾ ( 𝑋 × 𝑍 ) ) 𝑧 ) = ( ( 𝑢 ( +g𝐺 ) 𝑣 ) 𝑧 ) )
60 58 49 59 syl2anc ( ( ( ( ( ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑍𝑌 ) ∧ ∀ 𝑥𝑋𝑦𝑍 ( 𝑥 𝑦 ) ∈ 𝑍 ) ∧ 𝑧𝑍 ) ∧ ( 𝑢𝑋𝑣𝑋 ) ) → ( ( 𝑢 ( +g𝐺 ) 𝑣 ) ( ↾ ( 𝑋 × 𝑍 ) ) 𝑧 ) = ( ( 𝑢 ( +g𝐺 ) 𝑣 ) 𝑧 ) )
61 ovres ( ( 𝑣𝑋𝑧𝑍 ) → ( 𝑣 ( ↾ ( 𝑋 × 𝑍 ) ) 𝑧 ) = ( 𝑣 𝑧 ) )
62 44 49 61 syl2anc ( ( ( ( ( ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑍𝑌 ) ∧ ∀ 𝑥𝑋𝑦𝑍 ( 𝑥 𝑦 ) ∈ 𝑍 ) ∧ 𝑧𝑍 ) ∧ ( 𝑢𝑋𝑣𝑋 ) ) → ( 𝑣 ( ↾ ( 𝑋 × 𝑍 ) ) 𝑧 ) = ( 𝑣 𝑧 ) )
63 62 oveq2d ( ( ( ( ( ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑍𝑌 ) ∧ ∀ 𝑥𝑋𝑦𝑍 ( 𝑥 𝑦 ) ∈ 𝑍 ) ∧ 𝑧𝑍 ) ∧ ( 𝑢𝑋𝑣𝑋 ) ) → ( 𝑢 ( ↾ ( 𝑋 × 𝑍 ) ) ( 𝑣 ( ↾ ( 𝑋 × 𝑍 ) ) 𝑧 ) ) = ( 𝑢 ( ↾ ( 𝑋 × 𝑍 ) ) ( 𝑣 𝑧 ) ) )
64 55 60 63 3eqtr4d ( ( ( ( ( ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑍𝑌 ) ∧ ∀ 𝑥𝑋𝑦𝑍 ( 𝑥 𝑦 ) ∈ 𝑍 ) ∧ 𝑧𝑍 ) ∧ ( 𝑢𝑋𝑣𝑋 ) ) → ( ( 𝑢 ( +g𝐺 ) 𝑣 ) ( ↾ ( 𝑋 × 𝑍 ) ) 𝑧 ) = ( 𝑢 ( ↾ ( 𝑋 × 𝑍 ) ) ( 𝑣 ( ↾ ( 𝑋 × 𝑍 ) ) 𝑧 ) ) )
65 64 ralrimivva ( ( ( ( ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑍𝑌 ) ∧ ∀ 𝑥𝑋𝑦𝑍 ( 𝑥 𝑦 ) ∈ 𝑍 ) ∧ 𝑧𝑍 ) → ∀ 𝑢𝑋𝑣𝑋 ( ( 𝑢 ( +g𝐺 ) 𝑣 ) ( ↾ ( 𝑋 × 𝑍 ) ) 𝑧 ) = ( 𝑢 ( ↾ ( 𝑋 × 𝑍 ) ) ( 𝑣 ( ↾ ( 𝑋 × 𝑍 ) ) 𝑧 ) ) )
66 41 65 jca ( ( ( ( ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑍𝑌 ) ∧ ∀ 𝑥𝑋𝑦𝑍 ( 𝑥 𝑦 ) ∈ 𝑍 ) ∧ 𝑧𝑍 ) → ( ( ( 0g𝐺 ) ( ↾ ( 𝑋 × 𝑍 ) ) 𝑧 ) = 𝑧 ∧ ∀ 𝑢𝑋𝑣𝑋 ( ( 𝑢 ( +g𝐺 ) 𝑣 ) ( ↾ ( 𝑋 × 𝑍 ) ) 𝑧 ) = ( 𝑢 ( ↾ ( 𝑋 × 𝑍 ) ) ( 𝑣 ( ↾ ( 𝑋 × 𝑍 ) ) 𝑧 ) ) ) )
67 66 ralrimiva ( ( ( ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑍𝑌 ) ∧ ∀ 𝑥𝑋𝑦𝑍 ( 𝑥 𝑦 ) ∈ 𝑍 ) → ∀ 𝑧𝑍 ( ( ( 0g𝐺 ) ( ↾ ( 𝑋 × 𝑍 ) ) 𝑧 ) = 𝑧 ∧ ∀ 𝑢𝑋𝑣𝑋 ( ( 𝑢 ( +g𝐺 ) 𝑣 ) ( ↾ ( 𝑋 × 𝑍 ) ) 𝑧 ) = ( 𝑢 ( ↾ ( 𝑋 × 𝑍 ) ) ( 𝑣 ( ↾ ( 𝑋 × 𝑍 ) ) 𝑧 ) ) ) )
68 31 67 jca ( ( ( ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑍𝑌 ) ∧ ∀ 𝑥𝑋𝑦𝑍 ( 𝑥 𝑦 ) ∈ 𝑍 ) → ( ( ↾ ( 𝑋 × 𝑍 ) ) : ( 𝑋 × 𝑍 ) ⟶ 𝑍 ∧ ∀ 𝑧𝑍 ( ( ( 0g𝐺 ) ( ↾ ( 𝑋 × 𝑍 ) ) 𝑧 ) = 𝑧 ∧ ∀ 𝑢𝑋𝑣𝑋 ( ( 𝑢 ( +g𝐺 ) 𝑣 ) ( ↾ ( 𝑋 × 𝑍 ) ) 𝑧 ) = ( 𝑢 ( ↾ ( 𝑋 × 𝑍 ) ) ( 𝑣 ( ↾ ( 𝑋 × 𝑍 ) ) 𝑧 ) ) ) ) )
69 1 46 32 isga ( ( ↾ ( 𝑋 × 𝑍 ) ) ∈ ( 𝐺 GrpAct 𝑍 ) ↔ ( ( 𝐺 ∈ Grp ∧ 𝑍 ∈ V ) ∧ ( ( ↾ ( 𝑋 × 𝑍 ) ) : ( 𝑋 × 𝑍 ) ⟶ 𝑍 ∧ ∀ 𝑧𝑍 ( ( ( 0g𝐺 ) ( ↾ ( 𝑋 × 𝑍 ) ) 𝑧 ) = 𝑧 ∧ ∀ 𝑢𝑋𝑣𝑋 ( ( 𝑢 ( +g𝐺 ) 𝑣 ) ( ↾ ( 𝑋 × 𝑍 ) ) 𝑧 ) = ( 𝑢 ( ↾ ( 𝑋 × 𝑍 ) ) ( 𝑣 ( ↾ ( 𝑋 × 𝑍 ) ) 𝑧 ) ) ) ) ) )
70 16 68 69 sylanbrc ( ( ( ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑍𝑌 ) ∧ ∀ 𝑥𝑋𝑦𝑍 ( 𝑥 𝑦 ) ∈ 𝑍 ) → ( ↾ ( 𝑋 × 𝑍 ) ) ∈ ( 𝐺 GrpAct 𝑍 ) )
71 8 70 impbida ( ( ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑍𝑌 ) → ( ( ↾ ( 𝑋 × 𝑍 ) ) ∈ ( 𝐺 GrpAct 𝑍 ) ↔ ∀ 𝑥𝑋𝑦𝑍 ( 𝑥 𝑦 ) ∈ 𝑍 ) )