aks6d1c1p1

Description: Definition of the introspective relation. (Contributed by metakunt, 25-Apr-2025)

	Ref	Expression
Hypotheses	aks6d1c1p1.1	$⊢ \underset{˙}{\sim} = \{⟨e, f⟩ \| (e \in ℕ \land f \in B \land \forall y \in (K PrimRoots R) e \underset{˙}{\times} O (f) (y) = O (f) (e D y))\}$
	aks6d1c1p1.2	$⊢ φ \to F \in B$
	aks6d1c1p1.3	$⊢ φ \to E \in ℕ$
Assertion	aks6d1c1p1	$⊢ φ \to (E \underset{˙}{\sim} F \leftrightarrow \forall y \in (K PrimRoots R) E \underset{˙}{\times} O (F) (y) = O (F) (E D y))$

Proof

Step	Hyp	Ref	Expression
1		aks6d1c1p1.1	$⊢ \underset{˙}{\sim} = \{⟨e, f⟩ \| (e \in ℕ \land f \in B \land \forall y \in (K PrimRoots R) e \underset{˙}{\times} O (f) (y) = O (f) (e D y))\}$
2		aks6d1c1p1.2	$⊢ φ \to F \in B$
3		aks6d1c1p1.3	$⊢ φ \to E \in ℕ$
4		simpl	$⊢ (e = E \land f = F) \to e = E$
5	4	eleq1d	$⊢ (e = E \land f = F) \to (e \in ℕ \leftrightarrow E \in ℕ)$
6		simpr	$⊢ (e = E \land f = F) \to f = F$
7	6	eleq1d	$⊢ (e = E \land f = F) \to (f \in B \leftrightarrow F \in B)$
8	6	fveq2d	$⊢ (e = E \land f = F) \to O (f) = O (F)$
9	8	fveq1d	$⊢ (e = E \land f = F) \to O (f) (y) = O (F) (y)$
10	4 9	oveq12d	$⊢ (e = E \land f = F) \to e \underset{˙}{\times} O (f) (y) = E \underset{˙}{\times} O (F) (y)$
11	4	oveq1d	$⊢ (e = E \land f = F) \to e D y = E D y$
12	8 11	fveq12d	$⊢ (e = E \land f = F) \to O (f) (e D y) = O (F) (E D y)$
13	10 12	eqeq12d	$⊢ (e = E \land f = F) \to (e \underset{˙}{\times} O (f) (y) = O (f) (e D y) \leftrightarrow E \underset{˙}{\times} O (F) (y) = O (F) (E D y))$
14	13	ralbidv	$⊢ (e = E \land f = F) \to (\forall y \in (K PrimRoots R) e \underset{˙}{\times} O (f) (y) = O (f) (e D y) \leftrightarrow \forall y \in (K PrimRoots R) E \underset{˙}{\times} O (F) (y) = O (F) (E D y))$
15	5 7 14	3anbi123d	$⊢ (e = E \land f = F) \to ((e \in ℕ \land f \in B \land \forall y \in (K PrimRoots R) e \underset{˙}{\times} O (f) (y) = O (f) (e D y)) \leftrightarrow (E \in ℕ \land F \in B \land \forall y \in (K PrimRoots R) E \underset{˙}{\times} O (F) (y) = O (F) (E D y)))$
16	15 1	brabga	$⊢ (E \in ℕ \land F \in B) \to (E \underset{˙}{\sim} F \leftrightarrow (E \in ℕ \land F \in B \land \forall y \in (K PrimRoots R) E \underset{˙}{\times} O (F) (y) = O (F) (E D y)))$
17	3 2 16	syl2anc	$⊢ φ \to (E \underset{˙}{\sim} F \leftrightarrow (E \in ℕ \land F \in B \land \forall y \in (K PrimRoots R) E \underset{˙}{\times} O (F) (y) = O (F) (E D y)))$
18	17	biimpd	$⊢ φ \to (E \underset{˙}{\sim} F \to (E \in ℕ \land F \in B \land \forall y \in (K PrimRoots R) E \underset{˙}{\times} O (F) (y) = O (F) (E D y)))$
19	18	imp	$⊢ (φ \land E \underset{˙}{\sim} F) \to (E \in ℕ \land F \in B \land \forall y \in (K PrimRoots R) E \underset{˙}{\times} O (F) (y) = O (F) (E D y))$
20	19	simp3d	$⊢ (φ \land E \underset{˙}{\sim} F) \to \forall y \in (K PrimRoots R) E \underset{˙}{\times} O (F) (y) = O (F) (E D y)$
21	20	ex	$⊢ φ \to (E \underset{˙}{\sim} F \to \forall y \in (K PrimRoots R) E \underset{˙}{\times} O (F) (y) = O (F) (E D y))$
22	3 2	jca	$⊢ φ \to (E \in ℕ \land F \in B)$
23		df-3an	$⊢ (E \in ℕ \land F \in B \land \forall y \in (K PrimRoots R) E \underset{˙}{\times} O (F) (y) = O (F) (E D y)) \leftrightarrow ((E \in ℕ \land F \in B) \land \forall y \in (K PrimRoots R) E \underset{˙}{\times} O (F) (y) = O (F) (E D y))$
24	23	bicomi	$⊢ ((E \in ℕ \land F \in B) \land \forall y \in (K PrimRoots R) E \underset{˙}{\times} O (F) (y) = O (F) (E D y)) \leftrightarrow (E \in ℕ \land F \in B \land \forall y \in (K PrimRoots R) E \underset{˙}{\times} O (F) (y) = O (F) (E D y))$
25	24	a1i	$⊢ φ \to (((E \in ℕ \land F \in B) \land \forall y \in (K PrimRoots R) E \underset{˙}{\times} O (F) (y) = O (F) (E D y)) \leftrightarrow (E \in ℕ \land F \in B \land \forall y \in (K PrimRoots R) E \underset{˙}{\times} O (F) (y) = O (F) (E D y)))$
26	17	biimprd	$⊢ φ \to ((E \in ℕ \land F \in B \land \forall y \in (K PrimRoots R) E \underset{˙}{\times} O (F) (y) = O (F) (E D y)) \to E \underset{˙}{\sim} F)$
27	25 26	sylbid	$⊢ φ \to (((E \in ℕ \land F \in B) \land \forall y \in (K PrimRoots R) E \underset{˙}{\times} O (F) (y) = O (F) (E D y)) \to E \underset{˙}{\sim} F)$
28	27	imp	$⊢ (φ \land ((E \in ℕ \land F \in B) \land \forall y \in (K PrimRoots R) E \underset{˙}{\times} O (F) (y) = O (F) (E D y))) \to E \underset{˙}{\sim} F$
29	28	anassrs	$⊢ ((φ \land (E \in ℕ \land F \in B)) \land \forall y \in (K PrimRoots R) E \underset{˙}{\times} O (F) (y) = O (F) (E D y)) \to E \underset{˙}{\sim} F$
30	29	ex	$⊢ (φ \land (E \in ℕ \land F \in B)) \to (\forall y \in (K PrimRoots R) E \underset{˙}{\times} O (F) (y) = O (F) (E D y) \to E \underset{˙}{\sim} F)$
31	22 30	mpdan	$⊢ φ \to (\forall y \in (K PrimRoots R) E \underset{˙}{\times} O (F) (y) = O (F) (E D y) \to E \underset{˙}{\sim} F)$
32	21 31	impbid	$⊢ φ \to (E \underset{˙}{\sim} F \leftrightarrow \forall y \in (K PrimRoots R) E \underset{˙}{\times} O (F) (y) = O (F) (E D y))$

Metamath Proof Explorer

Theorem aks6d1c1p1

Proof