Theorem gass 18903

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.)

Hypothesis

Ref	Expression
gass.1	⊢ 𝑋 = (Base‘𝐺)

Assertion

Ref	Expression
gass	⊢ (( ⊕ ∈ (𝐺 GrpAct 𝑌) ∧ 𝑍 ⊆ 𝑌) → (( ⊕ ↾ (𝑋 × 𝑍)) ∈ (𝐺 GrpAct 𝑍) ↔ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑍 (𝑥 ⊕ 𝑦) ∈ 𝑍))

Distinct variable groups:   𝑥,𝑦,𝐺   𝑥,𝑋,𝑦   𝑥,𝑌,𝑦   𝑥,𝑍,𝑦   𝑥, ⊕ ,𝑦

Proof of Theorem gass

Dummy variables 𝑣 𝑢 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ovres 7430	. . . . 5 ⊢ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑍) → (𝑥( ⊕ ↾ (𝑋 × 𝑍))𝑦) = (𝑥 ⊕ 𝑦))
2	1	adantl 482	. . . 4 ⊢ (((( ⊕ ∈ (𝐺 GrpAct 𝑌) ∧ 𝑍 ⊆ 𝑌) ∧ ( ⊕ ↾ (𝑋 × 𝑍)) ∈ (𝐺 GrpAct 𝑍)) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑍)) → (𝑥( ⊕ ↾ (𝑋 × 𝑍))𝑦) = (𝑥 ⊕ 𝑦))
3		gass.1	. . . . . . 7 ⊢ 𝑋 = (Base‘𝐺)
4	3	gaf 18897	. . . . . 6 ⊢ (( ⊕ ↾ (𝑋 × 𝑍)) ∈ (𝐺 GrpAct 𝑍) → ( ⊕ ↾ (𝑋 × 𝑍)):(𝑋 × 𝑍)⟶𝑍)
5	4	adantl 482	. . . . 5 ⊢ ((( ⊕ ∈ (𝐺 GrpAct 𝑌) ∧ 𝑍 ⊆ 𝑌) ∧ ( ⊕ ↾ (𝑋 × 𝑍)) ∈ (𝐺 GrpAct 𝑍)) → ( ⊕ ↾ (𝑋 × 𝑍)):(𝑋 × 𝑍)⟶𝑍)
6	5	fovrnda 7435	. . . 4 ⊢ (((( ⊕ ∈ (𝐺 GrpAct 𝑌) ∧ 𝑍 ⊆ 𝑌) ∧ ( ⊕ ↾ (𝑋 × 𝑍)) ∈ (𝐺 GrpAct 𝑍)) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑍)) → (𝑥( ⊕ ↾ (𝑋 × 𝑍))𝑦) ∈ 𝑍)
7	2, 6	eqeltrrd 2842	. . 3 ⊢ (((( ⊕ ∈ (𝐺 GrpAct 𝑌) ∧ 𝑍 ⊆ 𝑌) ∧ ( ⊕ ↾ (𝑋 × 𝑍)) ∈ (𝐺 GrpAct 𝑍)) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑍)) → (𝑥 ⊕ 𝑦) ∈ 𝑍)
8	7	ralrimivva 3117	. 2 ⊢ ((( ⊕ ∈ (𝐺 GrpAct 𝑌) ∧ 𝑍 ⊆ 𝑌) ∧ ( ⊕ ↾ (𝑋 × 𝑍)) ∈ (𝐺 GrpAct 𝑍)) → ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑍 (𝑥 ⊕ 𝑦) ∈ 𝑍)
9		gagrp 18894	. . . . 5 ⊢ ( ⊕ ∈ (𝐺 GrpAct 𝑌) → 𝐺 ∈ Grp)
10	9	ad2antrr 723	. . . 4 ⊢ ((( ⊕ ∈ (𝐺 GrpAct 𝑌) ∧ 𝑍 ⊆ 𝑌) ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑍 (𝑥 ⊕ 𝑦) ∈ 𝑍) → 𝐺 ∈ Grp)
11		gaset 18895	. . . . . . 7 ⊢ ( ⊕ ∈ (𝐺 GrpAct 𝑌) → 𝑌 ∈ V)
12	11	adantr 481	. . . . . 6 ⊢ (( ⊕ ∈ (𝐺 GrpAct 𝑌) ∧ 𝑍 ⊆ 𝑌) → 𝑌 ∈ V)
13		simpr 485	. . . . . 6 ⊢ (( ⊕ ∈ (𝐺 GrpAct 𝑌) ∧ 𝑍 ⊆ 𝑌) → 𝑍 ⊆ 𝑌)
14	12, 13	ssexd 5252	. . . . 5 ⊢ (( ⊕ ∈ (𝐺 GrpAct 𝑌) ∧ 𝑍 ⊆ 𝑌) → 𝑍 ∈ V)
15	14	adantr 481	. . . 4 ⊢ ((( ⊕ ∈ (𝐺 GrpAct 𝑌) ∧ 𝑍 ⊆ 𝑌) ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑍 (𝑥 ⊕ 𝑦) ∈ 𝑍) → 𝑍 ∈ V)
16	10, 15	jca 512	. . 3 ⊢ ((( ⊕ ∈ (𝐺 GrpAct 𝑌) ∧ 𝑍 ⊆ 𝑌) ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑍 (𝑥 ⊕ 𝑦) ∈ 𝑍) → (𝐺 ∈ Grp ∧ 𝑍 ∈ V))
17	3	gaf 18897	. . . . . . . 8 ⊢ ( ⊕ ∈ (𝐺 GrpAct 𝑌) → ⊕ :(𝑋 × 𝑌)⟶𝑌)
18	17	ad2antrr 723	. . . . . . 7 ⊢ ((( ⊕ ∈ (𝐺 GrpAct 𝑌) ∧ 𝑍 ⊆ 𝑌) ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑍 (𝑥 ⊕ 𝑦) ∈ 𝑍) → ⊕ :(𝑋 × 𝑌)⟶𝑌)
19	18	ffnd 6598	. . . . . 6 ⊢ ((( ⊕ ∈ (𝐺 GrpAct 𝑌) ∧ 𝑍 ⊆ 𝑌) ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑍 (𝑥 ⊕ 𝑦) ∈ 𝑍) → ⊕ Fn (𝑋 × 𝑌))
20		simplr 766	. . . . . . 7 ⊢ ((( ⊕ ∈ (𝐺 GrpAct 𝑌) ∧ 𝑍 ⊆ 𝑌) ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑍 (𝑥 ⊕ 𝑦) ∈ 𝑍) → 𝑍 ⊆ 𝑌)
21		xpss2 5609	. . . . . . 7 ⊢ (𝑍 ⊆ 𝑌 → (𝑋 × 𝑍) ⊆ (𝑋 × 𝑌))
22	20, 21	syl 17	. . . . . 6 ⊢ ((( ⊕ ∈ (𝐺 GrpAct 𝑌) ∧ 𝑍 ⊆ 𝑌) ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑍 (𝑥 ⊕ 𝑦) ∈ 𝑍) → (𝑋 × 𝑍) ⊆ (𝑋 × 𝑌))
23		fnssres 6552	. . . . . 6 ⊢ (( ⊕ Fn (𝑋 × 𝑌) ∧ (𝑋 × 𝑍) ⊆ (𝑋 × 𝑌)) → ( ⊕ ↾ (𝑋 × 𝑍)) Fn (𝑋 × 𝑍))
24	19, 22, 23	syl2anc 584	. . . . 5 ⊢ ((( ⊕ ∈ (𝐺 GrpAct 𝑌) ∧ 𝑍 ⊆ 𝑌) ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑍 (𝑥 ⊕ 𝑦) ∈ 𝑍) → ( ⊕ ↾ (𝑋 × 𝑍)) Fn (𝑋 × 𝑍))
25		simpr 485	. . . . . 6 ⊢ ((( ⊕ ∈ (𝐺 GrpAct 𝑌) ∧ 𝑍 ⊆ 𝑌) ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑍 (𝑥 ⊕ 𝑦) ∈ 𝑍) → ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑍 (𝑥 ⊕ 𝑦) ∈ 𝑍)
26	1	eleq1d 2825	. . . . . . . 8 ⊢ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑍) → ((𝑥( ⊕ ↾ (𝑋 × 𝑍))𝑦) ∈ 𝑍 ↔ (𝑥 ⊕ 𝑦) ∈ 𝑍))
27	26	ralbidva 3122	. . . . . . 7 ⊢ (𝑥 ∈ 𝑋 → (∀𝑦 ∈ 𝑍 (𝑥( ⊕ ↾ (𝑋 × 𝑍))𝑦) ∈ 𝑍 ↔ ∀𝑦 ∈ 𝑍 (𝑥 ⊕ 𝑦) ∈ 𝑍))
28	27	ralbiia 3092	. . . . . 6 ⊢ (∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑍 (𝑥( ⊕ ↾ (𝑋 × 𝑍))𝑦) ∈ 𝑍 ↔ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑍 (𝑥 ⊕ 𝑦) ∈ 𝑍)
29	25, 28	sylibr 233	. . . . 5 ⊢ ((( ⊕ ∈ (𝐺 GrpAct 𝑌) ∧ 𝑍 ⊆ 𝑌) ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑍 (𝑥 ⊕ 𝑦) ∈ 𝑍) → ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑍 (𝑥( ⊕ ↾ (𝑋 × 𝑍))𝑦) ∈ 𝑍)
30		ffnov 7393	. . . . 5 ⊢ (( ⊕ ↾ (𝑋 × 𝑍)):(𝑋 × 𝑍)⟶𝑍 ↔ (( ⊕ ↾ (𝑋 × 𝑍)) Fn (𝑋 × 𝑍) ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑍 (𝑥( ⊕ ↾ (𝑋 × 𝑍))𝑦) ∈ 𝑍))
31	24, 29, 30	sylanbrc 583	. . . 4 ⊢ ((( ⊕ ∈ (𝐺 GrpAct 𝑌) ∧ 𝑍 ⊆ 𝑌) ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑍 (𝑥 ⊕ 𝑦) ∈ 𝑍) → ( ⊕ ↾ (𝑋 × 𝑍)):(𝑋 × 𝑍)⟶𝑍)
32		eqid 2740	. . . . . . . . . 10 ⊢ (0g‘𝐺) = (0g‘𝐺)
33	3, 32	grpidcl 18603	. . . . . . . . 9 ⊢ (𝐺 ∈ Grp → (0g‘𝐺) ∈ 𝑋)
34	10, 33	syl 17	. . . . . . . 8 ⊢ ((( ⊕ ∈ (𝐺 GrpAct 𝑌) ∧ 𝑍 ⊆ 𝑌) ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑍 (𝑥 ⊕ 𝑦) ∈ 𝑍) → (0g‘𝐺) ∈ 𝑋)
35		ovres 7430	. . . . . . . 8 ⊢ (((0g‘𝐺) ∈ 𝑋 ∧ 𝑧 ∈ 𝑍) → ((0g‘𝐺)( ⊕ ↾ (𝑋 × 𝑍))𝑧) = ((0g‘𝐺) ⊕ 𝑧))
36	34, 35	sylan 580	. . . . . . 7 ⊢ (((( ⊕ ∈ (𝐺 GrpAct 𝑌) ∧ 𝑍 ⊆ 𝑌) ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑍 (𝑥 ⊕ 𝑦) ∈ 𝑍) ∧ 𝑧 ∈ 𝑍) → ((0g‘𝐺)( ⊕ ↾ (𝑋 × 𝑍))𝑧) = ((0g‘𝐺) ⊕ 𝑧))
37		simpll 764	. . . . . . . 8 ⊢ ((( ⊕ ∈ (𝐺 GrpAct 𝑌) ∧ 𝑍 ⊆ 𝑌) ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑍 (𝑥 ⊕ 𝑦) ∈ 𝑍) → ⊕ ∈ (𝐺 GrpAct 𝑌))
38	20	sselda 3926	. . . . . . . 8 ⊢ (((( ⊕ ∈ (𝐺 GrpAct 𝑌) ∧ 𝑍 ⊆ 𝑌) ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑍 (𝑥 ⊕ 𝑦) ∈ 𝑍) ∧ 𝑧 ∈ 𝑍) → 𝑧 ∈ 𝑌)
39	32	gagrpid 18896	. . . . . . . 8 ⊢ (( ⊕ ∈ (𝐺 GrpAct 𝑌) ∧ 𝑧 ∈ 𝑌) → ((0g‘𝐺) ⊕ 𝑧) = 𝑧)
40	37, 38, 39	syl2an2r 682	. . . . . . 7 ⊢ (((( ⊕ ∈ (𝐺 GrpAct 𝑌) ∧ 𝑍 ⊆ 𝑌) ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑍 (𝑥 ⊕ 𝑦) ∈ 𝑍) ∧ 𝑧 ∈ 𝑍) → ((0g‘𝐺) ⊕ 𝑧) = 𝑧)
41	36, 40	eqtrd 2780	. . . . . 6 ⊢ (((( ⊕ ∈ (𝐺 GrpAct 𝑌) ∧ 𝑍 ⊆ 𝑌) ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑍 (𝑥 ⊕ 𝑦) ∈ 𝑍) ∧ 𝑧 ∈ 𝑍) → ((0g‘𝐺)( ⊕ ↾ (𝑋 × 𝑍))𝑧) = 𝑧)
42	37	ad2antrr 723	. . . . . . . . . 10 ⊢ ((((( ⊕ ∈ (𝐺 GrpAct 𝑌) ∧ 𝑍 ⊆ 𝑌) ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑍 (𝑥 ⊕ 𝑦) ∈ 𝑍) ∧ 𝑧 ∈ 𝑍) ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) → ⊕ ∈ (𝐺 GrpAct 𝑌))
43		simprl 768	. . . . . . . . . 10 ⊢ ((((( ⊕ ∈ (𝐺 GrpAct 𝑌) ∧ 𝑍 ⊆ 𝑌) ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑍 (𝑥 ⊕ 𝑦) ∈ 𝑍) ∧ 𝑧 ∈ 𝑍) ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) → 𝑢 ∈ 𝑋)
44		simprr 770	. . . . . . . . . 10 ⊢ ((((( ⊕ ∈ (𝐺 GrpAct 𝑌) ∧ 𝑍 ⊆ 𝑌) ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑍 (𝑥 ⊕ 𝑦) ∈ 𝑍) ∧ 𝑧 ∈ 𝑍) ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) → 𝑣 ∈ 𝑋)
45	38	adantr 481	. . . . . . . . . 10 ⊢ ((((( ⊕ ∈ (𝐺 GrpAct 𝑌) ∧ 𝑍 ⊆ 𝑌) ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑍 (𝑥 ⊕ 𝑦) ∈ 𝑍) ∧ 𝑧 ∈ 𝑍) ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) → 𝑧 ∈ 𝑌)
46		eqid 2740	. . . . . . . . . . 11 ⊢ (+g‘𝐺) = (+g‘𝐺)
47	3, 46	gaass 18899	. . . . . . . . . 10 ⊢ (( ⊕ ∈ (𝐺 GrpAct 𝑌) ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋 ∧ 𝑧 ∈ 𝑌)) → ((𝑢(+g‘𝐺)𝑣) ⊕ 𝑧) = (𝑢 ⊕ (𝑣 ⊕ 𝑧)))
48	42, 43, 44, 45, 47	syl13anc 1371	. . . . . . . . 9 ⊢ ((((( ⊕ ∈ (𝐺 GrpAct 𝑌) ∧ 𝑍 ⊆ 𝑌) ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑍 (𝑥 ⊕ 𝑦) ∈ 𝑍) ∧ 𝑧 ∈ 𝑍) ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) → ((𝑢(+g‘𝐺)𝑣) ⊕ 𝑧) = (𝑢 ⊕ (𝑣 ⊕ 𝑧)))
49		simplr 766	. . . . . . . . . . 11 ⊢ ((((( ⊕ ∈ (𝐺 GrpAct 𝑌) ∧ 𝑍 ⊆ 𝑌) ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑍 (𝑥 ⊕ 𝑦) ∈ 𝑍) ∧ 𝑧 ∈ 𝑍) ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) → 𝑧 ∈ 𝑍)
50		simpllr 773	. . . . . . . . . . 11 ⊢ ((((( ⊕ ∈ (𝐺 GrpAct 𝑌) ∧ 𝑍 ⊆ 𝑌) ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑍 (𝑥 ⊕ 𝑦) ∈ 𝑍) ∧ 𝑧 ∈ 𝑍) ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) → ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑍 (𝑥 ⊕ 𝑦) ∈ 𝑍)
51		ovrspc2v 7295	. . . . . . . . . . 11 ⊢ (((𝑣 ∈ 𝑋 ∧ 𝑧 ∈ 𝑍) ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑍 (𝑥 ⊕ 𝑦) ∈ 𝑍) → (𝑣 ⊕ 𝑧) ∈ 𝑍)
52	44, 49, 50, 51	syl21anc 835	. . . . . . . . . 10 ⊢ ((((( ⊕ ∈ (𝐺 GrpAct 𝑌) ∧ 𝑍 ⊆ 𝑌) ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑍 (𝑥 ⊕ 𝑦) ∈ 𝑍) ∧ 𝑧 ∈ 𝑍) ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) → (𝑣 ⊕ 𝑧) ∈ 𝑍)
53		ovres 7430	. . . . . . . . . 10 ⊢ ((𝑢 ∈ 𝑋 ∧ (𝑣 ⊕ 𝑧) ∈ 𝑍) → (𝑢( ⊕ ↾ (𝑋 × 𝑍))(𝑣 ⊕ 𝑧)) = (𝑢 ⊕ (𝑣 ⊕ 𝑧)))
54	43, 52, 53	syl2anc 584	. . . . . . . . 9 ⊢ ((((( ⊕ ∈ (𝐺 GrpAct 𝑌) ∧ 𝑍 ⊆ 𝑌) ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑍 (𝑥 ⊕ 𝑦) ∈ 𝑍) ∧ 𝑧 ∈ 𝑍) ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) → (𝑢( ⊕ ↾ (𝑋 × 𝑍))(𝑣 ⊕ 𝑧)) = (𝑢 ⊕ (𝑣 ⊕ 𝑧)))
55	48, 54	eqtr4d 2783	. . . . . . . 8 ⊢ ((((( ⊕ ∈ (𝐺 GrpAct 𝑌) ∧ 𝑍 ⊆ 𝑌) ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑍 (𝑥 ⊕ 𝑦) ∈ 𝑍) ∧ 𝑧 ∈ 𝑍) ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) → ((𝑢(+g‘𝐺)𝑣) ⊕ 𝑧) = (𝑢( ⊕ ↾ (𝑋 × 𝑍))(𝑣 ⊕ 𝑧)))
56	10	ad2antrr 723	. . . . . . . . . 10 ⊢ ((((( ⊕ ∈ (𝐺 GrpAct 𝑌) ∧ 𝑍 ⊆ 𝑌) ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑍 (𝑥 ⊕ 𝑦) ∈ 𝑍) ∧ 𝑧 ∈ 𝑍) ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) → 𝐺 ∈ Grp)
57	3, 46	grpcl 18581	. . . . . . . . . 10 ⊢ ((𝐺 ∈ Grp ∧ 𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋) → (𝑢(+g‘𝐺)𝑣) ∈ 𝑋)
58	56, 43, 44, 57	syl3anc 1370	. . . . . . . . 9 ⊢ ((((( ⊕ ∈ (𝐺 GrpAct 𝑌) ∧ 𝑍 ⊆ 𝑌) ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑍 (𝑥 ⊕ 𝑦) ∈ 𝑍) ∧ 𝑧 ∈ 𝑍) ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) → (𝑢(+g‘𝐺)𝑣) ∈ 𝑋)
59		ovres 7430	. . . . . . . . 9 ⊢ (((𝑢(+g‘𝐺)𝑣) ∈ 𝑋 ∧ 𝑧 ∈ 𝑍) → ((𝑢(+g‘𝐺)𝑣)( ⊕ ↾ (𝑋 × 𝑍))𝑧) = ((𝑢(+g‘𝐺)𝑣) ⊕ 𝑧))
60	58, 49, 59	syl2anc 584	. . . . . . . 8 ⊢ ((((( ⊕ ∈ (𝐺 GrpAct 𝑌) ∧ 𝑍 ⊆ 𝑌) ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑍 (𝑥 ⊕ 𝑦) ∈ 𝑍) ∧ 𝑧 ∈ 𝑍) ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) → ((𝑢(+g‘𝐺)𝑣)( ⊕ ↾ (𝑋 × 𝑍))𝑧) = ((𝑢(+g‘𝐺)𝑣) ⊕ 𝑧))
61		ovres 7430	. . . . . . . . . 10 ⊢ ((𝑣 ∈ 𝑋 ∧ 𝑧 ∈ 𝑍) → (𝑣( ⊕ ↾ (𝑋 × 𝑍))𝑧) = (𝑣 ⊕ 𝑧))
62	44, 49, 61	syl2anc 584	. . . . . . . . 9 ⊢ ((((( ⊕ ∈ (𝐺 GrpAct 𝑌) ∧ 𝑍 ⊆ 𝑌) ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑍 (𝑥 ⊕ 𝑦) ∈ 𝑍) ∧ 𝑧 ∈ 𝑍) ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) → (𝑣( ⊕ ↾ (𝑋 × 𝑍))𝑧) = (𝑣 ⊕ 𝑧))
63	62	oveq2d 7285	. . . . . . . 8 ⊢ ((((( ⊕ ∈ (𝐺 GrpAct 𝑌) ∧ 𝑍 ⊆ 𝑌) ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑍 (𝑥 ⊕ 𝑦) ∈ 𝑍) ∧ 𝑧 ∈ 𝑍) ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) → (𝑢( ⊕ ↾ (𝑋 × 𝑍))(𝑣( ⊕ ↾ (𝑋 × 𝑍))𝑧)) = (𝑢( ⊕ ↾ (𝑋 × 𝑍))(𝑣 ⊕ 𝑧)))
64	55, 60, 63	3eqtr4d 2790	. . . . . . 7 ⊢ ((((( ⊕ ∈ (𝐺 GrpAct 𝑌) ∧ 𝑍 ⊆ 𝑌) ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑍 (𝑥 ⊕ 𝑦) ∈ 𝑍) ∧ 𝑧 ∈ 𝑍) ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) → ((𝑢(+g‘𝐺)𝑣)( ⊕ ↾ (𝑋 × 𝑍))𝑧) = (𝑢( ⊕ ↾ (𝑋 × 𝑍))(𝑣( ⊕ ↾ (𝑋 × 𝑍))𝑧)))
65	64	ralrimivva 3117	. . . . . 6 ⊢ (((( ⊕ ∈ (𝐺 GrpAct 𝑌) ∧ 𝑍 ⊆ 𝑌) ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑍 (𝑥 ⊕ 𝑦) ∈ 𝑍) ∧ 𝑧 ∈ 𝑍) → ∀𝑢 ∈ 𝑋 ∀𝑣 ∈ 𝑋 ((𝑢(+g‘𝐺)𝑣)( ⊕ ↾ (𝑋 × 𝑍))𝑧) = (𝑢( ⊕ ↾ (𝑋 × 𝑍))(𝑣( ⊕ ↾ (𝑋 × 𝑍))𝑧)))
66	41, 65	jca 512	. . . . 5 ⊢ (((( ⊕ ∈ (𝐺 GrpAct 𝑌) ∧ 𝑍 ⊆ 𝑌) ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑍 (𝑥 ⊕ 𝑦) ∈ 𝑍) ∧ 𝑧 ∈ 𝑍) → (((0g‘𝐺)( ⊕ ↾ (𝑋 × 𝑍))𝑧) = 𝑧 ∧ ∀𝑢 ∈ 𝑋 ∀𝑣 ∈ 𝑋 ((𝑢(+g‘𝐺)𝑣)( ⊕ ↾ (𝑋 × 𝑍))𝑧) = (𝑢( ⊕ ↾ (𝑋 × 𝑍))(𝑣( ⊕ ↾ (𝑋 × 𝑍))𝑧))))
67	66	ralrimiva 3110	. . . 4 ⊢ ((( ⊕ ∈ (𝐺 GrpAct 𝑌) ∧ 𝑍 ⊆ 𝑌) ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑍 (𝑥 ⊕ 𝑦) ∈ 𝑍) → ∀𝑧 ∈ 𝑍 (((0g‘𝐺)( ⊕ ↾ (𝑋 × 𝑍))𝑧) = 𝑧 ∧ ∀𝑢 ∈ 𝑋 ∀𝑣 ∈ 𝑋 ((𝑢(+g‘𝐺)𝑣)( ⊕ ↾ (𝑋 × 𝑍))𝑧) = (𝑢( ⊕ ↾ (𝑋 × 𝑍))(𝑣( ⊕ ↾ (𝑋 × 𝑍))𝑧))))
68	31, 67	jca 512	. . 3 ⊢ ((( ⊕ ∈ (𝐺 GrpAct 𝑌) ∧ 𝑍 ⊆ 𝑌) ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑍 (𝑥 ⊕ 𝑦) ∈ 𝑍) → (( ⊕ ↾ (𝑋 × 𝑍)):(𝑋 × 𝑍)⟶𝑍 ∧ ∀𝑧 ∈ 𝑍 (((0g‘𝐺)( ⊕ ↾ (𝑋 × 𝑍))𝑧) = 𝑧 ∧ ∀𝑢 ∈ 𝑋 ∀𝑣 ∈ 𝑋 ((𝑢(+g‘𝐺)𝑣)( ⊕ ↾ (𝑋 × 𝑍))𝑧) = (𝑢( ⊕ ↾ (𝑋 × 𝑍))(𝑣( ⊕ ↾ (𝑋 × 𝑍))𝑧)))))
69	3, 46, 32	isga 18893	. . 3 ⊢ (( ⊕ ↾ (𝑋 × 𝑍)) ∈ (𝐺 GrpAct 𝑍) ↔ ((𝐺 ∈ Grp ∧ 𝑍 ∈ V) ∧ (( ⊕ ↾ (𝑋 × 𝑍)):(𝑋 × 𝑍)⟶𝑍 ∧ ∀𝑧 ∈ 𝑍 (((0g‘𝐺)( ⊕ ↾ (𝑋 × 𝑍))𝑧) = 𝑧 ∧ ∀𝑢 ∈ 𝑋 ∀𝑣 ∈ 𝑋 ((𝑢(+g‘𝐺)𝑣)( ⊕ ↾ (𝑋 × 𝑍))𝑧) = (𝑢( ⊕ ↾ (𝑋 × 𝑍))(𝑣( ⊕ ↾ (𝑋 × 𝑍))𝑧))))))
70	16, 68, 69	sylanbrc 583	. 2 ⊢ ((( ⊕ ∈ (𝐺 GrpAct 𝑌) ∧ 𝑍 ⊆ 𝑌) ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑍 (𝑥 ⊕ 𝑦) ∈ 𝑍) → ( ⊕ ↾ (𝑋 × 𝑍)) ∈ (𝐺 GrpAct 𝑍))
71	8, 70	impbida 798	1 ⊢ (( ⊕ ∈ (𝐺 GrpAct 𝑌) ∧ 𝑍 ⊆ 𝑌) → (( ⊕ ↾ (𝑋 × 𝑍)) ∈ (𝐺 GrpAct 𝑍) ↔ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑍 (𝑥 ⊕ 𝑦) ∈ 𝑍))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   = wceq 1542   ∈ wcel 2110  ∀wral 3066  Vcvv 3431   ⊆ wss 3892   × cxp 5587   ↾ cres 5591   Fn wfn 6426  ⟶wf 6427  ‘cfv 6431  (class class class)co 7269  Basecbs 16908  +_gcplusg 16958  0_gc0g 17146  Grpcgrp 18573   GrpAct cga 18891

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2711  ax-sep 5227  ax-nul 5234  ax-pow 5292  ax-pr 5356  ax-un 7580

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2072  df-mo 2542  df-eu 2571  df-clab 2718  df-cleq 2732  df-clel 2818  df-nfc 2891  df-ne 2946  df-ral 3071  df-rex 3072  df-reu 3073  df-rmo 3074  df-rab 3075  df-v 3433  df-sbc 3721  df-csb 3838  df-dif 3895  df-un 3897  df-in 3899  df-ss 3909  df-nul 4263  df-if 4466  df-pw 4541  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4846  df-iun 4932  df-br 5080  df-opab 5142  df-mpt 5163  df-id 5489  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-rn 5600  df-res 5601  df-iota 6389  df-fun 6433  df-fn 6434  df-f 6435  df-fv 6439  df-riota 7226  df-ov 7272  df-oprab 7273  df-mpo 7274  df-map 8598  df-0g 17148  df-mgm 18322  df-sgrp 18371  df-mnd 18382  df-grp 18576  df-ga 18892

This theorem is referenced by: (None)