mndifsplit

	Ref	Expression
Hypotheses	mndifsplit.b	$⊢ B = {Base}_{M}$
	mndifsplit.0g	$⊢ \underset{˙}{0} = 0_{M}$
	mndifsplit.pg	$⊢ \underset{˙}{+} = +_{M}$
Assertion	mndifsplit	$⊢ (M \in Mnd \land A \in B \land \neg (φ \land ψ)) \to if ((φ \lor ψ), A, \underset{˙}{0}) = if (φ, A, \underset{˙}{0}) \underset{˙}{+} if (ψ, A, \underset{˙}{0})$

Proof

Step	Hyp	Ref	Expression
1		mndifsplit.b	$⊢ B = {Base}_{M}$
2		mndifsplit.0g	$⊢ \underset{˙}{0} = 0_{M}$
3		mndifsplit.pg	$⊢ \underset{˙}{+} = +_{M}$
4		pm2.21	$⊢ \neg (φ \land ψ) \to ((φ \land ψ) \to if ((φ \lor ψ), A, \underset{˙}{0}) = if (φ, A, \underset{˙}{0}) \underset{˙}{+} if (ψ, A, \underset{˙}{0}))$
5	4	imp	$⊢ (\neg (φ \land ψ) \land (φ \land ψ)) \to if ((φ \lor ψ), A, \underset{˙}{0}) = if (φ, A, \underset{˙}{0}) \underset{˙}{+} if (ψ, A, \underset{˙}{0})$
6	5	3ad2antl3	$⊢ ((M \in Mnd \land A \in B \land \neg (φ \land ψ)) \land (φ \land ψ)) \to if ((φ \lor ψ), A, \underset{˙}{0}) = if (φ, A, \underset{˙}{0}) \underset{˙}{+} if (ψ, A, \underset{˙}{0})$
7	1 3 2	mndrid	$⊢ (M \in Mnd \land A \in B) \to A \underset{˙}{+} \underset{˙}{0} = A$
8	7	3adant3	$⊢ (M \in Mnd \land A \in B \land \neg (φ \land ψ)) \to A \underset{˙}{+} \underset{˙}{0} = A$
9	8	adantr	$⊢ ((M \in Mnd \land A \in B \land \neg (φ \land ψ)) \land (φ \land \neg ψ)) \to A \underset{˙}{+} \underset{˙}{0} = A$
10		iftrue	$⊢ φ \to if (φ, A, \underset{˙}{0}) = A$
11		iffalse	$⊢ \neg ψ \to if (ψ, A, \underset{˙}{0}) = \underset{˙}{0}$
12	10 11	oveqan12d	$⊢ (φ \land \neg ψ) \to if (φ, A, \underset{˙}{0}) \underset{˙}{+} if (ψ, A, \underset{˙}{0}) = A \underset{˙}{+} \underset{˙}{0}$
13	12	adantl	$⊢ ((M \in Mnd \land A \in B \land \neg (φ \land ψ)) \land (φ \land \neg ψ)) \to if (φ, A, \underset{˙}{0}) \underset{˙}{+} if (ψ, A, \underset{˙}{0}) = A \underset{˙}{+} \underset{˙}{0}$
14		iftrue	$⊢ (φ \lor ψ) \to if ((φ \lor ψ), A, \underset{˙}{0}) = A$
15	14	orcs	$⊢ φ \to if ((φ \lor ψ), A, \underset{˙}{0}) = A$
16	15	ad2antrl	$⊢ ((M \in Mnd \land A \in B \land \neg (φ \land ψ)) \land (φ \land \neg ψ)) \to if ((φ \lor ψ), A, \underset{˙}{0}) = A$
17	9 13 16	3eqtr4rd	$⊢ ((M \in Mnd \land A \in B \land \neg (φ \land ψ)) \land (φ \land \neg ψ)) \to if ((φ \lor ψ), A, \underset{˙}{0}) = if (φ, A, \underset{˙}{0}) \underset{˙}{+} if (ψ, A, \underset{˙}{0})$
18	1 3 2	mndlid	$⊢ (M \in Mnd \land A \in B) \to \underset{˙}{0} \underset{˙}{+} A = A$
19	18	3adant3	$⊢ (M \in Mnd \land A \in B \land \neg (φ \land ψ)) \to \underset{˙}{0} \underset{˙}{+} A = A$
20	19	adantr	$⊢ ((M \in Mnd \land A \in B \land \neg (φ \land ψ)) \land (\neg φ \land ψ)) \to \underset{˙}{0} \underset{˙}{+} A = A$
21		iffalse	$⊢ \neg φ \to if (φ, A, \underset{˙}{0}) = \underset{˙}{0}$
22		iftrue	$⊢ ψ \to if (ψ, A, \underset{˙}{0}) = A$
23	21 22	oveqan12d	$⊢ (\neg φ \land ψ) \to if (φ, A, \underset{˙}{0}) \underset{˙}{+} if (ψ, A, \underset{˙}{0}) = \underset{˙}{0} \underset{˙}{+} A$
24	23	adantl	$⊢ ((M \in Mnd \land A \in B \land \neg (φ \land ψ)) \land (\neg φ \land ψ)) \to if (φ, A, \underset{˙}{0}) \underset{˙}{+} if (ψ, A, \underset{˙}{0}) = \underset{˙}{0} \underset{˙}{+} A$
25	14	olcs	$⊢ ψ \to if ((φ \lor ψ), A, \underset{˙}{0}) = A$
26	25	ad2antll	$⊢ ((M \in Mnd \land A \in B \land \neg (φ \land ψ)) \land (\neg φ \land ψ)) \to if ((φ \lor ψ), A, \underset{˙}{0}) = A$
27	20 24 26	3eqtr4rd	$⊢ ((M \in Mnd \land A \in B \land \neg (φ \land ψ)) \land (\neg φ \land ψ)) \to if ((φ \lor ψ), A, \underset{˙}{0}) = if (φ, A, \underset{˙}{0}) \underset{˙}{+} if (ψ, A, \underset{˙}{0})$
28		simp1	$⊢ (M \in Mnd \land A \in B \land \neg (φ \land ψ)) \to M \in Mnd$
29	1 2	mndidcl	$⊢ M \in Mnd \to \underset{˙}{0} \in B$
30	1 3 2	mndlid	$⊢ (M \in Mnd \land \underset{˙}{0} \in B) \to \underset{˙}{0} \underset{˙}{+} \underset{˙}{0} = \underset{˙}{0}$
31	28 29 30	syl2anc2	$⊢ (M \in Mnd \land A \in B \land \neg (φ \land ψ)) \to \underset{˙}{0} \underset{˙}{+} \underset{˙}{0} = \underset{˙}{0}$
32	31	adantr	$⊢ ((M \in Mnd \land A \in B \land \neg (φ \land ψ)) \land (\neg φ \land \neg ψ)) \to \underset{˙}{0} \underset{˙}{+} \underset{˙}{0} = \underset{˙}{0}$
33	21 11	oveqan12d	$⊢ (\neg φ \land \neg ψ) \to if (φ, A, \underset{˙}{0}) \underset{˙}{+} if (ψ, A, \underset{˙}{0}) = \underset{˙}{0} \underset{˙}{+} \underset{˙}{0}$
34	33	adantl	$⊢ ((M \in Mnd \land A \in B \land \neg (φ \land ψ)) \land (\neg φ \land \neg ψ)) \to if (φ, A, \underset{˙}{0}) \underset{˙}{+} if (ψ, A, \underset{˙}{0}) = \underset{˙}{0} \underset{˙}{+} \underset{˙}{0}$
35		ioran	$⊢ \neg (φ \lor ψ) \leftrightarrow (\neg φ \land \neg ψ)$
36		iffalse	$⊢ \neg (φ \lor ψ) \to if ((φ \lor ψ), A, \underset{˙}{0}) = \underset{˙}{0}$
37	35 36	sylbir	$⊢ (\neg φ \land \neg ψ) \to if ((φ \lor ψ), A, \underset{˙}{0}) = \underset{˙}{0}$
38	37	adantl	$⊢ ((M \in Mnd \land A \in B \land \neg (φ \land ψ)) \land (\neg φ \land \neg ψ)) \to if ((φ \lor ψ), A, \underset{˙}{0}) = \underset{˙}{0}$
39	32 34 38	3eqtr4rd	$⊢ ((M \in Mnd \land A \in B \land \neg (φ \land ψ)) \land (\neg φ \land \neg ψ)) \to if ((φ \lor ψ), A, \underset{˙}{0}) = if (φ, A, \underset{˙}{0}) \underset{˙}{+} if (ψ, A, \underset{˙}{0})$
40	6 17 27 39	4casesdan	$⊢ (M \in Mnd \land A \in B \land \neg (φ \land ψ)) \to if ((φ \lor ψ), A, \underset{˙}{0}) = if (φ, A, \underset{˙}{0}) \underset{˙}{+} if (ψ, A, \underset{˙}{0})$

Metamath Proof Explorer

Theorem mndifsplit

Proof