ltrneq2

Description: The equality of two translations is determined by their equality at atoms. (Contributed by NM, 2-Mar-2014)

	Ref	Expression
Hypotheses	ltrneq2.a	$⊢ A = Atoms (K)$
	ltrneq2.h	$⊢ H = LHyp (K)$
	ltrneq2.t	$⊢ T = LTrn (K) (W)$
Assertion	ltrneq2	$⊢ ((K \in HL \land W \in H) \land F \in T \land G \in T) \to (\forall p \in A F (p) = G (p) \leftrightarrow F = G)$

Proof

Step	Hyp	Ref	Expression
1		ltrneq2.a	$⊢ A = Atoms (K)$
2		ltrneq2.h	$⊢ H = LHyp (K)$
3		ltrneq2.t	$⊢ T = LTrn (K) (W)$
4		simpl1	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land (x \in {Base}_{K} \land \forall p \in A F (p) = G (p) \land q \in A)) \to (K \in HL \land W \in H)$
5		simpl3	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land (x \in {Base}_{K} \land \forall p \in A F (p) = G (p) \land q \in A)) \to G \in T$
6		eqid	$⊢ {Base}_{K} = {Base}_{K}$
7	6 2 3	ltrn1o	$⊢ ((K \in HL \land W \in H) \land G \in T) \to G : {Base}_{K} \underset{1-1 onto}{⟶} {Base}_{K}$
8	4 5 7	syl2anc	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land (x \in {Base}_{K} \land \forall p \in A F (p) = G (p) \land q \in A)) \to G : {Base}_{K} \underset{1-1 onto}{⟶} {Base}_{K}$
9		simpl2	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land (x \in {Base}_{K} \land \forall p \in A F (p) = G (p) \land q \in A)) \to F \in T$
10		simpr3	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land (x \in {Base}_{K} \land \forall p \in A F (p) = G (p) \land q \in A)) \to q \in A$
11		eqid	$⊢ \leq_{K} = \leq_{K}$
12	11 1 2 3	ltrncnvat	$⊢ ((K \in HL \land W \in H) \land F \in T \land q \in A) \to F^{-1} (q) \in A$
13	4 9 10 12	syl3anc	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land (x \in {Base}_{K} \land \forall p \in A F (p) = G (p) \land q \in A)) \to F^{-1} (q) \in A$
14	6 1	atbase	$⊢ F^{-1} (q) \in A \to F^{-1} (q) \in {Base}_{K}$
15	13 14	syl	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land (x \in {Base}_{K} \land \forall p \in A F (p) = G (p) \land q \in A)) \to F^{-1} (q) \in {Base}_{K}$
16		f1ocnvfv1	$⊢ (G : {Base}_{K} \underset{1-1 onto}{⟶} {Base}_{K} \land F^{-1} (q) \in {Base}_{K}) \to G^{-1} (G (F^{-1} (q))) = F^{-1} (q)$
17	8 15 16	syl2anc	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land (x \in {Base}_{K} \land \forall p \in A F (p) = G (p) \land q \in A)) \to G^{-1} (G (F^{-1} (q))) = F^{-1} (q)$
18		simpr2	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land (x \in {Base}_{K} \land \forall p \in A F (p) = G (p) \land q \in A)) \to \forall p \in A F (p) = G (p)$
19		fveq2	$⊢ p = F^{-1} (q) \to F (p) = F (F^{-1} (q))$
20		fveq2	$⊢ p = F^{-1} (q) \to G (p) = G (F^{-1} (q))$
21	19 20	eqeq12d	$⊢ p = F^{-1} (q) \to (F (p) = G (p) \leftrightarrow F (F^{-1} (q)) = G (F^{-1} (q)))$
22	21	rspcv	$⊢ F^{-1} (q) \in A \to (\forall p \in A F (p) = G (p) \to F (F^{-1} (q)) = G (F^{-1} (q)))$
23	13 18 22	sylc	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land (x \in {Base}_{K} \land \forall p \in A F (p) = G (p) \land q \in A)) \to F (F^{-1} (q)) = G (F^{-1} (q))$
24	6 2 3	ltrn1o	$⊢ ((K \in HL \land W \in H) \land F \in T) \to F : {Base}_{K} \underset{1-1 onto}{⟶} {Base}_{K}$
25	4 9 24	syl2anc	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land (x \in {Base}_{K} \land \forall p \in A F (p) = G (p) \land q \in A)) \to F : {Base}_{K} \underset{1-1 onto}{⟶} {Base}_{K}$
26	6 1	atbase	$⊢ q \in A \to q \in {Base}_{K}$
27	10 26	syl	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land (x \in {Base}_{K} \land \forall p \in A F (p) = G (p) \land q \in A)) \to q \in {Base}_{K}$
28		f1ocnvfv2	$⊢ (F : {Base}_{K} \underset{1-1 onto}{⟶} {Base}_{K} \land q \in {Base}_{K}) \to F (F^{-1} (q)) = q$
29	25 27 28	syl2anc	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land (x \in {Base}_{K} \land \forall p \in A F (p) = G (p) \land q \in A)) \to F (F^{-1} (q)) = q$
30	23 29	eqtr3d	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land (x \in {Base}_{K} \land \forall p \in A F (p) = G (p) \land q \in A)) \to G (F^{-1} (q)) = q$
31	30	fveq2d	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land (x \in {Base}_{K} \land \forall p \in A F (p) = G (p) \land q \in A)) \to G^{-1} (G (F^{-1} (q))) = G^{-1} (q)$
32	17 31	eqtr3d	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land (x \in {Base}_{K} \land \forall p \in A F (p) = G (p) \land q \in A)) \to F^{-1} (q) = G^{-1} (q)$
33	32	breq1d	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land (x \in {Base}_{K} \land \forall p \in A F (p) = G (p) \land q \in A)) \to (F^{-1} (q) \leq_{K} x \leftrightarrow G^{-1} (q) \leq_{K} x)$
34		simpr1	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land (x \in {Base}_{K} \land \forall p \in A F (p) = G (p) \land q \in A)) \to x \in {Base}_{K}$
35		f1ocnvfv1	$⊢ (F : {Base}_{K} \underset{1-1 onto}{⟶} {Base}_{K} \land x \in {Base}_{K}) \to F^{-1} (F (x)) = x$
36	25 34 35	syl2anc	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land (x \in {Base}_{K} \land \forall p \in A F (p) = G (p) \land q \in A)) \to F^{-1} (F (x)) = x$
37	36	breq2d	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land (x \in {Base}_{K} \land \forall p \in A F (p) = G (p) \land q \in A)) \to (F^{-1} (q) \leq_{K} F^{-1} (F (x)) \leftrightarrow F^{-1} (q) \leq_{K} x)$
38		f1ocnvfv1	$⊢ (G : {Base}_{K} \underset{1-1 onto}{⟶} {Base}_{K} \land x \in {Base}_{K}) \to G^{-1} (G (x)) = x$
39	8 34 38	syl2anc	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land (x \in {Base}_{K} \land \forall p \in A F (p) = G (p) \land q \in A)) \to G^{-1} (G (x)) = x$
40	39	breq2d	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land (x \in {Base}_{K} \land \forall p \in A F (p) = G (p) \land q \in A)) \to (G^{-1} (q) \leq_{K} G^{-1} (G (x)) \leftrightarrow G^{-1} (q) \leq_{K} x)$
41	33 37 40	3bitr4d	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land (x \in {Base}_{K} \land \forall p \in A F (p) = G (p) \land q \in A)) \to (F^{-1} (q) \leq_{K} F^{-1} (F (x)) \leftrightarrow G^{-1} (q) \leq_{K} G^{-1} (G (x)))$
42		simpl1l	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land (x \in {Base}_{K} \land \forall p \in A F (p) = G (p) \land q \in A)) \to K \in HL$
43		eqid	$⊢ LAut (K) = LAut (K)$
44	2 43 3	ltrnlaut	$⊢ ((K \in HL \land W \in H) \land F \in T) \to F \in LAut (K)$
45	4 9 44	syl2anc	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land (x \in {Base}_{K} \land \forall p \in A F (p) = G (p) \land q \in A)) \to F \in LAut (K)$
46	6 2 3	ltrncl	$⊢ ((K \in HL \land W \in H) \land F \in T \land x \in {Base}_{K}) \to F (x) \in {Base}_{K}$
47	4 9 34 46	syl3anc	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land (x \in {Base}_{K} \land \forall p \in A F (p) = G (p) \land q \in A)) \to F (x) \in {Base}_{K}$
48	6 11 43	lautcnvle	$⊢ ((K \in HL \land F \in LAut (K)) \land (q \in {Base}_{K} \land F (x) \in {Base}_{K})) \to (q \leq_{K} F (x) \leftrightarrow F^{-1} (q) \leq_{K} F^{-1} (F (x)))$
49	42 45 27 47 48	syl22anc	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land (x \in {Base}_{K} \land \forall p \in A F (p) = G (p) \land q \in A)) \to (q \leq_{K} F (x) \leftrightarrow F^{-1} (q) \leq_{K} F^{-1} (F (x)))$
50	2 43 3	ltrnlaut	$⊢ ((K \in HL \land W \in H) \land G \in T) \to G \in LAut (K)$
51	4 5 50	syl2anc	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land (x \in {Base}_{K} \land \forall p \in A F (p) = G (p) \land q \in A)) \to G \in LAut (K)$
52	6 2 3	ltrncl	$⊢ ((K \in HL \land W \in H) \land G \in T \land x \in {Base}_{K}) \to G (x) \in {Base}_{K}$
53	4 5 34 52	syl3anc	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land (x \in {Base}_{K} \land \forall p \in A F (p) = G (p) \land q \in A)) \to G (x) \in {Base}_{K}$
54	6 11 43	lautcnvle	$⊢ ((K \in HL \land G \in LAut (K)) \land (q \in {Base}_{K} \land G (x) \in {Base}_{K})) \to (q \leq_{K} G (x) \leftrightarrow G^{-1} (q) \leq_{K} G^{-1} (G (x)))$
55	42 51 27 53 54	syl22anc	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land (x \in {Base}_{K} \land \forall p \in A F (p) = G (p) \land q \in A)) \to (q \leq_{K} G (x) \leftrightarrow G^{-1} (q) \leq_{K} G^{-1} (G (x)))$
56	41 49 55	3bitr4d	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land (x \in {Base}_{K} \land \forall p \in A F (p) = G (p) \land q \in A)) \to (q \leq_{K} F (x) \leftrightarrow q \leq_{K} G (x))$
57	56	3exp2	$⊢ ((K \in HL \land W \in H) \land F \in T \land G \in T) \to (x \in {Base}_{K} \to (\forall p \in A F (p) = G (p) \to (q \in A \to (q \leq_{K} F (x) \leftrightarrow q \leq_{K} G (x)))))$
58	57	imp	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land x \in {Base}_{K}) \to (\forall p \in A F (p) = G (p) \to (q \in A \to (q \leq_{K} F (x) \leftrightarrow q \leq_{K} G (x))))$
59	58	ralrimdv	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land x \in {Base}_{K}) \to (\forall p \in A F (p) = G (p) \to \forall q \in A (q \leq_{K} F (x) \leftrightarrow q \leq_{K} G (x)))$
60		simpl1l	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land x \in {Base}_{K}) \to K \in HL$
61		simpl1	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land x \in {Base}_{K}) \to (K \in HL \land W \in H)$
62		simpl2	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land x \in {Base}_{K}) \to F \in T$
63		simpr	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land x \in {Base}_{K}) \to x \in {Base}_{K}$
64	61 62 63 46	syl3anc	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land x \in {Base}_{K}) \to F (x) \in {Base}_{K}$
65		simpl3	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land x \in {Base}_{K}) \to G \in T$
66	61 65 63 52	syl3anc	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land x \in {Base}_{K}) \to G (x) \in {Base}_{K}$
67	6 11 1	hlateq	$⊢ (K \in HL \land F (x) \in {Base}_{K} \land G (x) \in {Base}_{K}) \to (\forall q \in A (q \leq_{K} F (x) \leftrightarrow q \leq_{K} G (x)) \leftrightarrow F (x) = G (x))$
68	60 64 66 67	syl3anc	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land x \in {Base}_{K}) \to (\forall q \in A (q \leq_{K} F (x) \leftrightarrow q \leq_{K} G (x)) \leftrightarrow F (x) = G (x))$
69	59 68	sylibd	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land x \in {Base}_{K}) \to (\forall p \in A F (p) = G (p) \to F (x) = G (x))$
70	69	ralrimdva	$⊢ ((K \in HL \land W \in H) \land F \in T \land G \in T) \to (\forall p \in A F (p) = G (p) \to \forall x \in {Base}_{K} F (x) = G (x))$
71	24	3adant3	$⊢ ((K \in HL \land W \in H) \land F \in T \land G \in T) \to F : {Base}_{K} \underset{1-1 onto}{⟶} {Base}_{K}$
72		f1ofn	$⊢ F : {Base}_{K} \underset{1-1 onto}{⟶} {Base}_{K} \to F Fn {Base}_{K}$
73	71 72	syl	$⊢ ((K \in HL \land W \in H) \land F \in T \land G \in T) \to F Fn {Base}_{K}$
74	7	3adant2	$⊢ ((K \in HL \land W \in H) \land F \in T \land G \in T) \to G : {Base}_{K} \underset{1-1 onto}{⟶} {Base}_{K}$
75		f1ofn	$⊢ G : {Base}_{K} \underset{1-1 onto}{⟶} {Base}_{K} \to G Fn {Base}_{K}$
76	74 75	syl	$⊢ ((K \in HL \land W \in H) \land F \in T \land G \in T) \to G Fn {Base}_{K}$
77		eqfnfv	$⊢ (F Fn {Base}_{K} \land G Fn {Base}_{K}) \to (F = G \leftrightarrow \forall x \in {Base}_{K} F (x) = G (x))$
78	73 76 77	syl2anc	$⊢ ((K \in HL \land W \in H) \land F \in T \land G \in T) \to (F = G \leftrightarrow \forall x \in {Base}_{K} F (x) = G (x))$
79	70 78	sylibrd	$⊢ ((K \in HL \land W \in H) \land F \in T \land G \in T) \to (\forall p \in A F (p) = G (p) \to F = G)$
80		fveq1	$⊢ F = G \to F (p) = G (p)$
81	80	ralrimivw	$⊢ F = G \to \forall p \in A F (p) = G (p)$
82	79 81	impbid1	$⊢ ((K \in HL \land W \in H) \land F \in T \land G \in T) \to (\forall p \in A F (p) = G (p) \leftrightarrow F = G)$

Metamath Proof Explorer

Theorem ltrneq2

Proof