cdlemk7

Description: Part of proof of Lemma K of Crawley p. 118. Line 5, p. 119. (Contributed by NM, 27-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}))))$
	cdlemk.v	$⊢ V = (G (P) \underset{˙}{\lor} X (P)) \underset{˙}{\land} (R (G \circ F^{-1}) \underset{˙}{\lor} R (X \circ F^{-1}))$
Assertion	cdlemk7	$⊢ (((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} V)$

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		cdlemk.v	$⊢ V = (G (P) \underset{˙}{\lor} X (P)) \underset{˙}{\land} (R (G \circ F^{-1}) \underset{˙}{\lor} R (X \circ F^{-1}))$
11		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))) \to ((K \in HL \land W \in H) \land F \in T \land G \in T)$
12		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))) \to ((N \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N))$
13		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))) \to F \neq {I ↾}_{B}$
14		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))) \to G \neq {I ↾}_{B}$
15		simp32	$⊢ (((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 R (G) \neq R (F)$
16		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))) \to R (X) \neq R (F)$
17	15 16	jca	$⊢ (((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 (R (G) \neq R (F) \land R (X) \neq R (F))$
18	1 2 3 4 5 6 7 8	cdlemk6	$⊢ (((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 (R (G) \neq R (F) \land R (X) \neq R (F)))) \to ((P \underset{˙}{\lor} G (P)) \underset{˙}{\land} (N (P) \underset{˙}{\lor} R (G \circ F^{-1}))) \underset{˙}{\leq} (((G (P) \underset{˙}{\lor} X (P)) \underset{˙}{\land} (R (G \circ F^{-1}) \underset{˙}{\lor} R (X \circ F^{-1}))) \underset{˙}{\lor} ((X (P) \underset{˙}{\lor} P) \underset{˙}{\land} (R (X \circ F^{-1}) \underset{˙}{\lor} N (P))))$
19	11 12 13 14 17 18	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))) \to ((P \underset{˙}{\lor} G (P)) \underset{˙}{\land} (N (P) \underset{˙}{\lor} R (G \circ F^{-1}))) \underset{˙}{\leq} (((G (P) \underset{˙}{\lor} X (P)) \underset{˙}{\land} (R (G \circ F^{-1}) \underset{˙}{\lor} R (X \circ F^{-1}))) \underset{˙}{\lor} ((X (P) \underset{˙}{\lor} P) \underset{˙}{\land} (R (X \circ F^{-1}) \underset{˙}{\lor} N (P))))$
20		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))) \to N \in T$
21		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))) \to (P \in A \land \neg P \underset{˙}{\leq} W)$
22		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))) \to R (F) = R (N)$
23	20 21 22	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))) \to (N \in T \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N))$
24	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}))$
25	11 23 13 14 15 24	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))) \to S (G) (P) = (P \underset{˙}{\lor} R (G)) \underset{˙}{\land} (N (P) \underset{˙}{\lor} R (G \circ F^{-1}))$
26		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))) \to (K \in HL \land W \in H)$
27		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))) \to G \in T$
28	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)$
29	26 27 21 28	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))) \to P \underset{˙}{\lor} R (G) = P \underset{˙}{\lor} G (P)$
30	29	oveq1d	$⊢ (((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 (P \underset{˙}{\lor} R (G)) \underset{˙}{\land} (N (P) \underset{˙}{\lor} R (G \circ F^{-1})) = (P \underset{˙}{\lor} G (P)) \underset{˙}{\land} (N (P) \underset{˙}{\lor} R (G \circ F^{-1}))$
31	25 30	eqtrd	$⊢ (((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) = (P \underset{˙}{\lor} G (P)) \underset{˙}{\land} (N (P) \underset{˙}{\lor} R (G \circ F^{-1}))$
32		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))) \to K \in HL$
33	32	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))) \to K \in Lat$
34		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))) \to F \in T$
35		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))) \to X \in T$
36	26 34 35	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))) \to ((K \in HL \land W \in H) \land F \in T \land X \in T)$
37		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))) \to X \neq {I ↾}_{B}$
38	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$
39	36 23 13 37 16 38	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))) \to S (X) (P) \in A$
40	1 4	atbase	$⊢ S (X) (P) \in A \to S (X) (P) \in B$
41	39 40	syl	$⊢ (((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 (X) (P) \in B$
42		simp11r	$⊢ (((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 W \in H$
43		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))) \to P \in A$
44	1 2 3 4 5 6 7 8 10	cdlemkvcl	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T \land X \in T) \land P \in A) \to V \in B$
45	32 42 34 27 35 43 44	syl231anc	$⊢ (((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 V \in B$
46	1 3	latjcom	$⊢ (K \in Lat \land S (X) (P) \in B \land V \in B) \to S (X) (P) \underset{˙}{\lor} V = V \underset{˙}{\lor} S (X) (P)$
47	33 41 45 46	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))) \to S (X) (P) \underset{˙}{\lor} V = V \underset{˙}{\lor} S (X) (P)$
48	10	a1i	$⊢ (((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 V = (G (P) \underset{˙}{\lor} X (P)) \underset{˙}{\land} (R (G \circ F^{-1}) \underset{˙}{\lor} R (X \circ F^{-1}))$
49	1 2 3 4 5 6 7 8 9	cdlemksv2	$⊢ (((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) = (P \underset{˙}{\lor} R (X)) \underset{˙}{\land} (N (P) \underset{˙}{\lor} R (X \circ F^{-1}))$
50	36 23 13 37 16 49	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))) \to S (X) (P) = (P \underset{˙}{\lor} R (X)) \underset{˙}{\land} (N (P) \underset{˙}{\lor} R (X \circ F^{-1}))$
51	2 3 4 5 6 7	trljat1	$⊢ ((K \in HL \land W \in H) \land X \in T \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to P \underset{˙}{\lor} R (X) = P \underset{˙}{\lor} X (P)$
52	26 35 21 51	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))) \to P \underset{˙}{\lor} R (X) = P \underset{˙}{\lor} X (P)$
53	2 4 5 6	ltrnat	$⊢ ((K \in HL \land W \in H) \land X \in T \land P \in A) \to X (P) \in A$
54	26 35 43 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))) \to X (P) \in A$
55	3 4	hlatjcom	$⊢ (K \in HL \land X (P) \in A \land P \in A) \to X (P) \underset{˙}{\lor} P = P \underset{˙}{\lor} X (P)$
56	32 54 43 55	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))) \to X (P) \underset{˙}{\lor} P = P \underset{˙}{\lor} X (P)$
57	52 56	eqtr4d	$⊢ (((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 P \underset{˙}{\lor} R (X) = X (P) \underset{˙}{\lor} P$
58	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$
59	26 20 43 58	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))) \to N (P) \in A$
60	35 34	jca	$⊢ (((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 (X \in T \land F \in T)$
61	4 5 6 7	trlcocnvat	$⊢ ((K \in HL \land W \in H) \land (X \in T \land F \in T) \land R (X) \neq R (F)) \to R (X \circ F^{-1}) \in A$
62	26 60 16 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))) \to R (X \circ F^{-1}) \in A$
63	3 4	hlatjcom	$⊢ (K \in HL \land N (P) \in A \land R (X \circ F^{-1}) \in A) \to N (P) \underset{˙}{\lor} R (X \circ F^{-1}) = R (X \circ F^{-1}) \underset{˙}{\lor} N (P)$
64	32 59 62 63	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))) \to N (P) \underset{˙}{\lor} R (X \circ F^{-1}) = R (X \circ F^{-1}) \underset{˙}{\lor} N (P)$
65	57 64	oveq12d	$⊢ (((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 (P \underset{˙}{\lor} R (X)) \underset{˙}{\land} (N (P) \underset{˙}{\lor} R (X \circ F^{-1})) = (X (P) \underset{˙}{\lor} P) \underset{˙}{\land} (R (X \circ F^{-1}) \underset{˙}{\lor} N (P))$
66	50 65	eqtrd	$⊢ (((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 (X) (P) = (X (P) \underset{˙}{\lor} P) \underset{˙}{\land} (R (X \circ F^{-1}) \underset{˙}{\lor} N (P))$
67	48 66	oveq12d	$⊢ (((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 V \underset{˙}{\lor} S (X) (P) = ((G (P) \underset{˙}{\lor} X (P)) \underset{˙}{\land} (R (G \circ F^{-1}) \underset{˙}{\lor} R (X \circ F^{-1}))) \underset{˙}{\lor} ((X (P) \underset{˙}{\lor} P) \underset{˙}{\land} (R (X \circ F^{-1}) \underset{˙}{\lor} N (P)))$
68	47 67	eqtrd	$⊢ (((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 (X) (P) \underset{˙}{\lor} V = ((G (P) \underset{˙}{\lor} X (P)) \underset{˙}{\land} (R (G \circ F^{-1}) \underset{˙}{\lor} R (X \circ F^{-1}))) \underset{˙}{\lor} ((X (P) \underset{˙}{\lor} P) \underset{˙}{\land} (R (X \circ F^{-1}) \underset{˙}{\lor} N (P)))$
69	19 31 68	3brtr4d	$⊢ (((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} V)$

Metamath Proof Explorer

Theorem cdlemk7

Proof