cdlemkid3N

Description: Lemma for cdlemkid . (Contributed by NM, 25-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)$
	cdlemk5.z	$⊢ Z = (P \underset{˙}{\lor} R (b)) \underset{˙}{\land} (N (P) \underset{˙}{\lor} R (b \circ F^{-1}))$
	cdlemk5.y	$⊢ Y = (P \underset{˙}{\lor} R (g)) \underset{˙}{\land} (Z \underset{˙}{\lor} R (g \circ b^{-1}))$
	cdlemk5.x	$⊢ X = (ι z \in T \| \forall b \in T ((b \neq {I ↾}_{B} \land R (b) \neq R (F) \land R (b) \neq R (g)) \to z (P) = Y))$
Assertion	cdlemkid3N	$⊢ ((K \in HL \land W \in H) \land (F \in T \land N \in T \land R (F) = R (N)) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land G = {I ↾}_{B})) \to ⦋ G / g ⦌ X = (ι z \in T \| \forall b \in T ((b \neq {I ↾}_{B} \land R (b) \neq R (F) \land R (b) \neq R (G)) \to z (P) = 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		cdlemk5.z	$⊢ Z = (P \underset{˙}{\lor} R (b)) \underset{˙}{\land} (N (P) \underset{˙}{\lor} R (b \circ F^{-1}))$
10		cdlemk5.y	$⊢ Y = (P \underset{˙}{\lor} R (g)) \underset{˙}{\land} (Z \underset{˙}{\lor} R (g \circ b^{-1}))$
11		cdlemk5.x	$⊢ X = (ι z \in T \| \forall b \in T ((b \neq {I ↾}_{B} \land R (b) \neq R (F) \land R (b) \neq R (g)) \to z (P) = Y))$
12		simp3r	$⊢ ((K \in HL \land W \in H) \land (F \in T \land N \in T \land R (F) = R (N)) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land G = {I ↾}_{B})) \to G = {I ↾}_{B}$
13	1 6 7	idltrn	$⊢ (K \in HL \land W \in H) \to {I ↾}_{B} \in T$
14	13	3ad2ant1	$⊢ ((K \in HL \land W \in H) \land (F \in T \land N \in T \land R (F) = R (N)) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land G = {I ↾}_{B})) \to {I ↾}_{B} \in T$
15	12 14	eqeltrd	$⊢ ((K \in HL \land W \in H) \land (F \in T \land N \in T \land R (F) = R (N)) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land G = {I ↾}_{B})) \to G \in T$
16	11	csbeq2i	$⊢ ⦋ G / g ⦌ X = ⦋ G / g ⦌ (ι z \in T \| \forall b \in T ((b \neq {I ↾}_{B} \land R (b) \neq R (F) \land R (b) \neq R (g)) \to z (P) = Y))$
17		csbriota	$⊢ ⦋ G / g ⦌ (ι z \in T \| \forall b \in T ((b \neq {I ↾}_{B} \land R (b) \neq R (F) \land R (b) \neq R (g)) \to z (P) = Y)) = (ι z \in T \| \underset{˙}{[} G / g \underset{˙}{]} \forall b \in T ((b \neq {I ↾}_{B} \land R (b) \neq R (F) \land R (b) \neq R (g)) \to z (P) = Y))$
18	17	a1i	$⊢ G \in T \to ⦋ G / g ⦌ (ι z \in T \| \forall b \in T ((b \neq {I ↾}_{B} \land R (b) \neq R (F) \land R (b) \neq R (g)) \to z (P) = Y)) = (ι z \in T \| \underset{˙}{[} G / g \underset{˙}{]} \forall b \in T ((b \neq {I ↾}_{B} \land R (b) \neq R (F) \land R (b) \neq R (g)) \to z (P) = Y))$
19	16 18	syl5eq	$⊢ G \in T \to ⦋ G / g ⦌ X = (ι z \in T \| \underset{˙}{[} G / g \underset{˙}{]} \forall b \in T ((b \neq {I ↾}_{B} \land R (b) \neq R (F) \land R (b) \neq R (g)) \to z (P) = Y))$
20		sbcralg	$⊢ G \in T \to (\underset{˙}{[} G / g \underset{˙}{]} \forall b \in T ((b \neq {I ↾}_{B} \land R (b) \neq R (F) \land R (b) \neq R (g)) \to z (P) = Y) \leftrightarrow \forall b \in T \underset{˙}{[} G / g \underset{˙}{]} ((b \neq {I ↾}_{B} \land R (b) \neq R (F) \land R (b) \neq R (g)) \to z (P) = Y))$
21		sbcimg	$⊢ G \in T \to (\underset{˙}{[} G / g \underset{˙}{]} ((b \neq {I ↾}_{B} \land R (b) \neq R (F) \land R (b) \neq R (g)) \to z (P) = Y) \leftrightarrow (\underset{˙}{[} G / g \underset{˙}{]} (b \neq {I ↾}_{B} \land R (b) \neq R (F) \land R (b) \neq R (g)) \to \underset{˙}{[} G / g \underset{˙}{]} z (P) = Y))$
22		sbc3an	$⊢ \underset{˙}{[} G / g \underset{˙}{]} (b \neq {I ↾}_{B} \land R (b) \neq R (F) \land R (b) \neq R (g)) \leftrightarrow (\underset{˙}{[} G / g \underset{˙}{]} b \neq {I ↾}_{B} \land \underset{˙}{[} G / g \underset{˙}{]} R (b) \neq R (F) \land \underset{˙}{[} G / g \underset{˙}{]} R (b) \neq R (g))$
23		sbcg	$⊢ G \in T \to (\underset{˙}{[} G / g \underset{˙}{]} b \neq {I ↾}_{B} \leftrightarrow b \neq {I ↾}_{B})$
24		sbcg	$⊢ G \in T \to (\underset{˙}{[} G / g \underset{˙}{]} R (b) \neq R (F) \leftrightarrow R (b) \neq R (F))$
25		sbcne12	$⊢ \underset{˙}{[} G / g \underset{˙}{]} R (b) \neq R (g) \leftrightarrow ⦋ G / g ⦌ R (b) \neq ⦋ G / g ⦌ R (g)$
26		csbconstg	$⊢ G \in T \to ⦋ G / g ⦌ R (b) = R (b)$
27		csbfv	$⊢ ⦋ G / g ⦌ R (g) = R (G)$
28	27	a1i	$⊢ G \in T \to ⦋ G / g ⦌ R (g) = R (G)$
29	26 28	neeq12d	$⊢ G \in T \to (⦋ G / g ⦌ R (b) \neq ⦋ G / g ⦌ R (g) \leftrightarrow R (b) \neq R (G))$
30	25 29	syl5bb	$⊢ G \in T \to (\underset{˙}{[} G / g \underset{˙}{]} R (b) \neq R (g) \leftrightarrow R (b) \neq R (G))$
31	23 24 30	3anbi123d	$⊢ G \in T \to ((\underset{˙}{[} G / g \underset{˙}{]} b \neq {I ↾}_{B} \land \underset{˙}{[} G / g \underset{˙}{]} R (b) \neq R (F) \land \underset{˙}{[} G / g \underset{˙}{]} R (b) \neq R (g)) \leftrightarrow (b \neq {I ↾}_{B} \land R (b) \neq R (F) \land R (b) \neq R (G)))$
32	22 31	syl5bb	$⊢ G \in T \to (\underset{˙}{[} G / g \underset{˙}{]} (b \neq {I ↾}_{B} \land R (b) \neq R (F) \land R (b) \neq R (g)) \leftrightarrow (b \neq {I ↾}_{B} \land R (b) \neq R (F) \land R (b) \neq R (G)))$
33		sbceq2g	$⊢ G \in T \to (\underset{˙}{[} G / g \underset{˙}{]} z (P) = Y \leftrightarrow z (P) = ⦋ G / g ⦌ Y)$
34	32 33	imbi12d	$⊢ G \in T \to ((\underset{˙}{[} G / g \underset{˙}{]} (b \neq {I ↾}_{B} \land R (b) \neq R (F) \land R (b) \neq R (g)) \to \underset{˙}{[} G / g \underset{˙}{]} z (P) = Y) \leftrightarrow ((b \neq {I ↾}_{B} \land R (b) \neq R (F) \land R (b) \neq R (G)) \to z (P) = ⦋ G / g ⦌ Y))$
35	21 34	bitrd	$⊢ G \in T \to (\underset{˙}{[} G / g \underset{˙}{]} ((b \neq {I ↾}_{B} \land R (b) \neq R (F) \land R (b) \neq R (g)) \to z (P) = Y) \leftrightarrow ((b \neq {I ↾}_{B} \land R (b) \neq R (F) \land R (b) \neq R (G)) \to z (P) = ⦋ G / g ⦌ Y))$
36	35	ralbidv	$⊢ G \in T \to (\forall b \in T \underset{˙}{[} G / g \underset{˙}{]} ((b \neq {I ↾}_{B} \land R (b) \neq R (F) \land R (b) \neq R (g)) \to z (P) = Y) \leftrightarrow \forall b \in T ((b \neq {I ↾}_{B} \land R (b) \neq R (F) \land R (b) \neq R (G)) \to z (P) = ⦋ G / g ⦌ Y))$
37	20 36	bitrd	$⊢ G \in T \to (\underset{˙}{[} G / g \underset{˙}{]} \forall b \in T ((b \neq {I ↾}_{B} \land R (b) \neq R (F) \land R (b) \neq R (g)) \to z (P) = Y) \leftrightarrow \forall b \in T ((b \neq {I ↾}_{B} \land R (b) \neq R (F) \land R (b) \neq R (G)) \to z (P) = ⦋ G / g ⦌ Y))$
38	37	riotabidv	$⊢ G \in T \to (ι z \in T \| \underset{˙}{[} G / g \underset{˙}{]} \forall b \in T ((b \neq {I ↾}_{B} \land R (b) \neq R (F) \land R (b) \neq R (g)) \to z (P) = Y)) = (ι z \in T \| \forall b \in T ((b \neq {I ↾}_{B} \land R (b) \neq R (F) \land R (b) \neq R (G)) \to z (P) = ⦋ G / g ⦌ Y))$
39	19 38	eqtrd	$⊢ G \in T \to ⦋ G / g ⦌ X = (ι z \in T \| \forall b \in T ((b \neq {I ↾}_{B} \land R (b) \neq R (F) \land R (b) \neq R (G)) \to z (P) = ⦋ G / g ⦌ Y))$
40	15 39	syl	$⊢ ((K \in HL \land W \in H) \land (F \in T \land N \in T \land R (F) = R (N)) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land G = {I ↾}_{B})) \to ⦋ G / g ⦌ X = (ι z \in T \| \forall b \in T ((b \neq {I ↾}_{B} \land R (b) \neq R (F) \land R (b) \neq R (G)) \to z (P) = ⦋ G / g ⦌ Y))$
41		simp11	$⊢ (((K \in HL \land W \in H) \land (F \in T \land N \in T \land R (F) = R (N)) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land G = {I ↾}_{B})) \land b \in T \land (b \neq {I ↾}_{B} \land R (b) \neq R (F) \land R (b) \neq R (G))) \to (K \in HL \land W \in H)$
42		simp12	$⊢ (((K \in HL \land W \in H) \land (F \in T \land N \in T \land R (F) = R (N)) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land G = {I ↾}_{B})) \land b \in T \land (b \neq {I ↾}_{B} \land R (b) \neq R (F) \land R (b) \neq R (G))) \to (F \in T \land N \in T \land R (F) = R (N))$
43		simp13l	$⊢ (((K \in HL \land W \in H) \land (F \in T \land N \in T \land R (F) = R (N)) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land G = {I ↾}_{B})) \land b \in T \land (b \neq {I ↾}_{B} \land R (b) \neq R (F) \land R (b) \neq R (G))) \to (P \in A \land \neg P \underset{˙}{\leq} W)$
44		simp13r	$⊢ (((K \in HL \land W \in H) \land (F \in T \land N \in T \land R (F) = R (N)) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land G = {I ↾}_{B})) \land b \in T \land (b \neq {I ↾}_{B} \land R (b) \neq R (F) \land R (b) \neq R (G))) \to G = {I ↾}_{B}$
45		simp2	$⊢ (((K \in HL \land W \in H) \land (F \in T \land N \in T \land R (F) = R (N)) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land G = {I ↾}_{B})) \land b \in T \land (b \neq {I ↾}_{B} \land R (b) \neq R (F) \land R (b) \neq R (G))) \to b \in T$
46		simp31	$⊢ (((K \in HL \land W \in H) \land (F \in T \land N \in T \land R (F) = R (N)) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land G = {I ↾}_{B})) \land b \in T \land (b \neq {I ↾}_{B} \land R (b) \neq R (F) \land R (b) \neq R (G))) \to b \neq {I ↾}_{B}$
47	45 46	jca	$⊢ (((K \in HL \land W \in H) \land (F \in T \land N \in T \land R (F) = R (N)) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land G = {I ↾}_{B})) \land b \in T \land (b \neq {I ↾}_{B} \land R (b) \neq R (F) \land R (b) \neq R (G))) \to (b \in T \land b \neq {I ↾}_{B})$
48	1 2 3 4 5 6 7 8 9 10	cdlemkid2	$⊢ ((K \in HL \land W \in H) \land (F \in T \land N \in T \land R (F) = R (N)) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land G = {I ↾}_{B} \land (b \in T \land b \neq {I ↾}_{B}))) \to ⦋ G / g ⦌ Y = P$
49	41 42 43 44 47 48	syl113anc	$⊢ (((K \in HL \land W \in H) \land (F \in T \land N \in T \land R (F) = R (N)) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land G = {I ↾}_{B})) \land b \in T \land (b \neq {I ↾}_{B} \land R (b) \neq R (F) \land R (b) \neq R (G))) \to ⦋ G / g ⦌ Y = P$
50	49	3expa	$⊢ ((((K \in HL \land W \in H) \land (F \in T \land N \in T \land R (F) = R (N)) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land G = {I ↾}_{B})) \land b \in T) \land (b \neq {I ↾}_{B} \land R (b) \neq R (F) \land R (b) \neq R (G))) \to ⦋ G / g ⦌ Y = P$
51	50	eqeq2d	$⊢ ((((K \in HL \land W \in H) \land (F \in T \land N \in T \land R (F) = R (N)) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land G = {I ↾}_{B})) \land b \in T) \land (b \neq {I ↾}_{B} \land R (b) \neq R (F) \land R (b) \neq R (G))) \to (z (P) = ⦋ G / g ⦌ Y \leftrightarrow z (P) = P)$
52	51	pm5.74da	$⊢ (((K \in HL \land W \in H) \land (F \in T \land N \in T \land R (F) = R (N)) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land G = {I ↾}_{B})) \land b \in T) \to (((b \neq {I ↾}_{B} \land R (b) \neq R (F) \land R (b) \neq R (G)) \to z (P) = ⦋ G / g ⦌ Y) \leftrightarrow ((b \neq {I ↾}_{B} \land R (b) \neq R (F) \land R (b) \neq R (G)) \to z (P) = P))$
53	52	ralbidva	$⊢ ((K \in HL \land W \in H) \land (F \in T \land N \in T \land R (F) = R (N)) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land G = {I ↾}_{B})) \to (\forall b \in T ((b \neq {I ↾}_{B} \land R (b) \neq R (F) \land R (b) \neq R (G)) \to z (P) = ⦋ G / g ⦌ Y) \leftrightarrow \forall b \in T ((b \neq {I ↾}_{B} \land R (b) \neq R (F) \land R (b) \neq R (G)) \to z (P) = P))$
54	53	riotabidv	$⊢ ((K \in HL \land W \in H) \land (F \in T \land N \in T \land R (F) = R (N)) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land G = {I ↾}_{B})) \to (ι z \in T \| \forall b \in T ((b \neq {I ↾}_{B} \land R (b) \neq R (F) \land R (b) \neq R (G)) \to z (P) = ⦋ G / g ⦌ Y)) = (ι z \in T \| \forall b \in T ((b \neq {I ↾}_{B} \land R (b) \neq R (F) \land R (b) \neq R (G)) \to z (P) = P))$
55	40 54	eqtrd	$⊢ ((K \in HL \land W \in H) \land (F \in T \land N \in T \land R (F) = R (N)) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land G = {I ↾}_{B})) \to ⦋ G / g ⦌ X = (ι z \in T \| \forall b \in T ((b \neq {I ↾}_{B} \land R (b) \neq R (F) \land R (b) \neq R (G)) \to z (P) = P))$

Metamath Proof Explorer

Theorem cdlemkid3N

Proof