Metamath Proof Explorer

Theorem ltrniotacnvval

Description: Converse value of the unique translation specified by a value. (Contributed by NM, 21-Feb-2014)

		Ref	Expression
	Hypotheses	ltrniotaval.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
		ltrniotaval.a	$⊢ A = Atoms (K)$
		ltrniotaval.h	$⊢ H = LHyp (K)$
		ltrniotaval.t	$⊢ T = LTrn (K) (W)$
		ltrniotaval.f	$⊢ F = (ι f \in T \| f (P) = Q)$
	Assertion	ltrniotacnvval	$⊢ ((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to F^{-1} (Q) = P$

Proof

Step	Hyp	Ref	Expression
1		ltrniotaval.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		ltrniotaval.a	$⊢ A = Atoms (K)$
3		ltrniotaval.h	$⊢ H = LHyp (K)$
4		ltrniotaval.t	$⊢ T = LTrn (K) (W)$
5		ltrniotaval.f	$⊢ F = (ι f \in T \| f (P) = Q)$
6		simp1	$⊢ ((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to (K \in HL \land W \in H)$
7	1 2 3 4 5	ltrniotacl	$⊢ ((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to F \in T$
8		eqid	$⊢ {Base}_{K} = {Base}_{K}$
9	8 3 4	ltrn1o	$⊢ ((K \in HL \land W \in H) \land F \in T) \to F : {Base}_{K} \underset{1-1 onto}{⟶} {Base}_{K}$
10	6 7 9	syl2anc	$⊢ ((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to F : {Base}_{K} \underset{1-1 onto}{⟶} {Base}_{K}$
11		simp2l	$⊢ ((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to P \in A$
12	8 2	atbase	$⊢ P \in A \to P \in {Base}_{K}$
13	11 12	syl	$⊢ ((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to P \in {Base}_{K}$
14	10 13	jca	$⊢ ((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to (F : {Base}_{K} \underset{1-1 onto}{⟶} {Base}_{K} \land P \in {Base}_{K})$
15	1 2 3 4 5	ltrniotaval	$⊢ ((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to F (P) = Q$
16		f1ocnvfv	$⊢ (F : {Base}_{K} \underset{1-1 onto}{⟶} {Base}_{K} \land P \in {Base}_{K}) \to (F (P) = Q \to F^{-1} (Q) = P)$
17	14 15 16	sylc	$⊢ ((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to F^{-1} (Q) = P$