Metamath Proof Explorer

Theorem orbstaval

Description: Value of the function at a given equivalence class element. (Contributed by Mario Carneiro, 15-Jan-2015) (Proof shortened by Mario Carneiro, 23-Dec-2016)

		Ref	Expression
	Hypotheses	gasta.1	$⊢ X = {Base}_{G}$
		gasta.2	$⊢ H = \{u \in X \| u \underset{˙}{\oplus} A = A\}$
		orbsta.r	$⊢ \underset{˙}{\sim} = G ~_{QG} H$
		orbsta.f	$⊢ F = ran (k \in X ⟼ ⟨[k] \underset{˙}{\sim}, k \underset{˙}{\oplus} A⟩)$
	Assertion	orbstaval	$⊢ ((\underset{˙}{\oplus} \in (G GrpAct Y) \land A \in Y) \land B \in X) \to F ([B] \underset{˙}{\sim}) = B \underset{˙}{\oplus} A$

Proof

Step	Hyp	Ref	Expression
1		gasta.1	$⊢ X = {Base}_{G}$
2		gasta.2	$⊢ H = \{u \in X \| u \underset{˙}{\oplus} A = A\}$
3		orbsta.r	$⊢ \underset{˙}{\sim} = G ~_{QG} H$
4		orbsta.f	$⊢ F = ran (k \in X ⟼ ⟨[k] \underset{˙}{\sim}, k \underset{˙}{\oplus} A⟩)$
5		ovexd	$⊢ ((\underset{˙}{\oplus} \in (G GrpAct Y) \land A \in Y) \land k \in X) \to k \underset{˙}{\oplus} A \in V$
6	1 2	gastacl	$⊢ (\underset{˙}{\oplus} \in (G GrpAct Y) \land A \in Y) \to H \in SubGrp (G)$
7	1 3	eqger	$⊢ H \in SubGrp (G) \to \underset{˙}{\sim} Er X$
8	6 7	syl	$⊢ (\underset{˙}{\oplus} \in (G GrpAct Y) \land A \in Y) \to \underset{˙}{\sim} Er X$
9	1	fvexi	$⊢ X \in V$
10	9	a1i	$⊢ (\underset{˙}{\oplus} \in (G GrpAct Y) \land A \in Y) \to X \in V$
11		oveq1	$⊢ k = B \to k \underset{˙}{\oplus} A = B \underset{˙}{\oplus} A$
12	1 2 3 4	orbstafun	$⊢ (\underset{˙}{\oplus} \in (G GrpAct Y) \land A \in Y) \to Fun F$
13	4 5 8 10 11 12	qliftval	$⊢ ((\underset{˙}{\oplus} \in (G GrpAct Y) \land A \in Y) \land B \in X) \to F ([B] \underset{˙}{\sim}) = B \underset{˙}{\oplus} A$