cdlemk12

Description: Part of proof of Lemma K of Crawley p. 118. Eq. 4, line 10, p. 119. (Contributed by NM, 30-Jun-2013)

	Ref	Expression
Hypotheses	cdlemk.b	$⊢ B = {Base}_{K}$
	cdlemk.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	cdlemk.j	$⊢ \underset{˙}{\lor} = join (K)$
	cdlemk.a	$⊢ A = Atoms (K)$
	cdlemk.h	$⊢ H = LHyp (K)$
	cdlemk.t	$⊢ T = LTrn (K) (W)$
	cdlemk.r	$⊢ R = trL (K) (W)$
	cdlemk.m	$⊢ \underset{˙}{\land} = meet (K)$
	cdlemk.s	$⊢ S = (f \in T ⟼ (ι i \in T \| i (P) = (P \underset{˙}{\lor} R (f)) \underset{˙}{\land} (N (P) \underset{˙}{\lor} R (f \circ F^{-1}))))$
Assertion	cdlemk12	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land ((N \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land X \neq {I ↾}_{B}) \land (R (G) \neq R (F) \land R (X) \neq R (F)) \land R (G) \neq R (X))) \to S (G) (P) = (P \underset{˙}{\lor} G (P)) \underset{˙}{\land} (S (X) (P) \underset{˙}{\lor} R (X \circ G^{-1}))$

Proof

Step	Hyp	Ref	Expression
1		cdlemk.b	$⊢ B = {Base}_{K}$
2		cdlemk.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		cdlemk.j	$⊢ \underset{˙}{\lor} = join (K)$
4		cdlemk.a	$⊢ A = Atoms (K)$
5		cdlemk.h	$⊢ H = LHyp (K)$
6		cdlemk.t	$⊢ T = LTrn (K) (W)$
7		cdlemk.r	$⊢ R = trL (K) (W)$
8		cdlemk.m	$⊢ \underset{˙}{\land} = meet (K)$
9		cdlemk.s	$⊢ S = (f \in T ⟼ (ι i \in T \| i (P) = (P \underset{˙}{\lor} R (f)) \underset{˙}{\land} (N (P) \underset{˙}{\lor} R (f \circ F^{-1}))))$
10		simp11l	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land ((N \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land X \neq {I ↾}_{B}) \land (R (G) \neq R (F) \land R (X) \neq R (F)) \land R (G) \neq R (X))) \to K \in HL$
11		simp22l	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land ((N \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land X \neq {I ↾}_{B}) \land (R (G) \neq R (F) \land R (X) \neq R (F)) \land R (G) \neq R (X))) \to P \in A$
12		simp11	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land ((N \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land X \neq {I ↾}_{B}) \land (R (G) \neq R (F) \land R (X) \neq R (F)) \land R (G) \neq R (X))) \to (K \in HL \land W \in H)$
13		simp13	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land ((N \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land X \neq {I ↾}_{B}) \land (R (G) \neq R (F) \land R (X) \neq R (F)) \land R (G) \neq R (X))) \to G \in T$
14	2 4 5 6	ltrnat	$⊢ ((K \in HL \land W \in H) \land G \in T \land P \in A) \to G (P) \in A$
15	12 13 11 14	syl3anc	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land ((N \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land X \neq {I ↾}_{B}) \land (R (G) \neq R (F) \land R (X) \neq R (F)) \land R (G) \neq R (X))) \to G (P) \in A$
16		simp12	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land ((N \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land X \neq {I ↾}_{B}) \land (R (G) \neq R (F) \land R (X) \neq R (F)) \land R (G) \neq R (X))) \to F \in T$
17		simp21r	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land ((N \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land X \neq {I ↾}_{B}) \land (R (G) \neq R (F) \land R (X) \neq R (F)) \land R (G) \neq R (X))) \to X \in T$
18	12 16 17	3jca	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land ((N \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land X \neq {I ↾}_{B}) \land (R (G) \neq R (F) \land R (X) \neq R (F)) \land R (G) \neq R (X))) \to ((K \in HL \land W \in H) \land F \in T \land X \in T)$
19		simp21l	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land ((N \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land X \neq {I ↾}_{B}) \land (R (G) \neq R (F) \land R (X) \neq R (F)) \land R (G) \neq R (X))) \to N \in T$
20		simp22	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land ((N \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land X \neq {I ↾}_{B}) \land (R (G) \neq R (F) \land R (X) \neq R (F)) \land R (G) \neq R (X))) \to (P \in A \land \neg P \underset{˙}{\leq} W)$
21		simp23	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land ((N \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land X \neq {I ↾}_{B}) \land (R (G) \neq R (F) \land R (X) \neq R (F)) \land R (G) \neq R (X))) \to R (F) = R (N)$
22	19 20 21	3jca	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land ((N \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land X \neq {I ↾}_{B}) \land (R (G) \neq R (F) \land R (X) \neq R (F)) \land R (G) \neq R (X))) \to (N \in T \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N))$
23		simp311	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land ((N \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land X \neq {I ↾}_{B}) \land (R (G) \neq R (F) \land R (X) \neq R (F)) \land R (G) \neq R (X))) \to F \neq {I ↾}_{B}$
24		simp313	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land ((N \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land X \neq {I ↾}_{B}) \land (R (G) \neq R (F) \land R (X) \neq R (F)) \land R (G) \neq R (X))) \to X \neq {I ↾}_{B}$
25		simp32r	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land ((N \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land X \neq {I ↾}_{B}) \land (R (G) \neq R (F) \land R (X) \neq R (F)) \land R (G) \neq R (X))) \to R (X) \neq R (F)$
26	1 2 3 4 5 6 7 8 9	cdlemksat	$⊢ (((K \in HL \land W \in H) \land F \in T \land X \in T) \land (N \in T \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land (F \neq {I ↾}_{B} \land X \neq {I ↾}_{B} \land R (X) \neq R (F))) \to S (X) (P) \in A$
27	18 22 23 24 25 26	syl113anc	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land ((N \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land X \neq {I ↾}_{B}) \land (R (G) \neq R (F) \land R (X) \neq R (F)) \land R (G) \neq R (X))) \to S (X) (P) \in A$
28		simp33	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land ((N \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land X \neq {I ↾}_{B}) \land (R (G) \neq R (F) \land R (X) \neq R (F)) \land R (G) \neq R (X))) \to R (G) \neq R (X)$
29	28	necomd	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land ((N \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land X \neq {I ↾}_{B}) \land (R (G) \neq R (F) \land R (X) \neq R (F)) \land R (G) \neq R (X))) \to R (X) \neq R (G)$
30	4 5 6 7	trlcocnvat	$⊢ ((K \in HL \land W \in H) \land (X \in T \land G \in T) \land R (X) \neq R (G)) \to R (X \circ G^{-1}) \in A$
31	12 17 13 29 30	syl121anc	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land ((N \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land X \neq {I ↾}_{B}) \land (R (G) \neq R (F) \land R (X) \neq R (F)) \land R (G) \neq R (X))) \to R (X \circ G^{-1}) \in A$
32		simp1	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land ((N \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land X \neq {I ↾}_{B}) \land (R (G) \neq R (F) \land R (X) \neq R (F)) \land R (G) \neq R (X))) \to ((K \in HL \land W \in H) \land F \in T \land G \in T)$
33		simp312	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land ((N \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land X \neq {I ↾}_{B}) \land (R (G) \neq R (F) \land R (X) \neq R (F)) \land R (G) \neq R (X))) \to G \neq {I ↾}_{B}$
34		simp32l	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land ((N \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land X \neq {I ↾}_{B}) \land (R (G) \neq R (F) \land R (X) \neq R (F)) \land R (G) \neq R (X))) \to R (G) \neq R (F)$
35	1 2 3 4 5 6 7 8 9	cdlemksat	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land (N \in T \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land (F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land R (G) \neq R (F))) \to S (G) (P) \in A$
36	32 22 23 33 34 35	syl113anc	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land ((N \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land X \neq {I ↾}_{B}) \land (R (G) \neq R (F) \land R (X) \neq R (F)) \land R (G) \neq R (X))) \to S (G) (P) \in A$
37	1 2 3 4 5 6 7 8 9	cdlemksv2	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land (N \in T \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land (F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land R (G) \neq R (F))) \to S (G) (P) = (P \underset{˙}{\lor} R (G)) \underset{˙}{\land} (N (P) \underset{˙}{\lor} R (G \circ F^{-1}))$
38	32 22 23 33 34 37	syl113anc	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land ((N \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land X \neq {I ↾}_{B}) \land (R (G) \neq R (F) \land R (X) \neq R (F)) \land R (G) \neq R (X))) \to S (G) (P) = (P \underset{˙}{\lor} R (G)) \underset{˙}{\land} (N (P) \underset{˙}{\lor} R (G \circ F^{-1}))$
39	10	hllatd	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land ((N \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land X \neq {I ↾}_{B}) \land (R (G) \neq R (F) \land R (X) \neq R (F)) \land R (G) \neq R (X))) \to K \in Lat$
40	1 4 5 6 7	trlnidat	$⊢ ((K \in HL \land W \in H) \land G \in T \land G \neq {I ↾}_{B}) \to R (G) \in A$
41	12 13 33 40	syl3anc	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land ((N \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land X \neq {I ↾}_{B}) \land (R (G) \neq R (F) \land R (X) \neq R (F)) \land R (G) \neq R (X))) \to R (G) \in A$
42	1 3 4	hlatjcl	$⊢ (K \in HL \land P \in A \land R (G) \in A) \to P \underset{˙}{\lor} R (G) \in B$
43	10 11 41 42	syl3anc	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land ((N \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land X \neq {I ↾}_{B}) \land (R (G) \neq R (F) \land R (X) \neq R (F)) \land R (G) \neq R (X))) \to P \underset{˙}{\lor} R (G) \in B$
44	2 4 5 6	ltrnat	$⊢ ((K \in HL \land W \in H) \land N \in T \land P \in A) \to N (P) \in A$
45	12 19 11 44	syl3anc	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land ((N \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land X \neq {I ↾}_{B}) \land (R (G) \neq R (F) \land R (X) \neq R (F)) \land R (G) \neq R (X))) \to N (P) \in A$
46	4 5 6 7	trlcocnvat	$⊢ ((K \in HL \land W \in H) \land (G \in T \land F \in T) \land R (G) \neq R (F)) \to R (G \circ F^{-1}) \in A$
47	12 13 16 34 46	syl121anc	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land ((N \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land X \neq {I ↾}_{B}) \land (R (G) \neq R (F) \land R (X) \neq R (F)) \land R (G) \neq R (X))) \to R (G \circ F^{-1}) \in A$
48	1 3 4	hlatjcl	$⊢ (K \in HL \land N (P) \in A \land R (G \circ F^{-1}) \in A) \to N (P) \underset{˙}{\lor} R (G \circ F^{-1}) \in B$
49	10 45 47 48	syl3anc	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land ((N \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land X \neq {I ↾}_{B}) \land (R (G) \neq R (F) \land R (X) \neq R (F)) \land R (G) \neq R (X))) \to N (P) \underset{˙}{\lor} R (G \circ F^{-1}) \in B$
50	1 2 8	latmle1	$⊢ (K \in Lat \land P \underset{˙}{\lor} R (G) \in B \land N (P) \underset{˙}{\lor} R (G \circ F^{-1}) \in B) \to ((P \underset{˙}{\lor} R (G)) \underset{˙}{\land} (N (P) \underset{˙}{\lor} R (G \circ F^{-1}))) \underset{˙}{\leq} (P \underset{˙}{\lor} R (G))$
51	39 43 49 50	syl3anc	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land ((N \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land X \neq {I ↾}_{B}) \land (R (G) \neq R (F) \land R (X) \neq R (F)) \land R (G) \neq R (X))) \to ((P \underset{˙}{\lor} R (G)) \underset{˙}{\land} (N (P) \underset{˙}{\lor} R (G \circ F^{-1}))) \underset{˙}{\leq} (P \underset{˙}{\lor} R (G))$
52	38 51	eqbrtrd	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land ((N \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land X \neq {I ↾}_{B}) \land (R (G) \neq R (F) \land R (X) \neq R (F)) \land R (G) \neq R (X))) \to S (G) (P) \underset{˙}{\leq} (P \underset{˙}{\lor} R (G))$
53	2 3 4 5 6 7	trljat1	$⊢ ((K \in HL \land W \in H) \land G \in T \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to P \underset{˙}{\lor} R (G) = P \underset{˙}{\lor} G (P)$
54	12 13 20 53	syl3anc	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land ((N \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land X \neq {I ↾}_{B}) \land (R (G) \neq R (F) \land R (X) \neq R (F)) \land R (G) \neq R (X))) \to P \underset{˙}{\lor} R (G) = P \underset{˙}{\lor} G (P)$
55	52 54	breqtrd	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land ((N \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land X \neq {I ↾}_{B}) \land (R (G) \neq R (F) \land R (X) \neq R (F)) \land R (G) \neq R (X))) \to S (G) (P) \underset{˙}{\leq} (P \underset{˙}{\lor} G (P))$
56		simp2	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land ((N \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land X \neq {I ↾}_{B}) \land (R (G) \neq R (F) \land R (X) \neq R (F)) \land R (G) \neq R (X))) \to ((N \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N))$
57		simp31	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land ((N \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land X \neq {I ↾}_{B}) \land (R (G) \neq R (F) \land R (X) \neq R (F)) \land R (G) \neq R (X))) \to (F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land X \neq {I ↾}_{B})$
58		eqid	$⊢ (G (P) \underset{˙}{\lor} X (P)) \underset{˙}{\land} (R (G \circ F^{-1}) \underset{˙}{\lor} R (X \circ F^{-1})) = (G (P) \underset{˙}{\lor} X (P)) \underset{˙}{\land} (R (G \circ F^{-1}) \underset{˙}{\lor} R (X \circ F^{-1}))$
59	1 2 3 4 5 6 7 8 9 58	cdlemk11	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land ((N \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land X \neq {I ↾}_{B}) \land R (G) \neq R (F) \land R (X) \neq R (F))) \to S (G) (P) \underset{˙}{\leq} (S (X) (P) \underset{˙}{\lor} R (X \circ G^{-1}))$
60	32 56 57 34 25 59	syl113anc	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land ((N \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land X \neq {I ↾}_{B}) \land (R (G) \neq R (F) \land R (X) \neq R (F)) \land R (G) \neq R (X))) \to S (G) (P) \underset{˙}{\leq} (S (X) (P) \underset{˙}{\lor} R (X \circ G^{-1}))$
61	2 3 4	hlatlej2	$⊢ (K \in HL \land P \in A \land R (G) \in A) \to R (G) \underset{˙}{\leq} (P \underset{˙}{\lor} R (G))$
62	10 11 41 61	syl3anc	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land ((N \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land X \neq {I ↾}_{B}) \land (R (G) \neq R (F) \land R (X) \neq R (F)) \land R (G) \neq R (X))) \to R (G) \underset{˙}{\leq} (P \underset{˙}{\lor} R (G))$
63	62 54	breqtrd	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land ((N \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land X \neq {I ↾}_{B}) \land (R (G) \neq R (F) \land R (X) \neq R (F)) \land R (G) \neq R (X))) \to R (G) \underset{˙}{\leq} (P \underset{˙}{\lor} G (P))$
64	1 2 3 4 5 6 7 8 9	cdlemksel	$⊢ (((K \in HL \land W \in H) \land F \in T \land X \in T) \land (N \in T \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land (F \neq {I ↾}_{B} \land X \neq {I ↾}_{B} \land R (X) \neq R (F))) \to S (X) \in T$
65	18 22 23 24 25 64	syl113anc	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land ((N \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land X \neq {I ↾}_{B}) \land (R (G) \neq R (F) \land R (X) \neq R (F)) \land R (G) \neq R (X))) \to S (X) \in T$
66	2 4 5 6	ltrnel	$⊢ ((K \in HL \land W \in H) \land S (X) \in T \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to (S (X) (P) \in A \land \neg S (X) (P) \underset{˙}{\leq} W)$
67	12 65 20 66	syl3anc	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land ((N \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land X \neq {I ↾}_{B}) \land (R (G) \neq R (F) \land R (X) \neq R (F)) \land R (G) \neq R (X))) \to (S (X) (P) \in A \land \neg S (X) (P) \underset{˙}{\leq} W)$
68	5 6	ltrncnv	$⊢ ((K \in HL \land W \in H) \land G \in T) \to G^{-1} \in T$
69	12 13 68	syl2anc	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land ((N \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land X \neq {I ↾}_{B}) \land (R (G) \neq R (F) \land R (X) \neq R (F)) \land R (G) \neq R (X))) \to G^{-1} \in T$
70	5 6 7	trlcnv	$⊢ ((K \in HL \land W \in H) \land G \in T) \to R (G^{-1}) = R (G)$
71	12 13 70	syl2anc	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land ((N \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land X \neq {I ↾}_{B}) \land (R (G) \neq R (F) \land R (X) \neq R (F)) \land R (G) \neq R (X))) \to R (G^{-1}) = R (G)$
72	71 28	eqnetrd	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land ((N \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land X \neq {I ↾}_{B}) \land (R (G) \neq R (F) \land R (X) \neq R (F)) \land R (G) \neq R (X))) \to R (G^{-1}) \neq R (X)$
73	1 5 6 7	trlcone	$⊢ ((K \in HL \land W \in H) \land (G^{-1} \in T \land X \in T) \land (R (G^{-1}) \neq R (X) \land X \neq {I ↾}_{B})) \to R (G^{-1}) \neq R (G^{-1} \circ X)$
74	12 69 17 72 24 73	syl122anc	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land ((N \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land X \neq {I ↾}_{B}) \land (R (G) \neq R (F) \land R (X) \neq R (F)) \land R (G) \neq R (X))) \to R (G^{-1}) \neq R (G^{-1} \circ X)$
75	74	necomd	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land ((N \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land X \neq {I ↾}_{B}) \land (R (G) \neq R (F) \land R (X) \neq R (F)) \land R (G) \neq R (X))) \to R (G^{-1} \circ X) \neq R (G^{-1})$
76	5 6	ltrncom	$⊢ ((K \in HL \land W \in H) \land G^{-1} \in T \land X \in T) \to G^{-1} \circ X = X \circ G^{-1}$
77	12 69 17 76	syl3anc	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land ((N \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land X \neq {I ↾}_{B}) \land (R (G) \neq R (F) \land R (X) \neq R (F)) \land R (G) \neq R (X))) \to G^{-1} \circ X = X \circ G^{-1}$
78	77	fveq2d	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land ((N \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land X \neq {I ↾}_{B}) \land (R (G) \neq R (F) \land R (X) \neq R (F)) \land R (G) \neq R (X))) \to R (G^{-1} \circ X) = R (X \circ G^{-1})$
79	75 78 71	3netr3d	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land ((N \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land X \neq {I ↾}_{B}) \land (R (G) \neq R (F) \land R (X) \neq R (F)) \land R (G) \neq R (X))) \to R (X \circ G^{-1}) \neq R (G)$
80	5 6	ltrnco	$⊢ ((K \in HL \land W \in H) \land X \in T \land G^{-1} \in T) \to X \circ G^{-1} \in T$
81	12 17 69 80	syl3anc	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land ((N \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land X \neq {I ↾}_{B}) \land (R (G) \neq R (F) \land R (X) \neq R (F)) \land R (G) \neq R (X))) \to X \circ G^{-1} \in T$
82	2 5 6 7	trlle	$⊢ ((K \in HL \land W \in H) \land X \circ G^{-1} \in T) \to R (X \circ G^{-1}) \underset{˙}{\leq} W$
83	12 81 82	syl2anc	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land ((N \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land X \neq {I ↾}_{B}) \land (R (G) \neq R (F) \land R (X) \neq R (F)) \land R (G) \neq R (X))) \to R (X \circ G^{-1}) \underset{˙}{\leq} W$
84	2 5 6 7	trlle	$⊢ ((K \in HL \land W \in H) \land G \in T) \to R (G) \underset{˙}{\leq} W$
85	12 13 84	syl2anc	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land ((N \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land X \neq {I ↾}_{B}) \land (R (G) \neq R (F) \land R (X) \neq R (F)) \land R (G) \neq R (X))) \to R (G) \underset{˙}{\leq} W$
86	2 3 4 5	lhp2atnle	$⊢ (((K \in HL \land W \in H) \land (S (X) (P) \in A \land \neg S (X) (P) \underset{˙}{\leq} W) \land R (X \circ G^{-1}) \neq R (G)) \land (R (X \circ G^{-1}) \in A \land R (X \circ G^{-1}) \underset{˙}{\leq} W) \land (R (G) \in A \land R (G) \underset{˙}{\leq} W)) \to \neg R (G) \underset{˙}{\leq} (S (X) (P) \underset{˙}{\lor} R (X \circ G^{-1}))$
87	12 67 79 31 83 41 85 86	syl322anc	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land ((N \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land X \neq {I ↾}_{B}) \land (R (G) \neq R (F) \land R (X) \neq R (F)) \land R (G) \neq R (X))) \to \neg R (G) \underset{˙}{\leq} (S (X) (P) \underset{˙}{\lor} R (X \circ G^{-1}))$
88		nbrne1	$⊢ (R (G) \underset{˙}{\leq} (P \underset{˙}{\lor} G (P)) \land \neg R (G) \underset{˙}{\leq} (S (X) (P) \underset{˙}{\lor} R (X \circ G^{-1}))) \to P \underset{˙}{\lor} G (P) \neq S (X) (P) \underset{˙}{\lor} R (X \circ G^{-1})$
89	63 87 88	syl2anc	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land ((N \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land X \neq {I ↾}_{B}) \land (R (G) \neq R (F) \land R (X) \neq R (F)) \land R (G) \neq R (X))) \to P \underset{˙}{\lor} G (P) \neq S (X) (P) \underset{˙}{\lor} R (X \circ G^{-1})$
90	2 3 8 4	2atm	$⊢ ((K \in HL \land P \in A \land G (P) \in A) \land (S (X) (P) \in A \land R (X \circ G^{-1}) \in A \land S (G) (P) \in A) \land (S (G) (P) \underset{˙}{\leq} (P \underset{˙}{\lor} G (P)) \land S (G) (P) \underset{˙}{\leq} (S (X) (P) \underset{˙}{\lor} R (X \circ G^{-1})) \land P \underset{˙}{\lor} G (P) \neq S (X) (P) \underset{˙}{\lor} R (X \circ G^{-1}))) \to S (G) (P) = (P \underset{˙}{\lor} G (P)) \underset{˙}{\land} (S (X) (P) \underset{˙}{\lor} R (X \circ G^{-1}))$
91	10 11 15 27 31 36 55 60 89 90	syl333anc	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land ((N \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land X \neq {I ↾}_{B}) \land (R (G) \neq R (F) \land R (X) \neq R (F)) \land R (G) \neq R (X))) \to S (G) (P) = (P \underset{˙}{\lor} G (P)) \underset{˙}{\land} (S (X) (P) \underset{˙}{\lor} R (X \circ G^{-1}))$

Metamath Proof Explorer

Theorem cdlemk12

Proof