This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Definition df-lmic

Description: Two modules are said to be isomorphic iff they are connected by at least one isomorphism. (Contributed by Stefan O'Rear, 25-Jan-2015)

		Ref	Expression
	Assertion	df-lmic	$⊢ ≃_{𝑚} = {LMIso}^{-1} [V ∖ 1_{𝑜}]$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		clmic	$class ≃_{𝑚}$
1		clmim	$class LMIso$
2	1	ccnv	$class {LMIso}^{-1}$
3		cvv	$class V$
4		c1o	$class 1_{𝑜}$
5	3 4	cdif	$class (V ∖ 1_{𝑜})$
6	2 5	cima	$class {LMIso}^{-1} [V ∖ 1_{𝑜}]$
7	0 6	wceq	$wff ≃_{𝑚} = {LMIso}^{-1} [V ∖ 1_{𝑜}]$