cdlemg41

Description: Convert cdlemg40 to function composition. TODO: Fix comment. (Contributed by NM, 31-May-2013)

	Ref	Expression
Hypotheses	cdlemg35.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	cdlemg35.j	$⊢ \underset{˙}{\lor} = join (K)$
	cdlemg35.m	$⊢ \underset{˙}{\land} = meet (K)$
	cdlemg35.a	$⊢ A = Atoms (K)$
	cdlemg35.h	$⊢ H = LHyp (K)$
	cdlemg35.t	$⊢ T = LTrn (K) (W)$
Assertion	cdlemg41	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (F \in T \land G \in T)) \to (P \underset{˙}{\lor} (F \circ G) (P)) \underset{˙}{\land} W = (Q \underset{˙}{\lor} (F \circ G) (Q)) \underset{˙}{\land} W$

Proof

Step	Hyp	Ref	Expression
1		cdlemg35.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		cdlemg35.j	$⊢ \underset{˙}{\lor} = join (K)$
3		cdlemg35.m	$⊢ \underset{˙}{\land} = meet (K)$
4		cdlemg35.a	$⊢ A = Atoms (K)$
5		cdlemg35.h	$⊢ H = LHyp (K)$
6		cdlemg35.t	$⊢ T = LTrn (K) (W)$
7	1 2 3 4 5 6	cdlemg40	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (F \in T \land G \in T)) \to (P \underset{˙}{\lor} F (G (P))) \underset{˙}{\land} W = (Q \underset{˙}{\lor} F (G (Q))) \underset{˙}{\land} W$
8		simp1	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (F \in T \land G \in T)) \to (K \in HL \land W \in H)$
9		simp3	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (F \in T \land G \in T)) \to (F \in T \land G \in T)$
10		simp2ll	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (F \in T \land G \in T)) \to P \in A$
11	1 4 5 6	ltrncoval	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T) \land P \in A) \to (F \circ G) (P) = F (G (P))$
12	8 9 10 11	syl3anc	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (F \in T \land G \in T)) \to (F \circ G) (P) = F (G (P))$
13	12	oveq2d	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (F \in T \land G \in T)) \to P \underset{˙}{\lor} (F \circ G) (P) = P \underset{˙}{\lor} F (G (P))$
14	13	oveq1d	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (F \in T \land G \in T)) \to (P \underset{˙}{\lor} (F \circ G) (P)) \underset{˙}{\land} W = (P \underset{˙}{\lor} F (G (P))) \underset{˙}{\land} W$
15		simp2rl	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (F \in T \land G \in T)) \to Q \in A$
16	1 4 5 6	ltrncoval	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T) \land Q \in A) \to (F \circ G) (Q) = F (G (Q))$
17	8 9 15 16	syl3anc	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (F \in T \land G \in T)) \to (F \circ G) (Q) = F (G (Q))$
18	17	oveq2d	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (F \in T \land G \in T)) \to Q \underset{˙}{\lor} (F \circ G) (Q) = Q \underset{˙}{\lor} F (G (Q))$
19	18	oveq1d	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (F \in T \land G \in T)) \to (Q \underset{˙}{\lor} (F \circ G) (Q)) \underset{˙}{\land} W = (Q \underset{˙}{\lor} F (G (Q))) \underset{˙}{\land} W$
20	7 14 19	3eqtr4d	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (F \in T \land G \in T)) \to (P \underset{˙}{\lor} (F \circ G) (P)) \underset{˙}{\land} W = (Q \underset{˙}{\lor} (F \circ G) (Q)) \underset{˙}{\land} W$

Metamath Proof Explorer

Theorem cdlemg41

Proof