Theorem isdomn5

Description: The right conjunct in the right hand side of the equivalence of isdomn is logically equivalent to a less symmetric version where one of the variables is restricted to be nonzero. (Contributed by SN, 16-Sep-2024)

	Ref	Expression
Assertion	isdomn5	$$⊢\forall a\in B\forall b\in B\left(a\underset{\dot{}}{·}b=\underset{\dot{}}{0}\to \left(a=\underset{\dot{}}{0}\vee b=\underset{\dot{}}{0}\right)\right)\leftrightarrow \forall a\in \left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\forall b\in B\left(a\underset{\dot{}}{·}b=\underset{\dot{}}{0}\to b=\underset{\dot{}}{0}\right)$$

Proof

Step	Hyp	Ref	Expression
1		bi2.04	$$⊢\left(\neg a=\underset{\dot{}}{0}\to \left(a\underset{\dot{}}{·}b=\underset{\dot{}}{0}\to b=\underset{\dot{}}{0}\right)\right)\leftrightarrow \left(a\underset{\dot{}}{·}b=\underset{\dot{}}{0}\to \left(\neg a=\underset{\dot{}}{0}\to b=\underset{\dot{}}{0}\right)\right)$$
2		df-ne	$$⊢a\ne \underset{\dot{}}{0}\leftrightarrow \neg a=\underset{\dot{}}{0}$$
3	2	imbi1i	$$⊢\left(a\ne \underset{\dot{}}{0}\to \left(a\underset{\dot{}}{·}b=\underset{\dot{}}{0}\to b=\underset{\dot{}}{0}\right)\right)\leftrightarrow \left(\neg a=\underset{\dot{}}{0}\to \left(a\underset{\dot{}}{·}b=\underset{\dot{}}{0}\to b=\underset{\dot{}}{0}\right)\right)$$
4		df-or	$$⊢\left(a=\underset{\dot{}}{0}\vee b=\underset{\dot{}}{0}\right)\leftrightarrow \left(\neg a=\underset{\dot{}}{0}\to b=\underset{\dot{}}{0}\right)$$
5	4	imbi2i	$$⊢\left(a\underset{\dot{}}{·}b=\underset{\dot{}}{0}\to \left(a=\underset{\dot{}}{0}\vee b=\underset{\dot{}}{0}\right)\right)\leftrightarrow \left(a\underset{\dot{}}{·}b=\underset{\dot{}}{0}\to \left(\neg a=\underset{\dot{}}{0}\to b=\underset{\dot{}}{0}\right)\right)$$
6	1 3 5	3bitr4ri	$$⊢\left(a\underset{\dot{}}{·}b=\underset{\dot{}}{0}\to \left(a=\underset{\dot{}}{0}\vee b=\underset{\dot{}}{0}\right)\right)\leftrightarrow \left(a\ne \underset{\dot{}}{0}\to \left(a\underset{\dot{}}{·}b=\underset{\dot{}}{0}\to b=\underset{\dot{}}{0}\right)\right)$$
7	6	2ralbii	$$⊢\forall a\in B\forall b\in B\left(a\underset{\dot{}}{·}b=\underset{\dot{}}{0}\to \left(a=\underset{\dot{}}{0}\vee b=\underset{\dot{}}{0}\right)\right)\leftrightarrow \forall a\in B\forall b\in B\left(a\ne \underset{\dot{}}{0}\to \left(a\underset{\dot{}}{·}b=\underset{\dot{}}{0}\to b=\underset{\dot{}}{0}\right)\right)$$
8		r19.21v	$$⊢\forall b\in B\left(a\ne \underset{\dot{}}{0}\to \left(a\underset{\dot{}}{·}b=\underset{\dot{}}{0}\to b=\underset{\dot{}}{0}\right)\right)\leftrightarrow \left(a\ne \underset{\dot{}}{0}\to \forall b\in B\left(a\underset{\dot{}}{·}b=\underset{\dot{}}{0}\to b=\underset{\dot{}}{0}\right)\right)$$
9	8	ralbii	$$⊢\forall a\in B\forall b\in B\left(a\ne \underset{\dot{}}{0}\to \left(a\underset{\dot{}}{·}b=\underset{\dot{}}{0}\to b=\underset{\dot{}}{0}\right)\right)\leftrightarrow \forall a\in B\left(a\ne \underset{\dot{}}{0}\to \forall b\in B\left(a\underset{\dot{}}{·}b=\underset{\dot{}}{0}\to b=\underset{\dot{}}{0}\right)\right)$$
10		raldifsnb	$$⊢\forall a\in B\left(a\ne \underset{\dot{}}{0}\to \forall b\in B\left(a\underset{\dot{}}{·}b=\underset{\dot{}}{0}\to b=\underset{\dot{}}{0}\right)\right)\leftrightarrow \forall a\in \left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\forall b\in B\left(a\underset{\dot{}}{·}b=\underset{\dot{}}{0}\to b=\underset{\dot{}}{0}\right)$$
11	7 9 10	3bitri	$$⊢\forall a\in B\forall b\in B\left(a\underset{\dot{}}{·}b=\underset{\dot{}}{0}\to \left(a=\underset{\dot{}}{0}\vee b=\underset{\dot{}}{0}\right)\right)\leftrightarrow \forall a\in \left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\forall b\in B\left(a\underset{\dot{}}{·}b=\underset{\dot{}}{0}\to b=\underset{\dot{}}{0}\right)$$