cdlemkfid1N

Description: Lemma for cdlemkfid3N . (Contributed by NM, 29-Jul-2013) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		cdlemk5.b	$⊢ B = {Base}_{K}$
2		cdlemk5.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		cdlemk5.j	$⊢ \underset{˙}{\lor} = join (K)$
4		cdlemk5.m	$⊢ \underset{˙}{\land} = meet (K)$
5		cdlemk5.a	$⊢ A = Atoms (K)$
6		cdlemk5.h	$⊢ H = LHyp (K)$
7		cdlemk5.t	$⊢ T = LTrn (K) (W)$
8		cdlemk5.r	$⊢ R = trL (K) (W)$
9		simp1	$⊢ ((K \in HL \land W \in H) \land (F \in T \land F \neq {I ↾}_{B} \land G \in T) \land (R (G) \neq R (F) \land (P \in A \land \neg P \underset{˙}{\leq} W))) \to (K \in HL \land W \in H)$
10		simp23	$⊢ ((K \in HL \land W \in H) \land (F \in T \land F \neq {I ↾}_{B} \land G \in T) \land (R (G) \neq R (F) \land (P \in A \land \neg P \underset{˙}{\leq} W))) \to G \in T$
11		simp3r	$⊢ ((K \in HL \land W \in H) \land (F \in T \land F \neq {I ↾}_{B} \land G \in T) \land (R (G) \neq R (F) \land (P \in A \land \neg P \underset{˙}{\leq} W))) \to (P \in A \land \neg P \underset{˙}{\leq} W)$
12	2 3 5 6 7 8	trljat3	$⊢ ((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) = G (P) \underset{˙}{\lor} R (G)$
13	9 10 11 12	syl3anc	$⊢ ((K \in HL \land W \in H) \land (F \in T \land F \neq {I ↾}_{B} \land G \in T) \land (R (G) \neq R (F) \land (P \in A \land \neg P \underset{˙}{\leq} W))) \to P \underset{˙}{\lor} R (G) = G (P) \underset{˙}{\lor} R (G)$
14		simp1l	$⊢ ((K \in HL \land W \in H) \land (F \in T \land F \neq {I ↾}_{B} \land G \in T) \land (R (G) \neq R (F) \land (P \in A \land \neg P \underset{˙}{\leq} W))) \to K \in HL$
15		simp21	$⊢ ((K \in HL \land W \in H) \land (F \in T \land F \neq {I ↾}_{B} \land G \in T) \land (R (G) \neq R (F) \land (P \in A \land \neg P \underset{˙}{\leq} W))) \to F \in T$
16		simp3rl	$⊢ ((K \in HL \land W \in H) \land (F \in T \land F \neq {I ↾}_{B} \land G \in T) \land (R (G) \neq R (F) \land (P \in A \land \neg P \underset{˙}{\leq} W))) \to P \in A$
17	2 5 6 7	ltrnat	$⊢ ((K \in HL \land W \in H) \land F \in T \land P \in A) \to F (P) \in A$
18	9 15 16 17	syl3anc	$⊢ ((K \in HL \land W \in H) \land (F \in T \land F \neq {I ↾}_{B} \land G \in T) \land (R (G) \neq R (F) \land (P \in A \land \neg P \underset{˙}{\leq} W))) \to F (P) \in A$
19	2 5 6 7	ltrnat	$⊢ ((K \in HL \land W \in H) \land G \in T \land P \in A) \to G (P) \in A$
20	9 10 16 19	syl3anc	$⊢ ((K \in HL \land W \in H) \land (F \in T \land F \neq {I ↾}_{B} \land G \in T) \land (R (G) \neq R (F) \land (P \in A \land \neg P \underset{˙}{\leq} W))) \to G (P) \in A$
21	3 5	hlatjcom	$⊢ (K \in HL \land F (P) \in A \land G (P) \in A) \to F (P) \underset{˙}{\lor} G (P) = G (P) \underset{˙}{\lor} F (P)$
22	14 18 20 21	syl3anc	$⊢ ((K \in HL \land W \in H) \land (F \in T \land F \neq {I ↾}_{B} \land G \in T) \land (R (G) \neq R (F) \land (P \in A \land \neg P \underset{˙}{\leq} W))) \to F (P) \underset{˙}{\lor} G (P) = G (P) \underset{˙}{\lor} F (P)$
23	2 3 5 6 7 8	trlcoabs2N	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to F (P) \underset{˙}{\lor} R (G \circ F^{-1}) = F (P) \underset{˙}{\lor} G (P)$
24	9 15 10 11 23	syl121anc	$⊢ ((K \in HL \land W \in H) \land (F \in T \land F \neq {I ↾}_{B} \land G \in T) \land (R (G) \neq R (F) \land (P \in A \land \neg P \underset{˙}{\leq} W))) \to F (P) \underset{˙}{\lor} R (G \circ F^{-1}) = F (P) \underset{˙}{\lor} G (P)$
25	6 7 8	trlcocnv	$⊢ ((K \in HL \land W \in H) \land F \in T \land G \in T) \to R (F \circ G^{-1}) = R (G \circ F^{-1})$
26	9 15 10 25	syl3anc	$⊢ ((K \in HL \land W \in H) \land (F \in T \land F \neq {I ↾}_{B} \land G \in T) \land (R (G) \neq R (F) \land (P \in A \land \neg P \underset{˙}{\leq} W))) \to R (F \circ G^{-1}) = R (G \circ F^{-1})$
27	26	oveq2d	$⊢ ((K \in HL \land W \in H) \land (F \in T \land F \neq {I ↾}_{B} \land G \in T) \land (R (G) \neq R (F) \land (P \in A \land \neg P \underset{˙}{\leq} W))) \to G (P) \underset{˙}{\lor} R (F \circ G^{-1}) = G (P) \underset{˙}{\lor} R (G \circ F^{-1})$
28	2 3 5 6 7 8	trlcoabs2N	$⊢ ((K \in HL \land W \in H) \land (G \in T \land F \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to G (P) \underset{˙}{\lor} R (F \circ G^{-1}) = G (P) \underset{˙}{\lor} F (P)$
29	9 10 15 11 28	syl121anc	$⊢ ((K \in HL \land W \in H) \land (F \in T \land F \neq {I ↾}_{B} \land G \in T) \land (R (G) \neq R (F) \land (P \in A \land \neg P \underset{˙}{\leq} W))) \to G (P) \underset{˙}{\lor} R (F \circ G^{-1}) = G (P) \underset{˙}{\lor} F (P)$
30	27 29	eqtr3d	$⊢ ((K \in HL \land W \in H) \land (F \in T \land F \neq {I ↾}_{B} \land G \in T) \land (R (G) \neq R (F) \land (P \in A \land \neg P \underset{˙}{\leq} W))) \to G (P) \underset{˙}{\lor} R (G \circ F^{-1}) = G (P) \underset{˙}{\lor} F (P)$
31	22 24 30	3eqtr4d	$⊢ ((K \in HL \land W \in H) \land (F \in T \land F \neq {I ↾}_{B} \land G \in T) \land (R (G) \neq R (F) \land (P \in A \land \neg P \underset{˙}{\leq} W))) \to F (P) \underset{˙}{\lor} R (G \circ F^{-1}) = G (P) \underset{˙}{\lor} R (G \circ F^{-1})$
32	13 31	oveq12d	$⊢ ((K \in HL \land W \in H) \land (F \in T \land F \neq {I ↾}_{B} \land G \in T) \land (R (G) \neq R (F) \land (P \in A \land \neg P \underset{˙}{\leq} W))) \to (P \underset{˙}{\lor} R (G)) \underset{˙}{\land} (F (P) \underset{˙}{\lor} R (G \circ F^{-1})) = (G (P) \underset{˙}{\lor} R (G)) \underset{˙}{\land} (G (P) \underset{˙}{\lor} R (G \circ F^{-1}))$
33	1 6 7 8	trlcl	$⊢ ((K \in HL \land W \in H) \land G \in T) \to R (G) \in B$
34	9 10 33	syl2anc	$⊢ ((K \in HL \land W \in H) \land (F \in T \land F \neq {I ↾}_{B} \land G \in T) \land (R (G) \neq R (F) \land (P \in A \land \neg P \underset{˙}{\leq} W))) \to R (G) \in B$
35		simp1r	$⊢ ((K \in HL \land W \in H) \land (F \in T \land F \neq {I ↾}_{B} \land G \in T) \land (R (G) \neq R (F) \land (P \in A \land \neg P \underset{˙}{\leq} W))) \to W \in H$
36		simp3l	$⊢ ((K \in HL \land W \in H) \land (F \in T \land F \neq {I ↾}_{B} \land G \in T) \land (R (G) \neq R (F) \land (P \in A \land \neg P \underset{˙}{\leq} W))) \to R (G) \neq R (F)$
37	5 6 7 8	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$
38	14 35 10 15 36 37	syl221anc	$⊢ ((K \in HL \land W \in H) \land (F \in T \land F \neq {I ↾}_{B} \land G \in T) \land (R (G) \neq R (F) \land (P \in A \land \neg P \underset{˙}{\leq} W))) \to R (G \circ F^{-1}) \in A$
39	2 5 6 7	ltrnel	$⊢ ((K \in HL \land W \in H) \land G \in T \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to (G (P) \in A \land \neg G (P) \underset{˙}{\leq} W)$
40	9 10 11 39	syl3anc	$⊢ ((K \in HL \land W \in H) \land (F \in T \land F \neq {I ↾}_{B} \land G \in T) \land (R (G) \neq R (F) \land (P \in A \land \neg P \underset{˙}{\leq} W))) \to (G (P) \in A \land \neg G (P) \underset{˙}{\leq} W)$
41	6 7	ltrncnv	$⊢ ((K \in HL \land W \in H) \land F \in T) \to F^{-1} \in T$
42	9 15 41	syl2anc	$⊢ ((K \in HL \land W \in H) \land (F \in T \land F \neq {I ↾}_{B} \land G \in T) \land (R (G) \neq R (F) \land (P \in A \land \neg P \underset{˙}{\leq} W))) \to F^{-1} \in T$
43	6 7 8	trlcnv	$⊢ ((K \in HL \land W \in H) \land F \in T) \to R (F^{-1}) = R (F)$
44	9 15 43	syl2anc	$⊢ ((K \in HL \land W \in H) \land (F \in T \land F \neq {I ↾}_{B} \land G \in T) \land (R (G) \neq R (F) \land (P \in A \land \neg P \underset{˙}{\leq} W))) \to R (F^{-1}) = R (F)$
45	36 44	neeqtrrd	$⊢ ((K \in HL \land W \in H) \land (F \in T \land F \neq {I ↾}_{B} \land G \in T) \land (R (G) \neq R (F) \land (P \in A \land \neg P \underset{˙}{\leq} W))) \to R (G) \neq R (F^{-1})$
46		simp22	$⊢ ((K \in HL \land W \in H) \land (F \in T \land F \neq {I ↾}_{B} \land G \in T) \land (R (G) \neq R (F) \land (P \in A \land \neg P \underset{˙}{\leq} W))) \to F \neq {I ↾}_{B}$
47	1 6 7	ltrncnvnid	$⊢ ((K \in HL \land W \in H) \land F \in T \land F \neq {I ↾}_{B}) \to F^{-1} \neq {I ↾}_{B}$
48	9 15 46 47	syl3anc	$⊢ ((K \in HL \land W \in H) \land (F \in T \land F \neq {I ↾}_{B} \land G \in T) \land (R (G) \neq R (F) \land (P \in A \land \neg P \underset{˙}{\leq} W))) \to F^{-1} \neq {I ↾}_{B}$
49	1 6 7 8	trlcone	$⊢ ((K \in HL \land W \in H) \land (G \in T \land F^{-1} \in T) \land (R (G) \neq R (F^{-1}) \land F^{-1} \neq {I ↾}_{B})) \to R (G) \neq R (G \circ F^{-1})$
50	9 10 42 45 48 49	syl122anc	$⊢ ((K \in HL \land W \in H) \land (F \in T \land F \neq {I ↾}_{B} \land G \in T) \land (R (G) \neq R (F) \land (P \in A \land \neg P \underset{˙}{\leq} W))) \to R (G) \neq R (G \circ F^{-1})$
51		eqid	$⊢ 0. (K) = 0. (K)$
52	51 5 6 7 8	trlator0	$⊢ ((K \in HL \land W \in H) \land G \in T) \to (R (G) \in A \lor R (G) = 0. (K))$
53	9 10 52	syl2anc	$⊢ ((K \in HL \land W \in H) \land (F \in T \land F \neq {I ↾}_{B} \land G \in T) \land (R (G) \neq R (F) \land (P \in A \land \neg P \underset{˙}{\leq} W))) \to (R (G) \in A \lor R (G) = 0. (K))$
54	2 6 7 8	trlle	$⊢ ((K \in HL \land W \in H) \land G \in T) \to R (G) \underset{˙}{\leq} W$
55	14 35 10 54	syl21anc	$⊢ ((K \in HL \land W \in H) \land (F \in T \land F \neq {I ↾}_{B} \land G \in T) \land (R (G) \neq R (F) \land (P \in A \land \neg P \underset{˙}{\leq} W))) \to R (G) \underset{˙}{\leq} W$
56	6 7	ltrnco	$⊢ ((K \in HL \land W \in H) \land G \in T \land F^{-1} \in T) \to G \circ F^{-1} \in T$
57	9 10 42 56	syl3anc	$⊢ ((K \in HL \land W \in H) \land (F \in T \land F \neq {I ↾}_{B} \land G \in T) \land (R (G) \neq R (F) \land (P \in A \land \neg P \underset{˙}{\leq} W))) \to G \circ F^{-1} \in T$
58	2 6 7 8	trlle	$⊢ ((K \in HL \land W \in H) \land G \circ F^{-1} \in T) \to R (G \circ F^{-1}) \underset{˙}{\leq} W$
59	9 57 58	syl2anc	$⊢ ((K \in HL \land W \in H) \land (F \in T \land F \neq {I ↾}_{B} \land G \in T) \land (R (G) \neq R (F) \land (P \in A \land \neg P \underset{˙}{\leq} W))) \to R (G \circ F^{-1}) \underset{˙}{\leq} W$
60	2 3 51 5 6	lhp2at0nle	$⊢ (((K \in HL \land W \in H) \land (G (P) \in A \land \neg G (P) \underset{˙}{\leq} W) \land R (G) \neq R (G \circ F^{-1})) \land ((R (G) \in A \lor R (G) = 0. (K)) \land R (G) \underset{˙}{\leq} W) \land (R (G \circ F^{-1}) \in A \land R (G \circ F^{-1}) \underset{˙}{\leq} W)) \to \neg R (G \circ F^{-1}) \underset{˙}{\leq} (G (P) \underset{˙}{\lor} R (G))$
61	9 40 50 53 55 38 59 60	syl322anc	$⊢ ((K \in HL \land W \in H) \land (F \in T \land F \neq {I ↾}_{B} \land G \in T) \land (R (G) \neq R (F) \land (P \in A \land \neg P \underset{˙}{\leq} W))) \to \neg R (G \circ F^{-1}) \underset{˙}{\leq} (G (P) \underset{˙}{\lor} R (G))$
62	1 2 3 4 5	2llnma1b	$⊢ (K \in HL \land (R (G) \in B \land G (P) \in A \land R (G \circ F^{-1}) \in A) \land \neg R (G \circ F^{-1}) \underset{˙}{\leq} (G (P) \underset{˙}{\lor} R (G))) \to (G (P) \underset{˙}{\lor} R (G)) \underset{˙}{\land} (G (P) \underset{˙}{\lor} R (G \circ F^{-1})) = G (P)$
63	14 34 20 38 61 62	syl131anc	$⊢ ((K \in HL \land W \in H) \land (F \in T \land F \neq {I ↾}_{B} \land G \in T) \land (R (G) \neq R (F) \land (P \in A \land \neg P \underset{˙}{\leq} W))) \to (G (P) \underset{˙}{\lor} R (G)) \underset{˙}{\land} (G (P) \underset{˙}{\lor} R (G \circ F^{-1})) = G (P)$
64	32 63	eqtrd	$⊢ ((K \in HL \land W \in H) \land (F \in T \land F \neq {I ↾}_{B} \land G \in T) \land (R (G) \neq R (F) \land (P \in A \land \neg P \underset{˙}{\leq} W))) \to (P \underset{˙}{\lor} R (G)) \underset{˙}{\land} (F (P) \underset{˙}{\lor} R (G \circ F^{-1})) = G (P)$

Metamath Proof Explorer

Theorem cdlemkfid1N

Proof