dihopelvalcpre

Description: Member of value of isomorphism H for a lattice K when -. X .<_ W , given auxiliary atom Q . TODO: refactor to be shorter and more understandable; add lemmas? (Contributed by NM, 13-Mar-2014)

	Ref	Expression
Hypotheses	dihopelvalcp.b	$⊢ B = {Base}_{K}$
	dihopelvalcp.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	dihopelvalcp.j	$⊢ \underset{˙}{\lor} = join (K)$
	dihopelvalcp.m	$⊢ \underset{˙}{\land} = meet (K)$
	dihopelvalcp.a	$⊢ A = Atoms (K)$
	dihopelvalcp.h	$⊢ H = LHyp (K)$
	dihopelvalcp.p	$⊢ P = oc (K) (W)$
	dihopelvalcp.t	$⊢ T = LTrn (K) (W)$
	dihopelvalcp.r	$⊢ R = trL (K) (W)$
	dihopelvalcp.e	$⊢ E = TEndo (K) (W)$
	dihopelvalcp.i	$⊢ I = DIsoH (K) (W)$
	dihopelvalcp.g	$⊢ G = (ι g \in T \| g (P) = Q)$
	dihopelvalcp.f	$⊢ F \in V$
	dihopelvalcp.s	$⊢ S \in V$
	dihopelvalcp.z	$⊢ Z = (h \in T ⟼ {I ↾}_{B})$
	dihopelvalcp.n	$⊢ N = DIsoB (K) (W)$
	dihopelvalcp.c	$⊢ C = DIsoC (K) (W)$
	dihopelvalcp.u	$⊢ U = DVecH (K) (W)$
	dihopelvalcp.d	$⊢ \underset{˙}{+} = +_{U}$
	dihopelvalcp.v	$⊢ V = LSubSp (U)$
	dihopelvalcp.y	$⊢ \underset{˙}{\oplus} = LSSum (U)$
	dihopelvalcp.o	$⊢ O = (a \in E, b \in E ⟼ (h \in T ⟼ a (h) \circ b (h)))$
Assertion	dihopelvalcpre	$⊢ ((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \to (⟨F, S⟩ \in I (X) \leftrightarrow ((F \in T \land S \in E) \land R (F \circ {S (G)}^{-1}) \underset{˙}{\leq} X))$

Proof

Step	Hyp	Ref	Expression
1		dihopelvalcp.b	$⊢ B = {Base}_{K}$
2		dihopelvalcp.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		dihopelvalcp.j	$⊢ \underset{˙}{\lor} = join (K)$
4		dihopelvalcp.m	$⊢ \underset{˙}{\land} = meet (K)$
5		dihopelvalcp.a	$⊢ A = Atoms (K)$
6		dihopelvalcp.h	$⊢ H = LHyp (K)$
7		dihopelvalcp.p	$⊢ P = oc (K) (W)$
8		dihopelvalcp.t	$⊢ T = LTrn (K) (W)$
9		dihopelvalcp.r	$⊢ R = trL (K) (W)$
10		dihopelvalcp.e	$⊢ E = TEndo (K) (W)$
11		dihopelvalcp.i	$⊢ I = DIsoH (K) (W)$
12		dihopelvalcp.g	$⊢ G = (ι g \in T \| g (P) = Q)$
13		dihopelvalcp.f	$⊢ F \in V$
14		dihopelvalcp.s	$⊢ S \in V$
15		dihopelvalcp.z	$⊢ Z = (h \in T ⟼ {I ↾}_{B})$
16		dihopelvalcp.n	$⊢ N = DIsoB (K) (W)$
17		dihopelvalcp.c	$⊢ C = DIsoC (K) (W)$
18		dihopelvalcp.u	$⊢ U = DVecH (K) (W)$
19		dihopelvalcp.d	$⊢ \underset{˙}{+} = +_{U}$
20		dihopelvalcp.v	$⊢ V = LSubSp (U)$
21		dihopelvalcp.y	$⊢ \underset{˙}{\oplus} = LSSum (U)$
22		dihopelvalcp.o	$⊢ O = (a \in E, b \in E ⟼ (h \in T ⟼ a (h) \circ b (h)))$
23	1 2 3 4 5 6 11 16 17 18 21	dihvalcq	$⊢ ((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \to I (X) = C (Q) \underset{˙}{\oplus} N (X \underset{˙}{\land} W)$
24	23	eleq2d	$⊢ ((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \to (⟨F, S⟩ \in I (X) \leftrightarrow ⟨F, S⟩ \in (C (Q) \underset{˙}{\oplus} N (X \underset{˙}{\land} W)))$
25		simp1	$⊢ ((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \to (K \in HL \land W \in H)$
26		simp3l	$⊢ ((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \to (Q \in A \land \neg Q \underset{˙}{\leq} W)$
27	2 5 6 18 17 20	diclss	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to C (Q) \in V$
28	25 26 27	syl2anc	$⊢ ((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \to C (Q) \in V$
29		simp1l	$⊢ ((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \to K \in HL$
30	29	hllatd	$⊢ ((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \to K \in Lat$
31		simp2l	$⊢ ((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \to X \in B$
32		simp1r	$⊢ ((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \to W \in H$
33	1 6	lhpbase	$⊢ W \in H \to W \in B$
34	32 33	syl	$⊢ ((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \to W \in B$
35	1 4	latmcl	$⊢ (K \in Lat \land X \in B \land W \in B) \to X \underset{˙}{\land} W \in B$
36	30 31 34 35	syl3anc	$⊢ ((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \to X \underset{˙}{\land} W \in B$
37	1 2 4	latmle2	$⊢ (K \in Lat \land X \in B \land W \in B) \to (X \underset{˙}{\land} W) \underset{˙}{\leq} W$
38	30 31 34 37	syl3anc	$⊢ ((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \to (X \underset{˙}{\land} W) \underset{˙}{\leq} W$
39	1 2 6 18 16 20	diblss	$⊢ ((K \in HL \land W \in H) \land (X \underset{˙}{\land} W \in B \land (X \underset{˙}{\land} W) \underset{˙}{\leq} W)) \to N (X \underset{˙}{\land} W) \in V$
40	25 36 38 39	syl12anc	$⊢ ((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \to N (X \underset{˙}{\land} W) \in V$
41	6 18 19 20 21	dvhopellsm	$⊢ ((K \in HL \land W \in H) \land C (Q) \in V \land N (X \underset{˙}{\land} W) \in V) \to (⟨F, S⟩ \in (C (Q) \underset{˙}{\oplus} N (X \underset{˙}{\land} W)) \leftrightarrow \exists x \exists y \exists z \exists w ((⟨x, y⟩ \in C (Q) \land ⟨z, w⟩ \in N (X \underset{˙}{\land} W)) \land ⟨F, S⟩ = ⟨x, y⟩ \underset{˙}{+} ⟨z, w⟩))$
42	25 28 40 41	syl3anc	$⊢ ((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \to (⟨F, S⟩ \in (C (Q) \underset{˙}{\oplus} N (X \underset{˙}{\land} W)) \leftrightarrow \exists x \exists y \exists z \exists w ((⟨x, y⟩ \in C (Q) \land ⟨z, w⟩ \in N (X \underset{˙}{\land} W)) \land ⟨F, S⟩ = ⟨x, y⟩ \underset{˙}{+} ⟨z, w⟩))$
43		vex	$⊢ x \in V$
44		vex	$⊢ y \in V$
45	2 5 6 7 8 10 17 12 43 44	dicopelval2	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to (⟨x, y⟩ \in C (Q) \leftrightarrow (x = y (G) \land y \in E))$
46	25 26 45	syl2anc	$⊢ ((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \to (⟨x, y⟩ \in C (Q) \leftrightarrow (x = y (G) \land y \in E))$
47	1 2 6 8 9 15 16	dibopelval3	$⊢ ((K \in HL \land W \in H) \land (X \underset{˙}{\land} W \in B \land (X \underset{˙}{\land} W) \underset{˙}{\leq} W)) \to (⟨z, w⟩ \in N (X \underset{˙}{\land} W) \leftrightarrow ((z \in T \land R (z) \underset{˙}{\leq} (X \underset{˙}{\land} W)) \land w = Z))$
48	25 36 38 47	syl12anc	$⊢ ((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \to (⟨z, w⟩ \in N (X \underset{˙}{\land} W) \leftrightarrow ((z \in T \land R (z) \underset{˙}{\leq} (X \underset{˙}{\land} W)) \land w = Z))$
49	46 48	anbi12d	$⊢ ((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \to ((⟨x, y⟩ \in C (Q) \land ⟨z, w⟩ \in N (X \underset{˙}{\land} W)) \leftrightarrow ((x = y (G) \land y \in E) \land ((z \in T \land R (z) \underset{˙}{\leq} (X \underset{˙}{\land} W)) \land w = Z)))$
50	49	anbi1d	$⊢ ((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \to (((⟨x, y⟩ \in C (Q) \land ⟨z, w⟩ \in N (X \underset{˙}{\land} W)) \land ⟨F, S⟩ = ⟨x, y⟩ \underset{˙}{+} ⟨z, w⟩) \leftrightarrow (((x = y (G) \land y \in E) \land ((z \in T \land R (z) \underset{˙}{\leq} (X \underset{˙}{\land} W)) \land w = Z)) \land ⟨F, S⟩ = ⟨x, y⟩ \underset{˙}{+} ⟨z, w⟩))$
51		simpl1	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land ((x = y (G) \land y \in E) \land ((z \in T \land R (z) \underset{˙}{\leq} (X \underset{˙}{\land} W)) \land w = Z))) \to (K \in HL \land W \in H)$
52		simprll	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land ((x = y (G) \land y \in E) \land ((z \in T \land R (z) \underset{˙}{\leq} (X \underset{˙}{\land} W)) \land w = Z))) \to x = y (G)$
53		simprlr	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land ((x = y (G) \land y \in E) \land ((z \in T \land R (z) \underset{˙}{\leq} (X \underset{˙}{\land} W)) \land w = Z))) \to y \in E$
54	2 5 6 7	lhpocnel2	$⊢ (K \in HL \land W \in H) \to (P \in A \land \neg P \underset{˙}{\leq} W)$
55	51 54	syl	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land ((x = y (G) \land y \in E) \land ((z \in T \land R (z) \underset{˙}{\leq} (X \underset{˙}{\land} W)) \land w = Z))) \to (P \in A \land \neg P \underset{˙}{\leq} W)$
56		simpl3l	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land ((x = y (G) \land y \in E) \land ((z \in T \land R (z) \underset{˙}{\leq} (X \underset{˙}{\land} W)) \land w = Z))) \to (Q \in A \land \neg Q \underset{˙}{\leq} W)$
57	2 5 6 8 12	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 G \in T$
58	51 55 56 57	syl3anc	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land ((x = y (G) \land y \in E) \land ((z \in T \land R (z) \underset{˙}{\leq} (X \underset{˙}{\land} W)) \land w = Z))) \to G \in T$
59	6 8 10	tendocl	$⊢ ((K \in HL \land W \in H) \land y \in E \land G \in T) \to y (G) \in T$
60	51 53 58 59	syl3anc	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land ((x = y (G) \land y \in E) \land ((z \in T \land R (z) \underset{˙}{\leq} (X \underset{˙}{\land} W)) \land w = Z))) \to y (G) \in T$
61	52 60	eqeltrd	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land ((x = y (G) \land y \in E) \land ((z \in T \land R (z) \underset{˙}{\leq} (X \underset{˙}{\land} W)) \land w = Z))) \to x \in T$
62		simprll	$⊢ ((x = y (G) \land y \in E) \land ((z \in T \land R (z) \underset{˙}{\leq} (X \underset{˙}{\land} W)) \land w = Z)) \to z \in T$
63	62	adantl	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land ((x = y (G) \land y \in E) \land ((z \in T \land R (z) \underset{˙}{\leq} (X \underset{˙}{\land} W)) \land w = Z))) \to z \in T$
64		simprrr	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land ((x = y (G) \land y \in E) \land ((z \in T \land R (z) \underset{˙}{\leq} (X \underset{˙}{\land} W)) \land w = Z))) \to w = Z$
65	1 6 8 10 15	tendo0cl	$⊢ (K \in HL \land W \in H) \to Z \in E$
66	51 65	syl	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land ((x = y (G) \land y \in E) \land ((z \in T \land R (z) \underset{˙}{\leq} (X \underset{˙}{\land} W)) \land w = Z))) \to Z \in E$
67	64 66	eqeltrd	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land ((x = y (G) \land y \in E) \land ((z \in T \land R (z) \underset{˙}{\leq} (X \underset{˙}{\land} W)) \land w = Z))) \to w \in E$
68		eqid	$⊢ Scalar (U) = Scalar (U)$
69		eqid	$⊢ +_{Scalar (U)} = +_{Scalar (U)}$
70	6 8 10 18 68 19 69	dvhopvadd	$⊢ ((K \in HL \land W \in H) \land (x \in T \land y \in E) \land (z \in T \land w \in E)) \to ⟨x, y⟩ \underset{˙}{+} ⟨z, w⟩ = ⟨x \circ z, y +_{Scalar (U)} w⟩$
71	51 61 53 63 67 70	syl122anc	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land ((x = y (G) \land y \in E) \land ((z \in T \land R (z) \underset{˙}{\leq} (X \underset{˙}{\land} W)) \land w = Z))) \to ⟨x, y⟩ \underset{˙}{+} ⟨z, w⟩ = ⟨x \circ z, y +_{Scalar (U)} w⟩$
72	6 8 10 18 68 22 69	dvhfplusr	$⊢ (K \in HL \land W \in H) \to +_{Scalar (U)} = O$
73	51 72	syl	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land ((x = y (G) \land y \in E) \land ((z \in T \land R (z) \underset{˙}{\leq} (X \underset{˙}{\land} W)) \land w = Z))) \to +_{Scalar (U)} = O$
74	73	oveqd	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land ((x = y (G) \land y \in E) \land ((z \in T \land R (z) \underset{˙}{\leq} (X \underset{˙}{\land} W)) \land w = Z))) \to y +_{Scalar (U)} w = y O w$
75	74	opeq2d	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land ((x = y (G) \land y \in E) \land ((z \in T \land R (z) \underset{˙}{\leq} (X \underset{˙}{\land} W)) \land w = Z))) \to ⟨x \circ z, y +_{Scalar (U)} w⟩ = ⟨x \circ z, y O w⟩$
76	71 75	eqtrd	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land ((x = y (G) \land y \in E) \land ((z \in T \land R (z) \underset{˙}{\leq} (X \underset{˙}{\land} W)) \land w = Z))) \to ⟨x, y⟩ \underset{˙}{+} ⟨z, w⟩ = ⟨x \circ z, y O w⟩$
77	76	eqeq2d	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land ((x = y (G) \land y \in E) \land ((z \in T \land R (z) \underset{˙}{\leq} (X \underset{˙}{\land} W)) \land w = Z))) \to (⟨F, S⟩ = ⟨x, y⟩ \underset{˙}{+} ⟨z, w⟩ \leftrightarrow ⟨F, S⟩ = ⟨x \circ z, y O w⟩)$
78	13 14	opth	$⊢ ⟨F, S⟩ = ⟨x \circ z, y O w⟩ \leftrightarrow (F = x \circ z \land S = y O w)$
79	64	oveq2d	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land ((x = y (G) \land y \in E) \land ((z \in T \land R (z) \underset{˙}{\leq} (X \underset{˙}{\land} W)) \land w = Z))) \to y O w = y O Z$
80	1 6 8 10 15 22	tendo0plr	$⊢ ((K \in HL \land W \in H) \land y \in E) \to y O Z = y$
81	51 53 80	syl2anc	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land ((x = y (G) \land y \in E) \land ((z \in T \land R (z) \underset{˙}{\leq} (X \underset{˙}{\land} W)) \land w = Z))) \to y O Z = y$
82	79 81	eqtrd	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land ((x = y (G) \land y \in E) \land ((z \in T \land R (z) \underset{˙}{\leq} (X \underset{˙}{\land} W)) \land w = Z))) \to y O w = y$
83	82	eqeq2d	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land ((x = y (G) \land y \in E) \land ((z \in T \land R (z) \underset{˙}{\leq} (X \underset{˙}{\land} W)) \land w = Z))) \to (S = y O w \leftrightarrow S = y)$
84	83	anbi2d	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land ((x = y (G) \land y \in E) \land ((z \in T \land R (z) \underset{˙}{\leq} (X \underset{˙}{\land} W)) \land w = Z))) \to ((F = x \circ z \land S = y O w) \leftrightarrow (F = x \circ z \land S = y))$
85	78 84	syl5bb	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land ((x = y (G) \land y \in E) \land ((z \in T \land R (z) \underset{˙}{\leq} (X \underset{˙}{\land} W)) \land w = Z))) \to (⟨F, S⟩ = ⟨x \circ z, y O w⟩ \leftrightarrow (F = x \circ z \land S = y))$
86	77 85	bitrd	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land ((x = y (G) \land y \in E) \land ((z \in T \land R (z) \underset{˙}{\leq} (X \underset{˙}{\land} W)) \land w = Z))) \to (⟨F, S⟩ = ⟨x, y⟩ \underset{˙}{+} ⟨z, w⟩ \leftrightarrow (F = x \circ z \land S = y))$
87	86	pm5.32da	$⊢ ((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \to ((((x = y (G) \land y \in E) \land ((z \in T \land R (z) \underset{˙}{\leq} (X \underset{˙}{\land} W)) \land w = Z)) \land ⟨F, S⟩ = ⟨x, y⟩ \underset{˙}{+} ⟨z, w⟩) \leftrightarrow (((x = y (G) \land y \in E) \land ((z \in T \land R (z) \underset{˙}{\leq} (X \underset{˙}{\land} W)) \land w = Z)) \land (F = x \circ z \land S = y)))$
88		simplll	$⊢ (((x = y (G) \land y \in E) \land ((z \in T \land R (z) \underset{˙}{\leq} (X \underset{˙}{\land} W)) \land w = Z)) \land (F = x \circ z \land S = y)) \to x = y (G)$
89	88	adantl	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land (((x = y (G) \land y \in E) \land ((z \in T \land R (z) \underset{˙}{\leq} (X \underset{˙}{\land} W)) \land w = Z)) \land (F = x \circ z \land S = y))) \to x = y (G)$
90		simprrr	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land (((x = y (G) \land y \in E) \land ((z \in T \land R (z) \underset{˙}{\leq} (X \underset{˙}{\land} W)) \land w = Z)) \land (F = x \circ z \land S = y))) \to S = y$
91	90	fveq1d	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land (((x = y (G) \land y \in E) \land ((z \in T \land R (z) \underset{˙}{\leq} (X \underset{˙}{\land} W)) \land w = Z)) \land (F = x \circ z \land S = y))) \to S (G) = y (G)$
92	89 91	eqtr4d	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land (((x = y (G) \land y \in E) \land ((z \in T \land R (z) \underset{˙}{\leq} (X \underset{˙}{\land} W)) \land w = Z)) \land (F = x \circ z \land S = y))) \to x = S (G)$
93	90	eqcomd	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land (((x = y (G) \land y \in E) \land ((z \in T \land R (z) \underset{˙}{\leq} (X \underset{˙}{\land} W)) \land w = Z)) \land (F = x \circ z \land S = y))) \to y = S$
94		coass	$⊢ ({S (G)}^{-1} \circ S (G)) \circ z = {S (G)}^{-1} \circ (S (G) \circ z)$
95		simpl1	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land (((x = y (G) \land y \in E) \land ((z \in T \land R (z) \underset{˙}{\leq} (X \underset{˙}{\land} W)) \land w = Z)) \land (F = x \circ z \land S = y))) \to (K \in HL \land W \in H)$
96		simpllr	$⊢ (((x = y (G) \land y \in E) \land ((z \in T \land R (z) \underset{˙}{\leq} (X \underset{˙}{\land} W)) \land w = Z)) \land (F = x \circ z \land S = y)) \to y \in E$
97	96	adantl	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land (((x = y (G) \land y \in E) \land ((z \in T \land R (z) \underset{˙}{\leq} (X \underset{˙}{\land} W)) \land w = Z)) \land (F = x \circ z \land S = y))) \to y \in E$
98	90 97	eqeltrd	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land (((x = y (G) \land y \in E) \land ((z \in T \land R (z) \underset{˙}{\leq} (X \underset{˙}{\land} W)) \land w = Z)) \land (F = x \circ z \land S = y))) \to S \in E$
99	58	adantrr	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land (((x = y (G) \land y \in E) \land ((z \in T \land R (z) \underset{˙}{\leq} (X \underset{˙}{\land} W)) \land w = Z)) \land (F = x \circ z \land S = y))) \to G \in T$
100	6 8 10	tendocl	$⊢ ((K \in HL \land W \in H) \land S \in E \land G \in T) \to S (G) \in T$
101	95 98 99 100	syl3anc	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land (((x = y (G) \land y \in E) \land ((z \in T \land R (z) \underset{˙}{\leq} (X \underset{˙}{\land} W)) \land w = Z)) \land (F = x \circ z \land S = y))) \to S (G) \in T$
102	1 6 8	ltrn1o	$⊢ ((K \in HL \land W \in H) \land S (G) \in T) \to S (G) : B \underset{1-1 onto}{⟶} B$
103	95 101 102	syl2anc	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land (((x = y (G) \land y \in E) \land ((z \in T \land R (z) \underset{˙}{\leq} (X \underset{˙}{\land} W)) \land w = Z)) \land (F = x \circ z \land S = y))) \to S (G) : B \underset{1-1 onto}{⟶} B$
104		f1ococnv1	$⊢ S (G) : B \underset{1-1 onto}{⟶} B \to {S (G)}^{-1} \circ S (G) = {I ↾}_{B}$
105	103 104	syl	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land (((x = y (G) \land y \in E) \land ((z \in T \land R (z) \underset{˙}{\leq} (X \underset{˙}{\land} W)) \land w = Z)) \land (F = x \circ z \land S = y))) \to {S (G)}^{-1} \circ S (G) = {I ↾}_{B}$
106	105	coeq1d	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land (((x = y (G) \land y \in E) \land ((z \in T \land R (z) \underset{˙}{\leq} (X \underset{˙}{\land} W)) \land w = Z)) \land (F = x \circ z \land S = y))) \to ({S (G)}^{-1} \circ S (G)) \circ z = ({I ↾}_{B}) \circ z$
107	62	ad2antrl	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land (((x = y (G) \land y \in E) \land ((z \in T \land R (z) \underset{˙}{\leq} (X \underset{˙}{\land} W)) \land w = Z)) \land (F = x \circ z \land S = y))) \to z \in T$
108	1 6 8	ltrn1o	$⊢ ((K \in HL \land W \in H) \land z \in T) \to z : B \underset{1-1 onto}{⟶} B$
109	95 107 108	syl2anc	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land (((x = y (G) \land y \in E) \land ((z \in T \land R (z) \underset{˙}{\leq} (X \underset{˙}{\land} W)) \land w = Z)) \land (F = x \circ z \land S = y))) \to z : B \underset{1-1 onto}{⟶} B$
110		f1of	$⊢ z : B \underset{1-1 onto}{⟶} B \to z : B ⟶ B$
111		fcoi2	$⊢ z : B ⟶ B \to ({I ↾}_{B}) \circ z = z$
112	109 110 111	3syl	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land (((x = y (G) \land y \in E) \land ((z \in T \land R (z) \underset{˙}{\leq} (X \underset{˙}{\land} W)) \land w = Z)) \land (F = x \circ z \land S = y))) \to ({I ↾}_{B}) \circ z = z$
113	106 112	eqtr2d	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land (((x = y (G) \land y \in E) \land ((z \in T \land R (z) \underset{˙}{\leq} (X \underset{˙}{\land} W)) \land w = Z)) \land (F = x \circ z \land S = y))) \to z = ({S (G)}^{-1} \circ S (G)) \circ z$
114		simprrl	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land (((x = y (G) \land y \in E) \land ((z \in T \land R (z) \underset{˙}{\leq} (X \underset{˙}{\land} W)) \land w = Z)) \land (F = x \circ z \land S = y))) \to F = x \circ z$
115	92	coeq1d	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land (((x = y (G) \land y \in E) \land ((z \in T \land R (z) \underset{˙}{\leq} (X \underset{˙}{\land} W)) \land w = Z)) \land (F = x \circ z \land S = y))) \to x \circ z = S (G) \circ z$
116	114 115	eqtrd	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land (((x = y (G) \land y \in E) \land ((z \in T \land R (z) \underset{˙}{\leq} (X \underset{˙}{\land} W)) \land w = Z)) \land (F = x \circ z \land S = y))) \to F = S (G) \circ z$
117	116	coeq1d	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land (((x = y (G) \land y \in E) \land ((z \in T \land R (z) \underset{˙}{\leq} (X \underset{˙}{\land} W)) \land w = Z)) \land (F = x \circ z \land S = y))) \to F \circ {S (G)}^{-1} = (S (G) \circ z) \circ {S (G)}^{-1}$
118	6 8	ltrncnv	$⊢ ((K \in HL \land W \in H) \land S (G) \in T) \to {S (G)}^{-1} \in T$
119	95 101 118	syl2anc	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land (((x = y (G) \land y \in E) \land ((z \in T \land R (z) \underset{˙}{\leq} (X \underset{˙}{\land} W)) \land w = Z)) \land (F = x \circ z \land S = y))) \to {S (G)}^{-1} \in T$
120	6 8	ltrnco	$⊢ ((K \in HL \land W \in H) \land S (G) \in T \land z \in T) \to S (G) \circ z \in T$
121	95 101 107 120	syl3anc	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land (((x = y (G) \land y \in E) \land ((z \in T \land R (z) \underset{˙}{\leq} (X \underset{˙}{\land} W)) \land w = Z)) \land (F = x \circ z \land S = y))) \to S (G) \circ z \in T$
122	6 8	ltrncom	$⊢ ((K \in HL \land W \in H) \land {S (G)}^{-1} \in T \land S (G) \circ z \in T) \to {S (G)}^{-1} \circ (S (G) \circ z) = (S (G) \circ z) \circ {S (G)}^{-1}$
123	95 119 121 122	syl3anc	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land (((x = y (G) \land y \in E) \land ((z \in T \land R (z) \underset{˙}{\leq} (X \underset{˙}{\land} W)) \land w = Z)) \land (F = x \circ z \land S = y))) \to {S (G)}^{-1} \circ (S (G) \circ z) = (S (G) \circ z) \circ {S (G)}^{-1}$
124	117 123	eqtr4d	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land (((x = y (G) \land y \in E) \land ((z \in T \land R (z) \underset{˙}{\leq} (X \underset{˙}{\land} W)) \land w = Z)) \land (F = x \circ z \land S = y))) \to F \circ {S (G)}^{-1} = {S (G)}^{-1} \circ (S (G) \circ z)$
125	94 113 124	3eqtr4a	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land (((x = y (G) \land y \in E) \land ((z \in T \land R (z) \underset{˙}{\leq} (X \underset{˙}{\land} W)) \land w = Z)) \land (F = x \circ z \land S = y))) \to z = F \circ {S (G)}^{-1}$
126		simplrr	$⊢ (((x = y (G) \land y \in E) \land ((z \in T \land R (z) \underset{˙}{\leq} (X \underset{˙}{\land} W)) \land w = Z)) \land (F = x \circ z \land S = y)) \to w = Z$
127	126	adantl	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land (((x = y (G) \land y \in E) \land ((z \in T \land R (z) \underset{˙}{\leq} (X \underset{˙}{\land} W)) \land w = Z)) \land (F = x \circ z \land S = y))) \to w = Z$
128	125 127	jca	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land (((x = y (G) \land y \in E) \land ((z \in T \land R (z) \underset{˙}{\leq} (X \underset{˙}{\land} W)) \land w = Z)) \land (F = x \circ z \land S = y))) \to (z = F \circ {S (G)}^{-1} \land w = Z)$
129	92 93 128	jca31	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land (((x = y (G) \land y \in E) \land ((z \in T \land R (z) \underset{˙}{\leq} (X \underset{˙}{\land} W)) \land w = Z)) \land (F = x \circ z \land S = y))) \to ((x = S (G) \land y = S) \land (z = F \circ {S (G)}^{-1} \land w = Z))$
130	129	ex	$⊢ ((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \to ((((x = y (G) \land y \in E) \land ((z \in T \land R (z) \underset{˙}{\leq} (X \underset{˙}{\land} W)) \land w = Z)) \land (F = x \circ z \land S = y)) \to ((x = S (G) \land y = S) \land (z = F \circ {S (G)}^{-1} \land w = Z)))$
131	130	pm4.71rd	$⊢ ((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \to ((((x = y (G) \land y \in E) \land ((z \in T \land R (z) \underset{˙}{\leq} (X \underset{˙}{\land} W)) \land w = Z)) \land (F = x \circ z \land S = y)) \leftrightarrow (((x = S (G) \land y = S) \land (z = F \circ {S (G)}^{-1} \land w = Z)) \land (((x = y (G) \land y \in E) \land ((z \in T \land R (z) \underset{˙}{\leq} (X \underset{˙}{\land} W)) \land w = Z)) \land (F = x \circ z \land S = y))))$
132	87 131	bitrd	$⊢ ((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \to ((((x = y (G) \land y \in E) \land ((z \in T \land R (z) \underset{˙}{\leq} (X \underset{˙}{\land} W)) \land w = Z)) \land ⟨F, S⟩ = ⟨x, y⟩ \underset{˙}{+} ⟨z, w⟩) \leftrightarrow (((x = S (G) \land y = S) \land (z = F \circ {S (G)}^{-1} \land w = Z)) \land (((x = y (G) \land y \in E) \land ((z \in T \land R (z) \underset{˙}{\leq} (X \underset{˙}{\land} W)) \land w = Z)) \land (F = x \circ z \land S = y))))$
133		simprrl	$⊢ ((((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land ((x = S (G) \land y = S) \land (z = F \circ {S (G)}^{-1} \land w = Z))) \land (((x = y (G) \land y \in E) \land ((z \in T \land R (z) \underset{˙}{\leq} (X \underset{˙}{\land} W)) \land w = Z)) \land (F = x \circ z \land S = y))) \to F = x \circ z$
134		simpll1	$⊢ ((((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land ((x = S (G) \land y = S) \land (z = F \circ {S (G)}^{-1} \land w = Z))) \land (((x = y (G) \land y \in E) \land ((z \in T \land R (z) \underset{˙}{\leq} (X \underset{˙}{\land} W)) \land w = Z)) \land (F = x \circ z \land S = y))) \to (K \in HL \land W \in H)$
135	88	adantl	$⊢ ((((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land ((x = S (G) \land y = S) \land (z = F \circ {S (G)}^{-1} \land w = Z))) \land (((x = y (G) \land y \in E) \land ((z \in T \land R (z) \underset{˙}{\leq} (X \underset{˙}{\land} W)) \land w = Z)) \land (F = x \circ z \land S = y))) \to x = y (G)$
136	96	adantl	$⊢ ((((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land ((x = S (G) \land y = S) \land (z = F \circ {S (G)}^{-1} \land w = Z))) \land (((x = y (G) \land y \in E) \land ((z \in T \land R (z) \underset{˙}{\leq} (X \underset{˙}{\land} W)) \land w = Z)) \land (F = x \circ z \land S = y))) \to y \in E$
137	134 54	syl	$⊢ ((((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land ((x = S (G) \land y = S) \land (z = F \circ {S (G)}^{-1} \land w = Z))) \land (((x = y (G) \land y \in E) \land ((z \in T \land R (z) \underset{˙}{\leq} (X \underset{˙}{\land} W)) \land w = Z)) \land (F = x \circ z \land S = y))) \to (P \in A \land \neg P \underset{˙}{\leq} W)$
138		simpl3l	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land ((x = S (G) \land y = S) \land (z = F \circ {S (G)}^{-1} \land w = Z))) \to (Q \in A \land \neg Q \underset{˙}{\leq} W)$
139	138	adantr	$⊢ ((((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land ((x = S (G) \land y = S) \land (z = F \circ {S (G)}^{-1} \land w = Z))) \land (((x = y (G) \land y \in E) \land ((z \in T \land R (z) \underset{˙}{\leq} (X \underset{˙}{\land} W)) \land w = Z)) \land (F = x \circ z \land S = y))) \to (Q \in A \land \neg Q \underset{˙}{\leq} W)$
140	134 137 139 57	syl3anc	$⊢ ((((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land ((x = S (G) \land y = S) \land (z = F \circ {S (G)}^{-1} \land w = Z))) \land (((x = y (G) \land y \in E) \land ((z \in T \land R (z) \underset{˙}{\leq} (X \underset{˙}{\land} W)) \land w = Z)) \land (F = x \circ z \land S = y))) \to G \in T$
141	134 136 140 59	syl3anc	$⊢ ((((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land ((x = S (G) \land y = S) \land (z = F \circ {S (G)}^{-1} \land w = Z))) \land (((x = y (G) \land y \in E) \land ((z \in T \land R (z) \underset{˙}{\leq} (X \underset{˙}{\land} W)) \land w = Z)) \land (F = x \circ z \land S = y))) \to y (G) \in T$
142	135 141	eqeltrd	$⊢ ((((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land ((x = S (G) \land y = S) \land (z = F \circ {S (G)}^{-1} \land w = Z))) \land (((x = y (G) \land y \in E) \land ((z \in T \land R (z) \underset{˙}{\leq} (X \underset{˙}{\land} W)) \land w = Z)) \land (F = x \circ z \land S = y))) \to x \in T$
143	62	ad2antrl	$⊢ ((((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land ((x = S (G) \land y = S) \land (z = F \circ {S (G)}^{-1} \land w = Z))) \land (((x = y (G) \land y \in E) \land ((z \in T \land R (z) \underset{˙}{\leq} (X \underset{˙}{\land} W)) \land w = Z)) \land (F = x \circ z \land S = y))) \to z \in T$
144	6 8	ltrnco	$⊢ ((K \in HL \land W \in H) \land x \in T \land z \in T) \to x \circ z \in T$
145	134 142 143 144	syl3anc	$⊢ ((((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land ((x = S (G) \land y = S) \land (z = F \circ {S (G)}^{-1} \land w = Z))) \land (((x = y (G) \land y \in E) \land ((z \in T \land R (z) \underset{˙}{\leq} (X \underset{˙}{\land} W)) \land w = Z)) \land (F = x \circ z \land S = y))) \to x \circ z \in T$
146	133 145	eqeltrd	$⊢ ((((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land ((x = S (G) \land y = S) \land (z = F \circ {S (G)}^{-1} \land w = Z))) \land (((x = y (G) \land y \in E) \land ((z \in T \land R (z) \underset{˙}{\leq} (X \underset{˙}{\land} W)) \land w = Z)) \land (F = x \circ z \land S = y))) \to F \in T$
147		simpl1l	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land ((x = S (G) \land y = S) \land (z = F \circ {S (G)}^{-1} \land w = Z))) \to K \in HL$
148	147	adantr	$⊢ ((((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land ((x = S (G) \land y = S) \land (z = F \circ {S (G)}^{-1} \land w = Z))) \land (((x = y (G) \land y \in E) \land ((z \in T \land R (z) \underset{˙}{\leq} (X \underset{˙}{\land} W)) \land w = Z)) \land (F = x \circ z \land S = y))) \to K \in HL$
149	148	hllatd	$⊢ ((((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land ((x = S (G) \land y = S) \land (z = F \circ {S (G)}^{-1} \land w = Z))) \land (((x = y (G) \land y \in E) \land ((z \in T \land R (z) \underset{˙}{\leq} (X \underset{˙}{\land} W)) \land w = Z)) \land (F = x \circ z \land S = y))) \to K \in Lat$
150	1 6 8 9	trlcl	$⊢ ((K \in HL \land W \in H) \land z \in T) \to R (z) \in B$
151	134 143 150	syl2anc	$⊢ ((((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land ((x = S (G) \land y = S) \land (z = F \circ {S (G)}^{-1} \land w = Z))) \land (((x = y (G) \land y \in E) \land ((z \in T \land R (z) \underset{˙}{\leq} (X \underset{˙}{\land} W)) \land w = Z)) \land (F = x \circ z \land S = y))) \to R (z) \in B$
152		simpl2l	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land ((x = S (G) \land y = S) \land (z = F \circ {S (G)}^{-1} \land w = Z))) \to X \in B$
153	152	adantr	$⊢ ((((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land ((x = S (G) \land y = S) \land (z = F \circ {S (G)}^{-1} \land w = Z))) \land (((x = y (G) \land y \in E) \land ((z \in T \land R (z) \underset{˙}{\leq} (X \underset{˙}{\land} W)) \land w = Z)) \land (F = x \circ z \land S = y))) \to X \in B$
154		simpl1r	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land ((x = S (G) \land y = S) \land (z = F \circ {S (G)}^{-1} \land w = Z))) \to W \in H$
155	154	adantr	$⊢ ((((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land ((x = S (G) \land y = S) \land (z = F \circ {S (G)}^{-1} \land w = Z))) \land (((x = y (G) \land y \in E) \land ((z \in T \land R (z) \underset{˙}{\leq} (X \underset{˙}{\land} W)) \land w = Z)) \land (F = x \circ z \land S = y))) \to W \in H$
156	155 33	syl	$⊢ ((((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land ((x = S (G) \land y = S) \land (z = F \circ {S (G)}^{-1} \land w = Z))) \land (((x = y (G) \land y \in E) \land ((z \in T \land R (z) \underset{˙}{\leq} (X \underset{˙}{\land} W)) \land w = Z)) \land (F = x \circ z \land S = y))) \to W \in B$
157	149 153 156 35	syl3anc	$⊢ ((((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land ((x = S (G) \land y = S) \land (z = F \circ {S (G)}^{-1} \land w = Z))) \land (((x = y (G) \land y \in E) \land ((z \in T \land R (z) \underset{˙}{\leq} (X \underset{˙}{\land} W)) \land w = Z)) \land (F = x \circ z \land S = y))) \to X \underset{˙}{\land} W \in B$
158		simprlr	$⊢ ((x = y (G) \land y \in E) \land ((z \in T \land R (z) \underset{˙}{\leq} (X \underset{˙}{\land} W)) \land w = Z)) \to R (z) \underset{˙}{\leq} (X \underset{˙}{\land} W)$
159	158	ad2antrl	$⊢ ((((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land ((x = S (G) \land y = S) \land (z = F \circ {S (G)}^{-1} \land w = Z))) \land (((x = y (G) \land y \in E) \land ((z \in T \land R (z) \underset{˙}{\leq} (X \underset{˙}{\land} W)) \land w = Z)) \land (F = x \circ z \land S = y))) \to R (z) \underset{˙}{\leq} (X \underset{˙}{\land} W)$
160	1 2 4	latmle1	$⊢ (K \in Lat \land X \in B \land W \in B) \to (X \underset{˙}{\land} W) \underset{˙}{\leq} X$
161	149 153 156 160	syl3anc	$⊢ ((((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land ((x = S (G) \land y = S) \land (z = F \circ {S (G)}^{-1} \land w = Z))) \land (((x = y (G) \land y \in E) \land ((z \in T \land R (z) \underset{˙}{\leq} (X \underset{˙}{\land} W)) \land w = Z)) \land (F = x \circ z \land S = y))) \to (X \underset{˙}{\land} W) \underset{˙}{\leq} X$
162	1 2 149 151 157 153 159 161	lattrd	$⊢ ((((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land ((x = S (G) \land y = S) \land (z = F \circ {S (G)}^{-1} \land w = Z))) \land (((x = y (G) \land y \in E) \land ((z \in T \land R (z) \underset{˙}{\leq} (X \underset{˙}{\land} W)) \land w = Z)) \land (F = x \circ z \land S = y))) \to R (z) \underset{˙}{\leq} X$
163	146 136 162	jca31	$⊢ ((((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land ((x = S (G) \land y = S) \land (z = F \circ {S (G)}^{-1} \land w = Z))) \land (((x = y (G) \land y \in E) \land ((z \in T \land R (z) \underset{˙}{\leq} (X \underset{˙}{\land} W)) \land w = Z)) \land (F = x \circ z \land S = y))) \to ((F \in T \land y \in E) \land R (z) \underset{˙}{\leq} X)$
164		simprll	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land ((x = S (G) \land y = S) \land (z = F \circ {S (G)}^{-1} \land w = Z))) \to x = S (G)$
165	164	adantr	$⊢ ((((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land ((x = S (G) \land y = S) \land (z = F \circ {S (G)}^{-1} \land w = Z))) \land ((F \in T \land y \in E) \land R (z) \underset{˙}{\leq} X)) \to x = S (G)$
166		simprlr	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land ((x = S (G) \land y = S) \land (z = F \circ {S (G)}^{-1} \land w = Z))) \to y = S$
167	166	adantr	$⊢ ((((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land ((x = S (G) \land y = S) \land (z = F \circ {S (G)}^{-1} \land w = Z))) \land ((F \in T \land y \in E) \land R (z) \underset{˙}{\leq} X)) \to y = S$
168	167	fveq1d	$⊢ ((((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land ((x = S (G) \land y = S) \land (z = F \circ {S (G)}^{-1} \land w = Z))) \land ((F \in T \land y \in E) \land R (z) \underset{˙}{\leq} X)) \to y (G) = S (G)$
169	165 168	eqtr4d	$⊢ ((((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land ((x = S (G) \land y = S) \land (z = F \circ {S (G)}^{-1} \land w = Z))) \land ((F \in T \land y \in E) \land R (z) \underset{˙}{\leq} X)) \to x = y (G)$
170		simprlr	$⊢ ((((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land ((x = S (G) \land y = S) \land (z = F \circ {S (G)}^{-1} \land w = Z))) \land ((F \in T \land y \in E) \land R (z) \underset{˙}{\leq} X)) \to y \in E$
171	169 170	jca	$⊢ ((((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land ((x = S (G) \land y = S) \land (z = F \circ {S (G)}^{-1} \land w = Z))) \land ((F \in T \land y \in E) \land R (z) \underset{˙}{\leq} X)) \to (x = y (G) \land y \in E)$
172		simprrl	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land ((x = S (G) \land y = S) \land (z = F \circ {S (G)}^{-1} \land w = Z))) \to z = F \circ {S (G)}^{-1}$
173	172	adantr	$⊢ ((((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land ((x = S (G) \land y = S) \land (z = F \circ {S (G)}^{-1} \land w = Z))) \land ((F \in T \land y \in E) \land R (z) \underset{˙}{\leq} X)) \to z = F \circ {S (G)}^{-1}$
174		simpll1	$⊢ ((((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land ((x = S (G) \land y = S) \land (z = F \circ {S (G)}^{-1} \land w = Z))) \land ((F \in T \land y \in E) \land R (z) \underset{˙}{\leq} X)) \to (K \in HL \land W \in H)$
175		simprll	$⊢ ((((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land ((x = S (G) \land y = S) \land (z = F \circ {S (G)}^{-1} \land w = Z))) \land ((F \in T \land y \in E) \land R (z) \underset{˙}{\leq} X)) \to F \in T$
176	167 170	eqeltrrd	$⊢ ((((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land ((x = S (G) \land y = S) \land (z = F \circ {S (G)}^{-1} \land w = Z))) \land ((F \in T \land y \in E) \land R (z) \underset{˙}{\leq} X)) \to S \in E$
177	174 54	syl	$⊢ ((((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land ((x = S (G) \land y = S) \land (z = F \circ {S (G)}^{-1} \land w = Z))) \land ((F \in T \land y \in E) \land R (z) \underset{˙}{\leq} X)) \to (P \in A \land \neg P \underset{˙}{\leq} W)$
178	138	adantr	$⊢ ((((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land ((x = S (G) \land y = S) \land (z = F \circ {S (G)}^{-1} \land w = Z))) \land ((F \in T \land y \in E) \land R (z) \underset{˙}{\leq} X)) \to (Q \in A \land \neg Q \underset{˙}{\leq} W)$
179	174 177 178 57	syl3anc	$⊢ ((((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land ((x = S (G) \land y = S) \land (z = F \circ {S (G)}^{-1} \land w = Z))) \land ((F \in T \land y \in E) \land R (z) \underset{˙}{\leq} X)) \to G \in T$
180	174 176 179 100	syl3anc	$⊢ ((((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land ((x = S (G) \land y = S) \land (z = F \circ {S (G)}^{-1} \land w = Z))) \land ((F \in T \land y \in E) \land R (z) \underset{˙}{\leq} X)) \to S (G) \in T$
181	174 180 118	syl2anc	$⊢ ((((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land ((x = S (G) \land y = S) \land (z = F \circ {S (G)}^{-1} \land w = Z))) \land ((F \in T \land y \in E) \land R (z) \underset{˙}{\leq} X)) \to {S (G)}^{-1} \in T$
182	6 8	ltrnco	$⊢ ((K \in HL \land W \in H) \land F \in T \land {S (G)}^{-1} \in T) \to F \circ {S (G)}^{-1} \in T$
183	174 175 181 182	syl3anc	$⊢ ((((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land ((x = S (G) \land y = S) \land (z = F \circ {S (G)}^{-1} \land w = Z))) \land ((F \in T \land y \in E) \land R (z) \underset{˙}{\leq} X)) \to F \circ {S (G)}^{-1} \in T$
184	173 183	eqeltrd	$⊢ ((((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land ((x = S (G) \land y = S) \land (z = F \circ {S (G)}^{-1} \land w = Z))) \land ((F \in T \land y \in E) \land R (z) \underset{˙}{\leq} X)) \to z \in T$
185		simprr	$⊢ ((((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land ((x = S (G) \land y = S) \land (z = F \circ {S (G)}^{-1} \land w = Z))) \land ((F \in T \land y \in E) \land R (z) \underset{˙}{\leq} X)) \to R (z) \underset{˙}{\leq} X$
186	2 6 8 9	trlle	$⊢ ((K \in HL \land W \in H) \land z \in T) \to R (z) \underset{˙}{\leq} W$
187	174 184 186	syl2anc	$⊢ ((((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land ((x = S (G) \land y = S) \land (z = F \circ {S (G)}^{-1} \land w = Z))) \land ((F \in T \land y \in E) \land R (z) \underset{˙}{\leq} X)) \to R (z) \underset{˙}{\leq} W$
188	147	adantr	$⊢ ((((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land ((x = S (G) \land y = S) \land (z = F \circ {S (G)}^{-1} \land w = Z))) \land ((F \in T \land y \in E) \land R (z) \underset{˙}{\leq} X)) \to K \in HL$
189	188	hllatd	$⊢ ((((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land ((x = S (G) \land y = S) \land (z = F \circ {S (G)}^{-1} \land w = Z))) \land ((F \in T \land y \in E) \land R (z) \underset{˙}{\leq} X)) \to K \in Lat$
190	174 184 150	syl2anc	$⊢ ((((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land ((x = S (G) \land y = S) \land (z = F \circ {S (G)}^{-1} \land w = Z))) \land ((F \in T \land y \in E) \land R (z) \underset{˙}{\leq} X)) \to R (z) \in B$
191	152	adantr	$⊢ ((((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land ((x = S (G) \land y = S) \land (z = F \circ {S (G)}^{-1} \land w = Z))) \land ((F \in T \land y \in E) \land R (z) \underset{˙}{\leq} X)) \to X \in B$
192	154	adantr	$⊢ ((((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land ((x = S (G) \land y = S) \land (z = F \circ {S (G)}^{-1} \land w = Z))) \land ((F \in T \land y \in E) \land R (z) \underset{˙}{\leq} X)) \to W \in H$
193	192 33	syl	$⊢ ((((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land ((x = S (G) \land y = S) \land (z = F \circ {S (G)}^{-1} \land w = Z))) \land ((F \in T \land y \in E) \land R (z) \underset{˙}{\leq} X)) \to W \in B$
194	1 2 4	latlem12	$⊢ (K \in Lat \land (R (z) \in B \land X \in B \land W \in B)) \to ((R (z) \underset{˙}{\leq} X \land R (z) \underset{˙}{\leq} W) \leftrightarrow R (z) \underset{˙}{\leq} (X \underset{˙}{\land} W))$
195	189 190 191 193 194	syl13anc	$⊢ ((((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land ((x = S (G) \land y = S) \land (z = F \circ {S (G)}^{-1} \land w = Z))) \land ((F \in T \land y \in E) \land R (z) \underset{˙}{\leq} X)) \to ((R (z) \underset{˙}{\leq} X \land R (z) \underset{˙}{\leq} W) \leftrightarrow R (z) \underset{˙}{\leq} (X \underset{˙}{\land} W))$
196	185 187 195	mpbi2and	$⊢ ((((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land ((x = S (G) \land y = S) \land (z = F \circ {S (G)}^{-1} \land w = Z))) \land ((F \in T \land y \in E) \land R (z) \underset{˙}{\leq} X)) \to R (z) \underset{˙}{\leq} (X \underset{˙}{\land} W)$
197		simprrr	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land ((x = S (G) \land y = S) \land (z = F \circ {S (G)}^{-1} \land w = Z))) \to w = Z$
198	197	adantr	$⊢ ((((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land ((x = S (G) \land y = S) \land (z = F \circ {S (G)}^{-1} \land w = Z))) \land ((F \in T \land y \in E) \land R (z) \underset{˙}{\leq} X)) \to w = Z$
199	184 196 198	jca31	$⊢ ((((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land ((x = S (G) \land y = S) \land (z = F \circ {S (G)}^{-1} \land w = Z))) \land ((F \in T \land y \in E) \land R (z) \underset{˙}{\leq} X)) \to ((z \in T \land R (z) \underset{˙}{\leq} (X \underset{˙}{\land} W)) \land w = Z)$
200	174 180 102	syl2anc	$⊢ ((((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land ((x = S (G) \land y = S) \land (z = F \circ {S (G)}^{-1} \land w = Z))) \land ((F \in T \land y \in E) \land R (z) \underset{˙}{\leq} X)) \to S (G) : B \underset{1-1 onto}{⟶} B$
201	200 104	syl	$⊢ ((((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land ((x = S (G) \land y = S) \land (z = F \circ {S (G)}^{-1} \land w = Z))) \land ((F \in T \land y \in E) \land R (z) \underset{˙}{\leq} X)) \to {S (G)}^{-1} \circ S (G) = {I ↾}_{B}$
202	201	coeq2d	$⊢ ((((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land ((x = S (G) \land y = S) \land (z = F \circ {S (G)}^{-1} \land w = Z))) \land ((F \in T \land y \in E) \land R (z) \underset{˙}{\leq} X)) \to F \circ ({S (G)}^{-1} \circ S (G)) = F \circ ({I ↾}_{B})$
203	1 6 8	ltrn1o	$⊢ ((K \in HL \land W \in H) \land F \in T) \to F : B \underset{1-1 onto}{⟶} B$
204	174 175 203	syl2anc	$⊢ ((((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land ((x = S (G) \land y = S) \land (z = F \circ {S (G)}^{-1} \land w = Z))) \land ((F \in T \land y \in E) \land R (z) \underset{˙}{\leq} X)) \to F : B \underset{1-1 onto}{⟶} B$
205		f1of	$⊢ F : B \underset{1-1 onto}{⟶} B \to F : B ⟶ B$
206		fcoi1	$⊢ F : B ⟶ B \to F \circ ({I ↾}_{B}) = F$
207	204 205 206	3syl	$⊢ ((((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land ((x = S (G) \land y = S) \land (z = F \circ {S (G)}^{-1} \land w = Z))) \land ((F \in T \land y \in E) \land R (z) \underset{˙}{\leq} X)) \to F \circ ({I ↾}_{B}) = F$
208	202 207	eqtr2d	$⊢ ((((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land ((x = S (G) \land y = S) \land (z = F \circ {S (G)}^{-1} \land w = Z))) \land ((F \in T \land y \in E) \land R (z) \underset{˙}{\leq} X)) \to F = F \circ ({S (G)}^{-1} \circ S (G))$
209		coass	$⊢ (F \circ {S (G)}^{-1}) \circ S (G) = F \circ ({S (G)}^{-1} \circ S (G))$
210	208 209	eqtr4di	$⊢ ((((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land ((x = S (G) \land y = S) \land (z = F \circ {S (G)}^{-1} \land w = Z))) \land ((F \in T \land y \in E) \land R (z) \underset{˙}{\leq} X)) \to F = (F \circ {S (G)}^{-1}) \circ S (G)$
211	6 8	ltrncom	$⊢ ((K \in HL \land W \in H) \land S (G) \in T \land F \circ {S (G)}^{-1} \in T) \to S (G) \circ (F \circ {S (G)}^{-1}) = (F \circ {S (G)}^{-1}) \circ S (G)$
212	174 180 183 211	syl3anc	$⊢ ((((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land ((x = S (G) \land y = S) \land (z = F \circ {S (G)}^{-1} \land w = Z))) \land ((F \in T \land y \in E) \land R (z) \underset{˙}{\leq} X)) \to S (G) \circ (F \circ {S (G)}^{-1}) = (F \circ {S (G)}^{-1}) \circ S (G)$
213	210 212	eqtr4d	$⊢ ((((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land ((x = S (G) \land y = S) \land (z = F \circ {S (G)}^{-1} \land w = Z))) \land ((F \in T \land y \in E) \land R (z) \underset{˙}{\leq} X)) \to F = S (G) \circ (F \circ {S (G)}^{-1})$
214	165 173	coeq12d	$⊢ ((((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land ((x = S (G) \land y = S) \land (z = F \circ {S (G)}^{-1} \land w = Z))) \land ((F \in T \land y \in E) \land R (z) \underset{˙}{\leq} X)) \to x \circ z = S (G) \circ (F \circ {S (G)}^{-1})$
215	213 214	eqtr4d	$⊢ ((((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land ((x = S (G) \land y = S) \land (z = F \circ {S (G)}^{-1} \land w = Z))) \land ((F \in T \land y \in E) \land R (z) \underset{˙}{\leq} X)) \to F = x \circ z$
216	167	eqcomd	$⊢ ((((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land ((x = S (G) \land y = S) \land (z = F \circ {S (G)}^{-1} \land w = Z))) \land ((F \in T \land y \in E) \land R (z) \underset{˙}{\leq} X)) \to S = y$
217	215 216	jca	$⊢ ((((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land ((x = S (G) \land y = S) \land (z = F \circ {S (G)}^{-1} \land w = Z))) \land ((F \in T \land y \in E) \land R (z) \underset{˙}{\leq} X)) \to (F = x \circ z \land S = y)$
218	171 199 217	jca31	$⊢ ((((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land ((x = S (G) \land y = S) \land (z = F \circ {S (G)}^{-1} \land w = Z))) \land ((F \in T \land y \in E) \land R (z) \underset{˙}{\leq} X)) \to (((x = y (G) \land y \in E) \land ((z \in T \land R (z) \underset{˙}{\leq} (X \underset{˙}{\land} W)) \land w = Z)) \land (F = x \circ z \land S = y))$
219	163 218	impbida	$⊢ (((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \land ((x = S (G) \land y = S) \land (z = F \circ {S (G)}^{-1} \land w = Z))) \to ((((x = y (G) \land y \in E) \land ((z \in T \land R (z) \underset{˙}{\leq} (X \underset{˙}{\land} W)) \land w = Z)) \land (F = x \circ z \land S = y)) \leftrightarrow ((F \in T \land y \in E) \land R (z) \underset{˙}{\leq} X))$
220	219	pm5.32da	$⊢ ((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \to ((((x = S (G) \land y = S) \land (z = F \circ {S (G)}^{-1} \land w = Z)) \land (((x = y (G) \land y \in E) \land ((z \in T \land R (z) \underset{˙}{\leq} (X \underset{˙}{\land} W)) \land w = Z)) \land (F = x \circ z \land S = y))) \leftrightarrow (((x = S (G) \land y = S) \land (z = F \circ {S (G)}^{-1} \land w = Z)) \land ((F \in T \land y \in E) \land R (z) \underset{˙}{\leq} X)))$
221		df-3an	$⊢ ((x = S (G) \land y = S) \land (z = F \circ {S (G)}^{-1} \land w = Z) \land ((F \in T \land y \in E) \land R (z) \underset{˙}{\leq} X)) \leftrightarrow (((x = S (G) \land y = S) \land (z = F \circ {S (G)}^{-1} \land w = Z)) \land ((F \in T \land y \in E) \land R (z) \underset{˙}{\leq} X))$
222	220 221	syl6bbr	$⊢ ((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \to ((((x = S (G) \land y = S) \land (z = F \circ {S (G)}^{-1} \land w = Z)) \land (((x = y (G) \land y \in E) \land ((z \in T \land R (z) \underset{˙}{\leq} (X \underset{˙}{\land} W)) \land w = Z)) \land (F = x \circ z \land S = y))) \leftrightarrow ((x = S (G) \land y = S) \land (z = F \circ {S (G)}^{-1} \land w = Z) \land ((F \in T \land y \in E) \land R (z) \underset{˙}{\leq} X)))$
223	50 132 222	3bitrd	$⊢ ((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \to (((⟨x, y⟩ \in C (Q) \land ⟨z, w⟩ \in N (X \underset{˙}{\land} W)) \land ⟨F, S⟩ = ⟨x, y⟩ \underset{˙}{+} ⟨z, w⟩) \leftrightarrow ((x = S (G) \land y = S) \land (z = F \circ {S (G)}^{-1} \land w = Z) \land ((F \in T \land y \in E) \land R (z) \underset{˙}{\leq} X)))$
224	223	4exbidv	$⊢ ((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \to (\exists x \exists y \exists z \exists w ((⟨x, y⟩ \in C (Q) \land ⟨z, w⟩ \in N (X \underset{˙}{\land} W)) \land ⟨F, S⟩ = ⟨x, y⟩ \underset{˙}{+} ⟨z, w⟩) \leftrightarrow \exists x \exists y \exists z \exists w ((x = S (G) \land y = S) \land (z = F \circ {S (G)}^{-1} \land w = Z) \land ((F \in T \land y \in E) \land R (z) \underset{˙}{\leq} X)))$
225		fvex	$⊢ S (G) \in V$
226	225	cnvex	$⊢ {S (G)}^{-1} \in V$
227	13 226	coex	$⊢ F \circ {S (G)}^{-1} \in V$
228	8	fvexi	$⊢ T \in V$
229	228	mptex	$⊢ (h \in T ⟼ {I ↾}_{B}) \in V$
230	15 229	eqeltri	$⊢ Z \in V$
231		biidd	$⊢ x = S (G) \to (((F \in T \land y \in E) \land R (z) \underset{˙}{\leq} X) \leftrightarrow ((F \in T \land y \in E) \land R (z) \underset{˙}{\leq} X))$
232		eleq1	$⊢ y = S \to (y \in E \leftrightarrow S \in E)$
233	232	anbi2d	$⊢ y = S \to ((F \in T \land y \in E) \leftrightarrow (F \in T \land S \in E))$
234	233	anbi1d	$⊢ y = S \to (((F \in T \land y \in E) \land R (z) \underset{˙}{\leq} X) \leftrightarrow ((F \in T \land S \in E) \land R (z) \underset{˙}{\leq} X))$
235		fveq2	$⊢ z = F \circ {S (G)}^{-1} \to R (z) = R (F \circ {S (G)}^{-1})$
236	235	breq1d	$⊢ z = F \circ {S (G)}^{-1} \to (R (z) \underset{˙}{\leq} X \leftrightarrow R (F \circ {S (G)}^{-1}) \underset{˙}{\leq} X)$
237	236	anbi2d	$⊢ z = F \circ {S (G)}^{-1} \to (((F \in T \land S \in E) \land R (z) \underset{˙}{\leq} X) \leftrightarrow ((F \in T \land S \in E) \land R (F \circ {S (G)}^{-1}) \underset{˙}{\leq} X))$
238		biidd	$⊢ w = Z \to (((F \in T \land S \in E) \land R (F \circ {S (G)}^{-1}) \underset{˙}{\leq} X) \leftrightarrow ((F \in T \land S \in E) \land R (F \circ {S (G)}^{-1}) \underset{˙}{\leq} X))$
239	225 14 227 230 231 234 237 238	ceqsex4v	$⊢ \exists x \exists y \exists z \exists w ((x = S (G) \land y = S) \land (z = F \circ {S (G)}^{-1} \land w = Z) \land ((F \in T \land y \in E) \land R (z) \underset{˙}{\leq} X)) \leftrightarrow ((F \in T \land S \in E) \land R (F \circ {S (G)}^{-1}) \underset{˙}{\leq} X)$
240	224 239	syl6bb	$⊢ ((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \to (\exists x \exists y \exists z \exists w ((⟨x, y⟩ \in C (Q) \land ⟨z, w⟩ \in N (X \underset{˙}{\land} W)) \land ⟨F, S⟩ = ⟨x, y⟩ \underset{˙}{+} ⟨z, w⟩) \leftrightarrow ((F \in T \land S \in E) \land R (F \circ {S (G)}^{-1}) \underset{˙}{\leq} X))$
241	24 42 240	3bitrd	$⊢ ((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land Q \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \to (⟨F, S⟩ \in I (X) \leftrightarrow ((F \in T \land S \in E) \land R (F \circ {S (G)}^{-1}) \underset{˙}{\leq} X))$

Metamath Proof Explorer

Theorem dihopelvalcpre

Proof