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

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 fovcdmda ⊢ ( ( ( ( ⊕ ∈ ( 𝐺 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 𝑍 ) ↔ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑍 ( 𝑥 ⊕ 𝑦 ) ∈ 𝑍 ) )