isclmp

Description: The predicate "is a subcomplex module". (Contributed by NM, 31-May-2008) (Revised by AV, 4-Oct-2021)

	Ref	Expression
Hypotheses	isclmp.t	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
	isclmp.a	$⊢ \underset{˙}{+} = +_{W}$
	isclmp.v	$⊢ V = {Base}_{W}$
	isclmp.s	$⊢ S = Scalar (W)$
	isclmp.k	$⊢ K = {Base}_{S}$
Assertion	isclmp	$⊢ W \in CMod \leftrightarrow ((W \in Grp \land S = ℂ_{fld} ↾_{𝑠} K \land K \in SubRing (ℂ_{fld})) \land \forall x \in V (1 \underset{˙}{\cdot} x = x \land \forall y \in K (y \underset{˙}{\cdot} x \in V \land \forall z \in V y \underset{˙}{\cdot} (x \underset{˙}{+} z) = (y \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} z) \land \forall z \in K ((z + y) \underset{˙}{\cdot} x = (z \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} x) \land z y \underset{˙}{\cdot} x = z \underset{˙}{\cdot} (y \underset{˙}{\cdot} x)))))$

Proof

Step	Hyp	Ref	Expression
1		isclmp.t	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
2		isclmp.a	$⊢ \underset{˙}{+} = +_{W}$
3		isclmp.v	$⊢ V = {Base}_{W}$
4		isclmp.s	$⊢ S = Scalar (W)$
5		isclmp.k	$⊢ K = {Base}_{S}$
6	4 5	isclm	$⊢ W \in CMod \leftrightarrow (W \in LMod \land S = ℂ_{fld} ↾_{𝑠} K \land K \in SubRing (ℂ_{fld}))$
7		eqid	$⊢ +_{S} = +_{S}$
8		eqid	$⊢ \cdot_{S} = \cdot_{S}$
9		eqid	$⊢ 1_{S} = 1_{S}$
10	3 2 1 4 5 7 8 9	islmod	$⊢ W \in LMod \leftrightarrow (W \in Grp \land S \in Ring \land \forall r \in K \forall y \in K \forall z \in V \forall x \in V ((y \underset{˙}{\cdot} x \in V \land y \underset{˙}{\cdot} (x \underset{˙}{+} z) = (y \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} z) \land (r +_{S} y) \underset{˙}{\cdot} x = (r \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} x)) \land ((r \cdot_{S} y) \underset{˙}{\cdot} x = r \underset{˙}{\cdot} (y \underset{˙}{\cdot} x) \land 1_{S} \underset{˙}{\cdot} x = x)))$
11	10	3anbi1i	$⊢ (W \in LMod \land S = ℂ_{fld} ↾_{𝑠} K \land K \in SubRing (ℂ_{fld})) \leftrightarrow ((W \in Grp \land S \in Ring \land \forall r \in K \forall y \in K \forall z \in V \forall x \in V ((y \underset{˙}{\cdot} x \in V \land y \underset{˙}{\cdot} (x \underset{˙}{+} z) = (y \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} z) \land (r +_{S} y) \underset{˙}{\cdot} x = (r \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} x)) \land ((r \cdot_{S} y) \underset{˙}{\cdot} x = r \underset{˙}{\cdot} (y \underset{˙}{\cdot} x) \land 1_{S} \underset{˙}{\cdot} x = x))) \land S = ℂ_{fld} ↾_{𝑠} K \land K \in SubRing (ℂ_{fld}))$
12		3anass	$⊢ ((W \in Grp \land S \in Ring \land \forall r \in K \forall y \in K \forall z \in V \forall x \in V ((y \underset{˙}{\cdot} x \in V \land y \underset{˙}{\cdot} (x \underset{˙}{+} z) = (y \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} z) \land (r +_{S} y) \underset{˙}{\cdot} x = (r \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} x)) \land ((r \cdot_{S} y) \underset{˙}{\cdot} x = r \underset{˙}{\cdot} (y \underset{˙}{\cdot} x) \land 1_{S} \underset{˙}{\cdot} x = x))) \land S = ℂ_{fld} ↾_{𝑠} K \land K \in SubRing (ℂ_{fld})) \leftrightarrow ((W \in Grp \land S \in Ring \land \forall r \in K \forall y \in K \forall z \in V \forall x \in V ((y \underset{˙}{\cdot} x \in V \land y \underset{˙}{\cdot} (x \underset{˙}{+} z) = (y \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} z) \land (r +_{S} y) \underset{˙}{\cdot} x = (r \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} x)) \land ((r \cdot_{S} y) \underset{˙}{\cdot} x = r \underset{˙}{\cdot} (y \underset{˙}{\cdot} x) \land 1_{S} \underset{˙}{\cdot} x = x))) \land (S = ℂ_{fld} ↾_{𝑠} K \land K \in SubRing (ℂ_{fld})))$
13		df-3an	$⊢ (W \in Grp \land S \in Ring \land \forall r \in K \forall y \in K \forall z \in V \forall x \in V ((y \underset{˙}{\cdot} x \in V \land y \underset{˙}{\cdot} (x \underset{˙}{+} z) = (y \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} z) \land (r +_{S} y) \underset{˙}{\cdot} x = (r \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} x)) \land ((r \cdot_{S} y) \underset{˙}{\cdot} x = r \underset{˙}{\cdot} (y \underset{˙}{\cdot} x) \land 1_{S} \underset{˙}{\cdot} x = x))) \leftrightarrow ((W \in Grp \land S \in Ring) \land \forall r \in K \forall y \in K \forall z \in V \forall x \in V ((y \underset{˙}{\cdot} x \in V \land y \underset{˙}{\cdot} (x \underset{˙}{+} z) = (y \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} z) \land (r +_{S} y) \underset{˙}{\cdot} x = (r \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} x)) \land ((r \cdot_{S} y) \underset{˙}{\cdot} x = r \underset{˙}{\cdot} (y \underset{˙}{\cdot} x) \land 1_{S} \underset{˙}{\cdot} x = x)))$
14	13	anbi1i	$⊢ ((W \in Grp \land S \in Ring \land \forall r \in K \forall y \in K \forall z \in V \forall x \in V ((y \underset{˙}{\cdot} x \in V \land y \underset{˙}{\cdot} (x \underset{˙}{+} z) = (y \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} z) \land (r +_{S} y) \underset{˙}{\cdot} x = (r \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} x)) \land ((r \cdot_{S} y) \underset{˙}{\cdot} x = r \underset{˙}{\cdot} (y \underset{˙}{\cdot} x) \land 1_{S} \underset{˙}{\cdot} x = x))) \land (S = ℂ_{fld} ↾_{𝑠} K \land K \in SubRing (ℂ_{fld}))) \leftrightarrow (((W \in Grp \land S \in Ring) \land \forall r \in K \forall y \in K \forall z \in V \forall x \in V ((y \underset{˙}{\cdot} x \in V \land y \underset{˙}{\cdot} (x \underset{˙}{+} z) = (y \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} z) \land (r +_{S} y) \underset{˙}{\cdot} x = (r \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} x)) \land ((r \cdot_{S} y) \underset{˙}{\cdot} x = r \underset{˙}{\cdot} (y \underset{˙}{\cdot} x) \land 1_{S} \underset{˙}{\cdot} x = x))) \land (S = ℂ_{fld} ↾_{𝑠} K \land K \in SubRing (ℂ_{fld})))$
15	12 14	bitri	$⊢ ((W \in Grp \land S \in Ring \land \forall r \in K \forall y \in K \forall z \in V \forall x \in V ((y \underset{˙}{\cdot} x \in V \land y \underset{˙}{\cdot} (x \underset{˙}{+} z) = (y \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} z) \land (r +_{S} y) \underset{˙}{\cdot} x = (r \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} x)) \land ((r \cdot_{S} y) \underset{˙}{\cdot} x = r \underset{˙}{\cdot} (y \underset{˙}{\cdot} x) \land 1_{S} \underset{˙}{\cdot} x = x))) \land S = ℂ_{fld} ↾_{𝑠} K \land K \in SubRing (ℂ_{fld})) \leftrightarrow (((W \in Grp \land S \in Ring) \land \forall r \in K \forall y \in K \forall z \in V \forall x \in V ((y \underset{˙}{\cdot} x \in V \land y \underset{˙}{\cdot} (x \underset{˙}{+} z) = (y \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} z) \land (r +_{S} y) \underset{˙}{\cdot} x = (r \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} x)) \land ((r \cdot_{S} y) \underset{˙}{\cdot} x = r \underset{˙}{\cdot} (y \underset{˙}{\cdot} x) \land 1_{S} \underset{˙}{\cdot} x = x))) \land (S = ℂ_{fld} ↾_{𝑠} K \land K \in SubRing (ℂ_{fld})))$
16		an32	$⊢ (((W \in Grp \land S \in Ring) \land \forall r \in K \forall y \in K \forall z \in V \forall x \in V ((y \underset{˙}{\cdot} x \in V \land y \underset{˙}{\cdot} (x \underset{˙}{+} z) = (y \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} z) \land (r +_{S} y) \underset{˙}{\cdot} x = (r \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} x)) \land ((r \cdot_{S} y) \underset{˙}{\cdot} x = r \underset{˙}{\cdot} (y \underset{˙}{\cdot} x) \land 1_{S} \underset{˙}{\cdot} x = x))) \land (S = ℂ_{fld} ↾_{𝑠} K \land K \in SubRing (ℂ_{fld}))) \leftrightarrow (((W \in Grp \land S \in Ring) \land (S = ℂ_{fld} ↾_{𝑠} K \land K \in SubRing (ℂ_{fld}))) \land \forall r \in K \forall y \in K \forall z \in V \forall x \in V ((y \underset{˙}{\cdot} x \in V \land y \underset{˙}{\cdot} (x \underset{˙}{+} z) = (y \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} z) \land (r +_{S} y) \underset{˙}{\cdot} x = (r \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} x)) \land ((r \cdot_{S} y) \underset{˙}{\cdot} x = r \underset{˙}{\cdot} (y \underset{˙}{\cdot} x) \land 1_{S} \underset{˙}{\cdot} x = x)))$
17	11 15 16	3bitri	$⊢ (W \in LMod \land S = ℂ_{fld} ↾_{𝑠} K \land K \in SubRing (ℂ_{fld})) \leftrightarrow (((W \in Grp \land S \in Ring) \land (S = ℂ_{fld} ↾_{𝑠} K \land K \in SubRing (ℂ_{fld}))) \land \forall r \in K \forall y \in K \forall z \in V \forall x \in V ((y \underset{˙}{\cdot} x \in V \land y \underset{˙}{\cdot} (x \underset{˙}{+} z) = (y \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} z) \land (r +_{S} y) \underset{˙}{\cdot} x = (r \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} x)) \land ((r \cdot_{S} y) \underset{˙}{\cdot} x = r \underset{˙}{\cdot} (y \underset{˙}{\cdot} x) \land 1_{S} \underset{˙}{\cdot} x = x)))$
18		an32	$⊢ ((W \in Grp \land S \in Ring) \land (S = ℂ_{fld} ↾_{𝑠} K \land K \in SubRing (ℂ_{fld}))) \leftrightarrow ((W \in Grp \land (S = ℂ_{fld} ↾_{𝑠} K \land K \in SubRing (ℂ_{fld}))) \land S \in Ring)$
19		3anass	$⊢ (W \in Grp \land S = ℂ_{fld} ↾_{𝑠} K \land K \in SubRing (ℂ_{fld})) \leftrightarrow (W \in Grp \land (S = ℂ_{fld} ↾_{𝑠} K \land K \in SubRing (ℂ_{fld})))$
20	19	bicomi	$⊢ (W \in Grp \land (S = ℂ_{fld} ↾_{𝑠} K \land K \in SubRing (ℂ_{fld}))) \leftrightarrow (W \in Grp \land S = ℂ_{fld} ↾_{𝑠} K \land K \in SubRing (ℂ_{fld}))$
21	20	anbi1i	$⊢ ((W \in Grp \land (S = ℂ_{fld} ↾_{𝑠} K \land K \in SubRing (ℂ_{fld}))) \land S \in Ring) \leftrightarrow ((W \in Grp \land S = ℂ_{fld} ↾_{𝑠} K \land K \in SubRing (ℂ_{fld})) \land S \in Ring)$
22	18 21	bitri	$⊢ ((W \in Grp \land S \in Ring) \land (S = ℂ_{fld} ↾_{𝑠} K \land K \in SubRing (ℂ_{fld}))) \leftrightarrow ((W \in Grp \land S = ℂ_{fld} ↾_{𝑠} K \land K \in SubRing (ℂ_{fld})) \land S \in Ring)$
23	22	anbi1i	$⊢ (((W \in Grp \land S \in Ring) \land (S = ℂ_{fld} ↾_{𝑠} K \land K \in SubRing (ℂ_{fld}))) \land \forall r \in K \forall y \in K \forall z \in V \forall x \in V ((y \underset{˙}{\cdot} x \in V \land y \underset{˙}{\cdot} (x \underset{˙}{+} z) = (y \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} z) \land (r +_{S} y) \underset{˙}{\cdot} x = (r \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} x)) \land ((r \cdot_{S} y) \underset{˙}{\cdot} x = r \underset{˙}{\cdot} (y \underset{˙}{\cdot} x) \land 1_{S} \underset{˙}{\cdot} x = x))) \leftrightarrow (((W \in Grp \land S = ℂ_{fld} ↾_{𝑠} K \land K \in SubRing (ℂ_{fld})) \land S \in Ring) \land \forall r \in K \forall y \in K \forall z \in V \forall x \in V ((y \underset{˙}{\cdot} x \in V \land y \underset{˙}{\cdot} (x \underset{˙}{+} z) = (y \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} z) \land (r +_{S} y) \underset{˙}{\cdot} x = (r \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} x)) \land ((r \cdot_{S} y) \underset{˙}{\cdot} x = r \underset{˙}{\cdot} (y \underset{˙}{\cdot} x) \land 1_{S} \underset{˙}{\cdot} x = x)))$
24		anass	$⊢ (((W \in Grp \land S = ℂ_{fld} ↾_{𝑠} K \land K \in SubRing (ℂ_{fld})) \land S \in Ring) \land \forall r \in K \forall y \in K \forall z \in V \forall x \in V ((y \underset{˙}{\cdot} x \in V \land y \underset{˙}{\cdot} (x \underset{˙}{+} z) = (y \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} z) \land (r +_{S} y) \underset{˙}{\cdot} x = (r \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} x)) \land ((r \cdot_{S} y) \underset{˙}{\cdot} x = r \underset{˙}{\cdot} (y \underset{˙}{\cdot} x) \land 1_{S} \underset{˙}{\cdot} x = x))) \leftrightarrow ((W \in Grp \land S = ℂ_{fld} ↾_{𝑠} K \land K \in SubRing (ℂ_{fld})) \land (S \in Ring \land \forall r \in K \forall y \in K \forall z \in V \forall x \in V ((y \underset{˙}{\cdot} x \in V \land y \underset{˙}{\cdot} (x \underset{˙}{+} z) = (y \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} z) \land (r +_{S} y) \underset{˙}{\cdot} x = (r \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} x)) \land ((r \cdot_{S} y) \underset{˙}{\cdot} x = r \underset{˙}{\cdot} (y \underset{˙}{\cdot} x) \land 1_{S} \underset{˙}{\cdot} x = x))))$
25		df-3an	$⊢ (y \underset{˙}{\cdot} x \in V \land y \underset{˙}{\cdot} (x \underset{˙}{+} z) = (y \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} z) \land (r +_{S} y) \underset{˙}{\cdot} x = (r \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} x)) \leftrightarrow ((y \underset{˙}{\cdot} x \in V \land y \underset{˙}{\cdot} (x \underset{˙}{+} z) = (y \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} z)) \land (r +_{S} y) \underset{˙}{\cdot} x = (r \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} x))$
26		ancom	$⊢ ((r \cdot_{S} y) \underset{˙}{\cdot} x = r \underset{˙}{\cdot} (y \underset{˙}{\cdot} x) \land 1_{S} \underset{˙}{\cdot} x = x) \leftrightarrow (1_{S} \underset{˙}{\cdot} x = x \land (r \cdot_{S} y) \underset{˙}{\cdot} x = r \underset{˙}{\cdot} (y \underset{˙}{\cdot} x))$
27	25 26	anbi12i	$⊢ ((y \underset{˙}{\cdot} x \in V \land y \underset{˙}{\cdot} (x \underset{˙}{+} z) = (y \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} z) \land (r +_{S} y) \underset{˙}{\cdot} x = (r \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} x)) \land ((r \cdot_{S} y) \underset{˙}{\cdot} x = r \underset{˙}{\cdot} (y \underset{˙}{\cdot} x) \land 1_{S} \underset{˙}{\cdot} x = x)) \leftrightarrow (((y \underset{˙}{\cdot} x \in V \land y \underset{˙}{\cdot} (x \underset{˙}{+} z) = (y \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} z)) \land (r +_{S} y) \underset{˙}{\cdot} x = (r \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} x)) \land (1_{S} \underset{˙}{\cdot} x = x \land (r \cdot_{S} y) \underset{˙}{\cdot} x = r \underset{˙}{\cdot} (y \underset{˙}{\cdot} x)))$
28		an4	$⊢ (((y \underset{˙}{\cdot} x \in V \land y \underset{˙}{\cdot} (x \underset{˙}{+} z) = (y \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} z)) \land (r +_{S} y) \underset{˙}{\cdot} x = (r \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} x)) \land (1_{S} \underset{˙}{\cdot} x = x \land (r \cdot_{S} y) \underset{˙}{\cdot} x = r \underset{˙}{\cdot} (y \underset{˙}{\cdot} x))) \leftrightarrow (((y \underset{˙}{\cdot} x \in V \land y \underset{˙}{\cdot} (x \underset{˙}{+} z) = (y \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} z)) \land 1_{S} \underset{˙}{\cdot} x = x) \land ((r +_{S} y) \underset{˙}{\cdot} x = (r \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} x) \land (r \cdot_{S} y) \underset{˙}{\cdot} x = r \underset{˙}{\cdot} (y \underset{˙}{\cdot} x)))$
29		an32	$⊢ ((y \underset{˙}{\cdot} x \in V \land y \underset{˙}{\cdot} (x \underset{˙}{+} z) = (y \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} z)) \land 1_{S} \underset{˙}{\cdot} x = x) \leftrightarrow ((y \underset{˙}{\cdot} x \in V \land 1_{S} \underset{˙}{\cdot} x = x) \land y \underset{˙}{\cdot} (x \underset{˙}{+} z) = (y \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} z))$
30		ancom	$⊢ (y \underset{˙}{\cdot} x \in V \land 1_{S} \underset{˙}{\cdot} x = x) \leftrightarrow (1_{S} \underset{˙}{\cdot} x = x \land y \underset{˙}{\cdot} x \in V)$
31	30	anbi1i	$⊢ ((y \underset{˙}{\cdot} x \in V \land 1_{S} \underset{˙}{\cdot} x = x) \land y \underset{˙}{\cdot} (x \underset{˙}{+} z) = (y \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} z)) \leftrightarrow ((1_{S} \underset{˙}{\cdot} x = x \land y \underset{˙}{\cdot} x \in V) \land y \underset{˙}{\cdot} (x \underset{˙}{+} z) = (y \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} z))$
32	29 31	bitri	$⊢ ((y \underset{˙}{\cdot} x \in V \land y \underset{˙}{\cdot} (x \underset{˙}{+} z) = (y \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} z)) \land 1_{S} \underset{˙}{\cdot} x = x) \leftrightarrow ((1_{S} \underset{˙}{\cdot} x = x \land y \underset{˙}{\cdot} x \in V) \land y \underset{˙}{\cdot} (x \underset{˙}{+} z) = (y \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} z))$
33	32	anbi1i	$⊢ (((y \underset{˙}{\cdot} x \in V \land y \underset{˙}{\cdot} (x \underset{˙}{+} z) = (y \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} z)) \land 1_{S} \underset{˙}{\cdot} x = x) \land ((r +_{S} y) \underset{˙}{\cdot} x = (r \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} x) \land (r \cdot_{S} y) \underset{˙}{\cdot} x = r \underset{˙}{\cdot} (y \underset{˙}{\cdot} x))) \leftrightarrow (((1_{S} \underset{˙}{\cdot} x = x \land y \underset{˙}{\cdot} x \in V) \land y \underset{˙}{\cdot} (x \underset{˙}{+} z) = (y \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} z)) \land ((r +_{S} y) \underset{˙}{\cdot} x = (r \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} x) \land (r \cdot_{S} y) \underset{˙}{\cdot} x = r \underset{˙}{\cdot} (y \underset{˙}{\cdot} x)))$
34	27 28 33	3bitri	$⊢ ((y \underset{˙}{\cdot} x \in V \land y \underset{˙}{\cdot} (x \underset{˙}{+} z) = (y \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} z) \land (r +_{S} y) \underset{˙}{\cdot} x = (r \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} x)) \land ((r \cdot_{S} y) \underset{˙}{\cdot} x = r \underset{˙}{\cdot} (y \underset{˙}{\cdot} x) \land 1_{S} \underset{˙}{\cdot} x = x)) \leftrightarrow (((1_{S} \underset{˙}{\cdot} x = x \land y \underset{˙}{\cdot} x \in V) \land y \underset{˙}{\cdot} (x \underset{˙}{+} z) = (y \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} z)) \land ((r +_{S} y) \underset{˙}{\cdot} x = (r \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} x) \land (r \cdot_{S} y) \underset{˙}{\cdot} x = r \underset{˙}{\cdot} (y \underset{˙}{\cdot} x)))$
35		fveq2	$⊢ S = ℂ_{fld} ↾_{𝑠} K \to 1_{S} = 1_{(ℂ_{fld} ↾_{𝑠} K)}$
36		eqid	$⊢ ℂ_{fld} ↾_{𝑠} K = ℂ_{fld} ↾_{𝑠} K$
37		eqid	$⊢ 1_{ℂ_{fld}} = 1_{ℂ_{fld}}$
38	36 37	subrg1	$⊢ K \in SubRing (ℂ_{fld}) \to 1_{ℂ_{fld}} = 1_{(ℂ_{fld} ↾_{𝑠} K)}$
39	38	eqcomd	$⊢ K \in SubRing (ℂ_{fld}) \to 1_{(ℂ_{fld} ↾_{𝑠} K)} = 1_{ℂ_{fld}}$
40	35 39	sylan9eq	$⊢ (S = ℂ_{fld} ↾_{𝑠} K \land K \in SubRing (ℂ_{fld})) \to 1_{S} = 1_{ℂ_{fld}}$
41		cnfld1	$⊢ 1 = 1_{ℂ_{fld}}$
42	40 41	eqtr4di	$⊢ (S = ℂ_{fld} ↾_{𝑠} K \land K \in SubRing (ℂ_{fld})) \to 1_{S} = 1$
43	42	oveq1d	$⊢ (S = ℂ_{fld} ↾_{𝑠} K \land K \in SubRing (ℂ_{fld})) \to 1_{S} \underset{˙}{\cdot} x = 1 \underset{˙}{\cdot} x$
44	43	eqeq1d	$⊢ (S = ℂ_{fld} ↾_{𝑠} K \land K \in SubRing (ℂ_{fld})) \to (1_{S} \underset{˙}{\cdot} x = x \leftrightarrow 1 \underset{˙}{\cdot} x = x)$
45	44	3adant1	$⊢ (W \in Grp \land S = ℂ_{fld} ↾_{𝑠} K \land K \in SubRing (ℂ_{fld})) \to (1_{S} \underset{˙}{\cdot} x = x \leftrightarrow 1 \underset{˙}{\cdot} x = x)$
46	45	ad2antrr	$⊢ (((W \in Grp \land S = ℂ_{fld} ↾_{𝑠} K \land K \in SubRing (ℂ_{fld})) \land (r \in K \land y \in K)) \land (z \in V \land x \in V)) \to (1_{S} \underset{˙}{\cdot} x = x \leftrightarrow 1 \underset{˙}{\cdot} x = x)$
47	46	anbi1d	$⊢ (((W \in Grp \land S = ℂ_{fld} ↾_{𝑠} K \land K \in SubRing (ℂ_{fld})) \land (r \in K \land y \in K)) \land (z \in V \land x \in V)) \to ((1_{S} \underset{˙}{\cdot} x = x \land y \underset{˙}{\cdot} x \in V) \leftrightarrow (1 \underset{˙}{\cdot} x = x \land y \underset{˙}{\cdot} x \in V))$
48	47	anbi1d	$⊢ (((W \in Grp \land S = ℂ_{fld} ↾_{𝑠} K \land K \in SubRing (ℂ_{fld})) \land (r \in K \land y \in K)) \land (z \in V \land x \in V)) \to (((1_{S} \underset{˙}{\cdot} x = x \land y \underset{˙}{\cdot} x \in V) \land y \underset{˙}{\cdot} (x \underset{˙}{+} z) = (y \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} z)) \leftrightarrow ((1 \underset{˙}{\cdot} x = x \land y \underset{˙}{\cdot} x \in V) \land y \underset{˙}{\cdot} (x \underset{˙}{+} z) = (y \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} z)))$
49		eqid	$⊢ +_{ℂ_{fld}} = +_{ℂ_{fld}}$
50	36 49	ressplusg	$⊢ K \in SubRing (ℂ_{fld}) \to +_{ℂ_{fld}} = +_{(ℂ_{fld} ↾_{𝑠} K)}$
51	50	adantl	$⊢ (S = ℂ_{fld} ↾_{𝑠} K \land K \in SubRing (ℂ_{fld})) \to +_{ℂ_{fld}} = +_{(ℂ_{fld} ↾_{𝑠} K)}$
52		cnfldadd	$⊢ + = +_{ℂ_{fld}}$
53	52	a1i	$⊢ (S = ℂ_{fld} ↾_{𝑠} K \land K \in SubRing (ℂ_{fld})) \to + = +_{ℂ_{fld}}$
54		fveq2	$⊢ S = ℂ_{fld} ↾_{𝑠} K \to +_{S} = +_{(ℂ_{fld} ↾_{𝑠} K)}$
55	54	adantr	$⊢ (S = ℂ_{fld} ↾_{𝑠} K \land K \in SubRing (ℂ_{fld})) \to +_{S} = +_{(ℂ_{fld} ↾_{𝑠} K)}$
56	51 53 55	3eqtr4rd	$⊢ (S = ℂ_{fld} ↾_{𝑠} K \land K \in SubRing (ℂ_{fld})) \to +_{S} = +$
57	56	3adant1	$⊢ (W \in Grp \land S = ℂ_{fld} ↾_{𝑠} K \land K \in SubRing (ℂ_{fld})) \to +_{S} = +$
58	57	oveqd	$⊢ (W \in Grp \land S = ℂ_{fld} ↾_{𝑠} K \land K \in SubRing (ℂ_{fld})) \to r +_{S} y = r + y$
59	58	ad2antrr	$⊢ (((W \in Grp \land S = ℂ_{fld} ↾_{𝑠} K \land K \in SubRing (ℂ_{fld})) \land (r \in K \land y \in K)) \land (z \in V \land x \in V)) \to r +_{S} y = r + y$
60	59	oveq1d	$⊢ (((W \in Grp \land S = ℂ_{fld} ↾_{𝑠} K \land K \in SubRing (ℂ_{fld})) \land (r \in K \land y \in K)) \land (z \in V \land x \in V)) \to (r +_{S} y) \underset{˙}{\cdot} x = (r + y) \underset{˙}{\cdot} x$
61	60	eqeq1d	$⊢ (((W \in Grp \land S = ℂ_{fld} ↾_{𝑠} K \land K \in SubRing (ℂ_{fld})) \land (r \in K \land y \in K)) \land (z \in V \land x \in V)) \to ((r +_{S} y) \underset{˙}{\cdot} x = (r \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} x) \leftrightarrow (r + y) \underset{˙}{\cdot} x = (r \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} x))$
62		eqid	$⊢ \cdot_{ℂ_{fld}} = \cdot_{ℂ_{fld}}$
63	36 62	ressmulr	$⊢ K \in SubRing (ℂ_{fld}) \to \cdot_{ℂ_{fld}} = \cdot_{(ℂ_{fld} ↾_{𝑠} K)}$
64	63	3ad2ant3	$⊢ (W \in Grp \land S = ℂ_{fld} ↾_{𝑠} K \land K \in SubRing (ℂ_{fld})) \to \cdot_{ℂ_{fld}} = \cdot_{(ℂ_{fld} ↾_{𝑠} K)}$
65		cnfldmul	$⊢ \times = \cdot_{ℂ_{fld}}$
66	65	a1i	$⊢ (W \in Grp \land S = ℂ_{fld} ↾_{𝑠} K \land K \in SubRing (ℂ_{fld})) \to \times = \cdot_{ℂ_{fld}}$
67		fveq2	$⊢ S = ℂ_{fld} ↾_{𝑠} K \to \cdot_{S} = \cdot_{(ℂ_{fld} ↾_{𝑠} K)}$
68	67	3ad2ant2	$⊢ (W \in Grp \land S = ℂ_{fld} ↾_{𝑠} K \land K \in SubRing (ℂ_{fld})) \to \cdot_{S} = \cdot_{(ℂ_{fld} ↾_{𝑠} K)}$
69	64 66 68	3eqtr4rd	$⊢ (W \in Grp \land S = ℂ_{fld} ↾_{𝑠} K \land K \in SubRing (ℂ_{fld})) \to \cdot_{S} = \times$
70	69	oveqd	$⊢ (W \in Grp \land S = ℂ_{fld} ↾_{𝑠} K \land K \in SubRing (ℂ_{fld})) \to r \cdot_{S} y = r y$
71	70	ad2antrr	$⊢ (((W \in Grp \land S = ℂ_{fld} ↾_{𝑠} K \land K \in SubRing (ℂ_{fld})) \land (r \in K \land y \in K)) \land (z \in V \land x \in V)) \to r \cdot_{S} y = r y$
72	71	oveq1d	$⊢ (((W \in Grp \land S = ℂ_{fld} ↾_{𝑠} K \land K \in SubRing (ℂ_{fld})) \land (r \in K \land y \in K)) \land (z \in V \land x \in V)) \to (r \cdot_{S} y) \underset{˙}{\cdot} x = r y \underset{˙}{\cdot} x$
73	72	eqeq1d	$⊢ (((W \in Grp \land S = ℂ_{fld} ↾_{𝑠} K \land K \in SubRing (ℂ_{fld})) \land (r \in K \land y \in K)) \land (z \in V \land x \in V)) \to ((r \cdot_{S} y) \underset{˙}{\cdot} x = r \underset{˙}{\cdot} (y \underset{˙}{\cdot} x) \leftrightarrow r y \underset{˙}{\cdot} x = r \underset{˙}{\cdot} (y \underset{˙}{\cdot} x))$
74	61 73	anbi12d	$⊢ (((W \in Grp \land S = ℂ_{fld} ↾_{𝑠} K \land K \in SubRing (ℂ_{fld})) \land (r \in K \land y \in K)) \land (z \in V \land x \in V)) \to (((r +_{S} y) \underset{˙}{\cdot} x = (r \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} x) \land (r \cdot_{S} y) \underset{˙}{\cdot} x = r \underset{˙}{\cdot} (y \underset{˙}{\cdot} x)) \leftrightarrow ((r + y) \underset{˙}{\cdot} x = (r \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} x) \land r y \underset{˙}{\cdot} x = r \underset{˙}{\cdot} (y \underset{˙}{\cdot} x)))$
75	48 74	anbi12d	$⊢ (((W \in Grp \land S = ℂ_{fld} ↾_{𝑠} K \land K \in SubRing (ℂ_{fld})) \land (r \in K \land y \in K)) \land (z \in V \land x \in V)) \to ((((1_{S} \underset{˙}{\cdot} x = x \land y \underset{˙}{\cdot} x \in V) \land y \underset{˙}{\cdot} (x \underset{˙}{+} z) = (y \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} z)) \land ((r +_{S} y) \underset{˙}{\cdot} x = (r \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} x) \land (r \cdot_{S} y) \underset{˙}{\cdot} x = r \underset{˙}{\cdot} (y \underset{˙}{\cdot} x))) \leftrightarrow (((1 \underset{˙}{\cdot} x = x \land y \underset{˙}{\cdot} x \in V) \land y \underset{˙}{\cdot} (x \underset{˙}{+} z) = (y \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} z)) \land ((r + y) \underset{˙}{\cdot} x = (r \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} x) \land r y \underset{˙}{\cdot} x = r \underset{˙}{\cdot} (y \underset{˙}{\cdot} x))))$
76	34 75	bitrid	$⊢ (((W \in Grp \land S = ℂ_{fld} ↾_{𝑠} K \land K \in SubRing (ℂ_{fld})) \land (r \in K \land y \in K)) \land (z \in V \land x \in V)) \to (((y \underset{˙}{\cdot} x \in V \land y \underset{˙}{\cdot} (x \underset{˙}{+} z) = (y \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} z) \land (r +_{S} y) \underset{˙}{\cdot} x = (r \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} x)) \land ((r \cdot_{S} y) \underset{˙}{\cdot} x = r \underset{˙}{\cdot} (y \underset{˙}{\cdot} x) \land 1_{S} \underset{˙}{\cdot} x = x)) \leftrightarrow (((1 \underset{˙}{\cdot} x = x \land y \underset{˙}{\cdot} x \in V) \land y \underset{˙}{\cdot} (x \underset{˙}{+} z) = (y \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} z)) \land ((r + y) \underset{˙}{\cdot} x = (r \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} x) \land r y \underset{˙}{\cdot} x = r \underset{˙}{\cdot} (y \underset{˙}{\cdot} x))))$
77	76	2ralbidva	$⊢ ((W \in Grp \land S = ℂ_{fld} ↾_{𝑠} K \land K \in SubRing (ℂ_{fld})) \land (r \in K \land y \in K)) \to (\forall z \in V \forall x \in V ((y \underset{˙}{\cdot} x \in V \land y \underset{˙}{\cdot} (x \underset{˙}{+} z) = (y \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} z) \land (r +_{S} y) \underset{˙}{\cdot} x = (r \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} x)) \land ((r \cdot_{S} y) \underset{˙}{\cdot} x = r \underset{˙}{\cdot} (y \underset{˙}{\cdot} x) \land 1_{S} \underset{˙}{\cdot} x = x)) \leftrightarrow \forall z \in V \forall x \in V (((1 \underset{˙}{\cdot} x = x \land y \underset{˙}{\cdot} x \in V) \land y \underset{˙}{\cdot} (x \underset{˙}{+} z) = (y \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} z)) \land ((r + y) \underset{˙}{\cdot} x = (r \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} x) \land r y \underset{˙}{\cdot} x = r \underset{˙}{\cdot} (y \underset{˙}{\cdot} x))))$
78	77	2ralbidva	$⊢ (W \in Grp \land S = ℂ_{fld} ↾_{𝑠} K \land K \in SubRing (ℂ_{fld})) \to (\forall r \in K \forall y \in K \forall z \in V \forall x \in V ((y \underset{˙}{\cdot} x \in V \land y \underset{˙}{\cdot} (x \underset{˙}{+} z) = (y \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} z) \land (r +_{S} y) \underset{˙}{\cdot} x = (r \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} x)) \land ((r \cdot_{S} y) \underset{˙}{\cdot} x = r \underset{˙}{\cdot} (y \underset{˙}{\cdot} x) \land 1_{S} \underset{˙}{\cdot} x = x)) \leftrightarrow \forall r \in K \forall y \in K \forall z \in V \forall x \in V (((1 \underset{˙}{\cdot} x = x \land y \underset{˙}{\cdot} x \in V) \land y \underset{˙}{\cdot} (x \underset{˙}{+} z) = (y \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} z)) \land ((r + y) \underset{˙}{\cdot} x = (r \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} x) \land r y \underset{˙}{\cdot} x = r \underset{˙}{\cdot} (y \underset{˙}{\cdot} x))))$
79		ralrot3	$⊢ \forall y \in K \forall z \in V \forall x \in V (((1 \underset{˙}{\cdot} x = x \land y \underset{˙}{\cdot} x \in V) \land y \underset{˙}{\cdot} (x \underset{˙}{+} z) = (y \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} z)) \land ((r + y) \underset{˙}{\cdot} x = (r \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} x) \land r y \underset{˙}{\cdot} x = r \underset{˙}{\cdot} (y \underset{˙}{\cdot} x))) \leftrightarrow \forall x \in V \forall y \in K \forall z \in V (((1 \underset{˙}{\cdot} x = x \land y \underset{˙}{\cdot} x \in V) \land y \underset{˙}{\cdot} (x \underset{˙}{+} z) = (y \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} z)) \land ((r + y) \underset{˙}{\cdot} x = (r \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} x) \land r y \underset{˙}{\cdot} x = r \underset{˙}{\cdot} (y \underset{˙}{\cdot} x)))$
80	79	ralbii	$⊢ \forall r \in K \forall y \in K \forall z \in V \forall x \in V (((1 \underset{˙}{\cdot} x = x \land y \underset{˙}{\cdot} x \in V) \land y \underset{˙}{\cdot} (x \underset{˙}{+} z) = (y \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} z)) \land ((r + y) \underset{˙}{\cdot} x = (r \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} x) \land r y \underset{˙}{\cdot} x = r \underset{˙}{\cdot} (y \underset{˙}{\cdot} x))) \leftrightarrow \forall r \in K \forall x \in V \forall y \in K \forall z \in V (((1 \underset{˙}{\cdot} x = x \land y \underset{˙}{\cdot} x \in V) \land y \underset{˙}{\cdot} (x \underset{˙}{+} z) = (y \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} z)) \land ((r + y) \underset{˙}{\cdot} x = (r \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} x) \land r y \underset{˙}{\cdot} x = r \underset{˙}{\cdot} (y \underset{˙}{\cdot} x)))$
81		ralcom	$⊢ \forall r \in K \forall x \in V \forall y \in K \forall z \in V (((1 \underset{˙}{\cdot} x = x \land y \underset{˙}{\cdot} x \in V) \land y \underset{˙}{\cdot} (x \underset{˙}{+} z) = (y \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} z)) \land ((r + y) \underset{˙}{\cdot} x = (r \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} x) \land r y \underset{˙}{\cdot} x = r \underset{˙}{\cdot} (y \underset{˙}{\cdot} x))) \leftrightarrow \forall x \in V \forall r \in K \forall y \in K \forall z \in V (((1 \underset{˙}{\cdot} x = x \land y \underset{˙}{\cdot} x \in V) \land y \underset{˙}{\cdot} (x \underset{˙}{+} z) = (y \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} z)) \land ((r + y) \underset{˙}{\cdot} x = (r \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} x) \land r y \underset{˙}{\cdot} x = r \underset{˙}{\cdot} (y \underset{˙}{\cdot} x)))$
82	80 81	bitri	$⊢ \forall r \in K \forall y \in K \forall z \in V \forall x \in V (((1 \underset{˙}{\cdot} x = x \land y \underset{˙}{\cdot} x \in V) \land y \underset{˙}{\cdot} (x \underset{˙}{+} z) = (y \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} z)) \land ((r + y) \underset{˙}{\cdot} x = (r \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} x) \land r y \underset{˙}{\cdot} x = r \underset{˙}{\cdot} (y \underset{˙}{\cdot} x))) \leftrightarrow \forall x \in V \forall r \in K \forall y \in K \forall z \in V (((1 \underset{˙}{\cdot} x = x \land y \underset{˙}{\cdot} x \in V) \land y \underset{˙}{\cdot} (x \underset{˙}{+} z) = (y \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} z)) \land ((r + y) \underset{˙}{\cdot} x = (r \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} x) \land r y \underset{˙}{\cdot} x = r \underset{˙}{\cdot} (y \underset{˙}{\cdot} x)))$
83		ralcom	$⊢ \forall r \in K \forall y \in K \forall z \in V (((1 \underset{˙}{\cdot} x = x \land y \underset{˙}{\cdot} x \in V) \land y \underset{˙}{\cdot} (x \underset{˙}{+} z) = (y \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} z)) \land ((r + y) \underset{˙}{\cdot} x = (r \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} x) \land r y \underset{˙}{\cdot} x = r \underset{˙}{\cdot} (y \underset{˙}{\cdot} x))) \leftrightarrow \forall y \in K \forall r \in K \forall z \in V (((1 \underset{˙}{\cdot} x = x \land y \underset{˙}{\cdot} x \in V) \land y \underset{˙}{\cdot} (x \underset{˙}{+} z) = (y \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} z)) \land ((r + y) \underset{˙}{\cdot} x = (r \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} x) \land r y \underset{˙}{\cdot} x = r \underset{˙}{\cdot} (y \underset{˙}{\cdot} x)))$
84	83	ralbii	$⊢ \forall x \in V \forall r \in K \forall y \in K \forall z \in V (((1 \underset{˙}{\cdot} x = x \land y \underset{˙}{\cdot} x \in V) \land y \underset{˙}{\cdot} (x \underset{˙}{+} z) = (y \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} z)) \land ((r + y) \underset{˙}{\cdot} x = (r \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} x) \land r y \underset{˙}{\cdot} x = r \underset{˙}{\cdot} (y \underset{˙}{\cdot} x))) \leftrightarrow \forall x \in V \forall y \in K \forall r \in K \forall z \in V (((1 \underset{˙}{\cdot} x = x \land y \underset{˙}{\cdot} x \in V) \land y \underset{˙}{\cdot} (x \underset{˙}{+} z) = (y \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} z)) \land ((r + y) \underset{˙}{\cdot} x = (r \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} x) \land r y \underset{˙}{\cdot} x = r \underset{˙}{\cdot} (y \underset{˙}{\cdot} x)))$
85		ralcom	$⊢ \forall r \in K \forall z \in V (((1 \underset{˙}{\cdot} x = x \land y \underset{˙}{\cdot} x \in V) \land y \underset{˙}{\cdot} (x \underset{˙}{+} z) = (y \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} z)) \land ((r + y) \underset{˙}{\cdot} x = (r \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} x) \land r y \underset{˙}{\cdot} x = r \underset{˙}{\cdot} (y \underset{˙}{\cdot} x))) \leftrightarrow \forall z \in V \forall r \in K (((1 \underset{˙}{\cdot} x = x \land y \underset{˙}{\cdot} x \in V) \land y \underset{˙}{\cdot} (x \underset{˙}{+} z) = (y \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} z)) \land ((r + y) \underset{˙}{\cdot} x = (r \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} x) \land r y \underset{˙}{\cdot} x = r \underset{˙}{\cdot} (y \underset{˙}{\cdot} x)))$
86	85	2ralbii	$⊢ \forall x \in V \forall y \in K \forall r \in K \forall z \in V (((1 \underset{˙}{\cdot} x = x \land y \underset{˙}{\cdot} x \in V) \land y \underset{˙}{\cdot} (x \underset{˙}{+} z) = (y \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} z)) \land ((r + y) \underset{˙}{\cdot} x = (r \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} x) \land r y \underset{˙}{\cdot} x = r \underset{˙}{\cdot} (y \underset{˙}{\cdot} x))) \leftrightarrow \forall x \in V \forall y \in K \forall z \in V \forall r \in K (((1 \underset{˙}{\cdot} x = x \land y \underset{˙}{\cdot} x \in V) \land y \underset{˙}{\cdot} (x \underset{˙}{+} z) = (y \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} z)) \land ((r + y) \underset{˙}{\cdot} x = (r \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} x) \land r y \underset{˙}{\cdot} x = r \underset{˙}{\cdot} (y \underset{˙}{\cdot} x)))$
87	82 84 86	3bitri	$⊢ \forall r \in K \forall y \in K \forall z \in V \forall x \in V (((1 \underset{˙}{\cdot} x = x \land y \underset{˙}{\cdot} x \in V) \land y \underset{˙}{\cdot} (x \underset{˙}{+} z) = (y \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} z)) \land ((r + y) \underset{˙}{\cdot} x = (r \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} x) \land r y \underset{˙}{\cdot} x = r \underset{˙}{\cdot} (y \underset{˙}{\cdot} x))) \leftrightarrow \forall x \in V \forall y \in K \forall z \in V \forall r \in K (((1 \underset{˙}{\cdot} x = x \land y \underset{˙}{\cdot} x \in V) \land y \underset{˙}{\cdot} (x \underset{˙}{+} z) = (y \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} z)) \land ((r + y) \underset{˙}{\cdot} x = (r \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} x) \land r y \underset{˙}{\cdot} x = r \underset{˙}{\cdot} (y \underset{˙}{\cdot} x)))$
88	78 87	bitrdi	$⊢ (W \in Grp \land S = ℂ_{fld} ↾_{𝑠} K \land K \in SubRing (ℂ_{fld})) \to (\forall r \in K \forall y \in K \forall z \in V \forall x \in V ((y \underset{˙}{\cdot} x \in V \land y \underset{˙}{\cdot} (x \underset{˙}{+} z) = (y \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} z) \land (r +_{S} y) \underset{˙}{\cdot} x = (r \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} x)) \land ((r \cdot_{S} y) \underset{˙}{\cdot} x = r \underset{˙}{\cdot} (y \underset{˙}{\cdot} x) \land 1_{S} \underset{˙}{\cdot} x = x)) \leftrightarrow \forall x \in V \forall y \in K \forall z \in V \forall r \in K (((1 \underset{˙}{\cdot} x = x \land y \underset{˙}{\cdot} x \in V) \land y \underset{˙}{\cdot} (x \underset{˙}{+} z) = (y \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} z)) \land ((r + y) \underset{˙}{\cdot} x = (r \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} x) \land r y \underset{˙}{\cdot} x = r \underset{˙}{\cdot} (y \underset{˙}{\cdot} x))))$
89	36	subrgring	$⊢ K \in SubRing (ℂ_{fld}) \to ℂ_{fld} ↾_{𝑠} K \in Ring$
90	89	3ad2ant3	$⊢ (W \in Grp \land S = ℂ_{fld} ↾_{𝑠} K \land K \in SubRing (ℂ_{fld})) \to ℂ_{fld} ↾_{𝑠} K \in Ring$
91		eleq1	$⊢ S = ℂ_{fld} ↾_{𝑠} K \to (S \in Ring \leftrightarrow ℂ_{fld} ↾_{𝑠} K \in Ring)$
92	91	3ad2ant2	$⊢ (W \in Grp \land S = ℂ_{fld} ↾_{𝑠} K \land K \in SubRing (ℂ_{fld})) \to (S \in Ring \leftrightarrow ℂ_{fld} ↾_{𝑠} K \in Ring)$
93	90 92	mpbird	$⊢ (W \in Grp \land S = ℂ_{fld} ↾_{𝑠} K \land K \in SubRing (ℂ_{fld})) \to S \in Ring$
94	93	biantrurd	$⊢ (W \in Grp \land S = ℂ_{fld} ↾_{𝑠} K \land K \in SubRing (ℂ_{fld})) \to (\forall r \in K \forall y \in K \forall z \in V \forall x \in V ((y \underset{˙}{\cdot} x \in V \land y \underset{˙}{\cdot} (x \underset{˙}{+} z) = (y \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} z) \land (r +_{S} y) \underset{˙}{\cdot} x = (r \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} x)) \land ((r \cdot_{S} y) \underset{˙}{\cdot} x = r \underset{˙}{\cdot} (y \underset{˙}{\cdot} x) \land 1_{S} \underset{˙}{\cdot} x = x)) \leftrightarrow (S \in Ring \land \forall r \in K \forall y \in K \forall z \in V \forall x \in V ((y \underset{˙}{\cdot} x \in V \land y \underset{˙}{\cdot} (x \underset{˙}{+} z) = (y \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} z) \land (r +_{S} y) \underset{˙}{\cdot} x = (r \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} x)) \land ((r \cdot_{S} y) \underset{˙}{\cdot} x = r \underset{˙}{\cdot} (y \underset{˙}{\cdot} x) \land 1_{S} \underset{˙}{\cdot} x = x))))$
95	3	grpbn0	$⊢ W \in Grp \to V \neq \emptyset$
96	95	3ad2ant1	$⊢ (W \in Grp \land S = ℂ_{fld} ↾_{𝑠} K \land K \in SubRing (ℂ_{fld})) \to V \neq \emptyset$
97	37	subrg1cl	$⊢ K \in SubRing (ℂ_{fld}) \to 1_{ℂ_{fld}} \in K$
98	97	ne0d	$⊢ K \in SubRing (ℂ_{fld}) \to K \neq \emptyset$
99	98	3ad2ant3	$⊢ (W \in Grp \land S = ℂ_{fld} ↾_{𝑠} K \land K \in SubRing (ℂ_{fld})) \to K \neq \emptyset$
100		ancom	$⊢ ((1 \underset{˙}{\cdot} x = x \land y \underset{˙}{\cdot} x \in V) \land y \underset{˙}{\cdot} (x \underset{˙}{+} z) = (y \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} z)) \leftrightarrow (y \underset{˙}{\cdot} (x \underset{˙}{+} z) = (y \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} z) \land (1 \underset{˙}{\cdot} x = x \land y \underset{˙}{\cdot} x \in V))$
101	100	anbi1i	$⊢ (((1 \underset{˙}{\cdot} x = x \land y \underset{˙}{\cdot} x \in V) \land y \underset{˙}{\cdot} (x \underset{˙}{+} z) = (y \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} z)) \land ((r + y) \underset{˙}{\cdot} x = (r \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} x) \land r y \underset{˙}{\cdot} x = r \underset{˙}{\cdot} (y \underset{˙}{\cdot} x))) \leftrightarrow ((y \underset{˙}{\cdot} (x \underset{˙}{+} z) = (y \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} z) \land (1 \underset{˙}{\cdot} x = x \land y \underset{˙}{\cdot} x \in V)) \land ((r + y) \underset{˙}{\cdot} x = (r \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} x) \land r y \underset{˙}{\cdot} x = r \underset{˙}{\cdot} (y \underset{˙}{\cdot} x)))$
102	101	a1i	$⊢ (V \neq \emptyset \land K \neq \emptyset) \to ((((1 \underset{˙}{\cdot} x = x \land y \underset{˙}{\cdot} x \in V) \land y \underset{˙}{\cdot} (x \underset{˙}{+} z) = (y \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} z)) \land ((r + y) \underset{˙}{\cdot} x = (r \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} x) \land r y \underset{˙}{\cdot} x = r \underset{˙}{\cdot} (y \underset{˙}{\cdot} x))) \leftrightarrow ((y \underset{˙}{\cdot} (x \underset{˙}{+} z) = (y \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} z) \land (1 \underset{˙}{\cdot} x = x \land y \underset{˙}{\cdot} x \in V)) \land ((r + y) \underset{˙}{\cdot} x = (r \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} x) \land r y \underset{˙}{\cdot} x = r \underset{˙}{\cdot} (y \underset{˙}{\cdot} x))))$
103	102	ralbidv	$⊢ (V \neq \emptyset \land K \neq \emptyset) \to (\forall r \in K (((1 \underset{˙}{\cdot} x = x \land y \underset{˙}{\cdot} x \in V) \land y \underset{˙}{\cdot} (x \underset{˙}{+} z) = (y \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} z)) \land ((r + y) \underset{˙}{\cdot} x = (r \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} x) \land r y \underset{˙}{\cdot} x = r \underset{˙}{\cdot} (y \underset{˙}{\cdot} x))) \leftrightarrow \forall r \in K ((y \underset{˙}{\cdot} (x \underset{˙}{+} z) = (y \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} z) \land (1 \underset{˙}{\cdot} x = x \land y \underset{˙}{\cdot} x \in V)) \land ((r + y) \underset{˙}{\cdot} x = (r \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} x) \land r y \underset{˙}{\cdot} x = r \underset{˙}{\cdot} (y \underset{˙}{\cdot} x))))$
104		r19.28zv	$⊢ K \neq \emptyset \to (\forall r \in K ((y \underset{˙}{\cdot} (x \underset{˙}{+} z) = (y \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} z) \land (1 \underset{˙}{\cdot} x = x \land y \underset{˙}{\cdot} x \in V)) \land ((r + y) \underset{˙}{\cdot} x = (r \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} x) \land r y \underset{˙}{\cdot} x = r \underset{˙}{\cdot} (y \underset{˙}{\cdot} x))) \leftrightarrow ((y \underset{˙}{\cdot} (x \underset{˙}{+} z) = (y \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} z) \land (1 \underset{˙}{\cdot} x = x \land y \underset{˙}{\cdot} x \in V)) \land \forall r \in K ((r + y) \underset{˙}{\cdot} x = (r \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} x) \land r y \underset{˙}{\cdot} x = r \underset{˙}{\cdot} (y \underset{˙}{\cdot} x))))$
105	104	adantl	$⊢ (V \neq \emptyset \land K \neq \emptyset) \to (\forall r \in K ((y \underset{˙}{\cdot} (x \underset{˙}{+} z) = (y \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} z) \land (1 \underset{˙}{\cdot} x = x \land y \underset{˙}{\cdot} x \in V)) \land ((r + y) \underset{˙}{\cdot} x = (r \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} x) \land r y \underset{˙}{\cdot} x = r \underset{˙}{\cdot} (y \underset{˙}{\cdot} x))) \leftrightarrow ((y \underset{˙}{\cdot} (x \underset{˙}{+} z) = (y \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} z) \land (1 \underset{˙}{\cdot} x = x \land y \underset{˙}{\cdot} x \in V)) \land \forall r \in K ((r + y) \underset{˙}{\cdot} x = (r \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} x) \land r y \underset{˙}{\cdot} x = r \underset{˙}{\cdot} (y \underset{˙}{\cdot} x))))$
106	103 105	bitrd	$⊢ (V \neq \emptyset \land K \neq \emptyset) \to (\forall r \in K (((1 \underset{˙}{\cdot} x = x \land y \underset{˙}{\cdot} x \in V) \land y \underset{˙}{\cdot} (x \underset{˙}{+} z) = (y \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} z)) \land ((r + y) \underset{˙}{\cdot} x = (r \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} x) \land r y \underset{˙}{\cdot} x = r \underset{˙}{\cdot} (y \underset{˙}{\cdot} x))) \leftrightarrow ((y \underset{˙}{\cdot} (x \underset{˙}{+} z) = (y \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} z) \land (1 \underset{˙}{\cdot} x = x \land y \underset{˙}{\cdot} x \in V)) \land \forall r \in K ((r + y) \underset{˙}{\cdot} x = (r \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} x) \land r y \underset{˙}{\cdot} x = r \underset{˙}{\cdot} (y \underset{˙}{\cdot} x))))$
107		anass	$⊢ ((y \underset{˙}{\cdot} (x \underset{˙}{+} z) = (y \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} z) \land (1 \underset{˙}{\cdot} x = x \land y \underset{˙}{\cdot} x \in V)) \land \forall r \in K ((r + y) \underset{˙}{\cdot} x = (r \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} x) \land r y \underset{˙}{\cdot} x = r \underset{˙}{\cdot} (y \underset{˙}{\cdot} x))) \leftrightarrow (y \underset{˙}{\cdot} (x \underset{˙}{+} z) = (y \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} z) \land ((1 \underset{˙}{\cdot} x = x \land y \underset{˙}{\cdot} x \in V) \land \forall r \in K ((r + y) \underset{˙}{\cdot} x = (r \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} x) \land r y \underset{˙}{\cdot} x = r \underset{˙}{\cdot} (y \underset{˙}{\cdot} x))))$
108		anass	$⊢ ((1 \underset{˙}{\cdot} x = x \land y \underset{˙}{\cdot} x \in V) \land \forall r \in K ((r + y) \underset{˙}{\cdot} x = (r \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} x) \land r y \underset{˙}{\cdot} x = r \underset{˙}{\cdot} (y \underset{˙}{\cdot} x))) \leftrightarrow (1 \underset{˙}{\cdot} x = x \land (y \underset{˙}{\cdot} x \in V \land \forall r \in K ((r + y) \underset{˙}{\cdot} x = (r \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} x) \land r y \underset{˙}{\cdot} x = r \underset{˙}{\cdot} (y \underset{˙}{\cdot} x))))$
109	108	anbi2i	$⊢ (y \underset{˙}{\cdot} (x \underset{˙}{+} z) = (y \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} z) \land ((1 \underset{˙}{\cdot} x = x \land y \underset{˙}{\cdot} x \in V) \land \forall r \in K ((r + y) \underset{˙}{\cdot} x = (r \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} x) \land r y \underset{˙}{\cdot} x = r \underset{˙}{\cdot} (y \underset{˙}{\cdot} x)))) \leftrightarrow (y \underset{˙}{\cdot} (x \underset{˙}{+} z) = (y \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} z) \land (1 \underset{˙}{\cdot} x = x \land (y \underset{˙}{\cdot} x \in V \land \forall r \in K ((r + y) \underset{˙}{\cdot} x = (r \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} x) \land r y \underset{˙}{\cdot} x = r \underset{˙}{\cdot} (y \underset{˙}{\cdot} x)))))$
110		ancom	$⊢ (y \underset{˙}{\cdot} (x \underset{˙}{+} z) = (y \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} z) \land (1 \underset{˙}{\cdot} x = x \land (y \underset{˙}{\cdot} x \in V \land \forall r \in K ((r + y) \underset{˙}{\cdot} x = (r \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} x) \land r y \underset{˙}{\cdot} x = r \underset{˙}{\cdot} (y \underset{˙}{\cdot} x))))) \leftrightarrow ((1 \underset{˙}{\cdot} x = x \land (y \underset{˙}{\cdot} x \in V \land \forall r \in K ((r + y) \underset{˙}{\cdot} x = (r \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} x) \land r y \underset{˙}{\cdot} x = r \underset{˙}{\cdot} (y \underset{˙}{\cdot} x)))) \land y \underset{˙}{\cdot} (x \underset{˙}{+} z) = (y \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} z))$
111	107 109 110	3bitri	$⊢ ((y \underset{˙}{\cdot} (x \underset{˙}{+} z) = (y \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} z) \land (1 \underset{˙}{\cdot} x = x \land y \underset{˙}{\cdot} x \in V)) \land \forall r \in K ((r + y) \underset{˙}{\cdot} x = (r \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} x) \land r y \underset{˙}{\cdot} x = r \underset{˙}{\cdot} (y \underset{˙}{\cdot} x))) \leftrightarrow ((1 \underset{˙}{\cdot} x = x \land (y \underset{˙}{\cdot} x \in V \land \forall r \in K ((r + y) \underset{˙}{\cdot} x = (r \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} x) \land r y \underset{˙}{\cdot} x = r \underset{˙}{\cdot} (y \underset{˙}{\cdot} x)))) \land y \underset{˙}{\cdot} (x \underset{˙}{+} z) = (y \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} z))$
112	106 111	bitrdi	$⊢ (V \neq \emptyset \land K \neq \emptyset) \to (\forall r \in K (((1 \underset{˙}{\cdot} x = x \land y \underset{˙}{\cdot} x \in V) \land y \underset{˙}{\cdot} (x \underset{˙}{+} z) = (y \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} z)) \land ((r + y) \underset{˙}{\cdot} x = (r \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} x) \land r y \underset{˙}{\cdot} x = r \underset{˙}{\cdot} (y \underset{˙}{\cdot} x))) \leftrightarrow ((1 \underset{˙}{\cdot} x = x \land (y \underset{˙}{\cdot} x \in V \land \forall r \in K ((r + y) \underset{˙}{\cdot} x = (r \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} x) \land r y \underset{˙}{\cdot} x = r \underset{˙}{\cdot} (y \underset{˙}{\cdot} x)))) \land y \underset{˙}{\cdot} (x \underset{˙}{+} z) = (y \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} z)))$
113	112	ralbidv	$⊢ (V \neq \emptyset \land K \neq \emptyset) \to (\forall z \in V \forall r \in K (((1 \underset{˙}{\cdot} x = x \land y \underset{˙}{\cdot} x \in V) \land y \underset{˙}{\cdot} (x \underset{˙}{+} z) = (y \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} z)) \land ((r + y) \underset{˙}{\cdot} x = (r \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} x) \land r y \underset{˙}{\cdot} x = r \underset{˙}{\cdot} (y \underset{˙}{\cdot} x))) \leftrightarrow \forall z \in V ((1 \underset{˙}{\cdot} x = x \land (y \underset{˙}{\cdot} x \in V \land \forall r \in K ((r + y) \underset{˙}{\cdot} x = (r \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} x) \land r y \underset{˙}{\cdot} x = r \underset{˙}{\cdot} (y \underset{˙}{\cdot} x)))) \land y \underset{˙}{\cdot} (x \underset{˙}{+} z) = (y \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} z)))$
114		r19.28zv	$⊢ V \neq \emptyset \to (\forall z \in V ((1 \underset{˙}{\cdot} x = x \land (y \underset{˙}{\cdot} x \in V \land \forall r \in K ((r + y) \underset{˙}{\cdot} x = (r \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} x) \land r y \underset{˙}{\cdot} x = r \underset{˙}{\cdot} (y \underset{˙}{\cdot} x)))) \land y \underset{˙}{\cdot} (x \underset{˙}{+} z) = (y \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} z)) \leftrightarrow ((1 \underset{˙}{\cdot} x = x \land (y \underset{˙}{\cdot} x \in V \land \forall r \in K ((r + y) \underset{˙}{\cdot} x = (r \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} x) \land r y \underset{˙}{\cdot} x = r \underset{˙}{\cdot} (y \underset{˙}{\cdot} x)))) \land \forall z \in V y \underset{˙}{\cdot} (x \underset{˙}{+} z) = (y \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} z)))$
115	114	adantr	$⊢ (V \neq \emptyset \land K \neq \emptyset) \to (\forall z \in V ((1 \underset{˙}{\cdot} x = x \land (y \underset{˙}{\cdot} x \in V \land \forall r \in K ((r + y) \underset{˙}{\cdot} x = (r \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} x) \land r y \underset{˙}{\cdot} x = r \underset{˙}{\cdot} (y \underset{˙}{\cdot} x)))) \land y \underset{˙}{\cdot} (x \underset{˙}{+} z) = (y \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} z)) \leftrightarrow ((1 \underset{˙}{\cdot} x = x \land (y \underset{˙}{\cdot} x \in V \land \forall r \in K ((r + y) \underset{˙}{\cdot} x = (r \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} x) \land r y \underset{˙}{\cdot} x = r \underset{˙}{\cdot} (y \underset{˙}{\cdot} x)))) \land \forall z \in V y \underset{˙}{\cdot} (x \underset{˙}{+} z) = (y \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} z)))$
116	113 115	bitrd	$⊢ (V \neq \emptyset \land K \neq \emptyset) \to (\forall z \in V \forall r \in K (((1 \underset{˙}{\cdot} x = x \land y \underset{˙}{\cdot} x \in V) \land y \underset{˙}{\cdot} (x \underset{˙}{+} z) = (y \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} z)) \land ((r + y) \underset{˙}{\cdot} x = (r \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} x) \land r y \underset{˙}{\cdot} x = r \underset{˙}{\cdot} (y \underset{˙}{\cdot} x))) \leftrightarrow ((1 \underset{˙}{\cdot} x = x \land (y \underset{˙}{\cdot} x \in V \land \forall r \in K ((r + y) \underset{˙}{\cdot} x = (r \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} x) \land r y \underset{˙}{\cdot} x = r \underset{˙}{\cdot} (y \underset{˙}{\cdot} x)))) \land \forall z \in V y \underset{˙}{\cdot} (x \underset{˙}{+} z) = (y \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} z)))$
117		anass	$⊢ ((1 \underset{˙}{\cdot} x = x \land (y \underset{˙}{\cdot} x \in V \land \forall r \in K ((r + y) \underset{˙}{\cdot} x = (r \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} x) \land r y \underset{˙}{\cdot} x = r \underset{˙}{\cdot} (y \underset{˙}{\cdot} x)))) \land \forall z \in V y \underset{˙}{\cdot} (x \underset{˙}{+} z) = (y \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} z)) \leftrightarrow (1 \underset{˙}{\cdot} x = x \land ((y \underset{˙}{\cdot} x \in V \land \forall r \in K ((r + y) \underset{˙}{\cdot} x = (r \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} x) \land r y \underset{˙}{\cdot} x = r \underset{˙}{\cdot} (y \underset{˙}{\cdot} x))) \land \forall z \in V y \underset{˙}{\cdot} (x \underset{˙}{+} z) = (y \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} z)))$
118		oveq1	$⊢ z = r \to z + y = r + y$
119	118	oveq1d	$⊢ z = r \to (z + y) \underset{˙}{\cdot} x = (r + y) \underset{˙}{\cdot} x$
120		oveq1	$⊢ z = r \to z \underset{˙}{\cdot} x = r \underset{˙}{\cdot} x$
121	120	oveq1d	$⊢ z = r \to (z \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} x) = (r \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} x)$
122	119 121	eqeq12d	$⊢ z = r \to ((z + y) \underset{˙}{\cdot} x = (z \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} x) \leftrightarrow (r + y) \underset{˙}{\cdot} x = (r \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} x))$
123		oveq1	$⊢ z = r \to z y = r y$
124	123	oveq1d	$⊢ z = r \to z y \underset{˙}{\cdot} x = r y \underset{˙}{\cdot} x$
125		oveq1	$⊢ z = r \to z \underset{˙}{\cdot} (y \underset{˙}{\cdot} x) = r \underset{˙}{\cdot} (y \underset{˙}{\cdot} x)$
126	124 125	eqeq12d	$⊢ z = r \to (z y \underset{˙}{\cdot} x = z \underset{˙}{\cdot} (y \underset{˙}{\cdot} x) \leftrightarrow r y \underset{˙}{\cdot} x = r \underset{˙}{\cdot} (y \underset{˙}{\cdot} x))$
127	122 126	anbi12d	$⊢ z = r \to (((z + y) \underset{˙}{\cdot} x = (z \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} x) \land z y \underset{˙}{\cdot} x = z \underset{˙}{\cdot} (y \underset{˙}{\cdot} x)) \leftrightarrow ((r + y) \underset{˙}{\cdot} x = (r \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} x) \land r y \underset{˙}{\cdot} x = r \underset{˙}{\cdot} (y \underset{˙}{\cdot} x)))$
128	127	cbvralvw	$⊢ \forall z \in K ((z + y) \underset{˙}{\cdot} x = (z \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} x) \land z y \underset{˙}{\cdot} x = z \underset{˙}{\cdot} (y \underset{˙}{\cdot} x)) \leftrightarrow \forall r \in K ((r + y) \underset{˙}{\cdot} x = (r \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} x) \land r y \underset{˙}{\cdot} x = r \underset{˙}{\cdot} (y \underset{˙}{\cdot} x))$
129	128	3anbi3i	$⊢ (y \underset{˙}{\cdot} x \in V \land \forall z \in V y \underset{˙}{\cdot} (x \underset{˙}{+} z) = (y \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} z) \land \forall z \in K ((z + y) \underset{˙}{\cdot} x = (z \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} x) \land z y \underset{˙}{\cdot} x = z \underset{˙}{\cdot} (y \underset{˙}{\cdot} x))) \leftrightarrow (y \underset{˙}{\cdot} x \in V \land \forall z \in V y \underset{˙}{\cdot} (x \underset{˙}{+} z) = (y \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} z) \land \forall r \in K ((r + y) \underset{˙}{\cdot} x = (r \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} x) \land r y \underset{˙}{\cdot} x = r \underset{˙}{\cdot} (y \underset{˙}{\cdot} x)))$
130		3anan32	$⊢ (y \underset{˙}{\cdot} x \in V \land \forall z \in V y \underset{˙}{\cdot} (x \underset{˙}{+} z) = (y \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} z) \land \forall r \in K ((r + y) \underset{˙}{\cdot} x = (r \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} x) \land r y \underset{˙}{\cdot} x = r \underset{˙}{\cdot} (y \underset{˙}{\cdot} x))) \leftrightarrow ((y \underset{˙}{\cdot} x \in V \land \forall r \in K ((r + y) \underset{˙}{\cdot} x = (r \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} x) \land r y \underset{˙}{\cdot} x = r \underset{˙}{\cdot} (y \underset{˙}{\cdot} x))) \land \forall z \in V y \underset{˙}{\cdot} (x \underset{˙}{+} z) = (y \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} z))$
131	129 130	bitri	$⊢ (y \underset{˙}{\cdot} x \in V \land \forall z \in V y \underset{˙}{\cdot} (x \underset{˙}{+} z) = (y \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} z) \land \forall z \in K ((z + y) \underset{˙}{\cdot} x = (z \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} x) \land z y \underset{˙}{\cdot} x = z \underset{˙}{\cdot} (y \underset{˙}{\cdot} x))) \leftrightarrow ((y \underset{˙}{\cdot} x \in V \land \forall r \in K ((r + y) \underset{˙}{\cdot} x = (r \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} x) \land r y \underset{˙}{\cdot} x = r \underset{˙}{\cdot} (y \underset{˙}{\cdot} x))) \land \forall z \in V y \underset{˙}{\cdot} (x \underset{˙}{+} z) = (y \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} z))$
132	131	bicomi	$⊢ ((y \underset{˙}{\cdot} x \in V \land \forall r \in K ((r + y) \underset{˙}{\cdot} x = (r \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} x) \land r y \underset{˙}{\cdot} x = r \underset{˙}{\cdot} (y \underset{˙}{\cdot} x))) \land \forall z \in V y \underset{˙}{\cdot} (x \underset{˙}{+} z) = (y \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} z)) \leftrightarrow (y \underset{˙}{\cdot} x \in V \land \forall z \in V y \underset{˙}{\cdot} (x \underset{˙}{+} z) = (y \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} z) \land \forall z \in K ((z + y) \underset{˙}{\cdot} x = (z \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} x) \land z y \underset{˙}{\cdot} x = z \underset{˙}{\cdot} (y \underset{˙}{\cdot} x)))$
133	132	anbi2i	$⊢ (1 \underset{˙}{\cdot} x = x \land ((y \underset{˙}{\cdot} x \in V \land \forall r \in K ((r + y) \underset{˙}{\cdot} x = (r \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} x) \land r y \underset{˙}{\cdot} x = r \underset{˙}{\cdot} (y \underset{˙}{\cdot} x))) \land \forall z \in V y \underset{˙}{\cdot} (x \underset{˙}{+} z) = (y \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} z))) \leftrightarrow (1 \underset{˙}{\cdot} x = x \land (y \underset{˙}{\cdot} x \in V \land \forall z \in V y \underset{˙}{\cdot} (x \underset{˙}{+} z) = (y \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} z) \land \forall z \in K ((z + y) \underset{˙}{\cdot} x = (z \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} x) \land z y \underset{˙}{\cdot} x = z \underset{˙}{\cdot} (y \underset{˙}{\cdot} x))))$
134	117 133	bitri	$⊢ ((1 \underset{˙}{\cdot} x = x \land (y \underset{˙}{\cdot} x \in V \land \forall r \in K ((r + y) \underset{˙}{\cdot} x = (r \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} x) \land r y \underset{˙}{\cdot} x = r \underset{˙}{\cdot} (y \underset{˙}{\cdot} x)))) \land \forall z \in V y \underset{˙}{\cdot} (x \underset{˙}{+} z) = (y \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} z)) \leftrightarrow (1 \underset{˙}{\cdot} x = x \land (y \underset{˙}{\cdot} x \in V \land \forall z \in V y \underset{˙}{\cdot} (x \underset{˙}{+} z) = (y \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} z) \land \forall z \in K ((z + y) \underset{˙}{\cdot} x = (z \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} x) \land z y \underset{˙}{\cdot} x = z \underset{˙}{\cdot} (y \underset{˙}{\cdot} x))))$
135	116 134	bitrdi	$⊢ (V \neq \emptyset \land K \neq \emptyset) \to (\forall z \in V \forall r \in K (((1 \underset{˙}{\cdot} x = x \land y \underset{˙}{\cdot} x \in V) \land y \underset{˙}{\cdot} (x \underset{˙}{+} z) = (y \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} z)) \land ((r + y) \underset{˙}{\cdot} x = (r \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} x) \land r y \underset{˙}{\cdot} x = r \underset{˙}{\cdot} (y \underset{˙}{\cdot} x))) \leftrightarrow (1 \underset{˙}{\cdot} x = x \land (y \underset{˙}{\cdot} x \in V \land \forall z \in V y \underset{˙}{\cdot} (x \underset{˙}{+} z) = (y \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} z) \land \forall z \in K ((z + y) \underset{˙}{\cdot} x = (z \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} x) \land z y \underset{˙}{\cdot} x = z \underset{˙}{\cdot} (y \underset{˙}{\cdot} x)))))$
136	135	ralbidv	$⊢ (V \neq \emptyset \land K \neq \emptyset) \to (\forall y \in K \forall z \in V \forall r \in K (((1 \underset{˙}{\cdot} x = x \land y \underset{˙}{\cdot} x \in V) \land y \underset{˙}{\cdot} (x \underset{˙}{+} z) = (y \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} z)) \land ((r + y) \underset{˙}{\cdot} x = (r \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} x) \land r y \underset{˙}{\cdot} x = r \underset{˙}{\cdot} (y \underset{˙}{\cdot} x))) \leftrightarrow \forall y \in K (1 \underset{˙}{\cdot} x = x \land (y \underset{˙}{\cdot} x \in V \land \forall z \in V y \underset{˙}{\cdot} (x \underset{˙}{+} z) = (y \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} z) \land \forall z \in K ((z + y) \underset{˙}{\cdot} x = (z \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} x) \land z y \underset{˙}{\cdot} x = z \underset{˙}{\cdot} (y \underset{˙}{\cdot} x)))))$
137		r19.28zv	$⊢ K \neq \emptyset \to (\forall y \in K (1 \underset{˙}{\cdot} x = x \land (y \underset{˙}{\cdot} x \in V \land \forall z \in V y \underset{˙}{\cdot} (x \underset{˙}{+} z) = (y \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} z) \land \forall z \in K ((z + y) \underset{˙}{\cdot} x = (z \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} x) \land z y \underset{˙}{\cdot} x = z \underset{˙}{\cdot} (y \underset{˙}{\cdot} x)))) \leftrightarrow (1 \underset{˙}{\cdot} x = x \land \forall y \in K (y \underset{˙}{\cdot} x \in V \land \forall z \in V y \underset{˙}{\cdot} (x \underset{˙}{+} z) = (y \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} z) \land \forall z \in K ((z + y) \underset{˙}{\cdot} x = (z \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} x) \land z y \underset{˙}{\cdot} x = z \underset{˙}{\cdot} (y \underset{˙}{\cdot} x)))))$
138	137	adantl	$⊢ (V \neq \emptyset \land K \neq \emptyset) \to (\forall y \in K (1 \underset{˙}{\cdot} x = x \land (y \underset{˙}{\cdot} x \in V \land \forall z \in V y \underset{˙}{\cdot} (x \underset{˙}{+} z) = (y \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} z) \land \forall z \in K ((z + y) \underset{˙}{\cdot} x = (z \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} x) \land z y \underset{˙}{\cdot} x = z \underset{˙}{\cdot} (y \underset{˙}{\cdot} x)))) \leftrightarrow (1 \underset{˙}{\cdot} x = x \land \forall y \in K (y \underset{˙}{\cdot} x \in V \land \forall z \in V y \underset{˙}{\cdot} (x \underset{˙}{+} z) = (y \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} z) \land \forall z \in K ((z + y) \underset{˙}{\cdot} x = (z \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} x) \land z y \underset{˙}{\cdot} x = z \underset{˙}{\cdot} (y \underset{˙}{\cdot} x)))))$
139	136 138	bitrd	$⊢ (V \neq \emptyset \land K \neq \emptyset) \to (\forall y \in K \forall z \in V \forall r \in K (((1 \underset{˙}{\cdot} x = x \land y \underset{˙}{\cdot} x \in V) \land y \underset{˙}{\cdot} (x \underset{˙}{+} z) = (y \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} z)) \land ((r + y) \underset{˙}{\cdot} x = (r \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} x) \land r y \underset{˙}{\cdot} x = r \underset{˙}{\cdot} (y \underset{˙}{\cdot} x))) \leftrightarrow (1 \underset{˙}{\cdot} x = x \land \forall y \in K (y \underset{˙}{\cdot} x \in V \land \forall z \in V y \underset{˙}{\cdot} (x \underset{˙}{+} z) = (y \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} z) \land \forall z \in K ((z + y) \underset{˙}{\cdot} x = (z \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} x) \land z y \underset{˙}{\cdot} x = z \underset{˙}{\cdot} (y \underset{˙}{\cdot} x)))))$
140	96 99 139	syl2anc	$⊢ (W \in Grp \land S = ℂ_{fld} ↾_{𝑠} K \land K \in SubRing (ℂ_{fld})) \to (\forall y \in K \forall z \in V \forall r \in K (((1 \underset{˙}{\cdot} x = x \land y \underset{˙}{\cdot} x \in V) \land y \underset{˙}{\cdot} (x \underset{˙}{+} z) = (y \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} z)) \land ((r + y) \underset{˙}{\cdot} x = (r \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} x) \land r y \underset{˙}{\cdot} x = r \underset{˙}{\cdot} (y \underset{˙}{\cdot} x))) \leftrightarrow (1 \underset{˙}{\cdot} x = x \land \forall y \in K (y \underset{˙}{\cdot} x \in V \land \forall z \in V y \underset{˙}{\cdot} (x \underset{˙}{+} z) = (y \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} z) \land \forall z \in K ((z + y) \underset{˙}{\cdot} x = (z \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} x) \land z y \underset{˙}{\cdot} x = z \underset{˙}{\cdot} (y \underset{˙}{\cdot} x)))))$
141	140	ralbidv	$⊢ (W \in Grp \land S = ℂ_{fld} ↾_{𝑠} K \land K \in SubRing (ℂ_{fld})) \to (\forall x \in V \forall y \in K \forall z \in V \forall r \in K (((1 \underset{˙}{\cdot} x = x \land y \underset{˙}{\cdot} x \in V) \land y \underset{˙}{\cdot} (x \underset{˙}{+} z) = (y \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} z)) \land ((r + y) \underset{˙}{\cdot} x = (r \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} x) \land r y \underset{˙}{\cdot} x = r \underset{˙}{\cdot} (y \underset{˙}{\cdot} x))) \leftrightarrow \forall x \in V (1 \underset{˙}{\cdot} x = x \land \forall y \in K (y \underset{˙}{\cdot} x \in V \land \forall z \in V y \underset{˙}{\cdot} (x \underset{˙}{+} z) = (y \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} z) \land \forall z \in K ((z + y) \underset{˙}{\cdot} x = (z \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} x) \land z y \underset{˙}{\cdot} x = z \underset{˙}{\cdot} (y \underset{˙}{\cdot} x)))))$
142	88 94 141	3bitr3d	$⊢ (W \in Grp \land S = ℂ_{fld} ↾_{𝑠} K \land K \in SubRing (ℂ_{fld})) \to ((S \in Ring \land \forall r \in K \forall y \in K \forall z \in V \forall x \in V ((y \underset{˙}{\cdot} x \in V \land y \underset{˙}{\cdot} (x \underset{˙}{+} z) = (y \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} z) \land (r +_{S} y) \underset{˙}{\cdot} x = (r \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} x)) \land ((r \cdot_{S} y) \underset{˙}{\cdot} x = r \underset{˙}{\cdot} (y \underset{˙}{\cdot} x) \land 1_{S} \underset{˙}{\cdot} x = x))) \leftrightarrow \forall x \in V (1 \underset{˙}{\cdot} x = x \land \forall y \in K (y \underset{˙}{\cdot} x \in V \land \forall z \in V y \underset{˙}{\cdot} (x \underset{˙}{+} z) = (y \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} z) \land \forall z \in K ((z + y) \underset{˙}{\cdot} x = (z \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} x) \land z y \underset{˙}{\cdot} x = z \underset{˙}{\cdot} (y \underset{˙}{\cdot} x)))))$
143	142	pm5.32i	$⊢ ((W \in Grp \land S = ℂ_{fld} ↾_{𝑠} K \land K \in SubRing (ℂ_{fld})) \land (S \in Ring \land \forall r \in K \forall y \in K \forall z \in V \forall x \in V ((y \underset{˙}{\cdot} x \in V \land y \underset{˙}{\cdot} (x \underset{˙}{+} z) = (y \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} z) \land (r +_{S} y) \underset{˙}{\cdot} x = (r \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} x)) \land ((r \cdot_{S} y) \underset{˙}{\cdot} x = r \underset{˙}{\cdot} (y \underset{˙}{\cdot} x) \land 1_{S} \underset{˙}{\cdot} x = x)))) \leftrightarrow ((W \in Grp \land S = ℂ_{fld} ↾_{𝑠} K \land K \in SubRing (ℂ_{fld})) \land \forall x \in V (1 \underset{˙}{\cdot} x = x \land \forall y \in K (y \underset{˙}{\cdot} x \in V \land \forall z \in V y \underset{˙}{\cdot} (x \underset{˙}{+} z) = (y \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} z) \land \forall z \in K ((z + y) \underset{˙}{\cdot} x = (z \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} x) \land z y \underset{˙}{\cdot} x = z \underset{˙}{\cdot} (y \underset{˙}{\cdot} x)))))$
144	23 24 143	3bitri	$⊢ (((W \in Grp \land S \in Ring) \land (S = ℂ_{fld} ↾_{𝑠} K \land K \in SubRing (ℂ_{fld}))) \land \forall r \in K \forall y \in K \forall z \in V \forall x \in V ((y \underset{˙}{\cdot} x \in V \land y \underset{˙}{\cdot} (x \underset{˙}{+} z) = (y \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} z) \land (r +_{S} y) \underset{˙}{\cdot} x = (r \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} x)) \land ((r \cdot_{S} y) \underset{˙}{\cdot} x = r \underset{˙}{\cdot} (y \underset{˙}{\cdot} x) \land 1_{S} \underset{˙}{\cdot} x = x))) \leftrightarrow ((W \in Grp \land S = ℂ_{fld} ↾_{𝑠} K \land K \in SubRing (ℂ_{fld})) \land \forall x \in V (1 \underset{˙}{\cdot} x = x \land \forall y \in K (y \underset{˙}{\cdot} x \in V \land \forall z \in V y \underset{˙}{\cdot} (x \underset{˙}{+} z) = (y \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} z) \land \forall z \in K ((z + y) \underset{˙}{\cdot} x = (z \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} x) \land z y \underset{˙}{\cdot} x = z \underset{˙}{\cdot} (y \underset{˙}{\cdot} x)))))$
145	6 17 144	3bitri	$⊢ W \in CMod \leftrightarrow ((W \in Grp \land S = ℂ_{fld} ↾_{𝑠} K \land K \in SubRing (ℂ_{fld})) \land \forall x \in V (1 \underset{˙}{\cdot} x = x \land \forall y \in K (y \underset{˙}{\cdot} x \in V \land \forall z \in V y \underset{˙}{\cdot} (x \underset{˙}{+} z) = (y \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} z) \land \forall z \in K ((z + y) \underset{˙}{\cdot} x = (z \underset{˙}{\cdot} x) \underset{˙}{+} (y \underset{˙}{\cdot} x) \land z y \underset{˙}{\cdot} x = z \underset{˙}{\cdot} (y \underset{˙}{\cdot} x)))))$

Metamath Proof Explorer

Theorem isclmp

Proof