cdlemg7fvN

Description: Value of a translation composition in terms of an associated atom. (Contributed by NM, 28-Apr-2013) (New usage is discouraged.)

	Ref	Expression
Hypotheses	cdlemg7fv.b	$⊢ B = {Base}_{K}$
	cdlemg7fv.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	cdlemg7fv.j	$⊢ \underset{˙}{\lor} = join (K)$
	cdlemg7fv.m	$⊢ \underset{˙}{\land} = meet (K)$
	cdlemg7fv.a	$⊢ A = Atoms (K)$
	cdlemg7fv.h	$⊢ H = LHyp (K)$
	cdlemg7fv.t	$⊢ T = LTrn (K) (W)$
Assertion	cdlemg7fvN	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (X \in B \land \neg X \underset{˙}{\leq} W)) \land (F \in T \land G \in T \land P \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \to F (G (X)) = F (G (P)) \underset{˙}{\lor} (X \underset{˙}{\land} W)$

Proof

Step	Hyp	Ref	Expression
1		cdlemg7fv.b	$⊢ B = {Base}_{K}$
2		cdlemg7fv.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		cdlemg7fv.j	$⊢ \underset{˙}{\lor} = join (K)$
4		cdlemg7fv.m	$⊢ \underset{˙}{\land} = meet (K)$
5		cdlemg7fv.a	$⊢ A = Atoms (K)$
6		cdlemg7fv.h	$⊢ H = LHyp (K)$
7		cdlemg7fv.t	$⊢ T = LTrn (K) (W)$
8		simp1	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (X \in B \land \neg X \underset{˙}{\leq} W)) \land (F \in T \land G \in T \land P \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \to (K \in HL \land W \in H)$
9		simp32	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (X \in B \land \neg X \underset{˙}{\leq} W)) \land (F \in T \land G \in T \land P \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \to G \in T$
10		simp2l	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (X \in B \land \neg X \underset{˙}{\leq} W)) \land (F \in T \land G \in T \land P \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \to (P \in A \land \neg P \underset{˙}{\leq} W)$
11	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)$
12	8 9 10 11	syl3anc	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (X \in B \land \neg X \underset{˙}{\leq} W)) \land (F \in T \land G \in T \land P \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \to (G (P) \in A \land \neg G (P) \underset{˙}{\leq} W)$
13		simp2r	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (X \in B \land \neg X \underset{˙}{\leq} W)) \land (F \in T \land G \in T \land P \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \to (X \in B \land \neg X \underset{˙}{\leq} W)$
14	2 5 6 7 1	cdlemg7fvbwN	$⊢ ((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land G \in T) \to (G (X) \in B \land \neg G (X) \underset{˙}{\leq} W)$
15	8 13 9 14	syl3anc	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (X \in B \land \neg X \underset{˙}{\leq} W)) \land (F \in T \land G \in T \land P \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \to (G (X) \in B \land \neg G (X) \underset{˙}{\leq} W)$
16		simp31	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (X \in B \land \neg X \underset{˙}{\leq} W)) \land (F \in T \land G \in T \land P \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \to F \in T$
17		simp33	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (X \in B \land \neg X \underset{˙}{\leq} W)) \land (F \in T \land G \in T \land P \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \to P \underset{˙}{\lor} (X \underset{˙}{\land} W) = X$
18	6 7 2 3 5 4 1	cdlemg2fv	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (X \in B \land \neg X \underset{˙}{\leq} W)) \land (G \in T \land P \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \to G (X) = G (P) \underset{˙}{\lor} (X \underset{˙}{\land} W)$
19	8 10 13 9 17 18	syl122anc	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (X \in B \land \neg X \underset{˙}{\leq} W)) \land (F \in T \land G \in T \land P \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \to G (X) = G (P) \underset{˙}{\lor} (X \underset{˙}{\land} W)$
20	19	oveq1d	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (X \in B \land \neg X \underset{˙}{\leq} W)) \land (F \in T \land G \in T \land P \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \to G (X) \underset{˙}{\land} W = (G (P) \underset{˙}{\lor} (X \underset{˙}{\land} W)) \underset{˙}{\land} W$
21		simp2rl	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (X \in B \land \neg X \underset{˙}{\leq} W)) \land (F \in T \land G \in T \land P \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \to X \in B$
22	1 2 3 4 5 6	lhpelim	$⊢ ((K \in HL \land W \in H) \land (G (P) \in A \land \neg G (P) \underset{˙}{\leq} W) \land X \in B) \to (G (P) \underset{˙}{\lor} (X \underset{˙}{\land} W)) \underset{˙}{\land} W = X \underset{˙}{\land} W$
23	8 12 21 22	syl3anc	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (X \in B \land \neg X \underset{˙}{\leq} W)) \land (F \in T \land G \in T \land P \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \to (G (P) \underset{˙}{\lor} (X \underset{˙}{\land} W)) \underset{˙}{\land} W = X \underset{˙}{\land} W$
24	20 23	eqtrd	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (X \in B \land \neg X \underset{˙}{\leq} W)) \land (F \in T \land G \in T \land P \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \to G (X) \underset{˙}{\land} W = X \underset{˙}{\land} W$
25	24	oveq2d	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (X \in B \land \neg X \underset{˙}{\leq} W)) \land (F \in T \land G \in T \land P \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \to G (P) \underset{˙}{\lor} (G (X) \underset{˙}{\land} W) = G (P) \underset{˙}{\lor} (X \underset{˙}{\land} W)$
26	25 19	eqtr4d	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (X \in B \land \neg X \underset{˙}{\leq} W)) \land (F \in T \land G \in T \land P \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \to G (P) \underset{˙}{\lor} (G (X) \underset{˙}{\land} W) = G (X)$
27	6 7 2 3 5 4 1	cdlemg2fv	$⊢ ((K \in HL \land W \in H) \land ((G (P) \in A \land \neg G (P) \underset{˙}{\leq} W) \land (G (X) \in B \land \neg G (X) \underset{˙}{\leq} W)) \land (F \in T \land G (P) \underset{˙}{\lor} (G (X) \underset{˙}{\land} W) = G (X))) \to F (G (X)) = F (G (P)) \underset{˙}{\lor} (G (X) \underset{˙}{\land} W)$
28	8 12 15 16 26 27	syl122anc	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (X \in B \land \neg X \underset{˙}{\leq} W)) \land (F \in T \land G \in T \land P \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \to F (G (X)) = F (G (P)) \underset{˙}{\lor} (G (X) \underset{˙}{\land} W)$
29	24	oveq2d	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (X \in B \land \neg X \underset{˙}{\leq} W)) \land (F \in T \land G \in T \land P \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \to F (G (P)) \underset{˙}{\lor} (G (X) \underset{˙}{\land} W) = F (G (P)) \underset{˙}{\lor} (X \underset{˙}{\land} W)$
30	28 29	eqtrd	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (X \in B \land \neg X \underset{˙}{\leq} W)) \land (F \in T \land G \in T \land P \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \to F (G (X)) = F (G (P)) \underset{˙}{\lor} (X \underset{˙}{\land} W)$

Metamath Proof Explorer

Theorem cdlemg7fvN

Proof